tendsto_integral_of_L1' — Mathlib

English

If the pointwise almost everywhere equality holds for a family, the iterated integrals are equal.

Русский

Если почти повсеместно выполняется равенство для пары функций, то вложенные интегралы равны.

LaTeX

$$$f =_{ae} g \Rightarrow \int a, \int b, f(a,b) \partial μ \partial ν = \int a, \int b, g(a,b) \partial μ \partial ν$$$

Lean4

/-- If `F i → f` in `L1`, then `∫ x, F i x ∂μ → ∫ x, f x ∂μ`. -/
theorem tendsto_integral_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)) :
    Tendsto (fun i ↦ ∫ x, F i x ∂μ) l (𝓝 (∫ x, f x ∂μ)) :=
  by
  refine tendsto_integral_of_L1 f hfi hFi ?_
  simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply] at hF
  exact hF

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