integral_tendsto_of_countably_generated

English

Under suitable conditions, the integral of f equals the limit integral of f as the bounding sets vary with i.

Русский

При соответствующих условиях интеграл f равен пределу интеграла, когда ограничивающие множества варьируются по i.

LaTeX

$$$\\int f = \\lim_i \\int_{φ i} f$$$

Lean4

theorem integral_tendsto_of_countably_generated [l.IsCountablyGenerated] {φ : ι → Set α} (hφ : AECover μ l φ)
    {f : α → E} (hfi : Integrable f μ) : Tendsto (fun i => ∫ x in φ i, f x ∂μ) l (𝓝 <| ∫ x, f x ∂μ) :=
  suffices h : Tendsto (fun i => ∫ x : α, (φ i).indicator f x ∂μ) l (𝓝 (∫ x : α, f x ∂μ)) from by convert h using 2;
    rw [integral_indicator (hφ.measurableSet _)]
  tendsto_integral_filter_of_dominated_convergence (fun x => ‖f x‖)
    (Eventually.of_forall fun i => hfi.aestronglyMeasurable.indicator <| hφ.measurableSet i)
    (Eventually.of_forall fun _ => ae_of_all _ fun _ => norm_indicator_le_norm_self _ _) hfi.norm
    (hφ.ae_tendsto_indicator f)

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