LeanMachineLearning exposition

1.3. ForMathlib.MeasureTheory.Measure.AbsolutelyContinuous🔗

Lemma about measures that assign non-zero probability to every singleton.

Module LeanMachineLearning.ForMathlib.MeasureTheory.Measure.AbsolutelyContinuous contains 1 exposed declarations.

absolutelyContinuous_of_measure_singleton_ne_zero🔗

LemmaMeasureTheory.Measure.absolutelyContinuous_of_measure_singleton_ne_zero
Details

No docstring.

🔗theorem
MeasureTheory.Measure.absolutelyContinuous_of_measure_singleton_ne_zero.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α}
  (h : ∀ (a : α), ν {a} ≠ 0) : AbsolutelyContinuous μ ν
MeasureTheory.Measure.absolutelyContinuous_of_measure_singleton_ne_zero.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α}
  {μ ν : Measure α}
  (h : ∀ (a : α), ν {a} ≠ 0) :
  AbsolutelyContinuous μ ν

Code

lemma absolutelyContinuous_of_measure_singleton_ne_zero (h : ∀ a, ν {a} ≠ 0) : μ ≪ ν
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
fun s hs ↦ by simp [(measure_null_iff_eq_empty_of_measure_singleton_ne_zero h).1 hs]
  1. MeasureTheory.Measure.absolutelyContinuous_of_measure_singleton_ne_zero