tendsto_setIntegral_of_L1' — Mathlib

English

If Fi → f in L1, then ∫ Fi → ∫ f.

Русский

Если Fi сходится к f в L1, то интеграл Fi сходится к интегралу f.

LaTeX

$$$\text{Tendsto } \int x, F_i(x) \partial μ \; \to \; \int x, f(x) \partial μ$ under L1 convergence$$

Lean4

/-- If `F i → f` in `L1`, then `∫ x in s, F i x ∂μ → ∫ x in s, f x ∂μ`. -/
theorem tendsto_setIntegral_of_L1' {ι} (f : α → G) (hfi : Integrable f μ) {F : ι → α → G} {l : Filter ι}
    (hFi : ∀ᶠ i in l, Integrable (F i) μ) (hF : Tendsto (fun i ↦ eLpNorm (F i - f) 1 μ) l (𝓝 0)) (s : Set α) :
    Tendsto (fun i ↦ ∫ x in s, F i x ∂μ) l (𝓝 (∫ x in s, f x ∂μ)) :=
  by
  refine tendsto_setIntegral_of_L1 f hfi hFi ?_ s
  simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply] at hF
  exact hF

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