exists_le_integral — Mathlib

English

There exists x with laverage ≤ f(x) for a nonnegative measurable f.

Русский

Существует x, для которого laverage ≤ f(x) для неотрицательной измеримой f.

LaTeX

$$$\\exists x, \\; \\operatorname{laverage}(f) \\le f(x)$$$

Lean4

/-- **First moment method**. The minimum of an integrable function is smaller than its integral. -/
theorem exists_le_integral (hf : Integrable f μ) : ∃ x, f x ≤ ∫ a, f a ∂μ := by
  simpa only [average_eq_integral] using exists_le_average (IsProbabilityMeasure.ne_zero μ) hf

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