exists_average_le — Mathlib

English

If μ is a finite measure and f is integrable, then there exists a point x such that f(x) is no larger than the average value of f with respect to μ.

Русский

Пусть μ—переменная конечная мера, а f—интегрируемая функция. Тогда существует точка x, для которой f(x) не превышает среднее значение f по μ.

LaTeX

$$$\\exists x,\\; f(x) \\le \\operatorname{average}_{\\mu} f = \\int a \\; f(a)\\,d\\mu\\, / \\, \\mu(\\text{dom})$$$

Lean4

/-- **First moment method**. The maximum of an integrable function is greater than its mean. -/
theorem exists_average_le (hμ : μ ≠ 0) (hf : Integrable f μ) : ∃ x, ⨍ a, f a ∂μ ≤ f x :=
  let ⟨x, hx⟩ := nonempty_of_measure_ne_zero (measure_average_le_pos hμ hf).ne'
  ⟨x, hx⟩

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