English
There exists x in s with f(x) ≤ ⨍⁻ a in s, f(a) ∂μ.
Русский
Существует x в s такое, что f(x) меньше или равно LAverage по s.
LaTeX
$$$\\exists x \\in s, \\; f(x) \\le ⨍^- a \\in s, f(a) \\partial\\mu$$$
Lean4
/-- **First moment method**. A measurable function is smaller than its mean on a set of positive
measure. -/
theorem measure_le_setLAverage_pos (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ∞) (hf : AEMeasurable f (μ.restrict s)) :
0 < μ ({x ∈ s | f x ≤ ⨍⁻ a in s, f a ∂μ}) :=
by
obtain h | h := eq_or_ne (∫⁻ a in s, f a ∂μ) ∞
· simpa [mul_top, hμ₁, laverage, h, top_div_of_ne_top hμ₁, pos_iff_ne_zero] using hμ
have := measure_le_setAverage_pos hμ hμ₁ (integrable_toReal_of_lintegral_ne_top hf h)
rw [← setOf_inter_eq_sep, ←
Measure.restrict_apply₀ (hf.aestronglyMeasurable.nullMeasurableSet_le aestronglyMeasurable_const)]
rw [← setOf_inter_eq_sep, ←
Measure.restrict_apply₀ (hf.ennreal_toReal.aestronglyMeasurable.nullMeasurableSet_le aestronglyMeasurable_const), ←
measure_diff_null (measure_eq_top_of_lintegral_ne_top hf h)] at this
refine this.trans_le (measure_mono ?_)
rintro x ⟨hfx, hx⟩
dsimp at hfx
rwa [← toReal_laverage hf, toReal_le_toReal hx (setLAverage_lt_top h).ne] at hfx
simp_rw [ae_iff, not_ne_iff]
exact measure_eq_top_of_lintegral_ne_top hf h
