cesaro — Mathlib

English

If a sequence u converges to l, then the Cesàro average of u converges to l as well.

Русский

Если последовательность u сходится к l, то её среднее по Цезаро также сходится к l.

LaTeX

$$$\operatorname{Tendsto}\left(n \mapsto \frac{1}{n} \sum_{i=0}^{n-1} u(i)\right) \to l$$$

Lean4

/-- The Cesaro average of a converging sequence converges to the same limit. -/
theorem cesaro {u : ℕ → ℝ} {l : ℝ} (h : Tendsto u atTop (𝓝 l)) :
    Tendsto (fun n : ℕ => (n⁻¹ : ℝ) * ∑ i ∈ range n, u i) atTop (𝓝 l) :=
  h.cesaro_smul

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