meas_le_lintegral₀ — Mathlib

English

If f is measurable and ε ≥ 0, then μ({x | ε ≤ f x}) ≤ ∫ f dμ / ε when ε > 0; in particular, for ε = 1, μ({x | 1 ≤ f x}) ≤ ∫ f dμ.

Русский

Если f измерима и ε ≥ 0, то μ{x: ε ≤ f(x)} ≤ ∫ f dμ / ε; для ε = 1 получаем μ{x: 1 ≤ f(x)} ≤ ∫ f dμ.

LaTeX

$$$$ μ\{x \mid ε \le f(x)\} \le \dfrac{1}{ε} \int f dμ, \quad ε > 0. $$$$

Lean4

theorem meas_le_lintegral₀ {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) {s : Set α} (hs : ∀ x ∈ s, 1 ≤ f x) :
    μ s ≤ ∫⁻ a, f a ∂μ := by
  apply le_trans _ (mul_meas_ge_le_lintegral₀ hf 1)
  rw [one_mul]
  exact measure_mono hs

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