3. The coefficient–eigenvalue relation🔗

Theorem3.1

Statement uses 2

Statement dependency previews

Preview

Definition 1.2

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Theorem 2.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The n-th Hecke operator acts on q-expansions by the divisor-sum formula a_m(T_n f) = \sum_{d \mid (m,n)} d^{k-1}\,\chi(d)\, a_{mn/d^2}(f) \qquad (\gcd(n,N)=1), for f \in M_k(N, \chi) (Definition 1.4, Definition 1.2). Following Miyake Theorem 4.5.3.

Lean code for Theorem3.1●1 theorem

theoremdefined in LeanModularForms/HeckeRIngs/GL2/FourierHecke.lean

complete

theorem HeckeRing.GL2.fourierCoeff_heckeT_n_period_one {N : ℕ} [NeZero N]
  (k : ℤ) (n : ℕ) [NeZero n] (hn : n.Coprime N) (χ : (ZMod N)ˣ →* ℂˣ)
  {f :
    ModularForm
      (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k}
  (hf : f ∈ HeckeRing.GL2.modFormCharSpace k χ) (m : ℕ) :
  (PowerSeries.coeff m)
      (UpperHalfPlane.qExpansion 1 ⇑((HeckeRing.GL2.heckeT_n k n) f)) =
    ∑ d ∈ (m.gcd n).divisors,
      if h : d.Coprime N then
        ↑d ^ (k - 1) * ↑(χ (ZMod.unitOfCoprime d h)) *
          (PowerSeries.coeff (m * n / (d * d)))
            (UpperHalfPlane.qExpansion 1 ⇑f)
      else 0

theorem HeckeRing.GL2.fourierCoeff_heckeT_n_period_one
  {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ)
  [NeZero n] (hn : n.Coprime N)
  (χ : (ZMod N)ˣ →* ℂˣ)
  {f :
    ModularForm
      (Subgroup.map
        (Matrix.SpecialLinearGroup.mapGL
          ℝ)
        (CongruenceSubgroup.Gamma1 N))
      k}
  (hf :
    f ∈
      HeckeRing.GL2.modFormCharSpace k χ)
  (m : ℕ) :
  (PowerSeries.coeff m)
      (UpperHalfPlane.qExpansion 1
        ⇑((HeckeRing.GL2.heckeT_n k n)
            f)) =
    ∑ d ∈ (m.gcd n).divisors,
      if h : d.Coprime N then
        ↑d ^ (k - 1) *
            ↑(χ
                (ZMod.unitOfCoprime d
                  h)) *
          (PowerSeries.coeff
              (m * n / (d * d)))
            (UpperHalfPlane.qExpansion 1
              ⇑f)
      else 0

**Period-1 general Fourier coefficient formula for `T_n`.** The same divisor-sum formula as
`fourierCoeff_heckeT_n`, `a_m(T_n f) = Σ_{d | gcd(m, n)} d^{k-1} · χ(d) · a_{mn/d²}(f)`, with
every `coeff` taken at the canonical Fourier period `h = 1`.

Proof for Theorem 3.1

uses 0

The formula is proved one prime power at a time: for T_p it reads a_m(T_p f) = a_{pm}(f) + \chi(p)\,p^{k-1} a_{m/p}(f), and the prime-power and coprime cases are assembled by the multiplicativity of T_n and a divisor-sum convolution identity.

Theorem3.2

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 3.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

The Fourier coefficients of an eigenform are recovered from its eigenvalues and its first coefficient (Definition 2.1): a_n(f) = a_1(f)\, \lambda_n \qquad (\gcd(n, N) = 1). For a normalised newform (a_1 = 1) this is simply \lambda_n = a_n(f). (Miyake Lemma 4.5.15(1).)

Lean code for Theorem3.2●2 theorems

theoremdefined in LeanModularForms/SMOObligations/StrongMultiplicityOneFull.lean

complete

theorem HeckeRing.GL2.Eigenform.coeff_eq_coeff_one_mul_eigenvalue {N : ℕ}
  [NeZero N] {k : ℤ} (g : HeckeRing.GL2.Eigenform N k)
  (χ : (ZMod N)ˣ →* ℂˣ)
  (hgχ : g.toModularForm' ∈ HeckeRing.GL2.modFormCharSpace k χ) (n : ℕ+)
  (hn : (↑n).Coprime N) :
  (PowerSeries.coeff ↑n) (UpperHalfPlane.qExpansion 1 ⇑g.toCuspForm) =
    (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑g.toCuspForm) *
      g.eigenvalue n

theorem HeckeRing.GL2.Eigenform.coeff_eq_coeff_one_mul_eigenvalue
  {N : ℕ} [NeZero N] {k : ℤ}
  (g : HeckeRing.GL2.Eigenform N k)
  (χ : (ZMod N)ˣ →* ℂˣ)
  (hgχ :
    g.toModularForm' ∈
      HeckeRing.GL2.modFormCharSpace k χ)
  (n : ℕ+) (hn : (↑n).Coprime N) :
  (PowerSeries.coeff ↑n)
      (UpperHalfPlane.qExpansion 1
        ⇑g.toCuspForm) =
    (PowerSeries.coeff 1)
        (UpperHalfPlane.qExpansion 1
          ⇑g.toCuspForm) *
      g.eigenvalue n

**Miyake Lemma 4.5.15(1)** (un-normalised form, period 1).  For an `Eigenform g`
lying in the Nebentypus space `χ` and `n` coprime to the level, the `n`-th Fourier
coefficient equals the leading coefficient times the classical Hecke eigenvalue:
`aₙ(g) = a₁(g) · λₙ(g)`.

theoremdefined in LeanModularForms/HeckeRIngs/GL2/Newforms/MainLemma.lean

complete

theorem HeckeRing.GL2.Newform.eigenvalue_eq_coeff {N : ℕ} [NeZero N] {k : ℤ}
  (f : HeckeRing.GL2.Newform N k) (n : ℕ+) (hn : (↑n).Coprime N)
  (χ : (ZMod N)ˣ →* ℂˣ)
  (hf_char : f.toModularForm' ∈ HeckeRing.GL2.modFormCharSpace k χ) :
  f.eigenvalue n =
    (PowerSeries.coeff ↑n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)

theorem HeckeRing.GL2.Newform.eigenvalue_eq_coeff
  {N : ℕ} [NeZero N] {k : ℤ}
  (f : HeckeRing.GL2.Newform N k) (n : ℕ+)
  (hn : (↑n).Coprime N)
  (χ : (ZMod N)ˣ →* ℂˣ)
  (hf_char :
    f.toModularForm' ∈
      HeckeRing.GL2.modFormCharSpace k
        χ) :
  f.eigenvalue n =
    (PowerSeries.coeff ↑n)
      (UpperHalfPlane.qExpansion 1
        ⇑f.toCuspForm)

For a `Newform` f lying in a character eigenspace `modFormCharSpace k χ`,
the eigenvalue at `n` (coprime to `N`) equals the `n`-th **canonical
Fourier coefficient** of `f` (period `h = 1`).  The character hypothesis
`hf_char` is required because `fourierCoeff_heckeT_n_period_one` is stated for
forms living in a single Nebentypus eigenspace.

Proof for Theorem 3.2

uses 1

Read off the first coefficient (m = 1) of T_n f = \lambda_n f using the divisor-sum formula (Theorem 3.1): the only surviving divisor term at m = 1 is d = 1, giving a_n(f) = \lambda_n\, a_1(f).

Theorem3.3

Statement uses 2

Statement dependency previews

Preview

Definition 2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Theorem 6.1

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

A nonzero common eigenfunction in the new subspace has nonvanishing leading coefficient, a_1 \ne 0 (Definition 2.1, Definition 4.3). (Miyake Lemma 4.6.11.)

Lean code for Theorem3.3●1 theorem

theoremdefined in LeanModularForms/SMOObligations/StrongMultiplicityOneFull.lean

complete

theorem HeckeRing.GL2.coeff_one_ne_zero_of_mem_cuspFormsNew_of_eigen {N : ℕ}
  [NeZero N] {k : ℤ} (g : HeckeRing.GL2.Eigenform N k)
  (χ : (ZMod N)ˣ →* ℂˣ)
  (hgχ : g.toModularForm' ∈ HeckeRing.GL2.modFormCharSpace k χ)
  (hg_new : g.toCuspForm ∈ HeckeRing.GL2.cuspFormsNew N k)
  (hg_ne : g.toCuspForm ≠ 0) :
  (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑g.toCuspForm) ≠ 0

theorem HeckeRing.GL2.coeff_one_ne_zero_of_mem_cuspFormsNew_of_eigen
  {N : ℕ} [NeZero N] {k : ℤ}
  (g : HeckeRing.GL2.Eigenform N k)
  (χ : (ZMod N)ˣ →* ℂˣ)
  (hgχ :
    g.toModularForm' ∈
      HeckeRing.GL2.modFormCharSpace k χ)
  (hg_new :
    g.toCuspForm ∈
      HeckeRing.GL2.cuspFormsNew N k)
  (hg_ne : g.toCuspForm ≠ 0) :
  (PowerSeries.coeff 1)
      (UpperHalfPlane.qExpansion 1
        ⇑g.toCuspForm) ≠
    0

**Miyake Lemma 4.6.11** (`Eigenform`/`cuspFormsNew` form).  A nonzero common
eigenfunction in the new subspace has nonvanishing leading Fourier coefficient.

Proof: if `a₁(g) = 0` then `aₙ(g) = 0` for all `(n,N)=1` (Lemma 4.5.15(1)),
so `g ∈ cuspFormsOld N k`; being also new and nonzero, this contradicts
`cuspFormsOld_disjoint_cuspFormsNew`.

Proof for Theorem 3.3

Proof uses 3

Proof dependency previews

Preview

Theorem 3.2

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

By contraposition: if a_1(g) = 0 then by Theorem 3.2 every coprime coefficient vanishes, a_n(g) = a_1(g)\,\lambda_n = 0, as does a_0 by cuspidality. A form with all coefficients away from N vanishing lies in the old subspace (Theorem 5.1); but g is also new, and the new and old subspaces meet only in 0 (Theorem 4.6), forcing g = 0.