The Modular Forms F and G

This file develops the modular forms F and G used in the construction of the magic function, including their q-expansions, vanishing orders, and behaviour on the positive imaginary axis.

noncomputable def F : UpperHalfPlane → ℂ

Equations

• F = (E₂ * E₄.toFun - E₆.toFun) ^ 2

noncomputable def F₁ : UpperHalfPlane → ℂ

F₁ = E₂ * E₄ - E₆, the square root of F.

Equations

• F₁ = E₂ * E₄.toFun - E₆.toFun

noncomputable def G (τ : UpperHalfPlane) : ℂ

Equations

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

noncomputable def negDE₂ : UpperHalfPlane → ℂ

Equations

• negDE₂ = -D E₂

noncomputable def Δ_fun : UpperHalfPlane → ℂ

Equations

• Δ_fun = 1728⁻¹ * (E₄.toFun ^ 3 - E₆.toFun ^ 2)

theorem Δ_fun_eq_Δ : Δ_fun = Δ

The discriminant Δ_fun = 1728⁻¹(E₄³ - E₆²) equals the standard discriminant Δ.

noncomputable def L₁₀ : UpperHalfPlane → ℂ

Equations

• L₁₀ = D F * G - F * D G

theorem L₁₀_eq_FD_G_sub_F_DG (z : UpperHalfPlane) : L₁₀ z = D F z * G z - F z * D G z

noncomputable def SerreDer_22_L₁₀ : UpperHalfPlane → ℂ

Equations

• SerreDer_22_L₁₀ = serre_D 22 L₁₀

noncomputable def FReal (t : ℝ) : ℝ

Equations

• FReal t = (Function.resToImagAxis F t).re

noncomputable def GReal (t : ℝ) : ℝ

Equations

• GReal t = (Function.resToImagAxis G t).re

noncomputable def FmodGReal (t : ℝ) : ℝ

Equations

• FmodGReal t = FReal t / GReal t

theorem F_eq_FReal (t : ℝ) : Function.resToImagAxis F t = ↑(FReal t)

theorem G_eq_GReal (t : ℝ) : Function.resToImagAxis G t = ↑(GReal t)

theorem F_eq_nine_DE₄_sq : F = 9 • D E₄.toFun ^ 2

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

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

theorem F_holo : MDiff F

theorem G_holo : MDiff G

theorem SerreF_holo : MDiff (serre_D 10 F)

theorem SerreG_holo : MDiff (serre_D 10 G)

theorem L₁₀_holo : MDiff L₁₀

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

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

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

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

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

theorem Δ_fun_imag_axis_pos : ResToImagAxis.Pos Δ_fun

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.

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.

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.

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

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.

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.

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

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.

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.

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

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

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.

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.

theorem DE₄_imag_axis_real : ResToImagAxis.Real (D E₄.toFun)

D E₄ is real on the imaginary axis.

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.

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.

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:

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

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.

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.

theorem negDE₂_imag_axis_real : ResToImagAxis.Real negDE₂

negDE₂ is real on the imaginary axis.

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.

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.

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.

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.

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.

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.

theorem F₁_imag_axis_real : ResToImagAxis.Real F₁

theorem FmodG_eq_FmodGReal {t : ℝ} : ↑(FmodGReal t) = Function.resToImagAxis F t / Function.resToImagAxis G t

FmodGReal t = F(it)/G(it) on the imaginary axis. (Placed here, after F/G_imag_axis_real, since the proof needs both realness facts.)

theorem L₁₀_SerreDer : L₁₀ = serre_D 10 F * G - F * serre_D 10 G

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.

theorem SerreDer_22_L₁₀_real : ResToImagAxis.Real SerreDer_22_L₁₀

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₁,₀).

theorem E₂E₄_sub_E₆_div_q_tendsto : Filter.Tendsto (fun (z : UpperHalfPlane) => (E₂ z * E₄ z - E₆ z) / Complex.exp (2 * ↑Real.pi * Complex.I * ↑z)) UpperHalfPlane.atImInfty (nhds 720)

(E₂E₄ - E₆) / q → 720 as im(z) → ∞.

