Helper lemmas for dimension-one arguments

theorem exists_smul_eq_of_rank_one {M : Type u_1} [AddCommGroup M] [Module ℂ M] (hrank : Module.rank ℂ M = 1) {e : M} (he : e ≠ 0) (f : M) : ∃ (c : ℂ), f = c • e

In a rank-one module, every element is a scalar multiple of any nonzero element.

theorem exists_smul_eq_of_rank_one' {M : Type u_1} [AddCommGroup M] [Module ℂ M] (hrank : Module.rank ℂ M = 1) {e : M} (he : e ≠ 0) (f : M) : ∃ (c : ℂ), c • e = f

Symmetric version: c • e = f instead of f = c • e.

theorem smul_modularForm_eq_pointwise {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} {f g : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k} {c : ℂ} (h : f = c • g) (z : UpperHalfPlane) : f z = c * g z

Convert smul equality of modular forms to pointwise equality.

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

Equations

• E₄ = (1 / 2) • ModularForm.eisensteinSeriesMF E₄._proof_1 standardcongruencecondition

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

Equations

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

theorem E4_eq : E₄ = E 4 E₄._proof_1

theorem E6_eq : E₆ = E 6 E₆._proof_1

theorem E4_apply (z : UpperHalfPlane) : E₄ z = (E 4 E₄._proof_1) z

theorem E6_apply (z : UpperHalfPlane) : E₆ z = (E 6 E₆._proof_1) z

theorem E₄_periodic (z : UpperHalfPlane) : E₄ (1 +ᵥ z) = E₄ z

E₄ is 1-periodic: E₄(z + 1) = E₄(z). This follows from E₄ being a modular form for Γ(1).

theorem E₆_periodic (z : UpperHalfPlane) : E₆ (1 +ᵥ z) = E₆ z

E₆ is 1-periodic: E₆(z + 1) = E₆(z). This follows from E₆ being a modular form for Γ(1).

theorem E₄_S_transform (z : UpperHalfPlane) : E₄ (ModularGroup.S • z) = ↑z ^ 4 * E₄ z

E₄ transforms under S as: E₄(-1/z) = z⁴ · E₄(z)

theorem E₆_S_transform (z : UpperHalfPlane) : E₆ (ModularGroup.S • z) = ↑z ^ 6 * E₆ z

