English
There exists x with f(x) ≤ laverage on s under ENNReal-valued measurable f.
Русский
Существует x, для которого f(x) не превышает LAverage на s для неотрицательных действительных значений.
LaTeX
$$$\\exists x, \\; x \\in s \\land f(x) \\le \\operatorname{laverage}_{\\mu|_s} f$$$
Lean4
/-- **First moment method**. A measurable function is greater than its mean on a set of positive
measure. -/
theorem measure_setLAverage_le_pos (hμ : μ s ≠ 0) (hs : NullMeasurableSet s μ) (hint : ∫⁻ a in s, f a ∂μ ≠ ∞) :
0 < μ ({x ∈ s | ⨍⁻ a in s, f a ∂μ ≤ f x}) :=
by
obtain hμ₁ | hμ₁ := eq_or_ne (μ s) ∞
· simp [setLAverage_eq, hμ₁]
obtain ⟨g, hg, hgf, hfg⟩ := exists_measurable_le_lintegral_eq (μ.restrict s) f
have hfg' : ⨍⁻ a in s, f a ∂μ = ⨍⁻ a in s, g a ∂μ := by simp_rw [laverage_eq, hfg]
rw [hfg] at hint
have := measure_setAverage_le_pos hμ hμ₁ (integrable_toReal_of_lintegral_ne_top hg.aemeasurable hint)
simp_rw [← setOf_inter_eq_sep, ← Measure.restrict_apply₀' hs, hfg']
rw [← setOf_inter_eq_sep, ← Measure.restrict_apply₀' hs, ←
measure_diff_null (measure_eq_top_of_lintegral_ne_top hg.aemeasurable hint)] at this
refine this.trans_le (measure_mono ?_)
rintro x ⟨hfx, hx⟩
dsimp at hfx
rw [← toReal_laverage hg.aemeasurable, toReal_le_toReal (setLAverage_lt_top hint).ne hx] at hfx
· exact hfx.trans (hgf _)
· simp_rw [ae_iff, not_ne_iff]
exact measure_eq_top_of_lintegral_ne_top hg.aemeasurable hint
