English
If f and g are uniformly tight with respect to p and μ and are AEStronglyMeasurable termwise, then f − g is uniformly tight with respect to p and μ.
Русский
Если у функций f и g есть униформная ограниченность (tightness) относительно p и μ и каждая пара f_i, g_i является AEStronglyMeasurable, то их разность f − g имеет ту же униформную ограниченность.
LaTeX
$$$\\operatorname{UnifTight}\\\\; f\\\\ p\\\\ μ \\\\land \\\\operatorname{UnifTight}\\\\; g\\\\ p\\\\ μ \\\\land \\\\forall i,\\\\ AEStronglyMeasurable\\\\; (f\\\\ i) \\\\land \\\\forall i,\\\\ AEStronglyMeasurable\\\\; (g\\\\ i) \\\\Rightarrow \\\\operatorname{UnifTight}\\\\; (f-g)\\\\; p\\\\; μ$$$
Lean4
protected theorem sub (hf : UnifTight f p μ) (hg : UnifTight g p μ) (hf_meas : ∀ i, AEStronglyMeasurable (f i) μ)
(hg_meas : ∀ i, AEStronglyMeasurable (g i) μ) : UnifTight (f - g) p μ :=
by
rw [sub_eq_add_neg]
exact hf.add hg.neg hf_meas fun i => (hg_meas i).neg
