English
If f and g have disjoint supports, then Integrable (f+g) μ is equivalent to Integrable f μ and Integrable g μ.
Русский
Если поддержки f и g не пересекаются, то Integrable(f+g) ⇔ Integrable(f) ∧ Integrable(g).
LaTeX
$$$\\operatorname{Disjoint}(\\operatorname{support} f, \\operatorname{support} g) \\Rightarrow (\\operatorname{Integrable}(f+g, \\mu) \\iff (\\operatorname{Integrable}(f, \\mu) \\land \\operatorname{Integrable}(g, \\mu))).$$$
Lean4
theorem integrable_add_of_disjoint {f g : α → E} (h : Disjoint (support f) (support g)) (hf : StronglyMeasurable f)
(hg : StronglyMeasurable g) : Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ :=
by
refine ⟨fun hfg => ⟨?_, ?_⟩, fun h => h.1.add h.2⟩
· rw [← indicator_add_eq_left h]; exact hfg.indicator hf.measurableSet_support
· rw [← indicator_add_eq_right h]; exact hfg.indicator hg.measurableSet_support
