tendsto_lintegral_apprSeq — Mathlib

English

For a closed set F in X and a finite measure μ, the integrals ∫⁻ hF.apprSeq n with respect to μ converge to μ(F) as n → ∞.

Русский

Для замкнутого множества F в X при конечной мере μ интегралы ∫⁻ hF.apprSeq n dμ сходятся к μ(F) при n → ∞.

LaTeX

$$$\\lim_{n \\to \\infty} \\int_X h_F.apprSeq(n)(x) \\, d\\mu(x) = (\\mu F)$$$

Lean4

/-- The integrals along a decreasing approximating sequence to the indicator of a closed set
tend to the measure of the closed set. -/
theorem tendsto_lintegral_apprSeq [MeasurableSpace X] [OpensMeasurableSpace X] (μ : Measure X) [IsFiniteMeasure μ] :
    Tendsto (fun n ↦ ∫⁻ x, hF.apprSeq n x ∂μ) atTop (𝓝 ((μ : Measure X) F)) :=
  measure_of_cont_bdd_of_tendsto_indicator μ hF.measurableSet hF.apprSeq (apprSeq_apply_le_one hF) (tendsto_apprSeq hF)

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