uniformIntegrable_average_real — Mathlib

English

The averaging of a uniformly integrable real-valued sequence is uniformly integrable.

Русский

Среднее по равномерно интегрируемой последовательности вещественных значений сохраняет равномерную интегрируемость.

LaTeX

$$$\mathrm{UniformIntegrable\,average\,real}(p,\mu):\; \mathrm{UniformIntegrable}\;\bigl(n \mapsto \frac{\sum_{i< n} f_i}{n}\bigr)\; p\; \mu$$$

Lean4

/-- The averaging of a uniformly integrable real-valued sequence is also uniformly integrable. -/
theorem uniformIntegrable_average_real (hp : 1 ≤ p) {f : ℕ → α → ℝ} (hf : UniformIntegrable f p μ) :
    UniformIntegrable (fun n => (∑ i ∈ Finset.range n, f i) / (n : α → ℝ)) p μ :=
  by
  convert uniformIntegrable_average hp hf using 2 with n
  ext x
  simp [div_eq_inv_mul]

Похожие утверждения