English
Uniform integrability is preserved by replacing each f_i by indicator of a subset; the Lp-norm bound carries over.
Русский
Униформная интегрируемость сохраняется при замене f_i индикатором подмножества; предел нормы Lp сохраняется.
LaTeX
$$$\\operatorname{indicator} (E) (f i) \\, p \\ μ \\Rightarrow \\text{same bound for indicator functions}$$$
Lean4
/-- Uniform integrability is preserved by restriction of the functions to a set. -/
protected theorem indicator (hf : UnifIntegrable f p μ) (E : Set α) : UnifIntegrable (fun i => E.indicator (f i)) p μ :=
fun ε hε ↦ by
obtain ⟨δ, hδ_pos, hε⟩ := hf hε
refine ⟨δ, hδ_pos, fun i s hs hμs ↦ ?_⟩
calc
eLpNorm (s.indicator (E.indicator (f i))) p μ = eLpNorm (E.indicator (s.indicator (f i))) p μ := by
simp only [indicator_indicator, inter_comm]
_ ≤ eLpNorm (s.indicator (f i)) p μ := (eLpNorm_indicator_le _)
_ ≤ ENNReal.ofReal ε := hε _ _ hs hμs
