exists_notMem_null_integral_le — Mathlib

English

There exists x not in a null set N with ∫ f ≤ f(x).

Русский

Существует x не из нулевого множества N, такое что интеграл ≤ f(x).

LaTeX

$$$\\exists x, x \\notin N \\land \\int a\, f(a)\\, d\\mu a \\le f(x)$$$

Lean4

/-- **First moment method**. The maximum of an integrable function is greater than its integral,
while avoiding a null set. -/
theorem exists_notMem_null_integral_le (hf : Integrable f μ) (hN : μ N = 0) : ∃ x, x ∉ N ∧ ∫ a, f a ∂μ ≤ f x := by
  simpa only [average_eq_integral] using exists_notMem_null_average_le (IsProbabilityMeasure.ne_zero μ) hf hN

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