exists_le_setAverage — Mathlib

English

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

Русский

Пусть μ(s) ≠ 0 и μ(s) ≠ ∞ и f интегрируема; существует x ∈ s, удовлетворяющее f(x) ≤ ⨍ a in s, f(a) ∂μ.

LaTeX

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

Lean4

/-- **First moment method**. The minimum of an integrable function is smaller than its mean. -/
theorem exists_le_setAverage (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ∞) (hf : IntegrableOn f s μ) :
    ∃ x ∈ s, f x ≤ ⨍ a in s, f a ∂μ :=
  let ⟨x, hx, h⟩ := nonempty_of_measure_ne_zero (measure_le_setAverage_pos hμ hμ₁ hf).ne'
  ⟨x, hx, h⟩

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