Sphere Packing in R^8

9. Proof of the Optimal Function Inequalities🔗

This chapter follows the inequality strategy refined in Lee (2024).

Lemma9.1
Group: Auxiliary functions <missing> and reformulation of inequalities. (6)
Hover another entry in this group to preview it.
Preview
Lemma 9.2
Blueprint label
  • «prop:ineqB»
Group
  • Auxiliary functions <missing> and reformulation of inequalities.
XL∃∀Nused by 1

Positivity of the first integral kernel A(t) on (0,\infty).

Proof

Equivalent to the first F \pm cG inequality.

Lemma9.2
Group: Auxiliary functions <missing> and reformulation of inequalities. (6)
Hover another entry in this group to preview it.
Preview
Lemma 9.1
Blueprint label
  • «prop:ineqA»
Group
  • Auxiliary functions <missing> and reformulation of inequalities.
XL∃∀Nused by 1

Positivity of the second integral kernel B(t) on (0,\infty).

Proof

Equivalent to the second F \pm cG inequality.

Definition9.3
Group: Auxiliary functions <missing> and reformulation of inequalities. (6)
Hover another entry in this group to preview it.
Preview
Lemma 9.1
Blueprint label
  • «prop:ineqA»
Group
  • Auxiliary functions <missing> and reformulation of inequalities.
AL∃∀Nused by 0

Define the core expressions F and G from Eisenstein/theta combinations.

Code for Definition9.3●2 definitions, 2 incomplete
  • axiom 
    F : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    F : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    G : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    G : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Direct algebraic definitions.

Lemma9.4
Group: Auxiliary functions <missing> and reformulation of inequalities. (6)
Hover another entry in this group to preview it.
Preview
Lemma 9.1
Blueprint label
  • «prop:ineqA»
Group
  • Auxiliary functions <missing> and reformulation of inequalities.
XL∃∀Nused by 1

Relate \phi_0 and \psi_S to F/\Delta and G/\Delta.

Proof

Substitute definitions and simplify.

Lemma9.5
Group: Auxiliary functions <missing> and reformulation of inequalities. (6)
Hover another entry in this group to preview it.
Preview
Lemma 9.1
Blueprint label
  • «prop:ineqA»
Group
  • Auxiliary functions <missing> and reformulation of inequalities.
XL∃∀Nused by 0

The positivity of A,B is equivalent to positivity of F \pm (18/\pi^2)G on the imaginary axis.

Proof

Combine Lemma 9.4 with discriminant positivity.

Lemma9.6
Group: Auxiliary functions <missing> and reformulation of inequalities. (6)
Hover another entry in this group to preview it.
Preview
Lemma 9.1
Blueprint label
  • «prop:ineqA»
Group
  • Auxiliary functions <missing> and reformulation of inequalities.
AL∃∀Nused by 1

F(it) and G(it) are positive for t > 0.

Code for Lemma9.6●2 definitions, 2 incomplete
  • axiom 
    F_imag_axis_pos : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    F_imag_axis_pos : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    G_imag_axis_pos : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    G_imag_axis_pos : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

From theta/discriminant positivity and Ramanujan identities.

Corollary9.7
Group: Auxiliary functions <missing> and reformulation of inequalities. (6)
Hover another entry in this group to preview it.
Preview
Lemma 9.1
Blueprint label
  • «prop:ineqA»
Group
  • Auxiliary functions <missing> and reformulation of inequalities.
AL∃∀Nused by 0

First strict inequality F + (18/\pi^2)G > 0.

Code for Corollary9.7●1 definition, incomplete
  • axiom 
    FG_inequality_1 : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    FG_inequality_1 : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Use Lemma 9.6 with the reformulation lemma.

Lemma9.8
Group: Differential equations and monotonicity control. (5)
Hover another entry in this group to preview it.
Preview
Corollary 9.9
Blueprint label
  • «cor:MLDE-pos»
Group
  • Differential equations and monotonicity control.
AL∃∀Nused by 1

Differential equations satisfied by F and G under Serre-derivative operators.

Code for Lemma9.8●2 definitions, 2 incomplete
  • axiom 
    MLDE_F : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    MLDE_F : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    MLDE_G : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    MLDE_G : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Apply Theorem 7.24 and Theorem 7.25.

Corollary9.9
Group: Differential equations and monotonicity control. (5)
Hover another entry in this group to preview it.
Preview
Lemma 9.8
Blueprint label
  • «lemma:FG-de»
Group
  • Differential equations and monotonicity control.
XL∃∀Nused by 1

A positivity-compatible differential inequality for the ratio expression used in the monotonicity step.

Proof

Combine Lemma 9.8 with Theorem 7.26.

Lemma9.10
Group: Differential equations and monotonicity control. (5)
Hover another entry in this group to preview it.
Preview
Lemma 9.8
Blueprint label
  • «lemma:FG-de»
Group
  • Differential equations and monotonicity control.
AL∃∀Nused by 1

Compute the right-limit near zero of the normalized quotient Q.

Code for Lemma9.10●1 definition, incomplete
  • axiom 
    FmodG_rightLimitAt_zero : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    FmodG_rightLimitAt_zero : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Use modular transformations and q-expansions.

Lemma9.11
Group: Differential equations and monotonicity control. (5)
Hover another entry in this group to preview it.
Preview
Lemma 9.8
Blueprint label
  • «lemma:FG-de»
Group
  • Differential equations and monotonicity control.
XL∃∀Nused by 1

Asymptotic control of the logarithmic derivative as t \to \infty.

Proof

From q-series derivative estimates.

Lemma9.12
Group: Differential equations and monotonicity control. (5)
Hover another entry in this group to preview it.
Preview
Lemma 9.8
Blueprint label
  • «lemma:FG-de»
Group
  • Differential equations and monotonicity control.
AL∃∀Nused by 1

The quotient function Q is strictly decreasing on (0,\infty).

Code for Lemma9.12●1 definition, incomplete
  • axiom 
    FmodG_strictAntiOn : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    FmodG_strictAntiOn : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Use Corollary 9.9 and boundary behavior from Lemma 9.10 and Lemma 9.11.

Corollary9.13
Group: Differential equations and monotonicity control. (5)
Hover another entry in this group to preview it.
Preview
Lemma 9.8
Blueprint label
  • «lemma:FG-de»
Group
  • Differential equations and monotonicity control.
AL∃∀Nused by 0

Second strict inequality F - (18/\pi^2)G > 0.

Code for Corollary9.13●1 definition, incomplete
  • axiom 
    FG_inequality_2 : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    FG_inequality_2 : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Apply monotonicity from Lemma 9.12.

Theorem9.14
XL∃∀Nused by 1

Construct g as an explicit linear combination of a and b such that:

  • g is radial Schwartz,

  • g has the required sign conditions,

  • g(0) = \widehat{g}(0) = 1.

Proof

Combine Lemma 8.12, Lemma 8.25, Lemma 8.14, Lemma 8.27, Lemma 9.1, Lemma 9.2, Lemma 8.15, and Lemma 8.28.