English
Let μ be a nonzero measure on α, and f: α → ℝ≥0∞ be a measurable function with a finite mean. Then for every null set N (i.e., μ(N) = 0) there exists some x ∉ N such that the mean value of f (with respect to μ) is less than or equal to f(x).
Русский
Пусть μ — ненулевое измерение на α, и пусть f: α → ℝ≥0∞ будет измеримой функцией с конечным средним значением. Тогда для любой нулевой плотности множества N (μ(N) = 0) существует некоторый x ∉ N such that среднее по f относительно μ не превосходит f(x).
LaTeX
$$$\\exists x\\, (x \\notin N)\\ \&\\ \\operatorname{lavg}_{\\mu}(f) \\le f(x)$$$
Lean4
/-- **First moment method**. The maximum of a measurable function is greater than its mean, while
avoiding a null set. -/
theorem exists_notMem_null_laverage_le (hμ : μ ≠ 0) (hint : ∫⁻ a : α, f a ∂μ ≠ ∞) (hN : μ N = 0) :
∃ x, x ∉ N ∧ ⨍⁻ a, f a ∂μ ≤ f x := by
have := measure_laverage_le_pos hμ hint
rw [← measure_diff_null hN] at this
obtain ⟨x, hx, hxN⟩ := nonempty_of_measure_ne_zero this.ne'
exact ⟨x, hxN, hx⟩
