English
If f is uniformly tight with respect to p and μ and f_n equals g_n almost everywhere for all n, then g is also uniformly tight with respect to p and μ.
Русский
Если f обладает униформной ограниченностью по отношению к p и μ и для всех n совпадает почти во множестве по мере μ функция f_n и g_n, то g тоже обладает униформной ограниченностью по отношению к p и μ.
LaTeX
$$$\\operatorname{UnifTight}\\\\; f\\\\ p\\\\ μ \\\\land \\\\forall n,\\\\ f_n=_{μ}^{a.e.} g_n \\\\Rightarrow \\\\operatorname{UnifTight}\\\\; g\\\\; p\\\\; μ$$$
Lean4
protected theorem aeeq (hf : UnifTight f p μ) (hfg : ∀ n, f n =ᵐ[μ] g n) : UnifTight g p μ :=
by
intro ε hε
obtain ⟨s, hμs, hfε⟩ := hf hε
refine ⟨s, hμs, fun n => (le_of_eq <| eLpNorm_congr_ae ?_).trans (hfε n)⟩
filter_upwards [hfg n] with x hx
simp only [indicator, mem_compl_iff, hx]
