SpherePacking.ModularForms.FG

F = 9 * (D E₄)² by Ramanujan's formula. From ramanujan_E₄: D E₄ = (1/3) * (E₂ * E₄ - E₆) Hence: E₂ * E₄ - E₆ = 3 * D E₄, so F = (E₂ * E₄ - E₆)² = 9 * (D E₄)².

source

theorem G_eq :

G = H₂ ^ 3 * (2 • H₂ ^ 2 + 5 • H₂ * H₄ + 5 • H₄ ^ 2)

source

theorem F_holo :

MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) F

source

theorem G_holo :

MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) G

source

theorem SerreF_holo :

MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) (serre_D 10 F)

source

theorem SerreG_holo :

MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) (serre_D 10 G)

source

theorem FReal_Differentiable {t : ℝ} (ht : 0 < t) :

DifferentiableAt ℝ FReal t

source

theorem GReal_Differentiable {t : ℝ} (ht : 0 < t) :

DifferentiableAt ℝ GReal t

source

theorem F_aux :

D F = 5 * 6⁻¹ * E₂ ^ 3 * E₄.toFun ^ 2 - 5 * 2⁻¹ * E₂ ^ 2 * E₄.toFun * E₆.toFun + 5 * 6⁻¹ * E₂ * E₄.toFun ^ 3 + 5 * 3⁻¹ * E₂ * E₆.toFun ^ 2 - 5 * 6⁻¹ * E₄.toFun ^ 2 * E₆.toFun

source

theorem MLDE_F :

serre_D 12 (serre_D 10 F) = 5 * 6⁻¹ * E₄.toFun * F + 7200 * Δ_fun * negDE₂

Modular linear differential equation satisfied by $F$.

source

theorem MLDE_G :

serre_D 12 (serre_D 10 G) = 5 * 6⁻¹ * E₄.toFun * G - 640 * Δ_fun * H₂

Modular linear differential equation satisfied by $G$.

source

theorem Δ_fun_imag_axis_pos :

ResToImagAxis.Pos Δ_fun

source

theorem qexp_arg_imag_axis_pnat (t : ℝ) (ht : 0 < t) (n : ℕ+) :

2 * ↑Real.pi * Complex.I * ↑↑n * ↑{ coe := Complex.I * ↑t, coe_im_pos := ⋯ } = ↑(-(2 * Real.pi * ↑↑n * t))

The q-expansion exponent argument on imaginary axis z=it with ℕ+ index. Simplifies 2πi * n * z where z=it to -2πnt.

source

theorem sigma_qexp_summable_generic (a b : ℕ) (z : UpperHalfPlane) :

Summable fun (n : ℕ+) => ↑↑n ^ a * ↑((ArithmeticFunction.sigma b) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)

Generic summability for n^a * σ_b(n) * exp(2πinz) series. Uses σ_b(n) ≤ n^(b+1) (sigma_bound) and a33 (a+b+1) for exponential summability.

source

theorem E₂_sigma_qexp (z : UpperHalfPlane) :

E₂ z = 1 - 24 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)

E₂ q-expansion in sigma form: E₂ = 1 - 24 * ∑ σ₁(n) * q^n. This follows from G2_q_exp and the definition E₂ = (1/(2*ζ(2))) • G₂. The proof expands the definitions and simplifies using ζ(2) = π²/6.

source

theorem sigma1_qexp_summable (z : UpperHalfPlane) :

Summable fun (n : ℕ+) => ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)

Summability of σ₁ q-series (for D_qexp_tsum_pnat hypothesis).

source

theorem sigma_qexp_deriv_bound_generic (k : ℕ) (K : Set ℂ) :

K ⊆ {w : ℂ | 0 < w.im} → IsCompact K → ∃ (u : ℕ+ → ℝ), Summable u ∧ ∀ (n : ℕ+) (z : ↑K), ‖↑((ArithmeticFunction.sigma k) ↑n) * (2 * ↑Real.pi * Complex.I * ↑↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)‖ ≤ u n

Generic derivative bound for σ_k q-series on compact sets. Uses σ_k(n) ≤ n^(k+1) (sigma_bound) and iter_deriv_comp_bound3 for exponential decay.

