measure_average_le_pos — Mathlib

English

Let μ be a finite measure with μ ≠ 0 and f integrable; then 0 < μ {x | ⨍ a in s, f a ∂μ ≤ f x}.

Русский

Пусть μ – конечная мера с μ ≠ 0 и f интегрируема; тогда 0 < μ {x | ⨍ a in s, f a ∂μ ≤ f x}.

LaTeX

$$$$ 0 < \mu \{ x \mid \laverage f ≤ f(x) \} $$$$

Lean4

/-- **First moment method**. An integrable function is greater than its mean on a set of positive
measure. -/
theorem measure_average_le_pos (hμ : μ ≠ 0) (hf : Integrable f μ) : 0 < μ {x | ⨍ a, f a ∂μ ≤ f x} := by
  simpa using measure_setAverage_le_pos (Measure.measure_univ_ne_zero.2 hμ) (measure_ne_top _ _) hf.integrableOn

Похожие утверждения