English
Let f be a continuous map X → E, s_i be a countable family of compact sets with union covering the space, and suppose the sum of ‖f.restrict s_i‖ times μ(real s_i) converges. Then f is integrable on the union.
Русский
Пусть f: X→E непрерывна, s_i — счетная семья компактов, чья объединение покрывает пространство; если сумма ‖f.restrict s_i‖ · μ(s_i) сходится, то f интегрируема на объединении.
LaTeX
$$$$\\text{IntegrableOn}(f, \\bigcup_i s_i, \\mu)$$ under the stated summability condition.$$
Lean4
/-- If `s` is a countable family of compact sets, `f` is a continuous function, and the sequence
`‖f.restrict (s i)‖ * μ (s i)` is summable, then `f` is integrable on the union of the `s i`. -/
theorem integrableOn_iUnion_of_summable_norm_restrict {f : C(X, E)} {s : ι → Compacts X}
(hf : Summable fun i : ι => ‖f.restrict (s i)‖ * μ.real (s i)) : IntegrableOn f (⋃ i : ι, s i) μ :=
by
refine
integrableOn_iUnion_of_summable_integral_norm
(fun i => (map_continuous f).continuousOn.integrableOn_compact (s i).isCompact)
(.of_nonneg_of_le (fun ι => integral_nonneg fun x => norm_nonneg _) (fun i => ?_) hf)
rw [← (Real.norm_of_nonneg (integral_nonneg fun x => norm_nonneg _) : ‖_‖ = ∫ x in s i, ‖f x‖ ∂μ)]
exact
norm_setIntegral_le_of_norm_le_const (s i).isCompact.measure_lt_top fun x hx =>
(norm_norm (f x)).symm ▸ (f.restrict (s i : Set X)).norm_coe_le_norm ⟨x, hx⟩
