noncomputable 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))

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 qExpansion_coe_smul {n : ℕ} [NeZero n] {k : ℤ} (a : ℂ) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma n)) k) : ModularFormClass.qExpansion ↑n ⇑(a • f) = ModularFormClass.qExpansion (↑n) (a • ⇑f)

theorem qExpansion_coe_smul_cusp {n : ℕ} [NeZero n] {k : ℤ} (a : ℂ) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma n)) k) : ModularFormClass.qExpansion ↑n ⇑(a • f) = ModularFormClass.qExpansion (↑n) (a • ⇑f)

theorem qExpansion_coe_sub {k : ℤ} (f g : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) : ModularFormClass.qExpansion ↑1 ⇑(f - g) = ModularFormClass.qExpansion (↑1) (⇑f - ⇑g)

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)

noncomputable 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) ⋯

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

noncomputable 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.

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)