English
If f is UnifIntegrable and almost everywhere equal to g, then g is UnifIntegrable.
Русский
Если f является UnifIntegrable и равно по мере почти everywhere функции g, то g тоже UnifIntegrable.
LaTeX
$$$\\operatorname{UnifIntegrable} f p μ \\land f =_{μ}^{a.e.} g \\Rightarrow \\operatorname{UnifIntegrable} g p μ$$$
Lean4
protected theorem add (hf : UnifIntegrable f p μ) (hg : UnifIntegrable g p μ) (hp : 1 ≤ p)
(hf_meas : ∀ i, AEStronglyMeasurable (f i) μ) (hg_meas : ∀ i, AEStronglyMeasurable (g i) μ) :
UnifIntegrable (f + g) p μ := by
intro ε hε
have hε2 : 0 < ε / 2 := half_pos hε
obtain ⟨δ₁, hδ₁_pos, hfδ₁⟩ := hf hε2
obtain ⟨δ₂, hδ₂_pos, hgδ₂⟩ := hg hε2
refine ⟨min δ₁ δ₂, lt_min hδ₁_pos hδ₂_pos, fun i s hs hμs => ?_⟩
simp_rw [Pi.add_apply, Set.indicator_add']
refine (eLpNorm_add_le ((hf_meas i).indicator hs) ((hg_meas i).indicator hs) hp).trans ?_
have hε_halves : ENNReal.ofReal ε = ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) := by
rw [← ENNReal.ofReal_add hε2.le hε2.le, add_halves]
rw [hε_halves]
exact
add_le_add (hfδ₁ i s hs (hμs.trans (ENNReal.ofReal_le_ofReal (min_le_left _ _))))
(hgδ₂ i s hs (hμs.trans (ENNReal.ofReal_le_ofReal (min_le_right _ _))))
