tendsto_integral_of_L1 — Mathlib

English

If f equals g almost everywhere, their integrals are equal.

Русский

Если f равна g почти всюду, их интегралы равны.

LaTeX

$$$f =_{ae} g \Rightarrow \int a, f(a) \partial μ = \int a, g(a) \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 => ∫⁻ x, ‖F i x - f x‖ₑ ∂μ) l (𝓝 0)) :
    Tendsto (fun i => ∫ x, F i x ∂μ) l (𝓝 <| ∫ x, f x ∂μ) :=
  by
  by_cases hG : CompleteSpace G
  · simp only [integral, hG, L1.integral]
    exact tendsto_setToFun_of_L1 (dominatedFinMeasAdditive_weightedSMul μ) f hfi hFi hF
  · simp [integral, hG, tendsto_const_nhds]

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