English
If a family f is UniformIntegrable, then the sequence of its arithmetic averages is also UniformIntegrable.
Русский
Если семейство f является равномерно интегрируемым, то последовательность её арифметических средних тоже равномерно интегрируема.
LaTeX
$$$\mathrm{UniformIntegrable}(f,p,\mu) \Rightarrow \mathrm{UniformIntegrable}(\lambda n. \sum_{i\in [0,n)} f_i / n, p, \mu)$$$
Lean4
/-- The averaging of a uniformly integrable sequence is also uniformly integrable. -/
theorem uniformIntegrable_average {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (hp : 1 ≤ p) {f : ℕ → α → E}
(hf : UniformIntegrable f p μ) : UniformIntegrable (fun (n : ℕ) => (n : ℝ)⁻¹ • (∑ i ∈ Finset.range n, f i)) p μ :=
by
obtain ⟨hf₁, hf₂, hf₃⟩ := hf
refine ⟨fun n => ?_, fun ε hε => ?_, ?_⟩
· exact (Finset.aestronglyMeasurable_sum _ fun i _ => hf₁ i).const_smul _
· obtain ⟨δ, hδ₁, hδ₂⟩ := hf₂ hε
refine ⟨δ, hδ₁, fun n s hs hle => ?_⟩
simp_rw [Finset.smul_sum, Finset.indicator_sum]
refine le_trans (eLpNorm_sum_le (fun i _ => ((hf₁ i).const_smul _).indicator hs) hp) ?_
have this i : s.indicator ((n : ℝ)⁻¹ • f i) = (↑n : ℝ)⁻¹ • s.indicator (f i) := indicator_const_smul _ _ _
obtain rfl | hn := eq_or_ne n 0
· simp
simp_rw [this, eLpNorm_const_smul, ← Finset.mul_sum]
rw [enorm_inv (by positivity), Real.enorm_natCast, ← ENNReal.div_eq_inv_mul]
refine ENNReal.div_le_of_le_mul' ?_
simpa using Finset.sum_le_card_nsmul (.range n) _ _ fun i _ => hδ₂ _ _ hs hle
· obtain ⟨C, hC⟩ := hf₃
simp_rw [Finset.smul_sum]
refine ⟨C, fun n => (eLpNorm_sum_le (fun i _ => (hf₁ i).const_smul _) hp).trans ?_⟩
obtain rfl | hn := eq_or_ne n 0
· simp
simp_rw [eLpNorm_const_smul, ← Finset.mul_sum]
rw [enorm_inv (by positivity), Real.enorm_natCast, ← ENNReal.div_eq_inv_mul]
refine ENNReal.div_le_of_le_mul' ?_
simpa using Finset.sum_le_card_nsmul (.range n) _ _ fun i _ => hC i