theorem D_cexp_div (c : ℂ) (z : UpperHalfPlane) : D (fun (w : UpperHalfPlane) => Complex.exp (c * ↑w)) z / Complex.exp (c * ↑z) = c / (2 * ↑Real.pi * Complex.I)

D(exp(cz))/exp(cz) = c/(2πi) for any coefficient c.

theorem logderiv_tendsto_of_div_exp_tendsto {F : UpperHalfPlane → ℂ} (hF : MDiff F) {a C : ℂ} (hC : C ≠ 0) (hlim : Filter.Tendsto (fun (z : UpperHalfPlane) => F z / Complex.exp (a * ↑z)) UpperHalfPlane.atImInfty (nhds C)) : Filter.Tendsto (fun (z : UpperHalfPlane) => D F z / F z) UpperHalfPlane.atImInfty (nhds (a / (2 * ↑Real.pi * Complex.I)))

If F z / exp(a·z) → C ≠ 0 at i∞, then D F / F → a/(2πi): the exponential contributes a/(2πi) and the bounded limit factor's log-derivative vanishes. Public so downstream files (e.g. #331's Θ₂ analysis) can reuse it.

theorem F_vanishing_order : Filter.Tendsto (fun (z : UpperHalfPlane) => F z / Complex.exp (2 * ↑Real.pi * Complex.I * 2 * ↑z)) UpperHalfPlane.atImInfty (nhds (720 ^ 2))

The vanishing order of F at infinity is 2. Blueprint: F = 720² * q² * (1 + O(q)), so F / q² → 720² as im(z) → ∞.

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

D(E₂E₄ - E₆) = 720 * ∑ n²·σ₃(n)·qⁿ. Key for the log-derivative limit: (D F)/F → 2 as z → i∞.

theorem D_F_div_F_tendsto : Filter.Tendsto (fun (z : UpperHalfPlane) => D F z / F z) UpperHalfPlane.atImInfty (nhds 2)

(D F)/F → 2 as im(z) → ∞. The log-derivative limit, following from F having vanishing order 2.

G-Side Asymptotic Analysis

Vanishing order and log-derivative limits for G, leading to eventual positivity of L₁,₀.

theorem G_vanishing_order : Filter.Tendsto (fun (z : UpperHalfPlane) => G z / Complex.exp (2 * ↑Real.pi * Complex.I * (3 / 2) * ↑z)) UpperHalfPlane.atImInfty (nhds 20480)

G / q^(3/2) → 20480 as im(z) → ∞. Here q^(3/2) = exp(2πi · (3/2) · z).

theorem D_G_div_G_tendsto : Filter.Tendsto (fun (z : UpperHalfPlane) => D G z / G z) UpperHalfPlane.atImInfty (nhds (3 / 2))

(D G)/G → 3/2 as im(z) → ∞.

theorem L₁₀_imag_axis_real : ResToImagAxis.Real L₁₀

L₁,₀(it) is real for all t > 0.

theorem L₁₀_div_FG_tendsto : Filter.Tendsto (fun (t : ℝ) => (Function.resToImagAxis L₁₀ t).re / ((Function.resToImagAxis F t).re * (Function.resToImagAxis G t).re)) Filter.atTop (nhds (1 / 2))

lim_{t→∞} L₁,₀(it)/(F(it)G(it)) = 1/2.

theorem L₁₀_eventually_pos_imag_axis : ResToImagAxis.EventuallyPos L₁₀

theorem L₁₀_pos : ResToImagAxis.Pos L₁₀

Monotonicity of F/G on the Imaginary Axis

Proposition 8.12 from the blueprint: the function FmodGReal(t) = F(it)/G(it) is strictly decreasing on (0, ∞).

theorem FmodGReal_differentiableOn : DifferentiableOn ℝ FmodGReal (Set.Ioi 0)

FmodGReal is differentiable on (0, ∞).

theorem deriv_FmodGReal (t : ℝ) (ht : 0 < t) : deriv FmodGReal t = -2 * Real.pi * (L₁₀ { coe := Complex.I * ↑t, coe_im_pos := ⋯ }).re / (G { coe := Complex.I * ↑t, coe_im_pos := ⋯ }).re ^ 2

