hasSum_integral_of_summable_integral_norm

English

Let F_i: α → G be integrable with a dominating summable bound bound_i, and suppose HasSum of F_i(a) exists almost everywhere to f(a). Then the HasSum of the integrals equals the integral of the sum: the series ∑_i ∫ F_i = ∫ f.

Русский

Пусть F_i: α → G интегрируемы с существующим суммирующим ограничителем bound_i, и предположим, что ∃ f such that HasSum(F_i(a)) = f(a) почти всюду. Тогда ∑_i ∫ F_i = ∫ f.

LaTeX

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

Lean4

theorem hasSum_integral_of_summable_integral_norm {ι} [Countable ι] {F : ι → α → E}
    (hF_int : ∀ i : ι, Integrable (F i) μ) (hF_sum : Summable fun i ↦ ∫ a, ‖F i a‖ ∂μ) :
    HasSum (∫ a, F · a ∂μ) (∫ a, (∑' i, F i a) ∂μ) :=
  by
  by_cases hE : CompleteSpace E; swap
  · simp [integral, hE, hasSum_zero]
  rw [integral_tsum (fun i ↦ (hF_int i).1)]
  · exact (hF_sum.of_norm_bounded fun i ↦ norm_integral_le_integral_norm _).hasSum
  have (i : ι) : ∫⁻ a, ‖F i a‖ₑ ∂μ = ‖∫ a, ‖F i a‖ ∂μ‖ₑ :=
    by
    dsimp [enorm]
    rw [lintegral_coe_eq_integral _ (hF_int i).norm, coe_nnreal_eq, coe_nnnorm,
      Real.norm_of_nonneg (integral_nonneg (fun a ↦ norm_nonneg (F i a)))]
    simp only [coe_nnnorm]
  rw [funext this]
  exact ENNReal.tsum_coe_ne_top_iff_summable.2 <| NNReal.summable_coe.1 hF_sum.abs

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