English
For a countable family of integrable functions f_i: α → G (with AEStronglyMeasurable), if the series ∑_i ∫ ‖f_i‖ is finite, then the integral and summation commute: ∫ α ∑_i f_i = ∑_i ∫ α f_i.
Русский
Пусть дано послідовність інтегрованих функцій f_i: α → G (AEStronglyMeasurable). Если послідовність сум ∑_i ∫ ‖f_i‖ обмежена, то інтеграл від суми дорівнює сумі інтегралів: ∫ α (∑_i f_i) dμ = ∑_i ∫ α f_i dμ.
LaTeX
$$$\\int_α \\Bigl(\\sum_i f_i(a)\\Bigr) \\,dμ(a) = \\sum_i \\int_α f_i(a) \\,dμ(a)$$$
Lean4
theorem integral_tsum {ι} [Countable ι] {f : ι → α → G} (hf : ∀ i, AEStronglyMeasurable (f i) μ)
(hf' : ∑' i, ∫⁻ a : α, ‖f i a‖ₑ ∂μ ≠ ∞) : ∫ a : α, ∑' i, f i a ∂μ = ∑' i, ∫ a : α, f i a ∂μ :=
by
by_cases hG : CompleteSpace G; swap
· simp [integral, hG]
have hf'' i : AEMeasurable (‖f i ·‖ₑ) μ := (hf i).enorm
have hhh : ∀ᵐ a : α ∂μ, Summable fun n => (‖f n a‖₊ : ℝ) :=
by
rw [← lintegral_tsum hf''] at hf'
refine (ae_lt_top' (AEMeasurable.ennreal_tsum hf'') hf').mono ?_
intro x hx
rw [← ENNReal.tsum_coe_ne_top_iff_summable_coe]
exact hx.ne
convert (MeasureTheory.hasSum_integral_of_dominated_convergence (fun i a => ‖f i a‖₊) hf _ hhh ⟨_, _⟩ _).tsum_eq.symm
· intro n
filter_upwards with x
rfl
· simp_rw [← NNReal.coe_tsum]
rw [aestronglyMeasurable_iff_aemeasurable]
apply AEMeasurable.coe_nnreal_real
apply AEMeasurable.nnreal_tsum
exact fun i => (hf i).nnnorm.aemeasurable
· dsimp [HasFiniteIntegral]
have : ∫⁻ a, ∑' n, ‖f n a‖ₑ ∂μ < ⊤ := by rwa [lintegral_tsum hf'', lt_top_iff_ne_top]
convert this using 1
apply lintegral_congr_ae
simp_rw [← coe_nnnorm, ← NNReal.coe_tsum, enorm_eq_nnnorm, NNReal.nnnorm_eq]
filter_upwards [hhh] with a ha
exact ENNReal.coe_tsum (NNReal.summable_coe.mp ha)
· filter_upwards [hhh] with x hx
exact hx.of_norm.hasSum
