English
If f is integrable with respect to the sum measure, then the family of numbers i ↦ ∫ f dμ_i has HasSum equal to the total integral over the sum: HasSum (i ↦ ∫ a, f a ∂μ_i) (∫ a, f a ∂(Measure.sum μ)).
Русский
Если f интегрируема по суммарной мере, то серия чисел i ↦ ∫ f dμ_i сходится и сумма равна интегралу по сумме: HasSum (i ↦ ∫ f dμ_i) (∫ f d(∑ μ_i)).
LaTeX
$$$$\text{HasSum}\left( i \mapsto \int a, f(a) \partial\mu_i \right) \left( \int a, f(a) \partial\Big(\sum_i \mu_i\Big) \right).$$$$
Lean4
theorem hasSum_integral_measure {ι} {m : MeasurableSpace α} {f : α → G} {μ : ι → Measure α}
(hf : Integrable f (Measure.sum μ)) : HasSum (fun i => ∫ a, f a ∂μ i) (∫ a, f a ∂Measure.sum μ) :=
by
have hfi : ∀ i, Integrable f (μ i) := fun i => hf.mono_measure (Measure.le_sum _ _)
simp only [HasSum, ← integral_finset_sum_measure fun i _ => hfi i]
refine Metric.nhds_basis_ball.tendsto_right_iff.mpr fun ε ε0 => ?_
lift ε to ℝ≥0 using ε0.le
have hf_lt : (∫⁻ x, ‖f x‖ₑ ∂Measure.sum μ) < ∞ := hf.2
have hmem : ∀ᶠ y in 𝓝 (∫⁻ x, ‖f x‖ₑ ∂Measure.sum μ), (∫⁻ x, ‖f x‖ₑ ∂Measure.sum μ) < y + ε :=
by
refine tendsto_id.add tendsto_const_nhds (lt_mem_nhds (α := ℝ≥0∞) <| ENNReal.lt_add_right ?_ ?_)
exacts [hf_lt.ne, ENNReal.coe_ne_zero.2 (NNReal.coe_ne_zero.1 ε0.ne')]
refine ((hasSum_lintegral_measure (fun x => ‖f x‖ₑ) μ).eventually hmem).mono fun s hs => ?_
obtain ⟨ν, hν⟩ : ∃ ν, (∑ i ∈ s, μ i) + ν = Measure.sum μ :=
by
refine ⟨Measure.sum fun i : ↥(sᶜ : Set ι) => μ i, ?_⟩
simpa only [← Measure.sum_coe_finset] using Measure.sum_add_sum_compl (s : Set ι) μ
rw [Metric.mem_ball, ← coe_nndist, NNReal.coe_lt_coe, ← ENNReal.coe_lt_coe, ← hν]
rw [← hν, integrable_add_measure] at hf
refine (nndist_integral_add_measure_le_lintegral hf.1 hf.2).trans_lt ?_
rw [← hν, lintegral_add_measure, lintegral_finset_sum_measure] at hs
exact lt_of_add_lt_add_left hs
