exists_notMem_null_le_laverage — Mathlib

English

Given a subset N of α with μ(N) = 0, there exists x ∉ N such that f(x) is at least the laverage of f.

Русский

Пусть N ⊆ α имеет μ(N) = 0. Тогда существует x ∉ N такое, что f(x) не меньше laverage(f).

LaTeX

$$$\\exists x\\, (x \\notin N) \\wedge \\operatorname{lavg}_{\\mu}(f) \\le f(x)$$$

Lean4

/-- **First moment method**. The minimum of a measurable function is smaller than its mean, while
avoiding a null set. -/
theorem exists_notMem_null_le_laverage (hμ : μ ≠ 0) (hf : AEMeasurable f μ) (hN : μ N = 0) :
    ∃ x, x ∉ N ∧ f x ≤ ⨍⁻ a, f a ∂μ := by
  have := measure_le_laverage_pos hμ hf
  rw [← measure_diff_null hN] at this
  obtain ⟨x, hx, hxN⟩ := nonempty_of_measure_ne_zero this.ne'
  exact ⟨x, hxN, hx⟩

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