The derivative of FmodGReal is (-2π) * L₁,₀(it) / G(it)².

theorem deriv_FmodGReal_neg (t : ℝ) (ht : 0 < t) : deriv FmodGReal t < 0

deriv FmodGReal t < 0 for all t > 0.

theorem FmodG_strictAntiOn : StrictAntiOn FmodGReal (Set.Ioi 0)

Proposition 8.12: FmodGReal is strictly decreasing on (0, ∞).

theorem I_mul_npow (w : ℂ) (n : ℕ) : (Complex.I * w) ^ n = Complex.I ^ (n % 4) * w ^ n

Reduce a power of I * w via I ^ 4 = 1.

theorem F_functional_equation (z : UpperHalfPlane) : F (ModularGroup.S • z) = ↑z ^ 12 * F z - 12 * Complex.I * ↑Real.pi ^ (-1) * ↑z ^ 11 * (F₁ * E₄.toFun) z - 36 * ↑Real.pi ^ (-2) * ↑z ^ 10 * E₄.toFun z ^ 2

theorem F_functional_equation' {t : ℝ} (ht : 0 < t) : ↑(FReal (1 / t)) = ↑t ^ 12 * ↑(FReal t) - 12 * ↑Real.pi ^ (-1) * ↑t ^ 11 * Function.resToImagAxis (F₁ * E₄.toFun) t + 36 * ↑Real.pi ^ (-2) * ↑t ^ 10 * Function.resToImagAxis E₄.toFun t ^ 2

Functional equation of $F$ restricted to the imaginary axis.

theorem G_functional_equation (z : UpperHalfPlane) : G (ModularGroup.S • z) = -↑z ^ 10 * H₄ z ^ 3 * (2 * H₄ z ^ 2 + 5 * H₂ z * H₄ z + 5 * H₂ z ^ 2)

Functional equation of $G$ under the modular inversion $S$.

theorem G_functional_equation' {t : ℝ} (ht : 0 < t) : ↑(GReal (1 / t)) = ↑t ^ 10 * Function.resToImagAxis H₄ t ^ 3 * (2 * Function.resToImagAxis H₄ t ^ 2 + 5 * Function.resToImagAxis H₂ t * Function.resToImagAxis H₄ t + 5 * Function.resToImagAxis H₂ t ^ 2)

Functional equation of $G$ restricted to the imaginary axis.

Helper lemmas for the limit computation

The following lemmas establish the asymptotic behavior needed for computing the limit of F/G as t → 0⁺.

theorem E₄_resToImagAxis_tendsto_one : Filter.Tendsto (Function.resToImagAxis E₄.toFun) Filter.atTop (nhds 1)

E₄.resToImagAxis tends to 1 at atTop.

theorem H₂_resToImagAxis_tendsto_zero : Filter.Tendsto (Function.resToImagAxis H₂) Filter.atTop (nhds 0)

H₂.resToImagAxis tends to 0 at atTop.

theorem H₄_resToImagAxis_tendsto_one : Filter.Tendsto (Function.resToImagAxis H₄) Filter.atTop (nhds 1)

H₄.resToImagAxis tends to 1 at atTop.

theorem F₁_isBigO_exp_atImInfty : F₁ =O[UpperHalfPlane.atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-(2 * Real.pi) * τ.im)

