tsum_intervalIntegral_eq_of_summable_norm

English

If a countable family of continuous maps f_i from R to E has summable restricted norms on a compact interval, then the tsum of interval integrals equals the interval integral of tsum.

Русский

Если последовательность непрерывных отображений f_i: R → E имеет суммируемые нормы ограничений на компактном интервале, то tsum-интегралы равны интегралу tsum.

LaTeX

$$$\\text{tsum}\\_i \\int_{a}^{b} f_i(x) \\,dx = \\int_{a}^{b} \\sum_i f_i(x) \\,dx$$$

Lean4

theorem tsum_intervalIntegral_eq_of_summable_norm [Countable ι] {f : ι → C(ℝ, E)}
    (hf_sum : Summable fun i : ι => ‖(f i).restrict (⟨uIcc a b, isCompact_uIcc⟩ : Compacts ℝ)‖) :
    ∑' i : ι, ∫ x in a..b, f i x = ∫ x in a..b, ∑' i : ι, f i x :=
  (hasSum_intervalIntegral_of_summable_norm hf_sum).tsum_eq

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