CesaroAlgebra

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Elementary algebra of the Cesàro window average

Algsuperdiff/Probability/CesaroWindow.lean defines the §4.2 window average cesaroAvg f n m = (m − n + 1)⁻¹ · ∑_{k ∈ [n, m]} f k

(avsum_{k=n}^m in ABK26, §4.2) together with the rpow bookkeeping and the Γ_σ centering layer, but proves nothing about the average as a linear functional. This module supplies that basic API: additivity, constants, scalar multiples, monotonicity, and a four-term convenience form matching the D₁ + D₂ + D₃ + const shape of the l.minimal.scale.sep decomposition.

Everything here assumes n ≤ m, which is exactly the condition making the window nonempty and the normalizing factor (m − n + 1 : ℝ) positive.

cesaroAvg_denom_pos and cesaroAvg_card are the cesaroAvg-facing names for the window facts already proved in CesaroWindow.lean (window_pos, natCast_card_Icc_int); they delegate rather than duplicate the proofs.

Main results

• Algsuperdiff.Probability.cesaroAvg_add
• Algsuperdiff.Probability.cesaroAvg_const_mul
• Algsuperdiff.Probability.cesaroAvg_mono
• Algsuperdiff.Probability.cesaroAvg_add4

References

• ABK26, l.minimal.scale.sep for the window average.

theorem Algsuperdiff.Probability.cesaroAvg_denom_pos {n m : ℤ} (hnm : n ≤ m) : 0 < ↑(m - n + 1)

The window normalizer (m − n + 1 : ℝ) is positive on a nonempty window.

theorem Algsuperdiff.Probability.cesaroAvg_card {n m : ℤ} (hnm : n ≤ m) : ↑(Finset.Icc n m).card = ↑(m - n + 1)

The window [n, m] has exactly m − n + 1 elements.

theorem Algsuperdiff.Probability.cesaroAvg_add (f g : ℤ → ℝ) (n m : ℤ) : cesaroAvg (fun (k : ℤ) => f k + g k) n m = cesaroAvg f n m + cesaroAvg g n m

cesaroAvg is additive in its integrand.

theorem Algsuperdiff.Probability.cesaroAvg_const_mul (c : ℝ) (f : ℤ → ℝ) (n m : ℤ) : cesaroAvg (fun (k : ℤ) => c * f k) n m = c * cesaroAvg f n m

cesaroAvg commutes with scalar multiplication of the integrand.

theorem Algsuperdiff.Probability.cesaroAvg_const {n m : ℤ} (hnm : n ≤ m) (c : ℝ) : cesaroAvg (fun (x : ℤ) => c) n m = c

The average of a constant over a nonempty window is that constant.

theorem Algsuperdiff.Probability.cesaroAvg_mono {f g : ℤ → ℝ} {n m : ℤ} (hnm : n ≤ m) (h : ∀ k ∈ Finset.Icc n m, f k ≤ g k) : cesaroAvg f n m ≤ cesaroAvg g n m

cesaroAvg is monotone in the integrand on the window.

theorem Algsuperdiff.Probability.cesaroAvg_add4 {n m : ℤ} (hnm : n ≤ m) (f₁ f₂ f₃ : ℤ → ℝ) (c : ℝ) : cesaroAvg (fun (k : ℤ) => f₁ k + f₂ k + f₃ k + c) n m = cesaroAvg f₁ n m + cesaroAvg f₂ n m + cesaroAvg f₃ n m + c

Three summands plus an additive constant — the shape produced by the D₁ + D₂ + D₃ decomposition of l.minimal.scale.sep.