Modular Forms

Results named in Tau Ceti's TauCeti.NumberTheory.ModularForms modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe Choie–Zagier criterion on k[ℳₙ] (Popa–Zagier, §3, Lemma 1)#

for n ≠ 0 and 2, 3 invertible in k, an element x ∈ k[ℳₙ] lies in (1 + S) k[ℳₙ] + (1 + U + U²) k[ℳₙ], with U = T * S, if and only if (1 - S) x ∈ (1 - T) k[ℳₙ], all products being left multiplications.

TauCeti.TraceFormulaMatrixModule.one_sub_S_apply_mem_range_one_sub_T_iff.{u_1} {n : ℤ}
  {k : Type u_1} [Ring k] [Invertible 2] [Invertible 3] (hn : n ≠ 0)
  {x : MonoidAlgebra k (TauCeti.TraceFormulaMatrixModule n)} :
  (1 -
          (Representation.ofMulAction k (Matrix.SpecialLinearGroup (Fin 2) ℤ)
              (TauCeti.TraceFormulaMatrixModule n))
            ModularGroup.S)
        x ∈
      (1 -
          (Representation.ofMulAction k (Matrix.SpecialLinearGroup (Fin 2) ℤ)
              (TauCeti.TraceFormulaMatrixModule n))
            ModularGroup.T).range ↔
    x ∈
      (1 +
            (Representation.ofMulAction k (Matrix.SpecialLinearGroup (Fin 2) ℤ)
                (TauCeti.TraceFormulaMatrixModule n))
              ModularGroup.S).range ⊔
        (1 +
              (Representation.ofMulAction k (Matrix.SpecialLinearGroup (Fin 2) ℤ)
                  (TauCeti.TraceFormulaMatrixModule n))
                (ModularGroup.T * ModularGroup.S) +
            (Representation.ofMulAction k (Matrix.SpecialLinearGroup (Fin 2) ℤ)
                  (TauCeti.TraceFormulaMatrixModule n))
                (ModularGroup.T * ModularGroup.S) ^
              2).range
Lean

Formalized in Tau Ceti as TauCeti.TraceFormulaMatrixModule.one_sub_S_apply_mem_range_one_sub_T_iff.

Sources
LeanTauCeti.TraceFormulaMatrixModule.one_sub_S_apply_mem_range_one_sub_T_iff
Uses 1
Proof usesThe Choie–Zagier criterion (Popa–Zagier, Lemma 1)

TheoremClassical Sturm bound for finite-index subgroups of SL(2, ℤ)# 

ModularForm.sturm_bound_finiteIndex_SL2Z {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
  [Γ.FiniteIndex] {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)
  (h :
    ↑((k * ↑Γ.index).toNat / 12) <
      (UpperHalfPlane.qExpansion
          (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ).strictWidthInfty ⇑f).order) :
  f = 0
Lean

Formalized in Tau Ceti as ModularForm.sturm_bound_finiteIndex_SL2Z.

Sources
LeanModularForm.sturm_bound_finiteIndex_SL2Z
Uses 1 · Used by 3
Proof usesSturm bound for subgroups of GL(2, ℝ) of finite relative index in SL(2, ℤ) with discrete strict periods
Used byA newform is an eigenvector of U_p at every prime p dividing the level, with eigenvalue a_p(f) · Popa–Zagier's ambient trace identity (Popa–Zagier, §2, Propositions 2 and 3) · Strong multiplicity one (Miyake, Theorem 4.6.12, fixed level)

TheoremDedekind's formula for the index of Γ₀(N)#

[SL₂(ℤ) : Γ₀(N)] = N ∏_{p ∣ N} (1 + 1/p), with the denominators cleared.

At level zero both sides vanish, since Γ₀(0) has infinite index. The proof is adapted from Mathlib's Nat.totient_mul_prod_primeFactors.

CongruenceSubgroup.Gamma0_index_mul_prod_primeFactors {N : ℕ} :
  (CongruenceSubgroup.Gamma0 N).index * ∏ p ∈ N.primeFactors, p = N * ∏ p ∈ N.primeFactors, (p + 1)
Lean

Formalized in Tau Ceti as CongruenceSubgroup.Gamma0_index_mul_prod_primeFactors.

Sources
LeanCongruenceSubgroup.Gamma0_index_mul_prod_primeFactors

TheoremThe Eichler–Selberg trace formula at level one#

For even k = w + 2 ≥ 4 and n ≥ 1, the trace of Tₙ on the cusp forms of weight k on SL(2, ℤ) is

tr(Tₙ | S_k) = -½ ∑_{t² ≤ 4n} H(4n - t²) P_k(t, n) - ½ ∑_{dd' = n} min(d, d')^(k-1),

with Hurwitz class numbers normalized by H(0) = -1/12 and P_k(t, n) = (dickson 2 n w).eval t. The sum over t runs over the integers with t² ≤ 4n, written as a filter of [-4n, 4n].

TauCeti.trace_heckeTCuspLevelOne_eq_neg_hurwitzClassNumber_sub_min {k : ℤ} {w : ℕ} (hk : k = ↑w + 2)
  (hw : Even w) (hw₀ : w ≠ 0) (n : ℕ) [NeZero n] :
  (LinearMap.trace ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k))
      (TauCeti.heckeTCuspLevelOne k n) =
    (-∑ t ∈ Finset.Icc (-4 * ↑n) (4 * ↑n) with t ^ 2 ≤ 4 * ↑n,
            ↑(TauCeti.hurwitzClassNumber (4 * ↑n - t ^ 2).toNat) *
              Polynomial.eval (↑t) (Polynomial.dickson 2 (↑n) w)) /
        2 -
      (∑ p ∈ n.divisorsAntidiagonal, ↑(min p.1 p.2) ^ (w + 1)) / 2