source

theorem sigma1_qexp_deriv_bound (K : Set ℂ) :

K ⊆ {w : ℂ | 0 < w.im} → IsCompact K → ∃ (u : ℕ+ → ℝ), Summable u ∧ ∀ (n : ℕ+) (k : ↑K), ‖↑((ArithmeticFunction.sigma 1) ↑n) * (2 * ↑Real.pi * Complex.I * ↑↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑k)‖ ≤ u n

Derivative bound for σ₁ q-series on compact sets (for D_qexp_tsum_pnat hypothesis). The bound uses σ₁(n) ≤ n² (sigma_bound) and iter_deriv_comp_bound3 for exponential decay.

source

theorem sigma3_qexp_summable (z : UpperHalfPlane) :

Summable fun (n : ℕ+) => ↑((ArithmeticFunction.sigma 3) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)

Summability of σ₃ q-series (for E₄ derivative).

source

theorem sigma3_qexp_deriv_bound (K : Set ℂ) :

K ⊆ {w : ℂ | 0 < w.im} → IsCompact K → ∃ (u : ℕ+ → ℝ), Summable u ∧ ∀ (n : ℕ+) (k : ↑K), ‖↑((ArithmeticFunction.sigma 3) ↑n) * (2 * ↑Real.pi * Complex.I * ↑↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑k)‖ ≤ u n

Derivative bound for σ₃ q-series on compact sets (for D_qexp_tsum_pnat hypothesis). The bound uses σ₃(n) ≤ n⁴ (sigma_bound) and iter_deriv_comp_bound3 for exponential decay.

source

theorem E₄_sigma_qexp (z : UpperHalfPlane) :

E₄ z = 1 + 240 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 3) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)

E₄ as explicit tsum (from E4_q_exp PowerSeries coefficients). Uses hasSum_qExpansion to convert from PowerSeries to tsum form.

source

theorem DE₄_qexp (z : UpperHalfPlane) :

D E₄.toFun z = 240 * ∑' (n : ℕ+), ↑↑n * ↑((ArithmeticFunction.sigma 3) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)

D E₄ q-expansion via termwise differentiation. D E₄ = 240 * ∑ n * σ₃(n) * qⁿ from differentiating E₄ = 1 + 240 * ∑ σ₃(n) * qⁿ.

source

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)

The q-expansion identity E₂E₄ - E₆ = 720·Σn·σ₃(n)·qⁿ. This follows from Ramanujan's formula: E₂E₄ - E₆ = 3·D(E₄), combined with D(E₄) = 240·Σn·σ₃(n)·qⁿ (since D multiplies q-coefficients by n).

source

theorem DE₄_term_re_pos (t : ℝ) (ht : 0 < t) (n : ℕ+) :

0 < (↑↑n * ↑((ArithmeticFunction.sigma 3) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑{ coe := Complex.I * ↑t, coe_im_pos := ⋯ })).re

Each term n*σ₃(n)*exp(-2πnt) in D E₄ q-expansion has positive real part on imaginary axis.

source

theorem DE₄_summable (t : ℝ) (ht : 0 < t) :

Summable fun (n : ℕ+) => ↑↑n * ↑((ArithmeticFunction.sigma 3) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑{ coe := Complex.I * ↑t, coe_im_pos := ⋯ })

D E₄ q-expansion series is summable on imaginary axis.

source

theorem DE₄_imag_axis_real :

ResToImagAxis.Real (D E₄.toFun)

D E₄ is real on the imaginary axis.

source

theorem DE₄_imag_axis_re_pos (t : ℝ) (ht : 0 < t) :

0 < (Function.resToImagAxis (D E₄.toFun) t).re

The real part of (D E₄)(it) is positive for t > 0.

source

theorem DE₄_imag_axis_pos :

ResToImagAxis.Pos (D E₄.toFun)

D E₄ is positive on the imaginary axis. Direct proof via q-expansion: D E₄ = 240 * ∑ n*σ₃(n)qⁿ (DE₄_qexp). On z = it, each term nσ₃(n)*e^(-2πnt) > 0, so the sum is positive.

