def E₄ : ModularForm (CongruenceSubgroup.Gamma 1) 4

Equations

• E₄ = (1 / 2) • ModularForm.eisensteinSeries_MF E₄._proof_11 standardcongruencecondition

def E₆ : ModularForm (CongruenceSubgroup.Gamma 1) 6

Equations

• E₆ = (1 / 2) • ModularForm.eisensteinSeries_MF E₆._proof_1 standardcongruencecondition

theorem E4_eq : E₄ = E 4 ⋯

theorem E6_eq : E₆ = E 6 ⋯

theorem E4_apply (z : UpperHalfPlane) : E₄ z = (E 4 ⋯) z

theorem E6_apply (z : UpperHalfPlane) : E₆ z = (E 6 ⋯) z

def φ₀ (z : UpperHalfPlane) : ℂ

Equations

• φ₀ z = (E₂ z * E₄ z - E₆ z) ^ 2 / Δ z

def φ₂' (z : UpperHalfPlane) : ℂ

Equations

• φ₂' z = E₄ z * (E₂ z * E₄ z - E₆ z) / Δ z

def φ₄' (z : UpperHalfPlane) : ℂ

Equations

• φ₄' z = E₄ z ^ 2 / Δ z

def φ₀'' (z : ℂ) : ℂ

Equations

• φ₀'' z = if hz : 0 < z.im then φ₀ ⟨z, hz⟩ else 0

def φ₂'' (z : ℂ) : ℂ

Equations

• φ₂'' z = if hz : 0 < z.im then φ₂' ⟨z, hz⟩ else 0

def φ₄'' (z : ℂ) : ℂ

Equations

• φ₄'' z = if hz : 0 < z.im then φ₄' ⟨z, hz⟩ else 0

instance instNeBotUpperHalfPlaneAtImInfty_spherePacking_1 : UpperHalfPlane.atImInfty.NeBot

def mul_Delta_map (k : ℤ) (f : ModularForm (CongruenceSubgroup.Gamma 1) (k - 12)) : ModularForm (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 Γ a) (z : UpperHalfPlane) : (ModularForm.mcast h f) z = f z

