Documentation

Atlas.EllipticCurves.code.ModularForms

structure WeakModularForm (Γ : Subgroup (GL (Fin 2) )) (k : ) extends SlashInvariantForm Γ k :

A weak modular form of weight k for a subgroup Γ ≤ GL(2, ℝ): a slash-invariant function on the upper half plane that is holomorphic (MDiff), but without any condition on growth at the cusps.

Instances For
    @[reducible, inline]

    Modular forms of weight k for the full modular group SL(2, ℤ) = Γ(1).

    Instances For

      Forgetful map: every modular form for SL(2, ℤ) is in particular a weak modular form (we drop the boundedness-at-cusps condition).

      Instances For
        @[reducible, inline]
        abbrev ModularFormGamma0 (N : ) (k : ) :

        Modular forms of weight k for the congruence subgroup Γ₀(N) ≤ SL(2, ℤ).

        Instances For
          @[reducible, inline]
          abbrev WeakModularFormGamma0 (N : ) (k : ) :

          Weak modular forms of weight k for Γ₀(N) (holomorphic and slash-invariant, without cuspidal growth condition).

          Instances For
            @[reducible, inline]
            abbrev CuspFormForSL2Z (k : ) :

            Cusp forms of weight k for the full modular group SL(2, ℤ) = Γ(1) (modular forms vanishing at every cusp).

            Instances For
              @[reducible, inline]
              abbrev CuspFormGamma0 (N : ) (k : ) :

              Cusp forms of weight k for the congruence subgroup Γ₀(N) ≤ SL(2, ℤ).

              Instances For

                A cusp form for SL(2, ℤ) is in particular a modular form (vanishing at cusps implies boundedness at cusps).

                Instances For

                  A cusp form for SL(2, ℤ) is in particular a weak modular form (drop both the boundedness and vanishing conditions at cusps).

                  Instances For

                    The Taylor–Wiles theorem: every semistable elliptic curve over is modular.

                    The Breuil–Conrad–Diamond–Taylor theorem extending Taylor–Wiles: every elliptic curve over is modular.

                    The Modularity Theorem for elliptic curves over : every elliptic curve over the rationals is modular.

                    Predicate stating that an integral Weierstrass model W is a model for the rational Weierstrass curve E, i.e. there is a -rational change of variables taking W (viewed over ) to E.

                    Instances For

                      Structure encoding that W is a minimal integral model for E: it is a model for E and its discriminant divides that of every other integral model of E.

                      Instances For

                        The minimal discriminant of a rational Weierstrass curve: the discriminant of its minimal integral model.

                        Instances For

                          The minimal discriminant of a rational Weierstrass curve is nonzero.

                          The minimal discriminant of E divides the discriminant of any integral Weierstrass model of E.

                          The (chosen) minimal integral Weierstrass model of a rational Weierstrass curve.

                          Instances For

                            The four possible reduction types of an elliptic curve at a prime: good reduction, split multiplicative reduction, nonsplit multiplicative reduction, or additive reduction.

                            Instances For

                              The reduction type of an elliptic curve E over at the prime p, computed from the reduction of its minimal model modulo p.

                              Instances For

                                The local conductor exponent of an elliptic curve at a prime, giving the power of that prime appearing in the global conductor.

                                Instances For

                                  At a prime of good reduction, the conductor exponent is 0.

                                  At a prime of split multiplicative reduction, the conductor exponent is 1.

                                  At a prime of nonsplit multiplicative reduction, the conductor exponent is 1.

                                  At a prime p > 3 of additive reduction, the conductor exponent is 2.

                                  The conductor of an elliptic curve over : the product over primes dividing the minimal discriminant of p raised to the local conductor exponent.

                                  Instances For

                                    The conductor of an elliptic curve over is positive.

                                    An elliptic curve over is semistable if it has good or multiplicative (but never additive) reduction at every prime.

                                    Instances For

                                      An elliptic curve with squarefree conductor is semistable.

                                      Characterisation: an elliptic curve over is semistable iff its conductor is squarefree.

                                      The trace of Frobenius of E at the prime p: at primes of good reduction it equals p + 1 − #E(𝔽_p), and at primes of bad reduction it takes the conventional values 0 (additive), 1 (split multiplicative), or −1 (nonsplit multiplicative).

                                      Instances For

                                        The local character χ(p): equals 1 at primes of good reduction and 0 at primes of bad reduction.

                                        Instances For

                                          The local L-polynomial at p: 1 − a_p X + p X² at primes of good reduction, and 1, 1 − X, or 1 + X at primes of additive, split multiplicative, or nonsplit multiplicative reduction respectively.

                                          Instances For

                                            The local Euler factor at p and complex variable s: the reciprocal of the local L-polynomial evaluated at p^{-s}.

                                            Instances For

                                              The (Hasse–Weil) L-function of an elliptic curve over , defined as the Euler product of local factors over all primes.

                                              Instances For

                                                The Euler product defining the L-function converges (as an unordered product) for Re(s) > 3/2.

                                                The local zeta function of E at p as a rational function in T: the local L-polynomial divided by (1 − T)(1 − pT).

                                                Instances For

                                                  The number of 𝔽_{p^n}-points on the reduction of E modulo p.

                                                  Instances For

                                                    At a prime of good reduction, the local zeta function admits an exponential expression in terms of the point counts over extensions of 𝔽_p.

                                                    Hasse bound: at a prime of good reduction, a_p² ≤ 4p, equivalently |a_p| ≤ 2√p.

                                                    An integral, normalized weight-2 newform: a level N together with integer Fourier coefficients a_n with a_0 = 0 and a_1 = 1.

                                                    Instances For

                                                      The integer Fourier coefficients of the (conjectural) weight-2 newform attached to the elliptic curve E.

                                                      Instances For

                                                        At every prime p, the p-th q-expansion coefficient of E agrees with the trace of Frobenius a_p(E).

                                                        Eichler–Shimura–Carayol: every integral normalized weight-2 newform f arises as the q-expansion of an elliptic curve E over of conductor f.level.

                                                        Variant of Eichler–Shimura–Carayol at primes: every integral normalized weight-2 newform comes from an elliptic curve whose traces of Frobenius match the newform's prime coefficients.

                                                        An elliptic curve E over is modular if there exists an integral weight-2 newform whose Fourier coefficients agree with the q-expansion coefficients of E.

                                                        Instances For

                                                          A modular elliptic curve E is associated with a newform whose level equals the conductor of E.

                                                          The L-function of a newform: the Dirichlet L-series with coefficients a_n ∈ ℂ.

                                                          Instances For

                                                            An elliptic curve E has a modular L-function if its L-function equals that of some newform whose level matches the conductor of E.

                                                            Instances For

                                                              The L-function of an elliptic curve agrees with the Dirichlet L-series formed from its q-expansion coefficients.

                                                              If the q-expansion coefficients of E agree with those of a newform f, then their L-functions agree.

                                                              Converse: if the L-functions of E and a newform f agree, then so do their coefficients.

                                                              The two notions of modularity (coefficient-level and L-function-level) coincide.

                                                              Modularity theorem (coefficient form): every elliptic curve over is modular at the level of Fourier coefficients.

                                                              Modularity theorem (L-function form): every elliptic curve over has a newform with matching L-function.

                                                              Global statement of the modularity theorem in the namespace's preferred form: every elliptic curve over is modular.

                                                              Predicate stating that p is a prime of good reduction for both E₁ and E₂.

                                                              Instances For

                                                                Faltings–Tate isogeny theorem: if E₁ and E₂ have matching traces of Frobenius at all but finitely many common good primes, then they are isogenous.

                                                                Isogenous elliptic curves have the same trace of Frobenius at every prime.

                                                                Isogenous elliptic curves have the same reduction type at every prime.

                                                                Isogenous elliptic curves have equal L-functions.

                                                                If two elliptic curves have the same L-function, then their traces of Frobenius agree at every prime.

                                                                Two elliptic curves over are isogenous iff they have the same L-function.

                                                                Two elliptic curves are isogenous iff there are only finitely many common good primes at which their traces of Frobenius differ.

                                                                Combined characterisation: isogeny is equivalent to equality of L-functions together with matching traces at almost all common good primes.

                                                                Global re-statement: two elliptic curves over are isogenous iff they have the same L-function.

                                                                A complex lattice Λ ⊂ ℂ: a pair of complex periods ω₁, ω₂ that are ℝ-linearly independent.

                                                                Instances For
                                                                  theorem HeckeOperatorProperties.ComplexLattice.ext {x y : ComplexLattice} (ω₁ : x.ω₁ = y.ω₁) (ω₂ : x.ω₂ = y.ω₂) :
                                                                  x = y
                                                                  @[reducible, inline]

                                                                  The free abelian group on the set of complex lattices, viewed as the divisor group of lattices.

                                                                  Instances For

                                                                    Coercion of a positive natural number n to a nonzero complex unit.

                                                                    Instances For

                                                                      The action of a nonzero complex scalar l on a complex lattice, scaling both periods.

                                                                      Instances For

                                                                        The Hecke operator T_n acting on the free abelian group of lattices: sends each lattice to the formal sum of its index-n sublattices.

                                                                        Instances For

                                                                          The Hecke operator at n = 1 is the identity.

                                                                          The homothety operator R_l: the ℤ-linear extension of the scaling action on lattices by the scalar l ∈ ℂˣ.

                                                                          Instances For

                                                                            Scalings compose by multiplication of scalars.

                                                                            The Hecke operator T_n commutes with every homothety R_l.

                                                                            Homotheties multiply: R_l ∘ R_μ = R_{lμ}.

                                                                            theorem HeckeOperatorProperties.hecke_multiplicative (m n : ℕ+) (h : (↑m).Coprime n) :
                                                                            heckeT (m * n) = heckeT m * heckeT n

                                                                            Multiplicativity of Hecke operators on coprime indices: T_{mn} = T_m ∘ T_n when gcd(m, n) = 1.

                                                                            The finite set of index-n sublattices of a given lattice L.

                                                                            Instances For

                                                                              Defining identity for the Hecke operator: T_n sends a basis lattice to the formal sum of its index-n sublattices.

                                                                              theorem HeckeOperatorProperties.heckeT_comp_counts_pairs (p : ) (hp : Nat.Prime p) (r : ) (L : ComplexLattice) :
                                                                              have pp := p, ; (heckeT (pp ^ (r + 1)) * heckeT pp) (FreeAbelianGroup.of L) = L'SubL pp L, L''SubL (pp ^ (r + 1)) L', FreeAbelianGroup.of L''

                                                                              The composition T_{p^{r+1}} ∘ T_p applied to a lattice unfolds to a double sum over sublattices counting pairs (L', L'').

                                                                              theorem HeckeOperatorProperties.pair_decomposition (p : ) (hp : Nat.Prime p) (r : ) (L : ComplexLattice) :
                                                                              have pp := p, ; L'SubL pp L, L''SubL (pp ^ (r + 1)) L', FreeAbelianGroup.of L'' = L''SubL (pp ^ (r + 2)) L, FreeAbelianGroup.of L'' + p L'''SubL (pp ^ r) L, FreeAbelianGroup.of (scaleLattice (pnatToComplexUnits pp) L''')

                                                                              The double sum decomposition: pairs (L', L'') of nested sublattices split into index-p^{r+2} sublattices of L plus a p-multiplied correction term from scaled index-p^r sublattices.

                                                                              theorem HeckeOperatorProperties.hecke_prime_power_recurrence (p : ) (hp : Nat.Prime p) (r : ) :
                                                                              have pp := p, ; heckeT (pp ^ (r + 2)) = heckeT (pp ^ (r + 1)) * heckeT pp - p (heckeT (pp ^ r) * homothetyR (pnatToComplexUnits pp))

                                                                              Recurrence for Hecke operators at prime powers: T_{p^{r+2}} = T_{p^{r+1}} T_p − p · T_{p^r} R_p.

                                                                              The generating set for the Hecke algebra (on divisors of lattices): all prime Hecke operators T_p and all prime homotheties R_p.

                                                                              Instances For

                                                                                Hecke operators at distinct primes commute, deduced from multiplicativity on coprime indices.

                                                                                Pairwise commutativity of the generating Hecke operators: any two generators in heckeGenerators commute.

                                                                                @[reducible]

                                                                                The subring of End ℤ DivL generated by the Hecke operators and homotheties is commutative.

                                                                                Instances For

                                                                                  Every prime-power Hecke operator T_{p^r} lies in the subring generated by prime Hecke operators and homotheties.

                                                                                  For every positive n, the Hecke operator T_n lies in the subring generated by heckeGenerators, by reduction to prime powers and multiplicativity.

                                                                                  The Hecke operator T_n acting on modular forms of weight k for SL(2, ℤ).

                                                                                  Instances For

                                                                                    The homothety operator R_l acting on modular forms of weight k for SL(2, ℤ).

                                                                                    Instances For
                                                                                      theorem HeckeMultiplicativity.homothetyR_MF_scalar (k : ) (p : ) (hp : Nat.Prime p) :
                                                                                      have pp := p, ; homothetyR_MF k (Units.mk0 pp ) = p ^ (k - 2) 1

                                                                                      On modular forms of weight k, the homothety by a prime p acts as multiplication by the scalar p^{k-2}.

                                                                                      Multiplicativity of Hecke operators on modular forms at coprime indices, inherited from the lattice version.

                                                                                      theorem HeckeMultiplicativity.hecke_prime_power_recurrence_MF_with_R (k : ) (p : ) (hp : Nat.Prime p) (r : ) :
                                                                                      have pp := p, ; heckeT_MF k (pp ^ (r + 2)) = heckeT_MF k (pp ^ (r + 1)) * heckeT_MF k pp - p (heckeT_MF k (pp ^ r) * homothetyR_MF k (Units.mk0 pp ))

                                                                                      The prime-power Hecke recurrence on modular forms in the form involving the homothety operator R_p.

                                                                                      theorem HeckeMultiplicativity.hecke_multiplicative_MF (k : ) (m n : ℕ+) (h : (↑m).Coprime n) :
                                                                                      heckeT_MF k (m * n) = heckeT_MF k m * heckeT_MF k n

                                                                                      Multiplicativity of Hecke operators on modular forms at coprime indices.

                                                                                      theorem HeckeMultiplicativity.hecke_prime_power_recurrence_MF (k : ) (p : ) (hp : Nat.Prime p) (r : ) :
                                                                                      have pp := p, ; heckeT_MF k (pp ^ (r + 2)) = heckeT_MF k (pp ^ (r + 1)) * heckeT_MF k pp - p ^ (k - 1) heckeT_MF k (pp ^ r)

                                                                                      The scalar form of the prime-power Hecke recurrence on weight-k modular forms: T_{p^{r+2}} = T_{p^{r+1}} T_p − p^{k-1} T_{p^r}.

                                                                                      The absolute Galois group of , Gal(ℚ̄/ℚ).

                                                                                      Instances For
                                                                                        @[implicit_reducible]

                                                                                        Group structure on the absolute Galois group of .

                                                                                        A choice of Frobenius element in Gal(ℚ̄/ℚ) for the prime p.

                                                                                        Instances For

                                                                                          The -adic Galois representation ρ_{E, ℓ} : Gal(ℚ̄/ℚ) → GL₂(ℤ_ℓ) associated to an elliptic curve E, arising from the Tate module.

                                                                                          Instances For
                                                                                            noncomputable def GaloisRepresentation.reductionModL ( : ) [Fact (Nat.Prime )] :
                                                                                            GL (Fin 2) ℤ_[] →* GL (Fin 2) (ZMod )

                                                                                            Reduction GL₂(ℤ_ℓ) → GL₂(𝔽_ℓ) modulo .

                                                                                            Instances For

                                                                                              The mod- Galois representation attached to E: the composition of the -adic representation with reduction modulo .

                                                                                              Instances For

                                                                                                At a prime p of good reduction, the trace of Frobenius on the -adic Galois representation of E equals the integer trace of Frobenius a_p(E) viewed in ℤ_ℓ.

                                                                                                A formal Dirichlet series, wrapping a sequence of complex coefficients.

                                                                                                Instances For

                                                                                                  The value at s of a Dirichlet series, defined as the L-series of its coefficient sequence.

                                                                                                  Instances For

                                                                                                    Summability of a Dirichlet series at s: the underlying L-series sum is summable.

                                                                                                    Instances For
                                                                                                      @[simp]

                                                                                                      Unfolding lemma: the eval of a Dirichlet series is definitionally the L-series of its coefficients.

                                                                                                      The Dirichlet series summability predicate unfolds to L-series summability.

                                                                                                      theorem NewformDefinition.DirichletSeries.summable_of_isBigO_rpow (L : DirichletSeries) {σ : } {s : } (hs : σ + 1 < s.re) (hO : L.coeffs =O[Filter.atTop] fun (n : ) => n ^ σ) :

                                                                                                      If the coefficients are O(n^σ) at infinity, the Dirichlet series is summable at every s with Re(s) > σ + 1.

                                                                                                      Under the same O(n^σ) hypothesis on coefficients, the Dirichlet series is differentiable on the half-plane Re(s) > σ + 1.

                                                                                                      The arithmetic rank of an elliptic curve over : the ℤ-rank of its Mordell–Weil group modulo torsion.

                                                                                                      Instances For

                                                                                                        The arithmetic rank is realised by an additive isomorphism E(ℚ)/tors ≃ ℤ^{rank}.

                                                                                                        The analytic continuation of the L-function of E to a function defined on all of .

                                                                                                        Instances For

                                                                                                          The extended L-function L_E is differentiable on all of .

                                                                                                          The analytic rank of an elliptic curve over : the order of vanishing of its extended L-function at s = 1.

                                                                                                          Instances For

                                                                                                            Specification of the analytic rank: L_E(s) = (s-1)^{rank_an} · g(s) with g differentiable and g(1) ≠ 0.

                                                                                                            The weak form of the Birch–Swinnerton-Dyer conjecture: the arithmetic and analytic ranks of an elliptic curve over coincide.

                                                                                                            Data for a cusp form: weight, level, and complex Fourier coefficients with a_0 = 0.

                                                                                                            Instances For

                                                                                                              The L-function attached to a cusp form's coefficient data: the Dirichlet L-series of its coefficients.

                                                                                                              Instances For

                                                                                                                The completed L-function of a cusp form: Λ(f, s) = N^{s/2} (2π)^{-s} Γ(s) L(f, s).

                                                                                                                Instances For
                                                                                                                  theorem HeckeAnalyticContinuation.hecke_analytic_continuation_and_functional_equation (f : CuspFormData) :
                                                                                                                  ∃ (L_ext : ), Differentiable L_ext (∀ (s : ), LSeriesSummable f.coeffs sL_ext s = LSeries f.coeffs s) ∃ (ε : ), (ε = 1 ε = -1) ∀ (s : ), f.level ^ (s / 2) * (2 * Real.pi) ^ (-s) * Complex.Gamma s * L_ext s = ε * (f.level ^ ((f.weight - s) / 2) * (2 * Real.pi) ^ (-(f.weight - s)) * Complex.Gamma (f.weight - s) * L_ext (f.weight - s))

                                                                                                                  Hecke's theorem: the L-function attached to a cusp form admits an entire extension L_ext to that agrees with the Dirichlet series on the region of summability and satisfies the functional equation Λ(s) = ε · Λ(k - s) with sign ε ∈ {±1}.

                                                                                                                  Data for a normalized newform: cusp-form data together with the normalization a_1 = 1.

                                                                                                                  Instances For

                                                                                                                    The principal Dirichlet character of conductor N at the prime p: equals 0 if p | N and 1 otherwise.

                                                                                                                    Instances For
                                                                                                                      noncomputable def EulerProductNewform.localEulerFactor (f : NewformData) (p : ) (s : ) :

                                                                                                                      The local Euler factor of a newform at the prime p: (1 - a_p p^{-s} + χ(p) p^{k-1} p^{-2s})^{-1}.

                                                                                                                      Instances For
                                                                                                                        noncomputable def EulerProductNewform.eulerProduct (f : NewformData) (s : ) :

                                                                                                                        The Euler product of a newform: the (unordered) product over primes of the local Euler factors.

                                                                                                                        Instances For

                                                                                                                          The L-function of a newform, as a Dirichlet series in its Fourier coefficients.

                                                                                                                          Instances For

                                                                                                                            The L-function of a newform admits an Euler product expansion over primes.

                                                                                                                            The root number w(E) ∈ {±1} of an elliptic curve over : the sign in the functional equation of its L-function.

                                                                                                                            Instances For

                                                                                                                              The root number of an elliptic curve is ±1.

                                                                                                                              Parity conjecture: the root number w(E) equals (−1)^{rank(E)}, expressing that the parity of the arithmetic rank matches the sign of the functional equation.

                                                                                                                              @[reducible, inline]

                                                                                                                              Cusp forms of weight k for the congruence subgroup Γ₀(N) ≤ SL(2, ℤ).

                                                                                                                              Instances For

                                                                                                                                The Hecke operator T_n acting on weight-k modular forms for SL(2, ℤ).

                                                                                                                                Instances For

                                                                                                                                  A fundamental domain in the upper half plane for the action of a congruence subgroup Γ ≤ SL(2, ℤ).

                                                                                                                                  Instances For

                                                                                                                                    The Petersson inner product on cusp forms (Definition 24.18): integrates f(τ) · conj(g(τ)) · y^{k-2} over a fundamental domain for Γ.

                                                                                                                                    Instances For

                                                                                                                                      The Petersson inner product is Hermitian: ⟨f, g⟩ = conj(⟨g, f⟩).

                                                                                                                                      The Petersson inner product is additive in its first argument.

                                                                                                                                      The Petersson inner product is -linear in its first argument.

                                                                                                                                      Positivity: the real part of ⟨f, f⟩ is nonnegative.

                                                                                                                                      The Hecke operator T_n acting on cusp forms for Γ₀(N), defined when gcd(n, N) = 1.

                                                                                                                                      Instances For

                                                                                                                                        Hecke operators on Γ₀(N) at indices coprime to N are self-adjoint with respect to the Petersson inner product.

                                                                                                                                        theorem SpectralTheorem.spectral_theorem_commuting_symmetric {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ι : Type u_3} [DecidableEq (ι𝕜)] {T : ιE →ₗ[𝕜] E} (hT : ∀ (i : ι), (T i).IsSymmetric) (hC : Pairwise (Function.onFun Commute T)) :
                                                                                                                                        DirectSum.IsInternal fun (χ : ι𝕜) => ⨅ (j : ι), Module.End.eigenspace (T j) (χ j)

                                                                                                                                        Spectral theorem for a family of commuting symmetric operators: the family admits a joint eigenspace decomposition, i.e. the joint eigenspaces give an internal direct sum decomposition of the whole space.

                                                                                                                                        theorem SpectralTheorem.spectral_theorem_commuting_symmetric_iSup {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {ι : Type u_3} {T : ιE →ₗ[𝕜] E} (hT : ∀ (i : ι), (T i).IsSymmetric) (hC : Pairwise (Function.onFun Commute T)) :
                                                                                                                                        ⨆ (χ : ι𝕜), ⨅ (i : ι), Module.End.eigenspace (T i) (χ i) =

                                                                                                                                        Spectral theorem (supremum version): the supremum of joint eigenspaces of a commuting family of symmetric operators is the whole space.

                                                                                                                                        theorem SpectralTheorem.directSum_isInternal_commuting_pair {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A B : E →ₗ[𝕜] E} (hA : A.IsSymmetric) (hB : B.IsSymmetric) (hAB : Commute A B) :

                                                                                                                                        Spectral theorem for a commuting pair of symmetric operators: the joint eigenspaces Eig_A(α) ∩ Eig_B(β) form an internal direct sum decomposition.

                                                                                                                                        The normalized (completed) L-function of an elliptic curve over : N^{s/2} (2π)^{-s} Γ(s) L(E, s).

                                                                                                                                        Instances For

                                                                                                                                          Convert an integral weight-2 newform to abstract cusp-form data (weight 2, same level, coefficients embedded in ).

                                                                                                                                          Instances For
                                                                                                                                            theorem LFunctionAnalyticContinuation.analytic_continuation_and_functional_equation (E : WeierstrassCurve.Affine ) [WeierstrassCurve.IsElliptic E] :
                                                                                                                                            ∃ (L_ext : ), Differentiable L_ext (∀ (s : ), LSeriesSummable (fun (n : ) => (NewformQExpansion.qExpansionCoeffs E n)) sL_ext s = EllipticCurveLFunction.LFunction E s) ∃ (w : ), (w = 1 w = -1) ∀ (s : ), (EllipticCurveReduction.conductor E) ^ (s / 2) * (2 * Real.pi) ^ (-s) * Complex.Gamma s * L_ext s = w * ((EllipticCurveReduction.conductor E) ^ ((2 - s) / 2) * (2 * Real.pi) ^ (-(2 - s)) * Complex.Gamma (2 - s) * L_ext (2 - s))

                                                                                                                                            The L-function of an elliptic curve over extends to an entire function on agreeing with L(E, s) on the region of summability and satisfies the functional equation Λ(s) = w · Λ(2 - s) with sign w ∈ {±1}.

                                                                                                                                            @[reducible, inline]

                                                                                                                                            Cusp forms of weight k for an arbitrary subgroup Γ ≤ SL(2, ℤ).

                                                                                                                                            Instances For

                                                                                                                                              The n-th q-expansion coefficient a_n(f) of a weight-k cusp form for SL(2, ℤ).

                                                                                                                                              Instances For

                                                                                                                                                For each fixed n, the map f ↦ a_n(f) is -linear.

                                                                                                                                                A cusp form is determined by its q-expansion: if every coefficient vanishes then the form itself is zero.

                                                                                                                                                A cusp form has zero constant term in its q-expansion: a_0(f) = 0.

                                                                                                                                                Corollary 24.15: for any cusp form f ∈ S_k(Γ₀(1)) and integers m, n with gcd(m, n) = 1, the Hecke operator satisfies a_m(T_n f) = a_{mn}(f).

                                                                                                                                                A cusp form is a Hecke eigenform if it is nonzero and is an eigenvector of every Hecke operator T_n.

                                                                                                                                                Instances For

                                                                                                                                                  A Hecke eigenform is normalized if its first Fourier coefficient is 1.

                                                                                                                                                  Instances For

                                                                                                                                                    For an eigenvector f of T_n with eigenvalue ev, we have a_n(f) = ev · a_1(f).

                                                                                                                                                    The first Fourier coefficient a_1(f) of a Hecke eigenform is nonzero.

                                                                                                                                                    theorem HeckeEigenformBasis.eigenspace_one_dimensional (k : ) (f g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ) (CongruenceSubgroup.Gamma 1)) k) (hf : IsEigenform k f) (hg : IsEigenform k g) (hsame : ∀ (n : ℕ+) (ev₁ ev₂ : ), (PeterssonInnerProduct.heckeOnCuspForms k n) f = ev₁ f(PeterssonInnerProduct.heckeOnCuspForms k n) g = ev₂ gev₁ = ev₂) :
                                                                                                                                                    ∃ (c : ), g = c f

                                                                                                                                                    Two Hecke eigenforms with the same system of eigenvalues differ by a scalar multiple (eigenspaces in the joint decomposition are one-dimensional).

                                                                                                                                                    For a normalized eigenform f, the Hecke eigenvalue at n equals the Fourier coefficient a_n(f).

                                                                                                                                                    The space of cusp forms is spanned by Hecke eigenforms: there exists a finite family of (linearly independent) eigenforms whose span is the whole space.

                                                                                                                                                    Every Hecke eigenform admits a normalization to a normalized eigenform: a nonzero scalar multiple with a_1 = 1.

                                                                                                                                                    The space of cusp forms admits a basis of normalized Hecke eigenforms.

                                                                                                                                                    The n-th Fourier coefficient of a weight-k cusp form for SL(2, ℤ).

                                                                                                                                                    Instances For

                                                                                                                                                      The 0-th Fourier coefficient of a cusp form vanishes.

                                                                                                                                                      Fourier coefficients are additive: a_n(f + g) = a_n(f) + a_n(g).

                                                                                                                                                      Fourier coefficients are -homogeneous: a_n(c · f) = c · a_n(f).

                                                                                                                                                      Cusp forms are determined by their full q-expansion: if all Fourier coefficients agree, the cusp forms are equal.

                                                                                                                                                      Theorem 24.14: for any cusp form f ∈ S_k(Γ₀(1)) and prime p, a_n(T_p f) = a_{np}(f) if p ∤ n, otherwise a_n(T_p f) = a_{np}(f) + p^{k-1} a_{n/p}(f).

                                                                                                                                                      The "non-dividing" case of Theorem 24.14: when p ∤ n, a_n(T_p f) = a_{np}(f).

                                                                                                                                                      The "dividing" case of Theorem 24.14: when p ∣ n, a_n(T_p f) = a_{np}(f) + p^{k-1} a_{n/p}(f).

                                                                                                                                                      The Hecke operator at n = 1 is the identity on cusp forms.

                                                                                                                                                      Multiplicativity of Hecke operators on cusp forms at coprime indices: T_{mn} = T_m ∘ T_n when gcd(m, n) = 1.

                                                                                                                                                      Prime-power recurrence for Hecke operators on cusp forms: T_{p^{r+2}} = T_{p^{r+1}} ∘ T_p − p^{k-1} · T_{p^r}.

                                                                                                                                                      For a prime p coprime to m, the Hecke action on Fourier coefficients specialises to a_m(T_p f) = a_{mp}(f).

                                                                                                                                                      Iteration to prime powers: for m coprime to the prime p, the action of T_{p^r} on Fourier coefficients satisfies a_m(T_{p^r} f) = a_{m p^r}(f).

                                                                                                                                                      General statement of Corollary 24.15 (coprime version): for gcd(m, n) = 1, a_m(T_n f) = a_{mn}(f).

                                                                                                                                                      The number ν₂(Γ) of elliptic points of order 2 for Γ ≤ SL(2, ℤ).

                                                                                                                                                      Instances For

                                                                                                                                                        The number ν₃(Γ) of elliptic points of order 3 for Γ ≤ SL(2, ℤ).

                                                                                                                                                        Instances For

                                                                                                                                                          The number ν_∞(Γ) of cusps of Γ ≤ SL(2, ℤ).

                                                                                                                                                          Instances For

                                                                                                                                                            The genus g(Γ) of the modular curve Γ\ℍ^*.

                                                                                                                                                            Instances For

                                                                                                                                                              Instance form: the space of modular forms M_k(Γ) is finite-dimensional over .

                                                                                                                                                              Instance form: the space of cusp forms S_k(Γ) is finite-dimensional over .

                                                                                                                                                              M_0(Γ) ≅ ℂ (constants): the space of weight-0 modular forms is 1-dimensional.

                                                                                                                                                              theorem ModularFormDimension.dim_modularForm_even (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )) (k : ) (hk_pos : 0 < k) (hk_even : Even k) :
                                                                                                                                                              (Module.finrank (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ) Γ) k)) = (k - 1) * ((genus Γ) - 1) + k / 4 * (nu2 Γ) + k / 3 * (nu3 Γ) + k / 2 * (nuInfty Γ)

                                                                                                                                                              Dimension formula for M_k(Γ) for even positive k, in terms of the genus, the elliptic point counts, and the number of cusps.

                                                                                                                                                              theorem ModularFormDimension.dim_cuspForm_even_gt2 (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) )) (k : ) (hk_gt2 : 2 < k) (hk_even : Even k) :
                                                                                                                                                              (Module.finrank (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ) Γ) k)) = (k - 1) * ((genus Γ) - 1) + k / 4 * (nu2 Γ) + k / 3 * (nu3 Γ) + (k / 2 - 1) * (nuInfty Γ)

                                                                                                                                                              Dimension formula for S_k(Γ) for even k > 2, with cusp contribution (k/2 − 1).

                                                                                                                                                              The new subspace S_k^{new}(Γ₀(N)) of cusp forms of weight k and level N, complementary to the old subspace coming from divisors of N.

                                                                                                                                                              Instances For
                                                                                                                                                                @[implicit_reducible]

                                                                                                                                                                Additive group structure on the new subspace of cusp forms.

                                                                                                                                                                @[implicit_reducible]

                                                                                                                                                                Anonymous instance: additive group structure on the new subspace of cusp forms.

                                                                                                                                                                @[implicit_reducible]

                                                                                                                                                                Complex vector space structure on the new subspace of cusp forms.

                                                                                                                                                                @[implicit_reducible]

                                                                                                                                                                Anonymous instance: complex vector space structure on the new subspace of cusp forms.

                                                                                                                                                                The new subspace S_k^{new}(Γ₀(N)) is finite-dimensional over .

                                                                                                                                                                Anonymous instance: the new subspace S_k^{new}(Γ₀(N)) is finite-dimensional over .

                                                                                                                                                                The inclusion of the new subspace into the full space of cusp forms for Γ₀(N).

                                                                                                                                                                Instances For

                                                                                                                                                                  The inclusion of the new subspace into the full space of cusp forms is injective.

                                                                                                                                                                  Hecke operators T_n restrict to endomorphisms of the new subspace.

                                                                                                                                                                  Instances For
                                                                                                                                                                    noncomputable def HeckeNewformDecomposition.qExpCoeffNew (N : ) (k : ) :

                                                                                                                                                                    The n-th q-expansion coefficient of an element of the new subspace.

                                                                                                                                                                    Instances For

                                                                                                                                                                      For each n, the map f ↦ a_n(f) on the new subspace is -linear.

                                                                                                                                                                      theorem HeckeNewformDecomposition.qExpCoeffNew_injective (N : ) (k : ) (f : NewSubspaceCuspForm N k) (h : ∀ (n : ), qExpCoeffNew N k f n = 0) :
                                                                                                                                                                      f = 0

                                                                                                                                                                      An element of the new subspace is determined by its q-expansion: if every coefficient vanishes, the form itself is zero.

                                                                                                                                                                      The constant term a_0 of any element of the new subspace vanishes.

                                                                                                                                                                      A new-subspace eigenform: a nonzero element that is an eigenvector of every Hecke operator restricted to the new subspace.

                                                                                                                                                                      Instances For

                                                                                                                                                                        A newform of level N and weight k: a new-subspace eigenform with first Fourier coefficient equal to 1.

                                                                                                                                                                        Instances For
                                                                                                                                                                          theorem HeckeNewformDecomposition.eigenvalue_eq_coeff_new (N : ) (k : ) (f : NewSubspaceCuspForm N k) (hf : IsNewform N k f) (n : ℕ+) (ev : ) (hev : (heckeOnNewSubspace N k n) f = ev f) :
                                                                                                                                                                          ev = qExpCoeffNew N k f n

                                                                                                                                                                          For a newform, every Hecke eigenvalue is equal to the corresponding Fourier coefficient.

                                                                                                                                                                          theorem HeckeNewformDecomposition.newform_basis (N : ) (k : ) :
                                                                                                                                                                          ∃ (ι : Type) (x : Fintype ι) (B : ιNewSubspaceCuspForm N k), (∀ (i : ι), IsNewform N k (B i)) LinearIndependent B Submodule.span (Set.range B) (∀ (i : ι) (n : ℕ+), (heckeOnNewSubspace N k n) (B i) = qExpCoeffNew N k (B i) n B i) (∀ (i : ι), Module.finrank ↥( B i) = 1) ∀ (i j : ι), (∀ (n : ), qExpCoeffNew N k (B i) n = qExpCoeffNew N k (B j) n)i = j

                                                                                                                                                                          Newform basis theorem: the new subspace S_k^{new}(Γ₀(N)) admits a canonical basis of newforms, each a Hecke eigenvector with eigenvalues equal to its Fourier coefficients, with corresponding one-dimensional eigenlines, and uniquely determined by its q-expansion.