English
Two Lp-functions sequences (f, g) that are a.e.-equal are uniformly integrable together; convergence of a.e.-equivalence transfers to uniform integrability.
Русский
Две последовательности функций в Lp, совпадающие почти везде, образуют одну и ту же равносильную меру; равенство a.e. переносит UniformIntegrable.
LaTeX
$$$\forall p: \text{Lp},\ f,g: \iota \to \alpha \to \beta,\ (f =ᵐ μ g) \,\Rightarrow\, UniformIntegrable f p μ \iff UniformIntegrable g p μ$$$
Lean4
theorem eLpNorm_indicator_le (hp_one : 1 ≤ p) (hp_top : p ≠ ∞) (hf : MemLp f p μ) {ε : ℝ} (hε : 0 < ε) :
∃ (δ : ℝ) (_ : 0 < δ),
∀ s, MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε :=
by
have hℒp := hf
obtain ⟨⟨f', hf', heq⟩, _⟩ := hf
obtain ⟨δ, hδpos, hδ⟩ := (hℒp.ae_eq heq).eLpNorm_indicator_le_of_meas hp_one hp_top hf' hε
refine ⟨δ, hδpos, fun s hs hμs => ?_⟩
convert hδ s hs hμs using 1
rw [eLpNorm_indicator_eq_eLpNorm_restrict hs, eLpNorm_indicator_eq_eLpNorm_restrict hs]
exact eLpNorm_congr_ae heq.restrict
