Documentation

SpherePacking.ModularForms.DimensionFormulas

def mul_Delta_map (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) (k - 12)) :

ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k

Equations

mul_Delta_map k f = ModularForm.mcast ⋯ (f.mul (ModForm_mk (CongruenceSubgroup.Gamma 1) 12 Delta))

Instances For

theorem mcast_apply {a b : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (h : a = b) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) a) (z : UpperHalfPlane) :

(ModularForm.mcast h f) z = f z

theorem mul_Delta_map_eq (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) (k - 12)) (z : UpperHalfPlane) :

(mul_Delta_map k f) z = f z * Delta z

theorem mul_Delta_map_eq_mul (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) (k - 12)) :

⇑(mul_Delta_map k f) = ⇑(f.mul (ModForm_mk (CongruenceSubgroup.Gamma 1) 12 Delta))

theorem mul_Delta_IsCuspForm (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) (k - 12)) :

IsCuspForm (CongruenceSubgroup.Gamma 1) k (mul_Delta_map k f)

def Modform_mul_Delta' (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) (k - 12)) :

CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k

Equations

Modform_mul_Delta' k f = IsCuspForm_to_CuspForm (CongruenceSubgroup.Gamma 1) k (mul_Delta_map k f) ⋯

Instances For

theorem mul_apply {k₁ k₂ : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (f : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k₁) (g : SlashInvariantForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k₂) (z : UpperHalfPlane) :

(f.mul g) z = f z * g z

theorem Modform_mul_Delta_apply (k : ℤ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) (k - 12)) (z : UpperHalfPlane) :

(Modform_mul_Delta' k f) z = f z * Delta z

def CuspForms_iso_Modforms (k : ℤ) :

CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k ≃ₗ[ℂ ] ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) (k - 12)

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem delta_eq_E4E6_const :

∃ (c : ℂ), c • Delta = Delta_E4_E6_aux

theorem cuspform_weight_lt_12_zero (k : ℤ) (hk : k < 12) :

Module.rank ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) = 0

theorem IsCuspForm_weight_lt_eq_zero (k : ℤ) (hk : k < 12) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : IsCuspForm (CongruenceSubgroup.Gamma 1) k f) :

f = 0

theorem Delta_E4_E6_eq :

ModForm_mk (CongruenceSubgroup.Gamma 1) 12 Delta_E4_E6_aux = (1 / 1728) • ((DirectSum.of (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1))) 4) E₄ ^ 3 - (DirectSum.of (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1))) 6) E₆ ^ 2) 12

theorem Delta_E4_E6_aux_q_one_term :

(PowerSeries.coeff 1) (ModularFormClass.qExpansion 1 Delta_E4_E6_aux) = 1

theorem Delta_E4_eqn :

Delta = Delta_E4_E6_aux

theorem weight_six_one_dimensional :

Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 6) = 1

theorem weight_four_one_dimensional :

Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 4) = 1

theorem weight_eight_one_dimensional (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) (hk3 : k < 12) :

Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) ↑k) = 1

theorem weight_two_zero (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 2) :

f = 0

theorem dim_modforms_eq_one_add_dim_cuspforms (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) :

Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) ↑k) = 1 + Module.rank ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) ↑k)

theorem dim_weight_two :

Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 2) = 0

theorem floor_lem1 (k a : ℚ) (ha : 0 < a) (hak : a ≤ k) :

1 + ⌊(k - a) / a⌋₊ = ⌊k / a⌋₊

theorem dim_modforms_lvl_one (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) :

Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) ↑k) = ↑(if 12 ∣ ↑k - 2 then ⌊↑k / 12⌋₊ else ⌊↑k / 12⌋₊ + 1)

theorem ModularForm.dimension_level_one (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) :

Module.rank ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) ↑k) = ↑(if 12 ∣ ↑k - 2 then ⌊↑k / 12⌋₊ else ⌊↑k / 12⌋₊ + 1)

theorem dim_gen_cong_levels (k : ℤ) (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (hΓ : Γ.index ≠ 0) :

FiniteDimensional ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)