Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.one_le_A

Carleson.ToMathlib.MeasureTheory.Measure.IsDoubling · Carleson/ToMathlib/MeasureTheory/Measure/IsDoubling.lean:313 to 324

Mathematical statement

Exact Lean statement

lemma one_le_A [Nonempty X] [μ.IsOpenPosMeasure] : 1 ≤ A

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma one_le_A [Nonempty X] [μ.IsOpenPosMeasure] : 1 ≤ A := by  obtain ⟨x⟩ := ‹Nonempty X›  have : 0 < μ.real (ball x 1) := measureReal_ball_pos x (by linarith)  apply le_of_mul_le_mul_right _ this  simp only [val_eq_coe, NNReal.coe_one, one_mul]  calc    μ.real (ball x 1)      ≤ μ.real (ball x (2 * 1)) := by        rw [mul_one]        exact ENNReal.toReal_mono (measure_ball_lt_top.ne)          (μ.mono (ball_subset_ball (by linarith)))    _ ≤ A * μ.real (ball x 1) := measureReal_ball_two_le_same x 1