theorem mul_Delta_map_eq (k : ℤ) (f : ModularForm (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 (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 (CongruenceSubgroup.Gamma 1) (k - 12)) : IsCuspForm (CongruenceSubgroup.Gamma 1) k (mul_Delta_map k f)

def Modform_mul_Delta' (k : ℤ) (f : ModularForm (CongruenceSubgroup.Gamma 1) (k - 12)) : CuspForm (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 Γ k₁) (g : SlashInvariantForm Γ k₂) (z : UpperHalfPlane) : (f.mul g) z = f z * g z

theorem Modform_mul_Delta_apply (k : ℤ) (f : ModularForm (CongruenceSubgroup.Gamma 1) (k - 12)) (z : UpperHalfPlane) : (Modform_mul_Delta' k f) z = f z * Delta z

def CuspForms_iso_Modforms (k : ℤ) : CuspForm (CongruenceSubgroup.Gamma 1) k ≃ₗ[ℂ] ModularForm (CongruenceSubgroup.Gamma 1) (k - 12)

Equations

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

theorem cuspfunc_lim_coef {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] (n : ℕ) (c : ℕ → ℂ) (f : F) [inst_1 : ModularFormClass F (CongruenceSubgroup.Gamma n) k] [inst_2 : NeZero n] (hf : ∀ (τ : UpperHalfPlane), HasSum (fun (m : ℕ) => c m • Function.Periodic.qParam ↑n ↑τ ^ m) (f τ)) (q : ℂ) (hq : ‖q‖ < 1) (hq1 : q ≠ 0) : HasSum (fun (m : ℕ) => c m • q ^ m) (SlashInvariantFormClass.cuspFunction n f q)

theorem summable_zero_pow {G : Type u_4} [NormedField G] (f : ℕ → G) : Summable fun (m : ℕ) => f m * 0 ^ m

theorem tsum_zero_pow (f : ℕ → ℂ) : ∑' (m : ℕ), f m * 0 ^ m = f 0

theorem cuspfunc_Zero {k : ℤ} {F : Type u_3} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) [NeZero n] [ModularFormClass F (CongruenceSubgroup.Gamma n) k] : SlashInvariantFormClass.cuspFunction n f 0 = (PowerSeries.coeff ℂ 0) (ModularFormClass.qExpansion n f)

theorem modfom_q_exp_cuspfunc {k : ℤ} {F : Type u_3} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (c : ℕ → ℂ) (f : F) [ModularFormClass F (CongruenceSubgroup.Gamma n) k] [NeZero n] (hf : ∀ (τ : UpperHalfPlane), HasSum (fun (m : ℕ) => c m • Function.Periodic.qParam ↑n ↑τ ^ m) (f τ)) (q : ℂ) : ‖q‖ < 1 → HasSum (fun (m : ℕ) => c m • q ^ m) (SlashInvariantFormClass.cuspFunction n f q)

theorem qParam_surj_onto_ball (n : ℕ) (r : ℝ) (hr : 0 < r) (hr2 : r < 1) [NeZero n] : ∃ (z : UpperHalfPlane), ‖Function.Periodic.qParam ↑n ↑z‖ = r

theorem q_exp_unique {k : ℤ} (n : ℕ) (c : ℕ → ℂ) (f : ModularForm (CongruenceSubgroup.Gamma n) k) [NeZero n] (hf : ∀ (τ : UpperHalfPlane), HasSum (fun (m : ℕ) => c m • Function.Periodic.qParam ↑n ↑τ ^ m) (f τ)) : c = fun (m : ℕ) => (PowerSeries.coeff ℂ m) (ModularFormClass.qExpansion n f)

theorem deriv_mul_eq (f g : ℂ → ℂ) (hf : Differentiable ℂ f) (hg : Differentiable ℂ g) : deriv (f * g) = deriv f * g + f * deriv g

theorem auxasdf (n : ℕ) : (PowerSeries.coeff ℂ n) (ModularFormClass.qExpansion 1 E₄ * ModularFormClass.qExpansion 1 E₆) = ∑ p ∈ Finset.antidiagonal n, (PowerSeries.coeff ℂ p.1) (ModularFormClass.qExpansion 1 E₄) * (PowerSeries.coeff ℂ p.2) (ModularFormClass.qExpansion 1 E₆)

theorem sigma_bound (k n : ℕ) : (ArithmeticFunction.sigma k) n ≤ n ^ (k + 1)

def Ek_q (k : ℕ) : ℕ → ℂ

Equations

• Ek_q k m = if m = 0 then 1 else 1 / riemannZeta ↑k * ((-2 * ↑Real.pi * Complex.I) ^ k / ↑(k - 1).factorial) * ↑((ArithmeticFunction.sigma (k - 1)) m)

theorem qexpsummable (k : ℕ) (hk : 3 ≤ ↑k) (z : UpperHalfPlane) : Summable fun (m : ℕ) => Ek_q k m • Function.Periodic.qParam 1 ↑z ^ m

theorem Ek_q_exp_zero (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) : (PowerSeries.coeff ℂ 0) (ModularFormClass.qExpansion 1 (E (↑k) hk)) = 1

theorem Ek_q_exp (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) : (fun (m : ℕ) => (PowerSeries.coeff ℂ m) (ModularFormClass.qExpansion 1 (E (↑k) hk))) = fun (m : ℕ) => if m = 0 then 1 else 1 / riemannZeta ↑k * ((-2 * ↑Real.pi * Complex.I) ^ k / ↑(k - 1).factorial) * ↑((ArithmeticFunction.sigma (k - 1)) m)

theorem E4_q_exp : (fun (m : ℕ) => (PowerSeries.coeff ℂ m) (ModularFormClass.qExpansion 1 E₄)) = fun (m : ℕ) => if m = 0 then 1 else 240 * ↑((ArithmeticFunction.sigma 3) m)

theorem E4_q_exp_zero : (PowerSeries.coeff ℂ 0) (ModularFormClass.qExpansion 1 E₄) = 1

@[simp]

theorem Complex.I_pow_six : I ^ 6 = -1

@[simp]

theorem bernoulli'_five : bernoulli' 5 = 0

@[simp]

theorem bernoulli'_six : bernoulli' 6 = 1 / 42

theorem E6_q_exp : (fun (m : ℕ) => (PowerSeries.coeff ℂ m) (ModularFormClass.qExpansion 1 E₆)) = fun (m : ℕ) => if m = 0 then 1 else -504 * ↑((ArithmeticFunction.sigma 5) m)

theorem E6_q_exp_zero : (PowerSeries.coeff ℂ 0) (ModularFormClass.qExpansion 1 E₆) = 1

theorem E4E6_coeff_zero_eq_zero : (PowerSeries.coeff ℂ 0) (ModularFormClass.qExpansion 1 ((1 / 1728) • ((DirectSum.of (ModularForm (CongruenceSubgroup.Gamma 1)) 4) E₄ ^ 3 - (DirectSum.of (ModularForm (CongruenceSubgroup.Gamma 1)) 6) E₆ ^ 2) 12)) = 0

def Delta_E4_E6_aux : CuspForm (CongruenceSubgroup.Gamma 1) 12

Equations

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

theorem Delta_cuspFuntion_eq : Set.EqOn (SlashInvariantFormClass.cuspFunction 1 Delta) (fun (y : ℂ) => y * ∏' (i : ℕ), (1 - y ^ (i + 1)) ^ 24) (Metric.ball 0 (1 / 2))

theorem Delta_ne_zero : Delta ≠ 0

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

theorem asdf : TendstoLocallyUniformlyOn (fun (n : ℕ) => ∏ x ∈ Finset.range n, fun (y : ℂ) => 1 - y ^ (x + 1)) (fun (x : ℂ) => ∏' (i : ℕ), (1 - x ^ (i + 1))) Filter.atTop (Metric.ball 0 (1 / 2))

theorem diffwithinat_prod_1 : DifferentiableWithinAt ℂ (fun (y : ℂ) => ∏' (i : ℕ), (1 - y ^ (i + 1)) ^ 24) (Metric.ball 0 (1 / 2)) 0

theorem Delta_q_one_term : (PowerSeries.coeff ℂ 1) (ModularFormClass.qExpansion 1 Delta) = 1

theorem sigma_zero (k : ℕ) : (ArithmeticFunction.sigma k) 0 = 0

theorem E4_q_exp_one : (PowerSeries.coeff ℂ 1) (ModularFormClass.qExpansion 1 E₄) = 240

theorem E6_q_exp_one : (PowerSeries.coeff ℂ 1) (ModularFormClass.qExpansion 1 E₆) = -504

theorem antidiagonal_one : Finset.antidiagonal 1 = {(1, 0), (0, 1)}

theorem E4_pow_q_exp_one : (PowerSeries.coeff ℂ 1) (ModularFormClass.qExpansion 1 (E₄.mul (E₄.mul E₄))) = 3 * 240

theorem cuspform_weight_lt_12_zero (k : ℤ) (hk : k < 12) : Module.rank ℂ (CuspForm (CongruenceSubgroup.Gamma 1) k) = 0

theorem IsCuspForm_weight_lt_eq_zero (k : ℤ) (hk : k < 12) (f : ModularForm (CongruenceSubgroup.Gamma 1) k) (hf : IsCuspForm (CongruenceSubgroup.Gamma 1) k f) : f = 0

theorem Ek_ne_zero (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) : E (↑k) hk ≠ 0

theorem E4_ne_zero : E₄ ≠ 0

theorem E6_ne_zero : E₆ ≠ 0

theorem modularForm_normalise {k : ℤ} (f : ModularForm (CongruenceSubgroup.Gamma 1) k) (hf : ¬IsCuspForm (CongruenceSubgroup.Gamma 1) k f) : (PowerSeries.coeff ℂ 0) (ModularFormClass.qExpansion 1 (((PowerSeries.coeff ℂ 0) (ModularFormClass.qExpansion 1 f))⁻¹ • f)) = 1

theorem PowerSeries.coeff_add (f g : PowerSeries ℂ) (n : ℕ) : (coeff ℂ n) (f + g) = (coeff ℂ n) f + (coeff ℂ n) g

theorem Delta_E4_E6_eq : ModForm_mk (CongruenceSubgroup.Gamma 1) 12 Delta_E4_E6_aux = (1 / 1728) • ((DirectSum.of (ModularForm (CongruenceSubgroup.Gamma 1)) 4) E₄ ^ 3 - (DirectSum.of (ModularForm (CongruenceSubgroup.Gamma 1)) 6) E₆ ^ 2) 12

instance instFunLikeForallUpperHalfPlaneComplex_spherePacking_1 : FunLike (UpperHalfPlane → ℂ) UpperHalfPlane ℂ

Equations

• instFunLikeForallUpperHalfPlaneComplex_spherePacking_1 = { coe := fun ⦃a₁ : UpperHalfPlane → ℂ⦄ => a₁, coe_injective' := ⋯ }

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 (CongruenceSubgroup.Gamma 1) 6) = 1

theorem weight_four_one_dimensional : Module.rank ℂ (ModularForm (CongruenceSubgroup.Gamma 1) 4) = 1

theorem weight_eight_one_dimensional (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) (hk3 : k < 12) : Module.rank ℂ (ModularForm (CongruenceSubgroup.Gamma 1) ↑k) = 1

theorem weight_two_zero (f : ModularForm (CongruenceSubgroup.Gamma 1) 2) : f = 0

theorem dim_modforms_eq_one_add_dim_cuspforms (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) : Module.rank ℂ (ModularForm (CongruenceSubgroup.Gamma 1) ↑k) = 1 + Module.rank ℂ (CuspForm (CongruenceSubgroup.Gamma 1) ↑k)

theorem dim_weight_two : Module.rank ℂ (ModularForm (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 (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 (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 Γ k)

theorem E₂_mul_E₄_sub_E₆ (z : UpperHalfPlane) : E₂ z * E₄ z - E₆ z = 720 * ∑' (n : ℕ+), ↑↑n * ↑((ArithmeticFunction.sigma 3) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)