exists_notMem_null_le_integral — Mathlib

English

There exists x not in N with f(x) ≤ ∫ f dμ when μ(N) = 0.

Русский

Существует x не принадлежащее N, для которого f(x) не превышает интеграл f по μ, если μ(N) = 0.

LaTeX

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

Lean4

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

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