exists_le_laverage — Mathlib

English

For any nonzero finite measure and AEMeasurable f: α → ℝ≥0∞, there exists a point x with f(x) not exceeding the laverage of f.

Русский

Для любой ненулевой конечной меры и AEMeasurable f: α → ℝ≥0∞ существует точка x, для которой f(x) не превосходит laverage(f).

LaTeX

$$$\\exists x\\, f(x) \\le \\operatorname{lavg}_{\\mu}(f)$$$

Lean4

/-- **First moment method**. The minimum of a measurable function is smaller than its mean. -/
theorem exists_le_laverage (hμ : μ ≠ 0) (hf : AEMeasurable f μ) : ∃ x, f x ≤ ⨍⁻ a, f a ∂μ :=
  let ⟨x, hx⟩ := nonempty_of_measure_ne_zero (measure_le_laverage_pos hμ hf).ne'
  ⟨x, hx⟩

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