Lean

Formalized in Tau Ceti as TauCeti.trace_heckeTCuspLevelOne_eq_neg_hurwitzClassNumber_sub_min.

Sources
LeanTauCeti.trace_heckeTCuspLevelOne_eq_neg_hurwitzClassNumber_sub_min
Uses 2
Proof usesCayley–Hamilton in size two · Popa–Zagier's ambient trace identity (Popa–Zagier, §2, Propositions 2 and 3)

TheoremHecke's abscissa bound for modular forms#

for weight k ≥ 0, the Dirichlet series of the q-expansion coefficients converges absolutely for Re s > k + 1 (from aₙ = O(nᵏ)).

ModularForm.abscissaOfAbsConv_qExpansion_coeff_le.{u_1} {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)}
  [Γ.IsArithmetic] {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (hk : 0 ≤ k) [ModularFormClass F Γ k]
  (f : F) :
  (LSeries.abscissaOfAbsConv fun n =>
      (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f)) ≤
    ↑↑k + 1
Lean

Formalized in Tau Ceti as ModularForm.abscissaOfAbsConv_qExpansion_coeff_le.

Sources
LeanModularForm.abscissaOfAbsConv_qExpansion_coeff_le

TheoremThe Lipschitz formula along residue classes#

For a function f of residues modulo v, a weight k ≥ 2 and z in the upper half-plane, ∑_{n ∈ ℤ} f(n) (z + n)^(-k) = (-2πi)^k / ((k-1)! v^k) ∑_{m ≥ 1} 𝓕f(-m) m^(k-1) e^(2πi m z / v), where 𝓕f(-m) = ∑_{r mod v} f(r) e^(2πi r m / v) is the discrete Fourier transform of f. For v = 1 this is f 0 times Mathlib's EisensteinSeries.qExpansion_identity_pnat.

TauCeti.EisensteinSeries.qExpansion_identity_zmod {v : ℕ} [NeZero v] (f : ZMod v → ℂ) {k : ℕ}
  (hk : 2 ≤ k) (z : UpperHalfPlane) :
  ∑' (n : ℤ), f ↑n * (↑z + ↑n) ^ (-↑k) =
    (-2 * ↑Real.pi * Complex.I) ^ k / (↑(k - 1).factorial * ↑v ^ k) *
      ∑' (m : ℕ+),
        ZMod.dft f (-↑↑m) * ↑↑m ^ (k - 1) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z / ↑v) ^ ↑m
Lean

Formalized in Tau Ceti as TauCeti.EisensteinSeries.qExpansion_identity_zmod.

Sources
LeanTauCeti.EisensteinSeries.qExpansion_identity_zmod
Used by 1
Used byThe cusp–Eisenstein decomposition of M_k(N, χ)

TheoremThe Petersson adjoint formula in the second argument#

For n coprime to N,

⟪f, Tₙ g⟫ = ⟪⟨n⟩⁻¹ Tₙ f, g⟫.

This is the Hermitian transpose of peterssonInnerCosets_heckeTCuspNat_left.

