Estimates for 1728·J and s₂ (Milla, arXiv:1809.00533v6, Chapter 5)

This file states the explicit estimates and q-series approximations of Chapter 5 ("Estimates") of Milla's proof of the Chudnovsky formula (arXiv:1809.00533v6):

• Chudnovsky.Jtilde : the truncation Jtilde of Klein's J-invariant (Theorem theonaeherJ of the paper), Jtilde(τ) = (1 + 240(q + 9q²))³ / (1728·q·(1 - q - q²)²⁴);
• Chudnovsky.s₂tilde : the truncation stilde₂ of Ramanujan's s₂ (Theorem theonaehers2 of the paper), stilde₂(τ) = (1 + 240(q + 9q²))/(1 - 504(q + 33q²)) · (1 - 24(q + 3q²) - 3/(π·Im τ));
• Chudnovsky.E₄trunc, Chudnovsky.E₆trunc, Chudnovsky.E₂starTrunc : the quadratic truncations X, Y, Z of Lemma lemxy of the paper;
• Chudnovsky.eisensteinTail : the Lambert-series tails R_w⁽ˡ⁾ = ∑_{n≥l} σ_{w-1}(n)·qⁿ (Lemma lemrestchaetz), with eisensteinTail k l corresponding to weight w = k + 1;
• Chudnovsky.sigma_le_pow_succ : σₖ(n) ≤ n^(k+1) (Lemma sigmaschaetz);
• Chudnovsky.norm_q_lt_of_mem_Region : |q| < e^(-7.852) for Im τ > 5/4 (Lemma archim-lem, with Mathlib's π > 3.1415 replacing Archimedes);
• Chudnovsky.norm_eisensteinTail_le and the concrete bounds norm_eisensteinTail_sigma₁/₃/₅ (Lemmas lemrestchaetz, lemrestkonkr);
• Chudnovsky.lemE6 : |E₆(τ)| > 0.8 on the region (Lemma lemE6);
• Chudnovsky.theonaeherJ : |1728·J - 1728·Jtilde| < 0.2 together with the bracketing 0.737/|q| < |1728·J| < 1.321/|q| and |J| > 1.096 (Theorem theonaeherJ);
• Chudnovsky.theonaehers2 : |s₂ - stilde₂| < 222000·|q|³ (Theorem theonaehers2).

All estimates hold on Chudnovsky.Region = {τ | Im τ > 5/4}.

Explicit q-truncations

The quadratic truncations X, Y, Z of the Eisenstein series (paper Lemma lemxy), and the resulting approximations Jtilde (paper Thm. theonaeherJ) and stilde₂ (paper Thm. theonaehers2). All are honest rational functions of the nome q τ (plus, for Z, the real quantity 3/(π·Im τ)), so the numerical phase can evaluate them directly.

noncomputable def Chudnovsky.E₄trunc (τ : UpperHalfPlane) : ℂ

The quadratic truncation X := E₄⁽²⁾ = 1 + 240(q + 9q²) of E₄ (paper Lemma lemxy).

Equations

• Chudnovsky.E₄trunc τ = 1 + 240 * (Chudnovsky.q τ + 9 * Chudnovsky.q τ ^ 2)

noncomputable def Chudnovsky.E₆trunc (τ : UpperHalfPlane) : ℂ

The quadratic truncation Y := E₆⁽²⁾ = 1 - 504(q + 33q²) of E₆ (paper Lemma lemxy).

Equations

• Chudnovsky.E₆trunc τ = 1 - 504 * (Chudnovsky.q τ + 33 * Chudnovsky.q τ ^ 2)

noncomputable def Chudnovsky.E₂starTrunc (τ : UpperHalfPlane) : ℂ

The quadratic truncation Z := E₂⁽²⁾ - 3/(π·Im τ) = 1 - 24(q + 3q²) - 3/(π·Im τ) of E₂* (paper Lemma lemxy).

Equations

• Chudnovsky.E₂starTrunc τ = 1 - 24 * (Chudnovsky.q τ + 3 * Chudnovsky.q τ ^ 2) - 3 / (↑Real.pi * ↑τ.im)

noncomputable def Chudnovsky.Jtilde (τ : UpperHalfPlane) : ℂ

The approximation Jtilde of Klein's J-invariant from Theorem theonaeherJ of the paper: Jtilde(τ) = (1 + 240(q + 9q²))³ / (1728·q·(1 - q - q²)²⁴).

The denominator (1 - q - q²)²⁴ is the truncation of ∏ (1-qⁿ)²⁴ = Δ/q coming from Euler's pentagonal number theorem (paper Remark penta).

Equations

• Chudnovsky.Jtilde τ = (1 + 240 * (Chudnovsky.q τ + 9 * Chudnovsky.q τ ^ 2)) ^ 3 / (1728 * Chudnovsky.q τ * (1 - Chudnovsky.q τ - Chudnovsky.q τ ^ 2) ^ 24)

theorem Chudnovsky.Jtilde_eq (τ : UpperHalfPlane) : Jtilde τ = E₄trunc τ ^ 3 / (1728 * q τ * (1 - q τ - q τ ^ 2) ^ 24)

theorem Chudnovsky.mul_Jtilde_eq (τ : UpperHalfPlane) : 1728 * Jtilde τ = (1 + 240 * (q τ + 9 * q τ ^ 2)) ^ 3 / (q τ * (1 - q τ - q τ ^ 2) ^ 24)

1728·Jtilde in the normalized form used in the paper and in the numerical phase.

noncomputable def Chudnovsky.s₂tilde (τ : UpperHalfPlane) : ℂ

The approximation stilde₂ of Ramanujan's s₂ from Theorem theonaehers2 of the paper: stilde₂(τ) = (1 + 240(q + 9q²))/(1 - 504(q + 33q²)) · (1 - 24(q + 3q²) - 3/(π·Im τ)).

Equations

• One or more equations did not get rendered due to their size.

theorem Chudnovsky.s₂tilde_eq (τ : UpperHalfPlane) : s₂tilde τ = E₄trunc τ / E₆trunc τ * E₂starTrunc τ

The σₖ bound (paper Lemma sigmaschaetz)

theorem Chudnovsky.sigma_le_pow_succ (k n : ℕ) : (ArithmeticFunction.sigma k) n ≤ n ^ (k + 1)

Paper Lemma sigmaschaetz: σₖ(n) ≤ n^(k+1). (The paper states this for n ≥ 1; with Mathlib's convention σ k 0 = 0 it holds for all n.)

The Archimedes lemma (paper Lemma archim-lem)

theorem Chudnovsky.norm_q_lt_of_mem_Region {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖q τ‖ < Real.exp (-7.852)

Paper Lemma archim-lem: if Im τ > 5/4 then |q| < e^(-7.852). Archimedes' bound π > 3 + 10/71 is replaced by Mathlib's Real.pi_gt_d4.

q-expansions of the Eisenstein series (paper Prop. sigmaeisen)

We derive the divisor-sum q-expansions of E₄, E₆ and E₂ from Mathlib's EisensteinSeries.q_expansion_bernoulli and EisensteinSeries.E2_eq_tsum_cexp, in a ℕ-indexed form suitable for splitting off the leading terms.

theorem Chudnovsky.summable_sigma_q (k : ℕ) (τ : UpperHalfPlane) : Summable fun (n : ℕ) => ↑((ArithmeticFunction.sigma k) n) * q τ ^ n

Summability of the divisor-sum q-series ∑ σₖ(n)·qⁿ (paper Prop. sigmaeisen).

theorem Chudnovsky.summable_norm_sigma_q (k : ℕ) (τ : UpperHalfPlane) : Summable fun (n : ℕ) => ↑((ArithmeticFunction.sigma k) n) * ‖q τ‖ ^ n

Summability of the (real, absolute) divisor-sum q-series ∑ σₖ(n)·|q|ⁿ.

theorem Chudnovsky.E₄_eq_tsum (τ : UpperHalfPlane) : ModularForm.E₄ τ = 1 + 240 * ∑' (n : ℕ), ↑((ArithmeticFunction.sigma 3) (n + 1)) * q τ ^ (n + 1)

Paper Prop. sigmaeisen: E₄(τ) = 1 + 240·∑_{n≥1} σ₃(n)·qⁿ.

theorem Chudnovsky.E₆_eq_tsum (τ : UpperHalfPlane) : ModularForm.E₆ τ = 1 - 504 * ∑' (n : ℕ), ↑((ArithmeticFunction.sigma 5) (n + 1)) * q τ ^ (n + 1)

Paper Prop. sigmaeisen: E₆(τ) = 1 - 504·∑_{n≥1} σ₅(n)·qⁿ.

theorem Chudnovsky.E2_eq_tsum (τ : UpperHalfPlane) : EisensteinSeries.E2 τ = 1 - 24 * ∑' (n : ℕ), ↑((ArithmeticFunction.sigma 1) (n + 1)) * q τ ^ (n + 1)

Paper Prop. sigmaeisen: E₂(τ) = 1 - 24·∑_{n≥1} σ₁(n)·qⁿ.

theorem Chudnovsky.tsum_sigma_split (k : ℕ) (τ : UpperHalfPlane) : ∑' (n : ℕ), ↑((ArithmeticFunction.sigma k) (n + 1)) * q τ ^ (n + 1) = ↑((ArithmeticFunction.sigma k) 1) * q τ ^ 1 + ↑((ArithmeticFunction.sigma k) 2) * q τ ^ 2 + ∑' (n : ℕ), ↑((ArithmeticFunction.sigma k) (n + 3)) * q τ ^ (n + 3)

Split off the first two terms of the divisor-sum q-series, leaving the tail ∑_{n≥3} σₖ(n)·qⁿ (the paper's R_{k+1}⁽³⁾).

theorem Chudnovsky.exp_neg_bound : Real.exp (-7.852) < 389e-6

Numerical bound e^(-7.852) < 0.000389, replacing the Archimedes step of the paper. Proved from Real.exp_one_gt_d9 and an 8-term Taylor lower bound for exp 0.852.

Geometric tail bounds for the Lambert-type series

(paper Lemmas lemrestchaetz and lemrestkonkr)

noncomputable def Chudnovsky.eisensteinTail (k l : ℕ) (τ : UpperHalfPlane) : ℂ

The tail of the divisor-sum (Lambert-type) q-series of the Eisenstein series of weight k + 1 (paper Lemma lemrestchaetz): eisensteinTail k l τ = ∑_{n ≥ l} σₖ(n)·qⁿ, i.e. the paper's R_w⁽ˡ⁾ with w = k + 1.

Equations

• Chudnovsky.eisensteinTail k l τ = ∑' (n : ℕ), ↑((ArithmeticFunction.sigma k) (n + l)) * Chudnovsky.q τ ^ (n + l)

theorem Chudnovsky.norm_eisensteinTail_le (k l : ℕ) (hl : 0 < l) (τ : UpperHalfPlane) (hs : (1 + 1 / ↑l) ^ (k + 1) * ‖q τ‖ < 1) : ‖eisensteinTail k l τ‖ ≤ ↑l ^ (k + 1) * ‖q τ‖ ^ l / (1 - (1 + 1 / ↑l) ^ (k + 1) * ‖q τ‖)

Paper Lemma lemrestchaetz (with w = k + 1 the Eisenstein weight): if (1 + 1/l)^(k+1)·|q| < 1 then |R_w⁽ˡ⁾| ≤ l^(k+1)·|q|^l / (1 - (1 + 1/l)^(k+1)·|q|).

theorem Chudnovsky.eisensteinTail_succ (k l : ℕ) (τ : UpperHalfPlane) : eisensteinTail k l τ = ↑((ArithmeticFunction.sigma k) l) * q τ ^ l + eisensteinTail k (l + 1) τ

The tail R⁽ˡ⁾ peels off its leading term: R⁽ˡ⁾ = σₖ(l)·qˡ + R⁽ˡ⁺¹⁾.

theorem Chudnovsky.norm_q_pos (τ : UpperHalfPlane) : 0 < ‖q τ‖

|q| > 0 on the region (q τ = e^{2πiτ} ≠ 0).

theorem Chudnovsky.norm_eisensteinTail_sigma₁ {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖eisensteinTail 1 3 τ‖ ≤ 4.007 * ‖q τ‖ ^ 3

Paper Lemma lemrestkonkr, first bound: |R₂⁽³⁾| ≤ 4.007·|q|³ for Im τ > 5/4.

theorem Chudnovsky.norm_eisensteinTail_sigma₃ {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖eisensteinTail 3 3 τ‖ ≤ 28.1 * ‖q τ‖ ^ 3

Paper Lemma lemrestkonkr, second bound: |R₄⁽³⁾| ≤ 28.1·|q|³ for Im τ > 5/4.

theorem Chudnovsky.norm_eisensteinTail_sigma₅ {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖eisensteinTail 5 3 τ‖ ≤ 245.6 * ‖q τ‖ ^ 3

Paper Lemma lemrestkonkr, third bound: |R₆⁽³⁾| ≤ 245.6·|q|³ for Im τ > 5/4.

Truncation errors (paper δX, δY, δZ of Lemma lemxy)

The Eisenstein series equal their quadratic truncations plus 240/-504/-24 times the corresponding tail R⁽³⁾.

theorem Chudnovsky.E₄_eq_trunc (τ : UpperHalfPlane) : ModularForm.E₄ τ = E₄trunc τ + 240 * eisensteinTail 3 3 τ

E₄ = X + δX with δX = 240·R₄⁽³⁾ (paper Lemma lemxy).

theorem Chudnovsky.E₆_eq_trunc (τ : UpperHalfPlane) : ModularForm.E₆ τ = E₆trunc τ - 504 * eisensteinTail 5 3 τ

E₆ = Y + δY with δY = -504·R₆⁽³⁾ (paper Lemma lemxy).

theorem Chudnovsky.E₂star_eq_trunc (τ : UpperHalfPlane) : E₂star τ = E₂starTrunc τ - 24 * eisensteinTail 1 3 τ

E₂* = Z + δZ with δZ = -24·R₂⁽³⁾ (paper Lemma lemxy).

The lower bound for E₆ (paper Lemma lemE6)

theorem Chudnovsky.norm_q_add_smul_sq_le {τ : UpperHalfPlane} {a : ℝ} (ha : 0 ≤ a) : ‖q τ + ↑a * q τ ^ 2‖ ≤ ‖q τ‖ + a * ‖q τ‖ ^ 2

Bound ‖q τ + a·q τ²‖ ≤ |q| + a·|q|² for a ≥ 0.

theorem Chudnovsky.lemE6 {τ : UpperHalfPlane} (hτ : τ ∈ Region) : 0.8 < ‖ModularForm.E₆ τ‖

Paper Lemma lemE6: |E₆(τ)| > 0.8 for Im τ > 5/4.

theorem Chudnovsky.E₆_ne_zero_of_mem_Region {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ModularForm.E₆ τ ≠ 0

Paper Lemma lemE6, "in particular": E₆(τ) ≠ 0 for Im τ > 5/4.

Truncation norm bounds (paper Lemma lemxy)

theorem Chudnovsky.norm_E₆trunc_ge {τ : UpperHalfPlane} (hτ : τ ∈ Region) : 0.8014 ≤ ‖E₆trunc τ‖

Paper Lemma lemxy: 0.8014 ≤ |Y| where Y = E₆⁽²⁾.

theorem Chudnovsky.E₆trunc_ne_zero {τ : UpperHalfPlane} (hτ : τ ∈ Region) : E₆trunc τ ≠ 0

theorem Chudnovsky.norm_E₄trunc_le {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖E₄trunc τ‖ ≤ 1.0937

Paper Lemma lemxy: |X| ≤ 1.0937 where X = E₄⁽²⁾.

theorem Chudnovsky.norm_E₂starTrunc_le {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖E₂starTrunc τ‖ ≤ 1.0094

Paper Lemma lemxy: |Z| ≤ 1.0094 where Z = E₂⁽²⁾ - 3/(π Im τ).

theorem Chudnovsky.norm_s₂tilde_le {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖s₂tilde τ‖ ≤ 1.3776

Paper: |stilde₂| ≤ 1.3776.

theorem Chudnovsky.norm_sub_E₄trunc_le {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖ModularForm.E₄ τ - E₄trunc τ‖ ≤ 6744 * ‖q τ‖ ^ 3

|δX| = |E₄ - X| ≤ 6744·|q|³.

theorem Chudnovsky.norm_sub_E₆trunc_le {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖ModularForm.E₆ τ - E₆trunc τ‖ ≤ 123783 * ‖q τ‖ ^ 3

|δY| = |E₆ - Y| ≤ 123783·|q|³.

theorem Chudnovsky.norm_sub_E₂starTrunc_le {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖E₂star τ - E₂starTrunc τ‖ ≤ 96.2 * ‖q τ‖ ^ 3

|δZ| = |E₂* - Z| ≤ 96.2·|q|³.

Klein's k and its truncation ktilde (paper Lemma lemk)

noncomputable def Chudnovsky.kfun (τ : UpperHalfPlane) : ℂ

The analytic function k(τ) = (E₄³ - E₆²)/(1728·q) = Δ/q (paper Lemma lemk).

Equations

• Chudnovsky.kfun τ = (ModularForm.E₄ τ ^ 3 - ModularForm.E₆ τ ^ 2) / (1728 * Chudnovsky.q τ)

noncomputable def Chudnovsky.ktilde (τ : UpperHalfPlane) : ℂ

The truncation ktilde(τ) = (1 - q - q²)²⁴ (paper Lemma lemk).

Equations

• Chudnovsky.ktilde τ = (1 - Chudnovsky.q τ - Chudnovsky.q τ ^ 2) ^ 24

theorem Chudnovsky.q_ne_zero (τ : UpperHalfPlane) : q τ ≠ 0

theorem Chudnovsky.mul_q_J_eq (τ : UpperHalfPlane) : 1728 * q τ * J τ = ModularForm.E₄ τ ^ 3 / kfun τ

1728·q·J = E₄³ / k.

theorem Chudnovsky.norm_one_sub_q_sub_sq {τ : UpperHalfPlane} : 1 - ‖q τ‖ - ‖q τ‖ ^ 2 ≤ ‖1 - q τ - q τ ^ 2‖ ∧ ‖1 - q τ - q τ ^ 2‖ ≤ 1 + ‖q τ‖ + ‖q τ‖ ^ 2

Bound 1 - |q| - |q|² ≤ ‖1 - q - q²‖ ≤ 1 + |q| + |q|².

theorem Chudnovsky.norm_ktilde_ge {τ : UpperHalfPlane} (hτ : τ ∈ Region) : 0.9907 ≤ ‖ktilde τ‖

Paper Lemma lemk: 0.9907 ≤ |ktilde|.

theorem Chudnovsky.norm_ktilde_le {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖ktilde τ‖ ≤ 1.0094

Paper Lemma lemk: |ktilde| ≤ 1.0094.

theorem Chudnovsky.ktilde_ne_zero {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ktilde τ ≠ 0

theorem Chudnovsky.mul_q_Jtilde_eq {τ : UpperHalfPlane} (hτ : τ ∈ Region) : 1728 * q τ * Jtilde τ = E₄trunc τ ^ 3 / ktilde τ

1728·q·Jtilde = X³ / ktilde.

theorem Chudnovsky.norm_sub_cube_E₄trunc_le {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖ModularForm.E₄ τ ^ 3 - E₄trunc τ ^ 3‖ ≤ 24202 * ‖q τ‖ ^ 3

Paper Lemma lemxy: |E₄³ - X³| ≤ 24202·|q|³ (moved above lemk, which consumes it).

theorem Chudnovsky.norm_E₆trunc_le {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖E₆trunc τ‖ ≤ 1.1987

Paper Lemma lemxy: |Y| ≤ 1.1987 where Y = E₆⁽²⁾.

theorem Chudnovsky.norm_sub_sq_E₆trunc_le {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖ModularForm.E₆ τ ^ 2 - E₆trunc τ ^ 2‖ ≤ 296780 * ‖q τ‖ ^ 3

|E₆² - Y²| ≤ 296780·|q|³ (paper Lemma lemk, the |E₆²-Y²|/(1728q) term).

theorem Chudnovsky.horner_norm_bound (p : ℂ) {ρ : ℝ} (hp : ‖p‖ ≤ ρ) (hρ : 0 ≤ ρ) (l : List ℤ) : ‖List.foldr (fun (a : ℤ) (acc : ℂ) => ↑a + p * acc) 0 l‖ ≤ List.foldr (fun (a : ℤ) (acc : ℝ) => |↑a| + ρ * acc) 0 l

Horner-form norm bound: for ‖p‖ ≤ ρ (0 ≤ ρ), the norm of a polynomial ∑ⱼ cⱼ·pʲ (written in Horner form via List.foldr) is bounded by the same fold with |cⱼ| and ρ. Used to bound the degree-46 polynomial remainder in lemk.

def Chudnovsky.lemkG : List ℤ

Coefficients (ascending) of the degree-46 polynomial G in the exact identity X³ - Y² - 1728·q·(1-q-q²)²⁴ = 1728·q³·G(q), used in lemk.

Equations

• One or more equations did not get rendered due to their size.

theorem Chudnovsky.lemk {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖kfun τ - ktilde τ‖ ≤ 365.6 * ‖q τ‖ ^ 2

Paper Lemma lemk (the one analytic input still admitted): the difference between Klein's k = Δ/q and its truncation ktilde = (1-q-q²)²⁴ is O(|q|²): |k - ktilde| ≤ 365.6·|q|².

Milla proves this by Taylor-expanding (1-q-q²)²⁴ to second order (bounding the third derivative) and comparing with the explicit expansion of (X³-Y²)/(1728q); the sharper |k - ktilde| < 25|q|⁵ needs Euler's pentagonal number theorem. Here we instead use the exact polynomial identity X³ - Y² - 1728·q·(1-q-q²)²⁴ = 1728·q³·G(q) (G of degree 46, with |G(q)| ≤ 179.8 bounded via horner_norm_bound), together with the truncation-error estimates |E₄³-X³| ≤ 24202|q|³ and |E₆²-Y²| ≤ 296780|q|³.

theorem Chudnovsky.norm_kfun_ge {τ : UpperHalfPlane} (hτ : τ ∈ Region) : 0.9907 - 365.6 * ‖q τ‖ ^ 2 ≤ ‖kfun τ‖

0.9907 - 365.6|q|² ≤ |k| (paper: |k| ≥ |ktilde| - |δktilde|).

theorem Chudnovsky.kfun_ne_zero {τ : UpperHalfPlane} (hτ : τ ∈ Region) : kfun τ ≠ 0

theorem Chudnovsky.norm_E₄trunc_ge {τ : UpperHalfPlane} (hτ : τ ∈ Region) : 0.9063 ≤ ‖E₄trunc τ‖

Paper Lemma lemxy: 0.9063 ≤ |X| where X = E₄⁽²⁾.

theorem Chudnovsky.norm_Jtilde2_le {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖E₄trunc τ ^ 3 / ktilde τ‖ ≤ 1.3206

Paper Lemma lem3: |Jtilde₂| ≤ 1.3206 where Jtilde₂ = X³/ktilde.

theorem Chudnovsky.norm_Jtilde2_ge {τ : UpperHalfPlane} (hτ : τ ∈ Region) : 0.7374 ≤ ‖E₄trunc τ ^ 3 / ktilde τ‖

Paper Lemma lem3: 0.7374 ≤ |Jtilde₂| where Jtilde₂ = X³/ktilde.

theorem Chudnovsky.lem3 {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖1728 * q τ * J τ - 1728 * q τ * Jtilde τ‖ ≤ 498 * ‖q τ‖ ^ 2

Paper Lemma lem3: |J₂ - Jtilde₂| ≤ 498·|q|².

Theorem theonaeherJ

theorem Chudnovsky.norm_mul_q_J_le {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖1728 * q τ * J τ‖ ≤ 1.3206 + 498 * ‖q τ‖ ^ 2

|J₂| = |1728·q·J| ≤ 1.3206 + 498|q|² (paper: |J₂| ≤ |Jtilde₂| + |δJtilde₂|).

theorem Chudnovsky.norm_mul_q_J_ge {τ : UpperHalfPlane} (hτ : τ ∈ Region) : 0.7374 - 498 * ‖q τ‖ ^ 2 ≤ ‖1728 * q τ * J τ‖

0.7374 - 498|q|² ≤ |J₂| = |1728·q·J| (paper: |J₂| ≥ |Jtilde₂| - |δJtilde₂|).

theorem Chudnovsky.theonaeherJ_approx {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖1728 * J τ - 1728 * Jtilde τ‖ < 500 * ‖q τ‖

Paper Theorem theonaeherJ, approximation bound in the sharper 500·|q| form: |1728·J(τ) - 1728·Jtilde(τ)| < 500·|q| for Im τ > 5/4.

theorem Chudnovsky.theonaeherJ {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖1728 * J τ - 1728 * Jtilde τ‖ < 0.2

Paper Theorem theonaeherJ, headline approximation bound: |1728·J(τ) - 1728·Jtilde(τ)| < 0.2 for Im τ > 5/4.

theorem Chudnovsky.theonaeherJ_lower {τ : UpperHalfPlane} (hτ : τ ∈ Region) : 0.737 / ‖q τ‖ < ‖1728 * J τ‖

Paper Theorem theonaeherJ, lower bracketing: 0.737/|q| < |1728·J(τ)| for Im τ > 5/4.

theorem Chudnovsky.theonaeherJ_upper {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖1728 * J τ‖ < 1.321 / ‖q τ‖

Paper Theorem theonaeherJ, upper bracketing: |1728·J(τ)| < 1.321/|q| for Im τ > 5/4.

theorem Chudnovsky.theonaeherJ_norm_J {τ : UpperHalfPlane} (hτ : τ ∈ Region) : 1.096 < ‖J τ‖

Paper Theorem theonaeherJ: |J(τ)| > 1.096 for Im τ > 5/4.

theorem Chudnovsky.one_lt_norm_J {τ : UpperHalfPlane} (hτ : τ ∈ Region) : 1 < ‖J τ‖

|J(τ)| > 1 for Im τ > 5/4; in particular J(τ) ≠ 0 and J(τ) ≠ 1 there.

Theorem theonaehers2

theorem Chudnovsky.theonaehers2 {τ : UpperHalfPlane} (hτ : τ ∈ Region) : ‖s₂ τ - s₂tilde τ‖ < 222000 * ‖q τ‖ ^ 3

Paper Theorem theonaehers2: |s₂(τ) - stilde₂(τ)| < 222000·|q|³ for Im τ > 5/4.