exists_notMem_null_average_le — Mathlib

English

There exists a point not in a given null set where the value of f is at least its mean.

Русский

Существует точка вне заданного нулевого множества, для которой значение f не меньше своего среднего значения.

LaTeX

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

Lean4

/-- **First moment method**. The maximum of an integrable function is greater than its mean, while
avoiding a null set. -/
theorem exists_notMem_null_average_le (hμ : μ ≠ 0) (hf : Integrable f μ) (hN : μ N = 0) :
    ∃ x, x ∉ N ∧ ⨍ a, f a ∂μ ≤ f x := by simpa [integral_neg, neg_div] using exists_notMem_null_le_average hμ hf.neg hN

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