English
Uniform integrability is preserved by restricting μ to a subset, preserving eLpNorm bounds.
Русский
Uniform Integrable сохраняется при ограничении μ на подмножество; сохраняются пределы eLpNorm.
LaTeX
$$$\\operatorname{UnifIntegrable} f p μ \\Rightarrow \\operatorname{UnifIntegrable} f p (μ\\restrict E)$$$
Lean4
/-- Uniform integrability is preserved by restriction of the measure to a set. -/
protected theorem restrict (hf : UnifIntegrable f p μ) (E : Set α) : UnifIntegrable f p (μ.restrict E) := fun ε hε ↦
by
obtain ⟨δ, hδ_pos, hδε⟩ := hf hε
refine ⟨δ, hδ_pos, fun i s hs hμs ↦ ?_⟩
rw [μ.restrict_apply hs, ← measure_toMeasurable] at hμs
calc
eLpNorm (indicator s (f i)) p (μ.restrict E) = eLpNorm (f i) p (μ.restrict (s ∩ E)) := by
rw [eLpNorm_indicator_eq_eLpNorm_restrict hs, μ.restrict_restrict hs]
_ ≤ eLpNorm (f i) p (μ.restrict (toMeasurable μ (s ∩ E))) :=
(eLpNorm_mono_measure _ <| Measure.restrict_mono (subset_toMeasurable _ _) le_rfl)
_ = eLpNorm (indicator (toMeasurable μ (s ∩ E)) (f i)) p μ :=
(eLpNorm_indicator_eq_eLpNorm_restrict (measurableSet_toMeasurable _ _)).symm
_ ≤ ENNReal.ofReal ε := hδε i _ (measurableSet_toMeasurable _ _) hμs