HeckeRing.GL2.peterssonInnerCosets_heckeTCuspNat_right {N n : ℕ} [NeZero N] [NeZero n] (k : ℤ)
  (hn : n.Coprime N)
  (f g :
    CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) :
  f.peterssonInnerCosets ((HeckeRing.GL2.heckeTCuspNat k n) g) =
    ((TauCeti.diamondOpCusp k (ZMod.unitOfCoprime n hn)⁻¹)
          ((HeckeRing.GL2.heckeTCuspNat k n) f)).peterssonInnerCosets
      g
Lean

Formalized in Tau Ceti as HeckeRing.GL2.peterssonInnerCosets_heckeTCuspNat_right.

Sources
LeanHeckeRing.GL2.peterssonInnerCosets_heckeTCuspNat_right
Uses 2 · Used by 2
Proof usesShimura's decomposition of a double coset into right cosets · The third isomorphism theorem for coset spaces
Used byA newform is an eigenvector of U_p at every prime p dividing the level, with eigenvalue a_p(f) · Popa–Zagier's ambient trace identity (Popa–Zagier, §2, Propositions 2 and 3)

TheoremPopa–Zagier's ambient trace identity (Popa–Zagier, §2, Propositions 2 and 3)#

for positive even w, k = w + 2, n ≥ 1, and any ξ ∈ ℂ[ℳₙ] satisfying both the period relation (A) and the exchange relations (B), the trace of ξ on the ambient space V_w of degree-w binary forms is 2 Tr(Tₙ | S_k(SL(2, ℤ))) + σ_{w+1}(n).

TauCeti.TraceFormulaMatrixModule.PeriodRelation.trace_periodAction_eq {k : ℤ} {w : ℕ}
  (hk : k = ↑w + 2) (hw : Even w) (hw₀ : w ≠ 0) (n : ℕ) [NeZero n]
  {ξ : MonoidAlgebra ℂ (TauCeti.TraceFormulaMatrixModule ↑n)}
  (hP : TauCeti.TraceFormulaMatrixModule.PeriodRelation ℂ (↑n) ξ)
  (hX : TauCeti.TraceFormulaMatrixModule.ExchangeRelations ℂ (↑n) ξ) :
  (LinearMap.trace ℂ ↥(MvPolynomial.homogeneousSubmodule (Fin 2) ℂ w))
      ((TauCeti.TraceFormulaMatrixModule.periodAction hw) ξ) =
    2 *
        (LinearMap.trace ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k))
          (TauCeti.heckeTCuspLevelOne k n) +
      ↑((ArithmeticFunction.sigma (w + 1)) n)
Lean

Formalized in Tau Ceti as TauCeti.TraceFormulaMatrixModule.PeriodRelation.trace_periodAction_eq.

Sources
LeanTauCeti.TraceFormulaMatrixModule.PeriodRelation.trace_periodAction_eq
Uses 13 · Used by 1
Proof usesA newform is an eigenvector of U_p at every prime p dividing the level, with eigenvalue a_p(f) · Cayley–Hamilton in size two · Classical Sturm bound for finite-index subgroups of SL(2, ℤ) · The Main Lemma, per character (Miyake, Lemma 4.6.8; Diamond–Shurman, Theorem 5.7.1) · Manin's lemma · The Petersson adjoint formula in the second argument · Popa–Zagier's criterion for (1 - T)·ℛₙ · Shimura's commutativity criterion (Proposition 3.8 of [Shimura][shimura1971]) · Shimura's decomposition of a double coset into right cosets · Sturm bound for subgroups of GL(2, ℝ) of finite relative index in SL(2, ℤ) with discrete strict periods · TauCeti.ModularSymbols · TauCeti.ModularSymbols.periodMap · The third isomorphism theorem for coset spaces
Used byThe Eichler–Selberg trace formula at level one

TheoremPopa–Zagier's criterion for (1 - T)·ℛₙ#

An element of k[ℳₙ] lies in the range of left multiplication by 1 - T if and only if its coefficients sum to zero along every orbit of Γ_∞ = ⟨T⟩.

TauCeti.TraceFormulaMatrixModule.mem_range_one_sub_T_iff.{u_1} {k : Type u_1} [CommRing k] {n : ℤ}
  {ζ : MonoidAlgebra k (TauCeti.TraceFormulaMatrixModule n)} :
  ζ ∈
      (1 -
          (Representation.ofMulAction k (Matrix.SpecialLinearGroup (Fin 2) ℤ)
              (TauCeti.TraceFormulaMatrixModule n))
            ModularGroup.T).range ↔
    (MonoidAlgebra.mapDomainLinearMap k k
          (Quotient.mk
            (MulAction.orbitRel (↥(Subgroup.zpowers ModularGroup.T))
              (TauCeti.TraceFormulaMatrixModule n))))
        ζ =
      0
