@[reducible, inline]

abbrev SelbergExpansion.SL2 (p : ℕ) : Type

The group SL₂(𝔽_p) of 2 × 2 matrices of determinant 1 over ℤ/pℤ.

noncomputable def SelbergExpansion.groupConv {G : Type u_1} [Fintype G] [Group G] (f₁ f₂ : G → ℂ) (g : G) : ℂ

The group convolution (f₁ * f₂)(g) = ∑_{g₁} f₁(g₁) f₂(g₁⁻¹ g) on a finite group G.

noncomputable def SelbergExpansion.convOp {G : Type u_1} [Fintype G] [Group G] (μ f : G → ℂ) : G → ℂ

Right convolution operator T_μ : f ↦ f * μ on functions G → ℂ.

noncomputable def SelbergExpansion.l2NormSq {G : Type u_1} [Fintype G] (f : G → ℂ) : ℝ

Squared ℓ² norm of f : G → ℂ, i.e. ∑_{g ∈ G} ‖f(g)‖².

def SelbergExpansion.IsMeanZero {G : Type u_1} [Fintype G] (f : G → ℂ) : Prop

A function f : G → ℂ is mean zero if ∑_{g ∈ G} f(g) = 0.

noncomputable def SelbergExpansion.sigma1 {G : Type u_1} [Fintype G] [Group G] (μ : G → ℂ) : ℝ

The "second-largest" singular value σ₁(T_μ) of the convolution operator T_μ, defined as the supremum of ‖T_μ f‖_{ℓ²} / ‖f‖_{ℓ²} over nonzero mean-zero f. Smaller σ₁ means better spectral gap / expansion.

noncomputable def SelbergExpansion.uniformMeasure {G : Type u_1} [DecidableEq G] (A : Finset G) (g : G) : ℂ

The uniform probability measure on a finite set A ⊆ G: g ↦ 1/|A| if g ∈ A, else 0.

def SelbergExpansion.cayleyEdgeCount {G : Type u_1} [DecidableEq G] [Group G] (A S T : Finset G) : ℕ

Number of edges in the Cayley graph on G with generators A going from S to T: pairs (s, t) ∈ S × T with s⁻¹ t ∈ A.

def SelbergExpansion.IsSymmetricMeasure {G : Type u_1} [Group G] (μ : G → ℂ) : Prop

A measure μ : G → ℂ is symmetric if μ(g) = μ(g⁻¹) for every g.

