integral_tsum_of_summable_integral_norm

English

If a sequence F_i is integrable and the series of norms ∑ ∫ ‖F_i‖ converges, then the sum of integrals equals the integral of the sum in normed spaces: HasSum (i ↦ ∫ F_i) (∫ tsum F_i).

Русский

Пусть F_i интегрируемы и сумма норм ∑ ∫ ‖F_i‖ сходится. Тогда сумма интегралов равна интегралу суммы в нормированном пространстве: HasSum(∑ ∫ F_i) = ∫ tsum F_i.

LaTeX

$$$\\text{HasSum}\\left(\\lambda i, \\int_α F_i(a)\\,dμ(a)\\right)\\left(\\int_α \\sum_i F_i(a) \\,dμ(a)\\right)$$$

Lean4

theorem integral_tsum_of_summable_integral_norm {ι} [Countable ι] {F : ι → α → E} (hF_int : ∀ i : ι, Integrable (F i) μ)
    (hF_sum : Summable fun i ↦ ∫ a, ‖F i a‖ ∂μ) : ∑' i, (∫ a, F i a ∂μ) = ∫ a, (∑' i, F i a) ∂μ :=
  (hasSum_integral_of_summable_integral_norm hF_int hF_sum).tsum_eq

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