English
Let f and g be families of α→β functions indexed by ι. If f and g are uniformly tight with respect to p and μ, and each f_i and g_i is AEStronglyMeasurable, then the pointwise sum f_i + g_i is uniformly tight with respect to p and μ.
Русский
Пусть f и g — семейства функций из α в β, индексируемые по ι. Если f и g имеют униформно ограниченность (uniform tightness) относительно p и μ, и для каждого i функции f_i и g_i являются AEStronglyMeasurable, то поперечное суммирование f_i + g_i тоже имеет униформно ограниченность относительно p и μ.
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 add (hf : UnifTight f p μ) (hg : UnifTight g p μ) (hf_meas : ∀ i, AEStronglyMeasurable (f i) μ)
(hg_meas : ∀ i, AEStronglyMeasurable (g i) μ) : UnifTight (f + g) p μ := fun ε hε ↦
by
rcases exists_Lp_half β μ p (coe_ne_zero.mpr hε.ne') with ⟨η, hη_pos, hη⟩
by_cases hη_top : η = ∞
· replace hη := hη_top ▸ hη
refine ⟨∅, (by simp), fun i ↦ ?_⟩
simp only [compl_empty, indicator_univ, Pi.add_apply]
exact (hη (f i) (g i) (hf_meas i) (hg_meas i) le_top le_top).le
obtain ⟨s, hμs, hsm, hfs, hgs⟩ :
∃ s ∈ μ.cofinite,
MeasurableSet s ∧ (∀ i, eLpNorm (s.indicator (f i)) p μ ≤ η) ∧ (∀ i, eLpNorm (s.indicator (g i)) p μ ≤ η) :=
((hf.eventually_cofinite_indicator hη_pos.ne').and
(hg.eventually_cofinite_indicator hη_pos.ne')).exists_measurable_mem_of_smallSets
refine ⟨sᶜ, ne_of_lt hμs, fun i ↦ ?_⟩
have η_cast : ↑η.toNNReal = η := coe_toNNReal hη_top
calc
eLpNorm (indicator sᶜᶜ (f i + g i)) p μ = eLpNorm (indicator s (f i) + indicator s (g i)) p μ := by
rw [compl_compl, indicator_add']
_ ≤ ε :=
le_of_lt <| hη _ _ ((hf_meas i).indicator hsm) ((hg_meas i).indicator hsm) (η_cast ▸ hfs i) (η_cast ▸ hgs i)