F₁ has exponential decay at infinity (it's essentially D E₄ which decays).

theorem F_isBigO_exp_atImInfty : F =O[UpperHalfPlane.atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-(4 * Real.pi) * τ.im)

F = F₁² has exponential decay O(exp(-4π im τ)) at infinity.

theorem F₁_mul_E₄_isBigO_exp_atImInfty : (F₁ * E₄.toFun) =O[UpperHalfPlane.atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-(2 * Real.pi) * τ.im)

F₁ * E₄ has exponential decay O(exp(-2π im τ)) at infinity, since F₁ decays and E₄ is bounded.

theorem sq_mul_FReal_tendsto_zero : Filter.Tendsto (fun (s : ℝ) => s ^ 2 * FReal s) Filter.atTop (nhds 0)

s² * FReal s → 0 as s → ∞.

theorem mul_F₁E₄_re_tendsto_zero : Filter.Tendsto (fun (s : ℝ) => s * (Function.resToImagAxis (F₁ * E₄.toFun) s).re) Filter.atTop (nhds 0)

s * Re((F₁ * E₄)(is)) → 0 as s → ∞.

theorem numerator_tendsto_at_infty : Filter.Tendsto (fun (s : ℝ) => s ^ 2 * FReal s - 12 * Real.pi ^ (-1) * (s * (Function.resToImagAxis (F₁ * E₄.toFun) s).re) + 36 * Real.pi ^ (-2) * (Function.resToImagAxis E₄.toFun s).re ^ 2) Filter.atTop (nhds (36 * Real.pi ^ (-2)))

The numerator expression N(s) = s² * FReal s - 12/π * s * (F₁*E₄)(is) + 36/π² * E₄(is)² tends to 36/π² as s → ∞.

theorem denominator_tendsto_at_infty : Filter.Tendsto (fun (s : ℝ) => (Function.resToImagAxis H₄ s).re ^ 3 * (2 * (Function.resToImagAxis H₄ s).re ^ 2 + 5 * (Function.resToImagAxis H₂ s).re * (Function.resToImagAxis H₄ s).re + 5 * (Function.resToImagAxis H₂ s).re ^ 2)) Filter.atTop (nhds 2)

The denominator expression D(s) = H₄(is)³ * (2H₄(is)² + 5H₂(is)H₄(is) + 5H₂(is)²) tends to 2 as s → ∞.

theorem G_functional_eq_real {s : ℝ} (hs : 0 < s) : GReal (1 / s) = s ^ 10 * (Function.resToImagAxis H₄ s).re ^ 3 * (2 * (Function.resToImagAxis H₄ s).re ^ 2 + 5 * (Function.resToImagAxis H₂ s).re * (Function.resToImagAxis H₄ s).re + 5 * (Function.resToImagAxis H₂ s).re ^ 2)

G(1/s) = s^10 * (H₄(is))³ * (2(H₄(is))² + 5H₂(is)H₄(is) + 5(H₂(is))²)

theorem FmodG_rightLimitAt_zero : Filter.Tendsto FmodGReal (nhdsWithin 0 (Set.Ioi 0)) (nhds (18 * Real.pi ^ (-2)))

$\lim_{t \to 0^+} F(it) / G(it) = 18 / \pi^2$.

Proof outline (following blueprint Lemma 8.8):

1. Change of variables: lim_{t→0⁺} F(it)/G(it) = lim_{s→∞} F(i/s)/G(i/s)
2. Apply functional equations:
   • F(i/s) = s^12F(is) - 12s^11/πF₁(is)E₄(is) + 36s^10/π²E₄(is)²
   • G(i/s) = s^10H₄(is)³(2H₄(is)² + 5H₄(is)*H₂(is) + 5H₂(is)²)
3. Divide to get: F(i/s)/G(i/s) = [s²F(is) - 12s/πF₁(is)E₄(is) + 36/π²E₄(is)²] / [H₄(is)³*(2H₄(is)² + 5H₄(is)*H₂(is) + 5H₂(is)²)]
4. As s→∞: F, F₁ are cusp forms (decay to 0), E₄(is)→1, H₂(is)→0, H₄(is)→1
5. Numerator → 36/π², denominator → 2, so limit = 18/π²

Main inequalities between $F$ and $G$ on the imaginary axis

theorem FG_inequality_1 {t : ℝ} (ht : 0 < t) : FReal t + 18 * Real.pi ^ (-2) * GReal t > 0

$F(it) + 18\pi^{-2} G(it) > 0$ for $t > 0$, since $F$ and $G$ are both positive on the imaginary axis.

theorem FG_inequality_2 {t : ℝ} (ht : 0 < t) : FReal t - 18 * Real.pi ^ (-2) * GReal t < 0

$F(it) - 18\pi^{-2} G(it) < 0$ for $t > 0$: the ratio $F/G$ is strictly antitone on the imaginary axis with right limit $18\pi^{-2}$ at $0$, so it stays strictly below $18\pi^{-2}$.