Module functions

Source

Expand description

Auto-generated module

🤖 Generated with SplitRS

Functions§

arrow
arrow3
arrow4
arrow5
atkin_lehner_eigenvalue_ty: AtkinLehnerEigenvalue : Nat → Newform → Int — eigenvalue of w_N on a newform: ±1.
atkin_lehner_involution_ty: AtkinLehnerInvolution : Nat → ModularForm → ModularForm — w_N involution on S_k(Γ₀(N)).
bool_ty
build_env: Build an environment containing the required named axioms for the spec structs.
build_modular_forms_env: Build the modular forms kernel environment.
check_ramanujan_congruence: Check Ramanujan’s congruence τ(n) ≡ σ_{11}(n) (mod 691) for n ≤ N.
cm_point_ty: CMPoint : Nat → Type — a CM point τ ∈ H: quadratic imaginary τ, fixed by an order in an imaginary quadratic field K.
cm_theory_ty: CMTheory : Nat → Prop — CM theory: explicit class field theory for imaginary quadratic fields via j-function values j(τ) for CM points τ.
coleman_family_ty: ColemanFamily : Nat → Type — Coleman family of overconvergent eigenforms varying p-adically in weight.
completed_l_function_ty: CompletedLFunction : ModularForm → Complex → Complex — Λ(f,s) = (2π)^{-s} Γ(s) L(f,s) (completed L-function).
complex_ty
congruence_subgroup_ty: CongruenceSubgroup : Nat → Type — Γ(N) = ker(SL₂(ℤ) → SL₂(ℤ/Nℤ)).
cst
cusp_form_dimension_ty: CuspFormDimension : Nat → Nat → Nat — dim S_k(Γ₀(N)).
cusp_form_ty: CuspForm : Nat → CongruenceSubgroup → Type — space S_k(Γ) of weight-k cusp forms for Γ.
cusp_resolution_ty: CuspResolution : Nat → Type — the resolution of cusps of X₀(N): local coordinates at each cusp.
cusp_ty: Cusp : CongruenceSubgroup → Type — cusps of the modular curve X(Γ).
deformation_ring_ty: DeformationRing : Nat → Type — the universal deformation ring R (pro-representable hull) of ρ̄.
deligne_semisimplicity_ty: DeligneSemiSimplicity : Newform → Prop — Deligne’s theorem: ρ_{f,l} is semi-simple and pure of weight k-1 (used in the proof of Weil conjectures for curves).
delta_form_ty: DeltaForm : Type — the discriminant modular form Δ ∈ S_{12}(SL₂(ℤ)).
diamond_operator_ty: DiamondOperator : Nat → Nat → ModularForm → ModularForm — ⟨d⟩ acting on M_k(Γ₁(N)).
dimension_s_k: Modular forms dimension formula (approximate).
eichler_shimura_construction_ty: EichlerShimuraConstruction : Newform → Prop — the construction of ρ_{f,l} via the l-adic cohomology of the modular curve X₀(N) (Eichler-Shimura relation).
eichler_shimura_pairing_ty: EichlerShimuraPairing : ModularForm → ModularSymbol → Complex — integration pairing ∫_{α}^{β} f(τ)(2πi τ)^j dτ.
eichler_shimura_relation_ty: EichlerShimuraRelation : Nat → Prop — T_p on cusp forms corresponds to Frobenius at p on Jac(X(Γ)).
eigencurve_ty: EigenvarietyCurve : Nat → Type — the eigencurve (Coleman-Mazur): a rigid analytic curve parametrising overconvergent eigenforms of all weights.
eisenstein_fourier_coeff: Fourier coefficient of E_k at n: a_0 = 1 (for normalized Eisenstein series G_k/2ζ(k)), a_n = σ_{k-1}(n) for n ≥ 1.
eisenstein_series_ty: EisensteinSeries : Nat → Type — Eisenstein series E_k (for k ≥ 4, even).
euler_product_mf_ty: EulerProduct_MF : ModularForm → Prop — L(f,s) = ∏_p (1 - a_p p^{-s} + p^{k-1-2s})^{-1} for f a newform.
famous_modular_forms: Famous modular forms table.
fermat_last_theorem_via_modularity_ty: FermatLastTheoremViaModularity : Prop — Fermat’s Last Theorem follows from Wiles’ R=T (modularity lifting) theorem.
fourier_coefficient_ty: FourierCoefficient : ModularForm → Nat → Complex — n-th Fourier coefficient a_n(f).
functional_equation_mf_ty: FunctionalEquation_MF : ModularForm → Prop — Λ(f,s) = ε·Λ(f̃, k-s) for some root number ε ∈ {±1}.
fundamental_domain_ty: FundamentalDomain : Type — standard fundamental domain F for SL₂(ℤ).
g_function_ty: GFunction : Nat → Type — non-normalised Eisenstein series G_k = ∑_{(c,d)≠(0,0)} (cτ+d)^{-k}.
galois_conjugate_mf_ty: GaloisConjugate_MF : Newform → Type — Galois conjugate forms: the orbit of f under Gal(Q(a_n)/Q).
galois_representation_mf_ty: GaloisRepresentation_MF : Newform → Nat → Type — l-adic Galois representation ρ_{f,l}: Gal(Q̄/Q) → GL₂(Q_l) attached to a newform f (Eichler-Shimura / Deligne).
gamma0_ty: Gamma0 : Nat → Type — Γ₀(N) = {[[a,b],[c,d]] : N|c}.
gamma1_ty: Gamma1 : Nat → Type — Γ₁(N) = {[[a,b],[c,d]] : N|c, a≡d≡1 mod N}.
gcd_u64
generator_s_ty: GeneratorS : ModularGroup — S = [[0,-1],[1,0]].
generator_t_ty: GeneratorT : ModularGroup — T = [[1,1],[0,1]].
gross_zagier_formula_ty: GrossZagierFormula : Nat → Prop — Gross-Zagier: L’(E,1) = (height of Heegner point) · (period).
gross_zagier_heegner_ty: GrossZagierHeegner : Nat → Prop — Gross-Zagier formula: L’(E, 1) is proportional to the Néron-Tate height of the Heegner point in J₀(N).
half_integer_weight_form_ty: HalfIntegerWeightForm : Nat → Nat → Type — modular form of weight k/2 (k odd) for Γ₀(4N) with nebentypus.
hecke_algebra_ty: HeckeAlgebra : Nat → CongruenceSubgroup → Type — commutative algebra generated by all T_n.
hecke_commutative_ty: HeckeCommutative : Nat → CongruenceSubgroup → Prop — the Hecke algebra is commutative: T_m T_n = T_n T_m.
hecke_eigenform_ty: HeckeEigenform : ModularForm → Prop — f is a simultaneous eigenform for all Hecke operators.
hecke_eigenvalue_ty: HeckeEigenvalue : ModularForm → Nat → Complex — eigenvalue λ_n(f) of T_n on f.
hecke_multiplicativity_ty: HeckeMultiplicativity : Nat → CongruenceSubgroup → Prop — T_mn = T_m ∘ T_n when gcd(m,n) = 1.
hecke_normal_operator_ty: HeckeNormalOperator : ModularForm → Prop — T_n is normal w.r.t. Petersson inner product: T_n* = T_n.
hecke_operator_ty: HeckeOperator : Nat → Nat → CongruenceSubgroup → Type — T_n acting on M_k(Γ).
hecke_tn_matrix_ty: HeckeTnMatrix : Nat → Nat → Type — explicit Hecke matrix double coset [Γ diag(1,n) Γ] acting on q-expansions.
hecke_tp_coefficients: Hecke operator T_p action on a modular form with Fourier coefficients a_n. If f = ∑ a_n q^n has weight k, then T_p(f) = ∑ b_n q^n where b_n = a_{pn} + p^{k-1} a_{n/p} (with a_{n/p}=0 if p∤n).
heegner_point_ty: HeegnerPoint : Nat → Type — a Heegner point on X₀(N): a CM point in the modular curve X₀(N).
hida_family_ty: HidaFamily : Nat → Nat → Type — Hida family: a p-adic analytic family of ordinary newforms of varying weight.
hilbert_modular_form_ty: HilbertModularForm : Nat → Type — Hilbert modular form over a totally real field of degree n.
holomorphic_at_cusps_ty: HolomorphicAtCusps : ModularForm → Prop — f is holomorphic at all cusps.
int_ty
jacobi_four_squares_ty: JacobiFormulaFourSquares : Nat → Nat — Jacobi’s four-square theorem: r_4(n) = 8 ∑_{d|n, 4∤d} d.
jacobi_theta_function_ty: JacobiThetaFunction : Complex → Complex → Complex — ϑ(z, τ) = ∑_{n∈ℤ} exp(πi n² τ + 2πi n z).
jacobian_of_modular_curve_ty: JacobianOfModularCurve : CongruenceSubgroup → Type — Jac(X(Γ)) as an abelian variety.
kohnen_variance_ty: KokbeVariance : Nat → Nat → Real — variance of a half-integer weight Fourier coefficient a(n): linked to L(f, 1/2) via Kohnen-Zagier / Waldspurger.
l_adic_representation_ty: LAdic_Representation : Newform → Nat → Prop — the l-adic representation is unramified at all p ∤ lN with Frobenius characteristic polynomial X² - a_p X + p^{k-1}.
l_function_mf_ty: LFunction_MF : ModularForm → Complex → Complex — L(f,s) = ∑ a_n(f)·n^{-s}.
langlands_correspondence_gl2_ty: LanglandsCorrespondence_GL2 : Newform → Type — automorphic representation of GL_2(ℚ\𝔸_ℚ) attached to a newform.
laplace_beltrami_eigenvalue_ty: LaplaceBeltramiEigenvalue : MaassForm → Real — spectral eigenvalue λ = s(1-s) (where s ∈ ℂ) of Δ acting on a Maass form.
maass_form_ty: MaassForm : Nat → Type — real-analytic eigenfunction of the Laplace-Beltrami operator Δ_k on Γ\H.
maass_l_function_ty: MaassLFunction : MaassForm → Complex → Complex — L-function L(f, s) = ∑ a_n n^{-s} for a Maass cusp form f.
manin_symbol_ty: ManinSymbol : Nat → Type — Manin symbol (c:d) ∈ P¹(ℤ/Nℤ).
modular_curve_ty: ModularCurve : CongruenceSubgroup → Type — modular curve Y(Γ) = Γ\H (or its compactification X(Γ)).
modular_form_conductor_ty: ModularFormConductor : Newform → Nat — arithmetic conductor N(f).
modular_form_dimension_ty: ModularFormDimension : Nat → Nat → Nat — dim M_k(Γ₀(N)) via Riemann-Roch / Gauss-Bonnet.
modular_form_lift_ty: ModularFormLift : Newform → Nat → Prop — base change / automorphic lift of a newform to GL_2 over a number field.
modular_form_ty: ModularForm : Nat → CongruenceSubgroup → Type — space M_k(Γ) of weight-k modular forms for Γ.
modular_form_weight_ty: ModularFormWeight : ModularForm → Nat — weight k of a modular form.
modular_group_ty: ModularGroup : Type — SL₂(ℤ) as a group.
modular_symbol_ty: ModularSymbol : Nat → CongruenceSubgroup → Type — {α, β} ∈ H_1(X(Γ), cusps, ℤ), the Manin-Eichler-Shimura symbol.
modular_unit_ty: ModularUnit : Nat → Type — a modular unit u on X₀(N): a rational function with zeros/poles only at cusps.
modularity_lifting_ty: ModularityLifting : Nat → Prop — R = T theorem: the universal deformation ring R of a residual Galois representation equals the Hecke algebra T (Taylor-Wiles 1995).
monstrous_moonshine_data: Monstrous moonshine conjecture (proved by Borcherds).
nat_ty
nebentypus_character_ty: NebentypusCharacter : Newform → Type — nebentypus character χ: (ℤ/Nℤ)× → ℂ× of a newform.
newform_decomposition_ty: NewformDecomposition : Nat → CongruenceSubgroup → Prop — S_k(Γ₀(N)) = S_k^{new}(N) ⊕ S_k^{old}(N).
newform_eigen_system_ty: NewformEigenSystem : Nat → Nat → Type — eigenpacket (system of Hecke eigenvalues) for a newform of weight k, level N.
newform_ty: Newform : Nat → Nat → Type — primitive newform of weight k and level N.
oldform_space_ty: OldformSpace : Nat → Nat → Type — space of oldforms of weight k, level N.
overconvergent_modular_form_ty: OverconvergentModularForm : Nat → Real → Type — p-adic overconvergent modular form of weight k and overconvergence radius r.
p_adic_l_function_mf_ty: PAdicLFunction_MF : Newform → Nat → Complex → Complex — p-adic L-function L_p(f, s) interpolating critical values L(f, j) (j = 1…k-1).
petersson_inner_product_ty: PeterssonInnerProduct : CuspForm → CuspForm → Complex — ⟨f, g⟩ = ∫_Γ\H f(τ)·ḡ(τ)·y^k dxdy/y².
petersson_norm_ty: PeterssonNorm : CuspForm → Real — ‖f‖² = ⟨f,f⟩.
poincare_series_ty: PoincareSeries : Nat → Nat → Complex → Complex — Poincaré series P_{k,m}(τ) = ∑{γ∈Γ∞\Γ} (cτ+d)^{-k} e^{2πimγτ}.
prop
psl2z_ty: PSL2Z : Type — PSL₂(ℤ) = SL₂(ℤ)/{±I}.
r2: Theta series coefficient: r_2(n) = #{(a,b) ∈ ℤ²: a²+b²=n}.
ramanujan_congruence_ty: RamanujanCongruence : Nat → Prop — τ(n) ≡ σ_{11}(n) (mod 691).
ramanujan_conjecture_ty: RamanujanConjecture : Nat → Prop — |τ(p)| ≤ 2·p^{11/2} for all primes p (proved by Deligne as Weil conjecture).
ramanujan_tau_ty: RamanujanTau : Nat → Int — τ(n) = n-th Fourier coefficient of Δ = q∏(1-q^n)^24.
ramanujan_tau_up_to: The Ramanujan tau function τ(n) for small n, computed via the identity Δ = q ∏_{n≥1}(1-q^n)^24. We compute coefficients up to N_MAX by convolution. This is an integer-exact computation for small n.
real_ty
register_modular_forms: Register all modular form axioms into an existing environment.
residual_representation_ty: ResidualRepresentation : Nat → Type — a mod-l Galois representation ρ̄: Gal(Q̄/Q) → GL₂(F_l).
root_number_ty: RootNumber : ModularForm → Int — global root number ε(f) ∈ {±1}.
sato_tate_conjecture_ty: SatoTateConjecture : Nat → Nat → Prop — equidistribution of a_p/(2√p) w.r.t. Sato-Tate measure (proved by Taylor et al.).
sato_tate_equidistribution_ty: SatoTateEquidistribution : Newform → Prop — Sato-Tate equidistribution: a_p/(2p^{(k-1)/2}) is equidistributed w.r.t. the Sato-Tate measure (Taylor-Barnet-Lamb-Geraghty-Harris 2011).
sato_tate_l_function_ty: SatoTateLFunction : Newform → Nat → Complex — symmetric power L-function Sym^n L(f, s) used in the proof of Sato-Tate.
sato_tate_measure_ty: SatoTateMeasure : Nat → Type — the Sato-Tate measure μ_ST on [-2,2]: (2/π)√(1 - x²/4) dx.
selberg_eigenvalue_conjecture_ty: SelvergEigenvalueConjecture : Prop — Selberg’s eigenvalue conjecture: all Maass cusp forms for Γ₀(N) have λ ≥ 1/4 (equivalently s = 1/2 + it, t real).
shimura_correspondence_ty: ShimuraCorrespondence : Nat → Prop — Shimura lifting: half-integer weight forms ↔ integer weight forms (Shimura 1973; explicit via Hecke correspondences).
shimura_reciprocity_ty: ShimuraReciprocity : Nat → Prop — Shimura reciprocity law: the action of Gal(K^ab/K) on CM values of modular functions via the Artin map.
siegel_modular_form_ty: SiegelModularForm : Nat → Nat → Type — Siegel modular form of weight k and degree g.
siegel_theta_series_ty: SiegelThetaSeries : Nat → Nat → Type — Siegel theta series θ_L of genus g attached to a positive-definite even integral lattice L of rank n.
siegel_unit_ty: SiegelUnit : Nat → Complex → Complex — Siegel unit g_a(τ) on the upper half-plane: special modular function.
sigma_k_minus_1: Compute σ_{k-1}(n) = ∑_{d|n} d^{k-1}, the divisor power sum.
strong_multiplicity_one_ty: StrongMultiplicityOne : Nat → Nat → Prop — two newforms with the same a_p for almost all p are identical.
subgroup_index_ty: SubgroupIndex : Nat → Nat — index [SL₂(ℤ) : Γ₀(N)].
subgroup_level_ty: SubgroupLevel : CongruenceSubgroup → Nat — level of a congruence subgroup.
tate_twist_mf_ty: TateTwist_MF : ModularForm → Nat → ModularForm — Tate twist f ⊗ χ for a Dirichlet character χ mod M.
taylor_wiles_method_ty: TaylorWilesMethod : Nat → Prop — the Taylor-Wiles patching method: proves R→T is an isomorphism by patching over auxiliary primes Q.
theta_series_lattice_ty: ThetaSeriesLattice : Nat → Type — theta series attached to a rank-n integral lattice.
theta_series_ty: ThetaSeries : Type → Type — theta series θ_L(τ) = ∑_{x∈L} q^{Q(x)} for a lattice L.
type0
vanishes_at_cusps_ty: VanishesAtCusps : ModularForm → Prop — f is a cusp form (a_0 = 0 at all cusps).
waldspurger_formula_ty: WaldspurgerFormula : Nat → Prop — Waldspurger’s theorem: central L-values L(f, 1/2, χ) encoded in Fourier coefficients of half-integer weight forms.
weyl_law_ty: WeylLaw : Nat → Prop — Weyl’s law: #{λ_j ≤ T} ~ (Area(Γ\H) / 4π) T as T → ∞ (Selberg).
x0n_ty: X0N : Nat → Type — compactified modular curve X₀(N) over ℚ.
x1n_ty: X1N : Nat → Type — compactified modular curve X₁(N) over ℚ.

Type Aliases§

HeckeOperatorMatrix: Type alias for backward compatibility.

Module functions

Module functions Copy item path

Functions§

Type Aliases§

Module functions