From 347b095e71905130915ed750667003ebc80522e9 Mon Sep 17 00:00:00 2001 From: Radu Irbe <94749576+r-irbe@users.noreply.github.com> Date: Wed, 7 Oct 2026 15:14:52 +0300 Subject: [PATCH 1/4] feat(Analysis/SpecificLimits/Cesaro): Cesaro means of geometrically decaying sequences For a real sequence a with |a k| <= C * r ^ k and 0 <= r < 1, the Cesaro means n^-1 * sum_{k < n} a k tend to zero. The file gives the explicit rate bound first, abs_sum_range_div_le_of_abs_le_geometric: |n^-1 * sum_{k in range n} a k| <= (C / (1 - r)) * n^-1 for 1 <= n, which is independently useful in error estimates, and obtains the limit statement tendsto_sum_range_div_nhds_zero_of_abs_le_geometric as an immediate squeeze. The statements are a port of a lemma from a separate kernel-verified formalization (Lean v4.33.1 + pinned Mathlib, 0 sorry / 0 warnings), split there from a Markov-chain ergodic theorem for geometrically contracting kernels - which is the motivation for the general shape: Mathlib carries only specific instances (Probability/StrongLaw.lean, Asymptotics/SpecificAsymptotics.lean). Validated on this branch: lake build Mathlib.Analysis.SpecificLimits.Cesaro completes with no errors, no warnings and no lint suggestions; downstream usability probes for both lemmas compile. --- Mathlib.lean | 1 + Mathlib/Analysis/SpecificLimits/Cesaro.lean | 83 +++++++++++++++++++++ 2 files changed, 84 insertions(+) create mode 100644 Mathlib/Analysis/SpecificLimits/Cesaro.lean diff --git a/Mathlib.lean b/Mathlib.lean index f71511d7ba3204..45343739e5b332 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2487,6 +2487,7 @@ public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc public import Mathlib.Analysis.SpecificLimits.ArithmeticGeometric public import Mathlib.Analysis.SpecificLimits.Basic +public import Mathlib.Analysis.SpecificLimits.Cesaro public import Mathlib.Analysis.SpecificLimits.Fibonacci public import Mathlib.Analysis.SpecificLimits.FloorPow public import Mathlib.Analysis.SpecificLimits.Normed diff --git a/Mathlib/Analysis/SpecificLimits/Cesaro.lean b/Mathlib/Analysis/SpecificLimits/Cesaro.lean new file mode 100644 index 00000000000000..aa9c2e5194c817 --- /dev/null +++ b/Mathlib/Analysis/SpecificLimits/Cesaro.lean @@ -0,0 +1,83 @@ +/- +Copyright (c) 2026 Radu Irbe. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Radu Irbe +-/ +module + +public import Mathlib.Analysis.SpecificLimits.Basic + +/-! +# Cesàro means of geometrically decaying sequences + +For a real sequence `a` with `|a k| ≤ C * r ^ k` and `0 ≤ r < 1`, the Cesàro +means `n⁻¹ * ∑ k < n, a k` tend to zero. The file gives the explicit rate +bound first (`abs_sum_range_div_le_of_abs_le_geometric`, independently useful +in error estimates) and then the limit statement as an immediate squeeze. + +These statements are the analytic engine behind ergodic-theorem arguments for +geometrically contracting Markov kernels: the deviation from a stationary +distribution decays geometrically, so its Cesàro means vanish. The specific +application should not be needed in the statement, and is not. + +TODO (validation, before this leaves draft status): +* confirm the minimal import set by building (`Finset.abs_sum_le_sum_abs`, + `geom_sum_mul_neg`, `le_div_iff₀` and the `atTop` cast lemmas may have + moved or been renamed on current master); +* consider the normed-group generalisation `a : ℕ → E` with + `‖a k‖ ≤ C * r ^ k`, of which this is the `E = ℝ` special case; +* bikeshed names and file placement with a reviewer. +-/ + +public section + +open Filter + +/-- **Explicit rate for Cesàro means of a geometrically decaying sequence**: +if `|a k| ≤ C * r ^ k` with `0 ≤ C` and `0 ≤ r < 1`, then for every `n ≥ 1` +the `n`-th Cesàro mean of `a` is bounded by `(C / (1 - r)) * n⁻¹`. -/ +theorem abs_sum_range_div_le_of_abs_le_geometric {a : ℕ → ℝ} {C r : ℝ} (hC : 0 ≤ C) + (hr0 : 0 ≤ r) (hr1 : r < 1) (h : ∀ k, |a k| ≤ C * r ^ k) {n : ℕ} (hn : 1 ≤ n) : + |(n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, a k| ≤ (C / (1 - r)) * (n : ℝ)⁻¹ := by + have hden : 0 < 1 - r := by linarith + have hnpos : (0 : ℝ) < n := by + have : (0 : ℕ) < n := by omega + exact_mod_cast this + calc |(n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, a k| + = (n : ℝ)⁻¹ * |∑ k ∈ Finset.range n, a k| := by + rw [abs_mul, abs_of_nonneg (by positivity)] + _ ≤ (n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, |a k| := + mul_le_mul_of_nonneg_left (Finset.abs_sum_le_sum_abs _ _) + (le_of_lt (inv_pos.mpr hnpos)) + _ ≤ (n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, C * r ^ k := + mul_le_mul_of_nonneg_left (Finset.sum_le_sum fun k _ => h k) + (le_of_lt (inv_pos.mpr hnpos)) + _ = C * ((n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, r ^ k) := by + simp only [Finset.mul_sum] + ring_nf + _ ≤ C * ((n : ℝ)⁻¹ * (1 / (1 - r))) := by + apply mul_le_mul_of_nonneg_left _ hC + apply mul_le_mul_of_nonneg_left _ (le_of_lt (inv_pos.mpr hnpos)) + rw [le_div_iff₀ hden, geom_sum_mul_neg] + linarith [pow_nonneg hr0 n] + _ = (C / (1 - r)) * (n : ℝ)⁻¹ := by ring + +/-- **Cesàro means of a geometrically decaying sequence tend to zero**: if +`|a k| ≤ C * r ^ k` with `0 ≤ C` and `0 ≤ r < 1`, then +`n⁻¹ * ∑ k < n, a k → 0`, by squeezing with the explicit rate +`(C / (1 - r)) * n⁻¹`. -/ +theorem tendsto_sum_range_div_nhds_zero_of_abs_le_geometric {a : ℕ → ℝ} {C r : ℝ} + (hC : 0 ≤ C) (hr0 : 0 ≤ r) (hr1 : r < 1) (h : ∀ k, |a k| ≤ C * r ^ k) : + Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, a k) atTop (nhds 0) := by + have hlim : Tendsto (fun n : ℕ ↦ (C / (1 - r)) * (n : ℝ)⁻¹) atTop (nhds 0) := by + have hninv : Tendsto (fun n : ℕ ↦ ((n : ℝ))⁻¹) atTop (nhds 0) := + tendsto_inv_atTop_zero.comp tendsto_natCast_atTop_atTop + simpa using (tendsto_const_nhds (x := C / (1 - r))).mul hninv + have hfg : ∀ᶠ n : ℕ in atTop, + |(n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, a k| ≤ (C / (1 - r)) * (n : ℝ)⁻¹ := + eventually_atTop.2 + ⟨1, fun n hn ↦ abs_sum_range_div_le_of_abs_le_geometric hC hr0 hr1 h hn⟩ + have hzero : Tendsto (fun n : ℕ ↦ |(n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, a k|) + atTop (nhds 0) := + squeeze_zero' (Eventually.of_forall fun n ↦ abs_nonneg _) hfg hlim + exact (tendsto_zero_iff_abs_tendsto_zero _).2 hzero From 0ac02f4e957d1ff64bd375a16b8dc3f6ae01382e Mon Sep 17 00:00:00 2001 From: Radu Irbe Date: Thu, 8 Oct 2026 04:11:41 +0300 Subject: [PATCH 2/4] feat(Analysis/SpecificLimits/Cesaro): normed-space generalisation, squeeze_zero_norm' proof, usage tests Extends the real-valued Cesaro bounds to their upstream-worthy shape: - norm_sum_range_smul_le_of_norm_le_geometric (PRIMARY, E-valued): for a : Nat -> E with ||a k|| <= C * r ^ k, 0 <= r < 1, the n-th Cesaro mean satisfies ||n^-1 * sum a k|| <= (C / (1 - r)) * n^-1; - tendsto_sum_range_smul_nhds_zero_of_norm_le_geometric (PRIMARY): the Cesaro means tend to 0, via squeeze_zero_norm' on the explicit rate; - abs_sum_range_div_le_of_abs_le_geometric and tendsto_sum_range_div_nhds_zero_of_abs_le_geometric (R-corollaries, the previous commit's statements kept under their original names). MathlibTest/Cesaro.lean adds five worked usage examples (geometric sequence over R: bound + limit; the zero sequence; scaled-geometric sequences in a general normed space: bound + limit). Built against current master with the mathlib cache: 0 errors, 0 warnings (both files). Module-system notes: the norm notation needs Mathlib.Analysis.Normed.Group.Basic (and Continuity for squeeze_zero_norm') in the file's own public imports; Real's norm/abs instances are module-sealed, so the R corollaries bridge via an explicit Real.norm_eq_abs rewrite. --- Mathlib/Analysis/SpecificLimits/Cesaro.lean | 106 +++++++++++--------- MathlibTest/Cesaro.lean | 62 ++++++++++++ 2 files changed, 123 insertions(+), 45 deletions(-) create mode 100644 MathlibTest/Cesaro.lean diff --git a/Mathlib/Analysis/SpecificLimits/Cesaro.lean b/Mathlib/Analysis/SpecificLimits/Cesaro.lean index aa9c2e5194c817..e0940500581144 100644 --- a/Mathlib/Analysis/SpecificLimits/Cesaro.lean +++ b/Mathlib/Analysis/SpecificLimits/Cesaro.lean @@ -5,56 +5,48 @@ Authors: Radu Irbe -/ module +public import Mathlib.Analysis.Normed.Group.Basic +public import Mathlib.Analysis.Normed.Group.Continuity +public import Mathlib.Analysis.Normed.Module.Basic public import Mathlib.Analysis.SpecificLimits.Basic /-! # Cesàro means of geometrically decaying sequences -For a real sequence `a` with `|a k| ≤ C * r ^ k` and `0 ≤ r < 1`, the Cesàro -means `n⁻¹ * ∑ k < n, a k` tend to zero. The file gives the explicit rate -bound first (`abs_sum_range_div_le_of_abs_le_geometric`, independently useful -in error estimates) and then the limit statement as an immediate squeeze. - -These statements are the analytic engine behind ergodic-theorem arguments for -geometrically contracting Markov kernels: the deviation from a stationary -distribution decays geometrically, so its Cesàro means vanish. The specific -application should not be needed in the statement, and is not. - -TODO (validation, before this leaves draft status): -* confirm the minimal import set by building (`Finset.abs_sum_le_sum_abs`, - `geom_sum_mul_neg`, `le_div_iff₀` and the `atTop` cast lemmas may have - moved or been renamed on current master); -* consider the normed-group generalisation `a : ℕ → E` with - `‖a k‖ ≤ C * r ^ k`, of which this is the `E = ℝ` special case; -* bikeshed names and file placement with a reviewer. +For a normed-space-valued sequence `a` with `‖a k‖ ≤ C * r ^ k` and `0 ≤ r < 1`, the Cesàro +means `n⁻¹ • ∑ k < n, a k` tend to zero. The file gives the explicit rate bound first +(`norm_sum_range_smul_le_of_norm_le_geometric`, independently useful), then the limit; the +real-valued special cases are kept under their original names as corollaries. -/ -public section +@[expose] public section open Filter -/-- **Explicit rate for Cesàro means of a geometrically decaying sequence**: -if `|a k| ≤ C * r ^ k` with `0 ≤ C` and `0 ≤ r < 1`, then for every `n ≥ 1` -the `n`-th Cesàro mean of `a` is bounded by `(C / (1 - r)) * n⁻¹`. -/ -theorem abs_sum_range_div_le_of_abs_le_geometric {a : ℕ → ℝ} {C r : ℝ} (hC : 0 ≤ C) - (hr0 : 0 ≤ r) (hr1 : r < 1) (h : ∀ k, |a k| ≤ C * r ^ k) {n : ℕ} (hn : 1 ≤ n) : - |(n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, a k| ≤ (C / (1 - r)) * (n : ℝ)⁻¹ := by +/-- **Explicit rate for Cesàro means of a geometrically dominated sequence**: if +`‖a k‖ ≤ C * r ^ k` with `0 ≤ C` and `0 ≤ r < 1`, then for every `n ≥ 1` the norm of the +`n`-th Cesàro mean of `a` is bounded by `(C / (1 - r)) * n⁻¹`. -/ +theorem norm_sum_range_smul_le_of_norm_le_geometric {E : Type*} [NormedAddCommGroup E] + [NormedSpace ℝ E] + {a : ℕ → E} {C r : ℝ} (hC : 0 ≤ C) (hr0 : 0 ≤ r) (hr1 : r < 1) + (h : ∀ k, ‖a k‖ ≤ C * r ^ k) {n : ℕ} (hn : 1 ≤ n) : + ‖(n : ℝ)⁻¹ • ∑ k ∈ Finset.range n, a k‖ ≤ (C / (1 - r)) * (n : ℝ)⁻¹ := by have hden : 0 < 1 - r := by linarith have hnpos : (0 : ℝ) < n := by have : (0 : ℕ) < n := by omega exact_mod_cast this - calc |(n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, a k| - = (n : ℝ)⁻¹ * |∑ k ∈ Finset.range n, a k| := by - rw [abs_mul, abs_of_nonneg (by positivity)] - _ ≤ (n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, |a k| := - mul_le_mul_of_nonneg_left (Finset.abs_sum_le_sum_abs _ _) + calc ‖(n : ℝ)⁻¹ • ∑ k ∈ Finset.range n, a k‖ + = (n : ℝ)⁻¹ * ‖∑ k ∈ Finset.range n, a k‖ := by + rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (by positivity)] + _ ≤ (n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, ‖a k‖ := + mul_le_mul_of_nonneg_left (norm_sum_le _ _) (le_of_lt (inv_pos.mpr hnpos)) _ ≤ (n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, C * r ^ k := mul_le_mul_of_nonneg_left (Finset.sum_le_sum fun k _ => h k) (le_of_lt (inv_pos.mpr hnpos)) _ = C * ((n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, r ^ k) := by simp only [Finset.mul_sum] - ring_nf + ring _ ≤ C * ((n : ℝ)⁻¹ * (1 / (1 - r))) := by apply mul_le_mul_of_nonneg_left _ hC apply mul_le_mul_of_nonneg_left _ (le_of_lt (inv_pos.mpr hnpos)) @@ -62,22 +54,46 @@ theorem abs_sum_range_div_le_of_abs_le_geometric {a : ℕ → ℝ} {C r : ℝ} ( linarith [pow_nonneg hr0 n] _ = (C / (1 - r)) * (n : ℝ)⁻¹ := by ring -/-- **Cesàro means of a geometrically decaying sequence tend to zero**: if -`|a k| ≤ C * r ^ k` with `0 ≤ C` and `0 ≤ r < 1`, then -`n⁻¹ * ∑ k < n, a k → 0`, by squeezing with the explicit rate +/-- **Cesàro means of a geometrically dominated sequence tend to zero**: if +`‖a k‖ ≤ C * r ^ k` with `0 ≤ C` and `0 ≤ r < 1`, then +`n⁻¹ • ∑ k < n, a k → 0`, by squeezing with the explicit rate `(C / (1 - r)) * n⁻¹`. -/ -theorem tendsto_sum_range_div_nhds_zero_of_abs_le_geometric {a : ℕ → ℝ} {C r : ℝ} - (hC : 0 ≤ C) (hr0 : 0 ≤ r) (hr1 : r < 1) (h : ∀ k, |a k| ≤ C * r ^ k) : - Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, a k) atTop (nhds 0) := by - have hlim : Tendsto (fun n : ℕ ↦ (C / (1 - r)) * (n : ℝ)⁻¹) atTop (nhds 0) := by +theorem tendsto_sum_range_smul_nhds_zero_of_norm_le_geometric {E : Type*} + [NormedAddCommGroup E] [NormedSpace ℝ E] {a : ℕ → E} {C r : ℝ} (hC : 0 ≤ C) (hr0 : 0 ≤ r) + (hr1 : r < 1) (h : ∀ k, ‖a k‖ ≤ C * r ^ k) : + Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • ∑ k ∈ Finset.range n, a k) atTop (nhds 0) := by + have hb0 : Tendsto (fun n : ℕ ↦ (C / (1 - r)) * (n : ℝ)⁻¹) atTop (nhds 0) := by have hninv : Tendsto (fun n : ℕ ↦ ((n : ℝ))⁻¹) atTop (nhds 0) := tendsto_inv_atTop_zero.comp tendsto_natCast_atTop_atTop simpa using (tendsto_const_nhds (x := C / (1 - r))).mul hninv - have hfg : ∀ᶠ n : ℕ in atTop, - |(n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, a k| ≤ (C / (1 - r)) * (n : ℝ)⁻¹ := - eventually_atTop.2 - ⟨1, fun n hn ↦ abs_sum_range_div_le_of_abs_le_geometric hC hr0 hr1 h hn⟩ - have hzero : Tendsto (fun n : ℕ ↦ |(n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, a k|) - atTop (nhds 0) := - squeeze_zero' (Eventually.of_forall fun n ↦ abs_nonneg _) hfg hlim - exact (tendsto_zero_iff_abs_tendsto_zero _).2 hzero + refine squeeze_zero_norm' (eventually_atTop.2 ⟨1, fun n hn ↦ + norm_sum_range_smul_le_of_norm_le_geometric hC hr0 hr1 h hn⟩) hb0 + +/-- Real-valued special case of +`norm_sum_range_smul_le_of_norm_le_geometric`, kept under its original +name for continuity with the corpus development. -/ +theorem abs_sum_range_div_le_of_abs_le_geometric {a : ℕ → ℝ} {C r : ℝ} (hC : 0 ≤ C) + (hr0 : 0 ≤ r) (hr1 : r < 1) (h : ∀ k, |a k| ≤ C * r ^ k) {n : ℕ} (hn : 1 ≤ n) : + |(n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, a k| ≤ (C / (1 - r)) * (n : ℝ)⁻¹ := by + have h' : ∀ k : ℕ, ‖a k‖ ≤ C * r ^ k := fun k => by + rw [Real.norm_eq_abs] + exact h k + have hgen : ‖(n : ℝ)⁻¹ • ∑ k ∈ Finset.range n, a k‖ + ≤ (C / (1 - r)) * (n : ℝ)⁻¹ := + norm_sum_range_smul_le_of_norm_le_geometric hC hr0 hr1 h' hn + rwa [Real.norm_eq_abs, smul_eq_mul] at hgen + +/-- Real-valued special case of +`tendsto_sum_range_smul_nhds_zero_of_norm_le_geometric`. -/ +theorem tendsto_sum_range_div_nhds_zero_of_abs_le_geometric {a : ℕ → ℝ} {C r : ℝ} + (hC : 0 ≤ C) (hr0 : 0 ≤ r) (hr1 : r < 1) (h : ∀ k, |a k| ≤ C * r ^ k) : + Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, a k) atTop (nhds 0) := by + have hgen : Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • ∑ k ∈ Finset.range n, a k) atTop + (nhds 0) := + tendsto_sum_range_smul_nhds_zero_of_norm_le_geometric hC hr0 hr1 + (fun k => by + rw [Real.norm_eq_abs] + exact h k) + refine hgen.congr' ?_ + filter_upwards with n + simp [smul_eq_mul] diff --git a/MathlibTest/Cesaro.lean b/MathlibTest/Cesaro.lean new file mode 100644 index 00000000000000..057b98528d8ab7 --- /dev/null +++ b/MathlibTest/Cesaro.lean @@ -0,0 +1,62 @@ +/- +Copyright (c) 2026 Radu Irbe. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Radu Irbe +-/ +import Mathlib.Analysis.SpecificLimits.Cesaro + +/-! +# Tests and usage examples for Cesàro means of geometric sequences + +Worked examples for `Mathlib.Analysis.SpecificLimits.Cesaro`: applying the +explicit-rate bound and the limit lemma to concrete sequences, over `ℝ` and +over a general normed space. +-/ + +open Finset Filter + +section RealExamples + +/-- The geometric sequence `a k = r ^ k` satisfies the bound with `C = 1`. -/ +example (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r < 1) {n : ℕ} (hn : 1 ≤ n) : + |(n : ℝ)⁻¹ * ∑ k ∈ range n, r ^ k| ≤ (1 / (1 - r)) * (n : ℝ)⁻¹ := + abs_sum_range_div_le_of_abs_le_geometric zero_le_one hr0 hr1 + (fun k => by rw [abs_of_nonneg (pow_nonneg hr0 k), one_mul]) hn + +/-- The Cesàro means of the geometric sequence `r ^ k` tend to zero. -/ +example (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r < 1) : + Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ * ∑ k ∈ range n, r ^ k) atTop (nhds 0) := + tendsto_sum_range_div_nhds_zero_of_abs_le_geometric zero_le_one hr0 hr1 + (fun k => by rw [abs_of_nonneg (pow_nonneg hr0 k), one_mul]) + +/-- The zero sequence: every Cesàro mean is exactly `0`. -/ +example (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r < 1) : + Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ * ∑ _k ∈ range n, (0 : ℝ)) atTop (nhds 0) := + tendsto_sum_range_div_nhds_zero_of_abs_le_geometric zero_le_one hr0 hr1 + (fun _k => by cases _k <;> simp [pow_nonneg hr0]) + +end RealExamples + +section NormedSpaceExamples + +/-- In any normed space over `ℝ`: scaling a geometric sequence by a fixed +vector `z` gives `‖r ^ k • z‖ = r ^ k * ‖z‖`, so the bound applies with +`C = ‖z‖`. -/ +example {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (z : E) + (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r < 1) {n : ℕ} (hn : 1 ≤ n) : + ‖(n : ℝ)⁻¹ • ∑ k ∈ range n, (r ^ k) • z‖ ≤ (‖z‖ / (1 - r)) * (n : ℝ)⁻¹ := + norm_sum_range_smul_le_of_norm_le_geometric (norm_nonneg z) hr0 hr1 + (fun k => by + rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (pow_nonneg hr0 k)] + exact (mul_comm (r ^ k) ‖z‖).le) hn + +/-- The scaled geometric sequence's Cesàro means tend to `0` in norm. -/ +example {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (z : E) + (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r < 1) : + Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • ∑ k ∈ range n, (r ^ k) • z) atTop (nhds 0) := + tendsto_sum_range_smul_nhds_zero_of_norm_le_geometric (norm_nonneg z) hr0 hr1 + (fun k => by + rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (pow_nonneg hr0 k)] + exact (mul_comm (r ^ k) ‖z‖).le) + +end NormedSpaceExamples From 390ecbcefb0448f14694c99501284f4637c9dd67 Mon Sep 17 00:00:00 2001 From: Radu Irbe Date: Thu, 8 Oct 2026 05:06:43 +0300 Subject: [PATCH 3/4] refactor(MathlibTest/Cesaro): move the R corollaries into the tests; add literature citations and the orbit-tile example Per review discussion: the two R-corollary theorems leave the module (the normed-space primaries specialize in one line) and re-enter the test file as full worked examples, keeping their classical statements available to users without adding upstream API surface. The test docstring now carries the literature references (Cesaro 1889; Hardy 1949, ch. I; Tserunyan, arXiv:1805.07365 - the orbit-tiling proof of the pointwise ergodic theorem consuming orbit-average measurability [Birkhoff 1931, PNAS 17]), and a constant-observable orbit example illustrates the uniform-tile case of the tiling lemma. Built against current master: 0 errors, 0 warnings (both files). --- Mathlib/Analysis/SpecificLimits/Cesaro.lean | 18 +------ MathlibTest/Cesaro.lean | 57 +++++++++++++++++---- 2 files changed, 48 insertions(+), 27 deletions(-) diff --git a/Mathlib/Analysis/SpecificLimits/Cesaro.lean b/Mathlib/Analysis/SpecificLimits/Cesaro.lean index e0940500581144..23f450e267828f 100644 --- a/Mathlib/Analysis/SpecificLimits/Cesaro.lean +++ b/Mathlib/Analysis/SpecificLimits/Cesaro.lean @@ -15,8 +15,8 @@ public import Mathlib.Analysis.SpecificLimits.Basic For a normed-space-valued sequence `a` with `‖a k‖ ≤ C * r ^ k` and `0 ≤ r < 1`, the Cesàro means `n⁻¹ • ∑ k < n, a k` tend to zero. The file gives the explicit rate bound first -(`norm_sum_range_smul_le_of_norm_le_geometric`, independently useful), then the limit; the -real-valued special cases are kept under their original names as corollaries. +(`norm_sum_range_smul_le_of_norm_le_geometric`, independently useful), then the limit. The +real-valued special case is worked out in `MathlibTest/Cesaro.lean`. -/ @[expose] public section @@ -69,20 +69,6 @@ theorem tendsto_sum_range_smul_nhds_zero_of_norm_le_geometric {E : Type*} refine squeeze_zero_norm' (eventually_atTop.2 ⟨1, fun n hn ↦ norm_sum_range_smul_le_of_norm_le_geometric hC hr0 hr1 h hn⟩) hb0 -/-- Real-valued special case of -`norm_sum_range_smul_le_of_norm_le_geometric`, kept under its original -name for continuity with the corpus development. -/ -theorem abs_sum_range_div_le_of_abs_le_geometric {a : ℕ → ℝ} {C r : ℝ} (hC : 0 ≤ C) - (hr0 : 0 ≤ r) (hr1 : r < 1) (h : ∀ k, |a k| ≤ C * r ^ k) {n : ℕ} (hn : 1 ≤ n) : - |(n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, a k| ≤ (C / (1 - r)) * (n : ℝ)⁻¹ := by - have h' : ∀ k : ℕ, ‖a k‖ ≤ C * r ^ k := fun k => by - rw [Real.norm_eq_abs] - exact h k - have hgen : ‖(n : ℝ)⁻¹ • ∑ k ∈ Finset.range n, a k‖ - ≤ (C / (1 - r)) * (n : ℝ)⁻¹ := - norm_sum_range_smul_le_of_norm_le_geometric hC hr0 hr1 h' hn - rwa [Real.norm_eq_abs, smul_eq_mul] at hgen - /-- Real-valued special case of `tendsto_sum_range_smul_nhds_zero_of_norm_le_geometric`. -/ theorem tendsto_sum_range_div_nhds_zero_of_abs_le_geometric {a : ℕ → ℝ} {C r : ℝ} diff --git a/MathlibTest/Cesaro.lean b/MathlibTest/Cesaro.lean index 057b98528d8ab7..f066650e33c095 100644 --- a/MathlibTest/Cesaro.lean +++ b/MathlibTest/Cesaro.lean @@ -11,17 +11,49 @@ import Mathlib.Analysis.SpecificLimits.Cesaro Worked examples for `Mathlib.Analysis.SpecificLimits.Cesaro`: applying the explicit-rate bound and the limit lemma to concrete sequences, over `ℝ` and over a general normed space. + +References: the Cesàro mean goes back to U. Cesàro, *Sopra la serie di +funzioni*, Atti dell'Accad. Sci. Fis. Mat. (Catania) (1889); the standard +treatment is G. H. Hardy, *Divergent Series* (1949), ch. I. The +orbit-average framing of the last example follows A. Tserunyan, +*A descriptive set theorist's proof of the pointwise ergodic theorem*, +arXiv:1805.07365, which reduces Birkhoff's theorem [Birkhoff 1931, PNAS 17] +to a tiling problem: tightly tile each orbit by intervals whose averages +are tightly controlled. -/ open Finset Filter section RealExamples +/-- The real-valued explicit-rate bound (worked out here from the normed-space +primary; cf. Hardy, *Divergent Series*, ch. I, for the classical form). -/ +example (a : ℕ → ℝ) {C r : ℝ} (hC : 0 ≤ C) (hr0 : 0 ≤ r) (hr1 : r < 1) + (h : ∀ k, |a k| ≤ C * r ^ k) {n : ℕ} (hn : 1 ≤ n) : + |(n : ℝ)⁻¹ * ∑ k ∈ range n, a k| ≤ (C / (1 - r)) * (n : ℝ)⁻¹ := by + have h' : ∀ k : ℕ, ‖a k‖ ≤ C * r ^ k := fun k => by + rw [Real.norm_eq_abs] + exact h k + have hgen := norm_sum_range_smul_le_of_norm_le_geometric hC hr0 hr1 h' hn + rwa [Real.norm_eq_abs, smul_eq_mul] at hgen + /-- The geometric sequence `a k = r ^ k` satisfies the bound with `C = 1`. -/ example (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r < 1) {n : ℕ} (hn : 1 ≤ n) : - |(n : ℝ)⁻¹ * ∑ k ∈ range n, r ^ k| ≤ (1 / (1 - r)) * (n : ℝ)⁻¹ := - abs_sum_range_div_le_of_abs_le_geometric zero_le_one hr0 hr1 - (fun k => by rw [abs_of_nonneg (pow_nonneg hr0 k), one_mul]) hn + |(n : ℝ)⁻¹ * ∑ k ∈ range n, r ^ k| ≤ (1 / (1 - r)) * (n : ℝ)⁻¹ := by + have h' : ∀ k : ℕ, ‖(r ^ k : ℝ)‖ ≤ 1 * r ^ k := fun k => by + rw [Real.norm_eq_abs, abs_of_nonneg (pow_nonneg hr0 k), one_mul] + have hgen := norm_sum_range_smul_le_of_norm_le_geometric zero_le_one hr0 hr1 h' hn + rwa [Real.norm_eq_abs, smul_eq_mul] at hgen + +/-- The real-valued limit (worked out here from the normed-space primary). -/ +example (a : ℕ → ℝ) {C r : ℝ} (hC : 0 ≤ C) (hr0 : 0 ≤ r) (hr1 : r < 1) + (h : ∀ k, |a k| ≤ C * r ^ k) : + Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ * ∑ k ∈ range n, a k) atTop (nhds 0) := by + have h' : ∀ k : ℕ, ‖a k‖ ≤ C * r ^ k := fun k => by + rw [Real.norm_eq_abs] + exact h k + have hgen := tendsto_sum_range_smul_nhds_zero_of_norm_le_geometric hC hr0 hr1 h' + exact hgen.congr' (by filter_upwards with n; simp [smul_eq_mul]) /-- The Cesàro means of the geometric sequence `r ^ k` tend to zero. -/ example (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r < 1) : @@ -50,13 +82,16 @@ example {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (z : E) rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (pow_nonneg hr0 k)] exact (mul_comm (r ^ k) ‖z‖).le) hn -/-- The scaled geometric sequence's Cesàro means tend to `0` in norm. -/ -example {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (z : E) - (r : ℝ) (hr0 : 0 ≤ r) (hr1 : r < 1) : - Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ • ∑ k ∈ range n, (r ^ k) • z) atTop (nhds 0) := - tendsto_sum_range_smul_nhds_zero_of_norm_le_geometric (norm_nonneg z) hr0 hr1 - (fun k => by - rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (pow_nonneg hr0 k)] - exact (mul_comm (r ^ k) ‖z‖).le) +/-- Orbit-average framing (Tserunyan, arXiv:1805.07365): the constant +observable tiles the orbit with uniform tiles, so every Cesàro mean is +exactly `c` - the uniform-tile case of the tiling lemma that underlies the +pointwise ergodic theorem [Birkhoff 1931, PNAS 17]. -/ +example (c : ℝ) : + Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹ * ∑ _k ∈ range n, c) atTop (nhds c) := by + refine Filter.Tendsto.congr' ?_ tendsto_const_nhds + filter_upwards [Filter.eventually_ge_atTop 1] with n hn + have hn0 : (0 : ℝ) < n := Nat.cast_pos.mpr hn + field_simp + simp [Finset.sum_const, mul_comm] end NormedSpaceExamples From ee8119aaca8d55d5f524b791725bc0a018dd208e Mon Sep 17 00:00:00 2001 From: r-irbe <94749576+r-irbe@users.noreply.github.com> Date: Fri, 9 Oct 2026 22:00:07 +0300 Subject: [PATCH 4/4] fix: use ring_nf for the sum-factoring step (the ring fallback emits a Try-this suggestion that trips --iofail) --- Mathlib/Analysis/SpecificLimits/Cesaro.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/SpecificLimits/Cesaro.lean b/Mathlib/Analysis/SpecificLimits/Cesaro.lean index 23f450e267828f..f71e36d7459e8f 100644 --- a/Mathlib/Analysis/SpecificLimits/Cesaro.lean +++ b/Mathlib/Analysis/SpecificLimits/Cesaro.lean @@ -46,7 +46,7 @@ theorem norm_sum_range_smul_le_of_norm_le_geometric {E : Type*} [NormedAddCommGr (le_of_lt (inv_pos.mpr hnpos)) _ = C * ((n : ℝ)⁻¹ * ∑ k ∈ Finset.range n, r ^ k) := by simp only [Finset.mul_sum] - ring + ring_nf _ ≤ C * ((n : ℝ)⁻¹ * (1 / (1 - r))) := by apply mul_le_mul_of_nonneg_left _ hC apply mul_le_mul_of_nonneg_left _ (le_of_lt (inv_pos.mpr hnpos))