measure_le_average_pos — Mathlib

English

Let hμ, hμ₁ be nonzero and f integrable on μ; then there exists x ∈ s such that f x ≤ ⨍⁻ a in s, f a ∂μ.

Русский

Пусть μ(s) ≠ 0, μ(s) ≠ ∞ и f ∈ Integrable μ.restrict s; существует x ∈ s, такое что f(x) ≤ ⨍⁻ a in s, f a ∂μ.

LaTeX

$$$$ \exists x \in s, \; f(x) \leq \laverage_{s} f $$$$

Lean4

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

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