English
Let f be a function taking values in a normed space E, and let the sets s_i form a countable index family. If each f restricted to s_i is integrable and the sum of the integrals of the norms over s_i is finite, then f is integrable on the union of the s_i.
Русский
Пусть f принимает значения в нормированном пространстве E, и индексы i образуют счетное множество. Если каждая ограниченная на s_i функция интегрируема и сумма норм интегралов по s_i сходится, то f интегрируема на объединении s_i.
LaTeX
$$$$\\text{IntegrableOn}(f, \\bigcup_i s_i, \\mu)$$ given the stated summability condition on the norms.$$
Lean4
theorem integrableOn_iUnion_of_summable_integral_norm {f : X → E} {s : ι → Set X} (hi : ∀ i : ι, IntegrableOn f (s i) μ)
(h : Summable fun i : ι => ∫ x : X in s i, ‖f x‖ ∂μ) : IntegrableOn f (iUnion s) μ :=
by
refine ⟨AEStronglyMeasurable.iUnion fun i => (hi i).1, (lintegral_iUnion_le _ _).trans_lt ?_⟩
have B := fun i => lintegral_coe_eq_integral (fun x : X => ‖f x‖₊) (hi i).norm
simp_rw [enorm_eq_nnnorm, tsum_congr B]
have S' :
Summable fun i : ι => (⟨∫ x : X in s i, ‖f x‖₊ ∂μ, integral_nonneg fun x => NNReal.coe_nonneg _⟩ : NNReal) := by
rw [← NNReal.summable_coe]; exact h
have S'' := ENNReal.tsum_coe_eq S'.hasSum
simp_rw [ENNReal.coe_nnreal_eq, NNReal.coe_mk, coe_nnnorm] at S''
convert ENNReal.ofReal_lt_top