E₆ transforms under S as: E₆(-1/z) = z⁶ · E₆(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 φ₀ { coe := z, coe_im_pos := hz } else 0

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

Equations

• φ₂'' z = if hz : 0 < z.im then φ₂' { coe := z, coe_im_pos := hz } else 0

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

Equations

• φ₄'' z = if hz : 0 < z.im then φ₄' { coe := z, coe_im_pos := hz } else 0

theorem φ₀''_def {z : ℂ} (hz : 0 < z.im) : φ₀'' z = φ₀ { coe := z, coe_im_pos := hz }

theorem φ₀''_mem_upperHalfPlane {z : ℂ} (hz : z ∈ UpperHalfPlane.upperHalfPlaneSet) : φ₀'' z = φ₀ { coe := z, coe_im_pos := hz }

theorem φ₀''_coe_upperHalfPlane (z : UpperHalfPlane) : φ₀'' ↑z = φ₀ z

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) [hn : 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) [hn : 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 : ℕ) (y : ℂ) => ∏ x ∈ Finset.range n, (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

Imaginary Axis Properties

Properties of Eisenstein series when restricted to the positive imaginary axis z = I*t.

theorem neg_two_pi_I_pow_even_real (k : ℕ) (hk : Even k) : ((-2 * ↑Real.pi * Complex.I) ^ k).im = 0

(-2πi)^k is real for even k.

theorem exp_imag_axis_arg (t : ℝ) (ht : 0 < t) (n : ℕ+) : 2 * ↑Real.pi * Complex.I * ↑{ coe := Complex.I * ↑t, coe_im_pos := ⋯ } * ↑↑n = ↑(-(2 * Real.pi * ↑↑n * t))

On imaginary axis z = I*t, the q-expansion exponent 2πi·n·z reduces to -(2πnt). This is useful for reusing the same algebraic simplification across E₂, E₄, E₆.

theorem E_even_imag_axis_real (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) : ResToImagAxis.Real (E (↑k) hk).toFun

E_k(it) is real for all t > 0 when k is even and k ≥ 4. This is the generalized theorem from which E₄_imag_axis_real and E₆_imag_axis_real follow.

theorem E₄_imag_axis_real : ResToImagAxis.Real E₄.toFun

E₄(it) is real for all t > 0.

theorem E₆_imag_axis_real : ResToImagAxis.Real E₆.toFun

E₆(it) is real for all t > 0.

theorem E₂_imag_axis_real : ResToImagAxis.Real E₂

E₂(it) is real for all t > 0.

Boundedness of E₂

theorem norm_exp_two_pi_I_le_exp_neg_two_pi (z : UpperHalfPlane) (hz : 1 ≤ z.im) : ‖Complex.exp (2 * ↑Real.pi * Complex.I * ↑z)‖ ≤ Real.exp (-2 * Real.pi)

For im(z) ≥ 1, ‖exp(2πiz)‖ ≤ exp(-2π).

This bound on the q-parameter is useful for estimating q-expansions when im(z) ≥ 1.

theorem norm_tsum_logDeriv_expo_le {q : ℂ} (hq : ‖q‖ < 1) : ‖∑' (n : ℕ+), ↑↑n * q ^ ↑n / (1 - q ^ ↑n)‖ ≤ ‖q‖ / (1 - ‖q‖) ^ 3

Bound on the q-series ∑ n·qⁿ/(1-qⁿ) that appears in E₂.

For ‖q‖ < 1, we have ‖∑ₙ₌₁ n·qⁿ/(1-qⁿ)‖ ≤ ‖q‖/(1-‖q‖)³.

The key estimates are:

• |1-qⁿ| ≥ 1-|q|ⁿ ≥ 1-|q| for n ≥ 1
• |n·qⁿ/(1-qⁿ)| ≤ n·|q|ⁿ/(1-|q|)
• ∑ n·rⁿ = r/(1-r)², so ∑ n·rⁿ/(1-r) = r/(1-r)³

theorem norm_tsum_logDeriv_expo_le_of_norm_le {q : ℂ} {r : ℝ} (hqr : ‖q‖ ≤ r) (hr : r < 1) : ‖∑' (n : ℕ+), ↑↑n * q ^ ↑n / (1 - q ^ ↑n)‖ ≤ r / (1 - r) ^ 3

Monotone version of norm_tsum_logDeriv_expo_le: if ‖q‖ ≤ r < 1, then ‖∑ n·qⁿ/(1-qⁿ)‖ ≤ r/(1-r)³. Useful when we have a uniform bound on ‖q‖.

theorem E₂_isBoundedAtImInfty : UpperHalfPlane.IsBoundedAtImInfty E₂

E₂ is bounded at infinity.

Uses E₂_eq: E₂(z) = 1 - 24·Σₙ₌₁ n·qⁿ/(1-qⁿ) where q = exp(2πiz). For im(z) ≥ 1, |q| ≤ exp(-2π), so by norm_tsum_logDeriv_expo_le, |E₂| ≤ 1 + 24·exp(-2π)/(1-exp(-2π))³.

theorem E₄_isBoundedAtImInfty : UpperHalfPlane.IsBoundedAtImInfty E₄.toFun

E₄ is bounded at infinity (as a modular form).

theorem E₂_mul_E₄_isBoundedAtImInfty : UpperHalfPlane.IsBoundedAtImInfty (E₂ * E₄.toFun)

The product E₂ · E₄ is bounded at infinity.