English
Let hμ, hμ₁ be that μ s ≠ 0 and μ s ≠ ∞, and f integrable on s. Then μ({x ∈ s | f x ≤ ⨍ a in s, f a ∂μ}) > 0.
Русский
Пусть μ(s) ≠ 0 и μ(s) ≠ ∞ и f интегрируема на s. Тогда множество {x ∈ s | f(x) ≤ ⨍ a in s, f(a) dμ} имеет положительную меру.
LaTeX
$$$$ 0 < \mu \big\{ x \in s \mid f(x) \leq \laverage_{s} f \big\} $$$$
Lean4
/-- **First moment method**. An integrable function is smaller than its mean on a set of positive
measure. -/
theorem measure_le_setAverage_pos (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ∞) (hf : IntegrableOn f s μ) :
0 < μ ({x ∈ s | f x ≤ ⨍ a in s, f a ∂μ}) :=
by
refine pos_iff_ne_zero.2 fun H => ?_
replace H : (μ.restrict s) {x | f x ≤ ⨍ a in s, f a ∂μ} = 0 :=
by
rwa [restrict_apply₀, inter_comm]
exact AEStronglyMeasurable.nullMeasurableSet_le hf.1 aestronglyMeasurable_const
haveI := Fact.mk hμ₁.lt_top
refine (integral_sub_average (μ.restrict s) f).not_gt ?_
refine (setIntegral_pos_iff_support_of_nonneg_ae ?_ ?_).2 ?_
· refine measure_mono_null (fun x hx ↦ ?_) H
simp only [Pi.zero_apply, sub_nonneg, mem_compl_iff, mem_setOf_eq, not_le] at hx
exact hx.le
· exact hf.sub (integrableOn_const hμ₁)
· rwa [pos_iff_ne_zero, inter_comm, ← diff_compl, ← diff_inter_self_eq_diff, measure_diff_null]
refine measure_mono_null ?_ (measure_inter_eq_zero_of_restrict H)
exact inter_subset_inter_left _ fun a ha => (sub_eq_zero.1 <| of_not_not ha).le
