theorem SelbergExpansion.convOp_const {G : Type u_1} [Fintype G] [Group G] (μ : G → ℂ) (c : ℂ) (hμ_sum : ∑ g : G, μ g = 1) : (convOp μ fun (x : G) => c) = fun (x : G) => c

If μ is a probability distribution on G (i.e. ∑ g, μ g = 1), then the convolution operator convOp μ fixes constant functions: convOp μ (fun _ => c) = fun _ => c.

theorem SelbergExpansion.convOp_add {G : Type u_1} [Fintype G] [Group G] (μ f₁ f₂ : G → ℂ) : convOp μ (f₁ + f₂) = convOp μ f₁ + convOp μ f₂

The convolution operator convOp μ is additive in its second argument: convOp μ (f₁ + f₂) = convOp μ f₁ + convOp μ f₂.

theorem SelbergExpansion.convOp_meanZero {G : Type u_1} [Fintype G] [Group G] (μ f : G → ℂ) (hf : IsMeanZero f) : IsMeanZero (convOp μ f)

If f : G → ℂ has mean zero (i.e. ∑ g, f g = 0), then so does convOp μ f.

theorem SelbergExpansion.iterate_convOp_meanZero {G : Type u_1} [Fintype G] [Group G] (μ f : G → ℂ) (hf : IsMeanZero f) (n : ℕ) : IsMeanZero ((convOp μ)^[n] f)

Iterating the convolution operator convOp μ preserves the mean-zero property of f.

theorem SelbergExpansion.convPow_sub_const {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (μ : G → ℂ) (c : ℂ) (hμ_sum : ∑ g : G, μ g = 1) (K : ℕ) : (fun (g : G) => convPow μ K g - c) = (convOp μ)^[K] fun (g : G) => (if g = 1 then 1 else 0) - c

For a probability measure μ, the $K$-fold convolution convPow μ K minus the constant c equals the $K$-fold iterate of convOp μ applied to δ_{1_G} - c.

theorem SelbergExpansion.sigma1_bddAbove_general {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (μ : G → ℂ) : BddAbove {r : ℝ | ∃ (f : G → ℂ), IsMeanZero f ∧ l2NormSq f ≠ 0 ∧ r = √(l2NormSq (convOp μ f)) / √(l2NormSq f)}

The set of operator-norm ratios ‖convOp μ f‖₂ / ‖f‖₂ over nonzero mean-zero functions f : G → ℂ is bounded above (so the supremum σ₁(T_μ) is well-defined).

theorem SelbergExpansion.l2NormSq_convOp_le_sigma1_sq {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (μ f : G → ℂ) (hf_mz : IsMeanZero f) (hf_ne : l2NormSq f ≠ 0) : l2NormSq (convOp μ f) ≤ sigma1 μ ^ 2 * l2NormSq f

Operator-norm bound: for any mean-zero f : G → ℂ with nonzero $L^2$ norm, ‖convOp μ f‖₂² ≤ σ₁(T_μ)² · ‖f‖₂².

theorem SelbergExpansion.l2NormSq_iterate_convOp_le {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (μ f : G → ℂ) (hf_mz : IsMeanZero f) (K : ℕ) : l2NormSq ((convOp μ)^[K] f) ≤ sigma1 μ ^ (2 * K) * l2NormSq f

Iterated operator-norm bound: for any mean-zero f, the $K$-fold convolution satisfies ‖(T_μ)^K f‖₂² ≤ σ₁(T_μ)^{2K} · ‖f‖₂².

theorem SelbergExpansion.delta_sub_uniform_meanZero {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] : IsMeanZero fun (g : G) => (if g = 1 then 1 else 0) - 1 / ↑(Fintype.card G)

The function δ_{1_G} - 1/|G| (point mass at the identity minus the uniform distribution) has total sum zero.

theorem SelbergExpansion.l2NormSq_delta_sub_uniform_le_one {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] : (l2NormSq fun (g : G) => (if g = 1 then 1 else 0) - 1 / ↑(Fintype.card G)) ≤ 1

The squared $L^2$ norm of δ_{1_G} - 1/|G| is at most $1$ (in fact equals $1 - 1/|G|$).

theorem SelbergExpansion.l2_mixing_sigma1 {G : Type u_2} [Fintype G] [DecidableEq G] [Group G] (μ : G → ℂ) (K : ℕ) (hμ_prob : ∑ g : G, μ g = 1) : (l2NormSq fun (g : G) => convPow μ K g - 1 / ↑(Fintype.card G)) ≤ sigma1 μ ^ (2 * K)

$L^2$ mixing for random walks on finite groups: if μ is a probability measure on a finite group G with second-largest singular value σ₁(T_μ), then after K steps the distribution convPow μ K is close to uniform in $L^2$: $$\|T_\mu^K \delta_{g_0} - 1/|G|\|_{L^2}^2 \le \sigma_1(T_\mu)^{2K}.$$