measure_setAverage_le_pos — Mathlib

English

Let hμ, hμ₁ be nontrivial and f integrable; then there exists x ∈ s with 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**. An integrable function is greater than its mean on a set of positive
measure. -/
theorem measure_setAverage_le_pos (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ∞) (hf : IntegrableOn f s μ) :
    0 < μ ({x ∈ s | ⨍ a in s, f a ∂μ ≤ f x}) := by
  simpa [integral_neg, neg_div] using measure_le_setAverage_pos hμ hμ₁ hf.neg

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