Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.eq_zero_of_isDoubling_zero

Carleson.ToMathlib.MeasureTheory.Measure.IsDoubling · Carleson/ToMathlib/MeasureTheory/Measure/IsDoubling.lean:43 to 53

Mathematical statement

Exact Lean statement

lemma eq_zero_of_isDoubling_zero [MeasurableSpace X] (μ : Measure X) [hμ : μ.IsDoubling 0] :
    μ = 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma eq_zero_of_isDoubling_zero [MeasurableSpace X] (μ : Measure X) [hμ : μ.IsDoubling 0] :    μ = 0 := by  rcases isEmpty_or_nonempty X with hX | ⟨⟨x⟩⟩  · exact eq_zero_of_isEmpty μ  have M (r : ℝ) : μ (ball x r) = 0 := by    have := hμ.measure_ball_two_le_same x (r / 2)    simp only [ENNReal.coe_zero, zero_mul, nonpos_iff_eq_zero] at this    convert this    ring  rw [← measure_univ_eq_zero, ← iUnion_ball_nat x]  exact measure_iUnion_null_iff.mpr fun i ↦ M ↑i