def E₄ : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 4

Equations

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

def E₆ : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (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

theorem cuspfunc_lim_coef {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] (n : ℕ) (c : ℕ → ℂ) (f : F) [inst_1 : ModularFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (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_2} [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_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) [NeZero n] [ModularFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (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_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (c : ℕ → ℂ) (f : F) [ModularFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (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 (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (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 (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)) = 0

def Delta_E4_E6_aux : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (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 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 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 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 (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (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 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)