exists_laverage_le — Mathlib

English

There exists x such that laverage ≤ f(x) for ENNReal-valued f under μ ≠ 0.

Русский

Существует x, для которого laverage ≤ f(x) при μ ≠ 0.

LaTeX

$$$\\exists x, \\; \\laverage_{μ} f \\le f(x)$$$

Lean4

/-- **First moment method**. The maximum of a measurable function is greater than its mean. -/
theorem exists_laverage_le (hμ : μ ≠ 0) (hint : ∫⁻ a, f a ∂μ ≠ ∞) : ∃ x, ⨍⁻ a, f a ∂μ ≤ f x :=
  let ⟨x, hx⟩ := nonempty_of_measure_ne_zero (measure_laverage_le_pos hμ hint).ne'
  ⟨x, hx⟩

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