Lean

Formalized in Tau Ceti as TauCeti.TraceFormulaMatrixModule.mem_range_one_sub_T_iff.

Sources
LeanTauCeti.TraceFormulaMatrixModule.mem_range_one_sub_T_iff
Used by 1
Used byPopa–Zagier's ambient trace identity (Popa–Zagier, §2, Propositions 2 and 3)

TheoremStrong multiplicity one (Miyake, Theorem 4.6.12, fixed level)#

two newforms of level N and weight k whose eigenvalues agree at every index coprime to N outside a finite set are equal. No assumption is made on the nebentypus.

HeckeRing.GL2.Newform.eq_of_forall_notMem_eigenvalue_eq {N : ℕ} [NeZero N] {k : ℤ}
  {f g : HeckeRing.GL2.Newform N k} {S : Finset ℕ}
  (h : ∀ (n : ℕ+) (hn : (↑n).Coprime N), ↑n ∉ S → f.eigenvalue n hn = g.eigenvalue n hn) : f = g
Lean

Formalized in Tau Ceti as HeckeRing.GL2.Newform.eq_of_forall_notMem_eigenvalue_eq.

Sources
LeanHeckeRing.GL2.Newform.eq_of_forall_notMem_eigenvalue_eq
Uses 4
Proof usesClassical Sturm bound for finite-index subgroups of SL(2, ℤ) · The Main Lemma, per character (Miyake, Lemma 4.6.8; Diamond–Shurman, Theorem 5.7.1) · Shimura's commutativity criterion (Proposition 3.8 of [Shimura][shimura1971]) · Shimura's decomposition of a double coset into right cosets

TheoremSturm bound for subgroups of GL(2, ℝ) of finite relative index in SL(2, ℤ) with discrete strict periods#

A modular form of weight k whose q-expansion at the cusp ∞ has order strictly greater than k · [𝒮ℒ : 𝒢 ⊓ 𝒮ℒ] / 12 is identically zero.

ModularForm.sturm_bound_finiteIndex {𝒢 : Subgroup (GL (Fin 2) ℝ)}
  [𝒢.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL ℝ).range] {k : ℤ} (f : ModularForm 𝒢 k)
  [DiscreteTopology ↥𝒢.strictPeriods]
  (h :
    ↑((k *
              ↑(Nat.card
                  (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸
                    𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range))).toNat /
          12) <
      (UpperHalfPlane.qExpansion 𝒢.strictWidthInfty ⇑f).order) :
  f = 0
Lean

Formalized in Tau Ceti as ModularForm.sturm_bound_finiteIndex.

Sources
LeanModularForm.sturm_bound_finiteIndex
Used by 4
Used byA newform is an eigenvector of U_p at every prime p dividing the level, with eigenvalue a_p(f) · The cusp–Eisenstein decomposition of M_k(N, χ) · Classical Sturm bound for finite-index subgroups of SL(2, ℤ) · Popa–Zagier's ambient trace identity (Popa–Zagier, §2, Propositions 2 and 3)

TheoremWeber's identity#

Weber's identity g₀⁴ + g₁⁴ + g₂⁴ = 0 for the level-two Siegel functions g₀ = g_{(0, 1/2)}, g₁ = g_{(1/2, 0)} and g₂ = g_{(1/2, 1/2)}. In Weber's notation it reads 𝔣₁⁸ + 𝔣₂⁸ = 𝔣⁸.

TauCeti.ModularForm.siegelFunction_pow_four_add_add (τ : UpperHalfPlane) :
  TauCeti.ModularForm.siegelFunction ![0, 1 / 2] ↑τ ^ 4 +
        TauCeti.ModularForm.siegelFunction ![1 / 2, 0] ↑τ ^ 4 +
      TauCeti.ModularForm.siegelFunction ![1 / 2, 1 / 2] ↑τ ^ 4 =
    0
Lean

Formalized in Tau Ceti as TauCeti.ModularForm.siegelFunction_pow_four_add_add.

Sources
LeanTauCeti.ModularForm.siegelFunction_pow_four_add_add
Uses 3
Statement usesThe Siegel function g_r(τ) attached to r = (r₁, r₂) ∈ ℝ²
Proof usesEuler's identity (TauCeti.tprod_one_add_pow_mul_tprod_one_sub_pow_odd) · TauCeti.qTheta

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.