source

theorem negDE₂_qexp (z : UpperHalfPlane) :

negDE₂ z = 24 * ∑' (n : ℕ+), ↑↑n * ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)

Q-expansion identity: negDE₂ = 24 * ∑ n * σ₁(n) * q^n From Ramanujan's formula: D E₂ = (E₂² - E₄)/12, so -D E₂ = (E₄ - E₂²)/12. And the derivative of E₂ = 1 - 24∑ σ₁(n) q^n gives -D E₂ = 24 ∑ n σ₁(n) q^n. See blueprint equation at line 136 of modform-ineq.tex. Proof outline:

E₂_sigma_qexp: E₂ = 1 - 24 * ∑ σ₁(n) * q^n
D_qexp_tsum_pnat: D(∑ a(n) * q^n) = ∑ n * a(n) * q^n
negDE₂ = -D E₂ = -D(1 - 24∑...) = 24 * ∑ n * σ₁(n) * q^n

source

theorem negDE₂_summable (t : ℝ) (ht : 0 < t) :

Summable fun (n : ℕ+) => ↑↑n * ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑{ coe := Complex.I * ↑t, coe_im_pos := ⋯ })

The q-expansion series for negDE₂ is summable.

source

theorem negDE₂_term_re_pos (t : ℝ) (ht : 0 < t) (n : ℕ+) :

0 < (↑↑n * ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑{ coe := Complex.I * ↑t, coe_im_pos := ⋯ })).re

Each term n*σ₁(n)*exp(-2πnt) in the q-expansion of negDE₂ has positive real part.

source

theorem negDE₂_imag_axis_real :

ResToImagAxis.Real negDE₂

negDE₂ is real on the imaginary axis.

source

theorem negDE₂_imag_axis_re_pos (t : ℝ) (ht : 0 < t) :

0 < (Function.resToImagAxis negDE₂ t).re

The real part of negDE₂(it) is positive for t > 0.

source

theorem negDE₂_imag_axis_pos :

ResToImagAxis.Pos negDE₂

Imaginary Axis Properties #

Properties of G and F when restricted to the positive imaginary axis z = I*t.

source

theorem G_imag_axis_pos :

ResToImagAxis.Pos G

G(it) > 0 for all t > 0. Blueprint: Lemma 8.6 - follows from H₂(it) > 0 and H₄(it) > 0. G = H₂³ (2H₂² + 5H₂H₄ + 5H₄²) is positive since all factors are positive.

source

theorem G_imag_axis_real :

ResToImagAxis.Real G

G(it) is real for all t > 0. Blueprint: G = H₂³ (2H₂² + 5H₂H₄ + 5H₄²), product of real functions.

source

theorem F_imag_axis_pos :

ResToImagAxis.Pos F

F(it) > 0 for all t > 0. Blueprint: F = 9*(D E₄)² and D E₄ > 0 on imaginary axis.

source

theorem F_imag_axis_real :

ResToImagAxis.Real F

F(it) is real for all t > 0. Blueprint: Follows from E₂, E₄, E₆ having real values on the imaginary axis.

source

theorem L₁₀_SerreDer :

L₁₀ = serre_D 10 F * G - F * serre_D 10 G

source

theorem SerreDer_22_L₁₀_SerreDer :

SerreDer_22_L₁₀ = serre_D 12 (serre_D 10 F) * G - F * serre_D 12 (serre_D 10 G)

Serre Derivative Positivity of L₁,₀ #

We compute ∂₂₂ L₁,₀ explicitly via the modular linear differential equations for F and G, and show it is positive on the imaginary axis.

source

theorem SerreDer_22_L₁₀_real :

ResToImagAxis.Real SerreDer_22_L₁₀

source

theorem SerreDer_22_L₁₀_pos :

ResToImagAxis.Pos SerreDer_22_L₁₀

Asymptotic Analysis of F at Infinity #

Vanishing orders and log-derivative limits for the F-side analysis. These are used to establish L₁₀_eventually_pos_imag_axis (large-t positivity of L₁,₀).

source

theorem E₂E₄_sub_E₆_div_q_tendsto :