def SelbergExpansion.convPow {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (μ : G → ℂ) : ℕ → G → ℂ

Convolution powers of μ: μ^{*0} is the delta at the identity, and μ^{*(n+1)} = μ^{*n} * μ.

theorem SelbergExpansion.groupConv_reflect {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (f₁ f₂ : G → ℂ) (x : G) : groupConv f₁ f₂ x⁻¹ = groupConv (fun (g : G) => f₂ g⁻¹) (fun (g : G) => f₁ g⁻¹) x

Reflection identity for group convolution: (f₁ * f₂)(x⁻¹) = (f₂(·⁻¹) * f₁(·⁻¹))(x).

theorem SelbergExpansion.groupConv_assoc {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (f₁ f₂ f₃ : G → ℂ) : groupConv (groupConv f₁ f₂) f₃ = groupConv f₁ (groupConv f₂ f₃)

Associativity of group convolution: (f₁ * f₂) * f₃ = f₁ * (f₂ * f₃).

theorem SelbergExpansion.groupConv_delta_right {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (f : G → ℂ) : (groupConv f fun (g : G) => if g = 1 then 1 else 0) = f

Right identity for group convolution: convolving with the delta at the identity recovers the function.

theorem SelbergExpansion.groupConv_delta_left {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (f : G → ℂ) : groupConv (fun (g : G) => if g = 1 then 1 else 0) f = f

Left identity for group convolution: the delta at the identity is a left unit.

theorem SelbergExpansion.groupConv_comm_convPow {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (μ : G → ℂ) (n : ℕ) : groupConv μ (convPow μ n) = groupConv (convPow μ n) μ

The convolution μ * μ^{*n} equals μ^{*n} * μ; in particular μ commutes with its own convolution powers.

theorem SelbergExpansion.convPow_symmetric {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (μ : G → ℂ) (hμ : IsSymmetricMeasure μ) (K : ℕ) (g : G) : convPow μ K g = convPow μ K g⁻¹

If μ is a symmetric measure, then so is each convolution power μ^{*K}.

theorem SelbergExpansion.convPow_conj {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (μ : G → ℂ) (hreal : ∀ (g : G), (starRingEnd ℂ) (μ g) = μ g) (K : ℕ) (g : G) : (starRingEnd ℂ) (convPow μ K g) = convPow μ K g

If μ takes only real values, then each convolution power μ^{*K} is also real-valued (closed under complex conjugation).

theorem SelbergExpansion.convPow_add {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (μ : G → ℂ) (m n : ℕ) : convPow μ (m + n) = groupConv (convPow μ m) (convPow μ n)

Additive law for convolution powers: μ^{*(m+n)} = μ^{*m} * μ^{*n}.

theorem SelbergExpansion.cayleyEdgeCount_eq_card_mul_sum {G : Type u_1} [DecidableEq G] [Group G] (A S T : Finset G) (hA : A.Nonempty) : ↑(cayleyEdgeCount A S T) = ↑A.card * ∑ s ∈ S, ∑ t ∈ T, (uniformMeasure A (s⁻¹ * t)).re

Re-expressing the Cayley edge count via the uniform measure on A: #E(S, T) = |A| · ∑_{s ∈ S} ∑_{t ∈ T} Re(u_A(s⁻¹ t)).

theorem SelbergExpansion.weighted_jensen_univ {G : Type u_1} [Fintype G] (w x : G → ℝ) (hw : ∀ (g : G), 0 ≤ w g) : (∑ g : G, w g * x g) ^ 2 ≤ (∑ g : G, w g) * ∑ g : G, w g * x g ^ 2

Weighted Jensen / Cauchy–Schwarz inequality on a finite set with nonnegative weights w: (∑ w_g x_g)² ≤ (∑ w_g)(∑ w_g x_g²).

theorem SelbergExpansion.l2NormSq_convOp_le {G : Type u_2} [Fintype G] [DecidableEq G] [Group G] (μ f : G → ℂ) (hμ_nonneg : ∀ (g : G), 0 ≤ (μ g).re) (hμ_im : ∀ (g : G), (μ g).im = 0) (hμ_sum : ∑ g : G, μ g = 1) : l2NormSq (convOp μ f) ≤ l2NormSq f

Contraction property: if μ is a real, nonnegative probability measure on G, then convolution by μ is an ℓ²-contraction: ‖T_μ f‖_{ℓ²} ≤ ‖f‖_{ℓ²}.

theorem SelbergExpansion.l2NormSq_nonneg {G : Type u_1} [Fintype G] (f : G → ℂ) : 0 ≤ l2NormSq f

The ℓ² squared norm is nonnegative.

theorem SelbergExpansion.expansion_mixing_sum_bound {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (A : Finset G) (hA : A.Nonempty) (S T : Finset G) : (1 - sigma1 (uniformMeasure A)) * (↑S.card * ↑T.card / ↑(Fintype.card G)) ≤ ∑ s ∈ S, ∑ t ∈ T, (uniformMeasure A (s⁻¹ * t)).re

Expander mixing (sum form). For any finite group G and nonempty A ⊆ G, the weighted sum ∑_{s ∈ S} ∑_{t ∈ T} u_A(s⁻¹ t) is at least (1 − σ₁(T_A)) · |S||T| / |G|.

theorem SelbergExpansion.expansion_lower_bound {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (A S : Finset G) : ↑(cayleyEdgeCount A S (Finset.univ \ S)) ≥ (1 - sigma1 (uniformMeasure A)) * (↑A.card * ↑S.card * ↑(Finset.univ \ S).card / ↑(Fintype.card G))

Expansion lower bound (cut form). For any S ⊆ G with complement Sᶜ, the number of Cayley edges between S and Sᶜ satisfies |E(S, Sᶜ)| ≥ (1 − σ₁(T_A)) · |A| · |S| · |Sᶜ| / |G|.

theorem SelbergExpansion.symmetric_l2_norm_eq_identity_eval {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (μ : G → ℂ) (hμ : IsSymmetricMeasure μ) (K : ℕ) (hreal : ∀ (g : G), (starRingEnd ℂ) (μ g) = μ g) : ↑(l2NormSq (convPow μ K)) = convPow μ (2 * K) 1

For a symmetric, real-valued measure μ, ‖μ^{*K}‖_{ℓ²}² = μ^{*2K}(I), the value of the 2K-fold convolution at the identity (lemma lem-B_T in the textbook).

@[implicit_reducible]

instance SelbergExpansion.instDecidableEqSL2 (p : ℕ) : DecidableEq (SL2 p)

Decidable equality on SL₂(𝔽_p) inherited from the underlying matrix subtype.

def SelbergExpansion.sl2ZBall (T : ℝ) : Set (Matrix.SpecialLinearGroup (Fin 2) ℤ)

The set of integer 2 × 2 unimodular matrices g ∈ SL₂(ℤ) of "size" at most T, i.e. with Frobenius squared norm g₀₀² + g₀₁² + g₁₀² + g₁₁² ≤ ⌊T²⌋.

def SelbergExpansion.congruenceSubgroup (p : ℕ) : Set (Matrix.SpecialLinearGroup (Fin 2) ℤ)

The principal congruence subgroup Γ(p) ⊆ SL₂(ℤ): matrices congruent to the identity modulo p.

theorem SelbergExpansion.sl2_rep_min_dimension (p : ℕ) [Fact (Nat.Prime p)] (V : Type u_1) [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ (SL2 p) V) (hρ : ¬∀ (g : SL2 p), ρ g = 1) : Module.finrank ℂ V ≥ (p - 1) / 2

Frobenius dimension bound (lem-rep). Any nontrivial finite-dimensional complex representation ρ : SL₂(𝔽_p) → U(V) has dimension ≥ (p − 1)/2.

theorem SelbergExpansion.l2NormSq_nonneg' {G : Type u_1} [Fintype G] (f : G → ℂ) : 0 ≤ l2NormSq f

The ℓ² squared norm is nonnegative (alternative form without group/decidable hypotheses).

theorem SelbergExpansion.l2NormSq_pos_of_ne {G : Type u_1} [Fintype G] {f : G → ℂ} (h : l2NormSq f ≠ 0) : 0 < l2NormSq f

If ‖f‖_{ℓ²}² ≠ 0, then it is strictly positive.

theorem SelbergExpansion.sqrt_div_le_sqrt {A B C : ℝ} (hB : 0 < B) (hC : 0 ≤ C) (h : A ≤ C * B) : √A / √B ≤ √C

Elementary inequality: if A ≤ C·B with B > 0 and C ≥ 0, then √A/√B ≤ √C.

theorem SelbergExpansion.sigma1_sq_le_of_bound {G : Type u_1} [Fintype G] [DecidableEq G] [Group G] (μ : G → ℂ) (B : ℝ) (hB : 0 ≤ B) (hbdd : ∀ (f : G → ℂ), IsMeanZero f → l2NormSq f ≠ 0 → l2NormSq (convOp μ f) ≤ B * l2NormSq f) : sigma1 μ ^ 2 ≤ B

If ‖T_μ f‖_{ℓ²}² ≤ B · ‖f‖_{ℓ²}² for all mean-zero nonzero f, then σ₁(T_μ)² ≤ B.

theorem SelbergExpansion.spectral_bound_sl2 (p : ℕ) [hp : Fact (Nat.Prime p)] (μ f : SL2 p → ℂ) (hf_mz : IsMeanZero f) (hf_ne : l2NormSq f ≠ 0) : l2NormSq (convOp μ f) ≤ 4 * ↑p ^ 2 * l2NormSq μ * l2NormSq f

Spectral bound on SL₂(𝔽_p). For any μ : SL₂(𝔽_p) → ℂ and any nonzero mean-zero f, ‖T_μ f‖_{ℓ²}² ≤ 4 p² · ‖μ‖_{ℓ²}² · ‖f‖_{ℓ²}².

theorem SelbergExpansion.l2_bound_sigma1 : ∃ C > 0, ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (μ : SL2 p → ℂ), sigma1 μ ^ 2 ≤ C * ↑p ^ 2 * l2NormSq μ

Theorem (thm-ell²). There is a universal constant C > 0 such that for every prime p and every μ : SL₂(𝔽_p) → ℂ, σ₁(T_μ)² ≤ C p² · ‖μ‖_{ℓ²(G)}².

theorem SelbergExpansion.sl2ZBall_finite (T : ℝ) : (sl2ZBall T).Finite

The integer ball sl2ZBall T ⊆ SL₂(ℤ) is finite, since its matrices have bounded entries.

theorem SelbergExpansion.sl2ZBall_card_growth : ∃ (c : ℝ) (C : ℝ), 0 < c ∧ 0 < C ∧ ∀ T ≥ 2, c * T ^ 2 ≤ ↑⋯.toFinset.card ∧ ↑⋯.toFinset.card ≤ C * T ^ 2

The cardinality of sl2ZBall T grows like T²: there exist c, C > 0 such that c·T² ≤ |sl2ZBall T| ≤ C·T² for all T ≥ 2.

theorem SelbergExpansion.congruence_coset_equidistribution : ∃ C > 0, ∀ (p : ℕ), Nat.Prime p → ∀ T > ↑p ^ 2, ↑⋯.toFinset.card ≤ C / ↑p ^ 3 * ↑⋯.toFinset.card

Cosets of Γ(p) equidistribute in sl2ZBall T for large T: the number of elements of sl2ZBall T lying in the congruence subgroup Γ(p) is at most C · |sl2ZBall T| / p³.

theorem SelbergExpansion.congruence_kernel_ball_count : ∃ C > 0, ∀ (p : ℕ) [Fact (Nat.Prime p)], ∀ T > ↑p ^ 2, ∃ (hfin : (congruenceSubgroup p ∩ sl2ZBall T).Finite), ↑hfin.toFinset.card ≤ C * ↑p ^ (-3) * T ^ 2

Counting elements of Γ(p) of bounded size: there is C > 0 such that for all primes p and T > p², |Γ(p) ∩ sl2ZBall T| ≤ C · p⁻³ · T².