measure_support_eapprox_lt_top — Mathlib

English

If the total integral of f is finite, then the supports of eapprox f n have finite measure for each n.

Русский

Если интеграл f конечен, то подмножества поддержки eapprox f n имеют конечную меру для каждого n.

LaTeX

$$$$ \\mu(\\mathrm{supp}(eapprox f n)) < \\infty. $$$$

Lean4

theorem measure_support_eapprox_lt_top {f : α → ℝ≥0∞} (hf_meas : Measurable f) (hf : ∫⁻ x, f x ∂μ ≠ ∞) (n : ℕ) :
    μ (Function.support (eapprox f n)) < ∞ :=
  measure_support_lt_top_of_lintegral_ne_top <| ((lintegral_eapprox_le_lintegral hf_meas n).trans_lt hf.lt_top).ne

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