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

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

Equations

• E₄ = E 4 E₄._proof_1

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

Equations

• E₆ = E 6 E₆._proof_1

theorem E₄_periodic (z : UpperHalfPlane) : E₄ (1 +ᵥ z) = E₄ 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₄_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)

noncomputable def φ₀ (z : UpperHalfPlane) : ℂ

Equations

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

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

Equations

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

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

Equations

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

noncomputable 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 φ₀''_coe_upperHalfPlane (z : UpperHalfPlane) : φ₀'' ↑z = φ₀ z

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

theorem E4_q_exp_zero : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑E₄) = 1

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

theorem E6_q_exp_zero : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑E₆) = 1

theorem E4E6_coeff_zero_eq_zero : (PowerSeries.coeff 0) (UpperHalfPlane.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

noncomputable 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_ne_zero : Delta ≠ 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 neg_two_pi_I_pow_even_real (k : ℕ) (hk : Even k) : ((-2 * ↑Real.pi * Complex.I) ^ k).im = 0

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