exists_notMem_null_le_average — Mathlib

English

Let μ be a finite measure with μ(μ) ≠ 0, and f integrable. Then there exists x not in a null set N with the average of f bounded above by f(x).

Русский

Пусть μ—конечная мера с μ ≠ 0, и f интегрируема. Тогда существует x, не принадлежащее нулевой мере N, такое что среднее значение f ≤ f(x).

LaTeX

$$$\\exists x, x \\notin N \\land \\big( \\langle f(x) \\rangle \\ge \\operatorname{average}_{\\mu} f \\big)$$$

Lean4

/-- **First moment method**. The minimum of an integrable function is smaller than its mean, while
avoiding a null set. -/
theorem exists_notMem_null_le_average (hμ : μ ≠ 0) (hf : Integrable f μ) (hN : μ N = 0) :
    ∃ x, x ∉ N ∧ f x ≤ ⨍ a, f a ∂μ := by
  have := measure_le_average_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⟩

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