Sphere Packing in R^8

8. Fourier Eigenfunctions with Double Zeroes🔗

The strategy in this chapter matches the original blueprint and feeds into the final inequality theorem for the optimal function.

Definition8.1
Group: Auxiliary modular expressions and integral formulas defining <missing> . (6)
Hover another entry in this group to preview it.
Preview
Lemma 8.2
Blueprint label
  • «lemma:phi0-transform»
Group
  • Auxiliary modular expressions and integral formulas defining <missing> .
XL∃∀Nused by 0

Define the functions \phi_{-4}, \phi_{-2}, \phi_0 from E_2,E_4,E_6,\Delta.

Proof

Direct algebraic definitions.

Lemma8.2
Group: Auxiliary modular expressions and integral formulas defining <missing> . (6)
Hover another entry in this group to preview it.
Preview
Definition 8.1
Blueprint label
  • «def:phi4-phi2-phi0»
Group
  • Auxiliary modular expressions and integral formulas defining <missing> .
XL∃∀Nused by 0

Transformation laws for \phi_0 under T and S.

Proof

Expand definitions and use transformation formulas from the modular-forms chapter.

Definition8.3
Group: Auxiliary modular expressions and integral formulas defining <missing> . (6)
Hover another entry in this group to preview it.
Preview
Definition 8.1
Blueprint label
  • «def:phi4-phi2-phi0»
Group
  • Auxiliary modular expressions and integral formulas defining <missing> .
AL∃∀Nused by 0

Define a via six contour integrals built from \phi_0.

Code for Definition8.3●2 definitions, 2 incomplete
  • axiom 
    MagicFunction.a.RealIntegrals.a' : PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

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

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

Direct integral definition.

Lemma8.4
Group: Auxiliary modular expressions and integral formulas defining <missing> . (6)
Hover another entry in this group to preview it.
Preview
Definition 8.1
Blueprint label
  • «def:phi4-phi2-phi0»
Group
  • Auxiliary modular expressions and integral formulas defining <missing> .
AL∃∀Nused by 1

Polynomial Fourier-coefficient growth implies growth bounds for ratios by \Delta.

Code for Lemma8.4●1 definition, incomplete
  • axiom 
    MagicFunction.PolyFourierCoeffBound.DivDiscBoundOfPolyFourierCoeff :
  PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

Use nonvanishing of \Delta and coefficient growth.

Corollary8.5
Group: Auxiliary modular expressions and integral formulas defining <missing> . (6)
Hover another entry in this group to preview it.
Preview
Definition 8.1
Blueprint label
  • «def:phi4-phi2-phi0»
Group
  • Auxiliary modular expressions and integral formulas defining <missing> .
XL∃∀N
Used by 3
Hover a use site to preview it.
Preview
Corollary 8.6
Blueprint label
  • «cor:phi2-bound»
Uses target in
  • proof

Global bound for \phi_0(it) on the positive imaginary axis.

Proof

Combine q-expansions with Lemma 8.4.

Corollary8.6
Group: Auxiliary modular expressions and integral formulas defining <missing> . (6)
Hover another entry in this group to preview it.
Preview
Definition 8.1
Blueprint label
  • «def:phi4-phi2-phi0»
Group
  • Auxiliary modular expressions and integral formulas defining <missing> .
XL∃∀Nused by 1

Global bound for \phi_{-2}(it).

Proof

Same method as Corollary 8.5.

Corollary8.7
Group: Auxiliary modular expressions and integral formulas defining <missing> . (6)
Hover another entry in this group to preview it.
Preview
Definition 8.1
Blueprint label
  • «def:phi4-phi2-phi0»
Group
  • Auxiliary modular expressions and integral formulas defining <missing> .
XL∃∀Nused by 1

Global bound for \phi_{-4}(it).

Proof

Same method as Corollary 8.5.

Lemma8.8
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.9
Blueprint label
  • «lem:bound-I1-I3-I5»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
XL∃∀N
Used by 2
Hover a use site to preview it.
Preview
Lemma 8.9
Blueprint label
  • «lem:bound-I1-I3-I5»
Uses target in
  • proof

General contour-integral estimate used to bound each I_j term.

Proof

Estimate the exponential kernel on vertical and horizontal paths.

Lemma8.9
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.8
Blueprint label
  • «lem:integral-bound»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
XL∃∀Nused by 0

Bounds for I_1, I_3, I_5.

Proof

Apply Lemma 8.8 and the \phi growth bounds.

Lemma8.10
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.8
Blueprint label
  • «lem:integral-bound»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
XL∃∀Nused by 0

Bounds for I_2, I_4, I_6.

Proof

Apply Lemma 8.8 and the \phi growth bounds.

Lemma8.11
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.8
Blueprint label
  • «lem:integral-bound»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
AL∃∀Nused by 0

a is a radial Schwartz function.

Code for Lemma8.11●1 definition, incomplete
  • axiom 
    MagicFunction.FourierEigenfunctions.a : PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

Combine the integral-term bounds with Theorem 5.8.

Lemma8.12
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.8
Blueprint label
  • «lem:integral-bound»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
AL∃∀Nused by 1

a is a Fourier eigenfunction with eigenvalue +1.

Code for Lemma8.12●1 definition, incomplete
  • axiom 
    MagicFunction.a.Fourier.eig_a : PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

Use Gaussian Fourier transforms plus contour manipulations.

Corollary8.13
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.8
Blueprint label
  • «lem:integral-bound»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
XL∃∀Nused by 0

Asymptotic control of \phi_0(it) for t \to 0 and t \to \infty.

Proof

Derive from Corollary 8.5, Corollary 8.6, and Corollary 8.7.

Lemma8.14
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.8
Blueprint label
  • «lem:integral-bound»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
XL∃∀Nused by 1

a has double zeroes at lattice vectors with norm larger than \sqrt{2}.

Proof

Use the alternative integral form and asymptotic cancellation.

Lemma8.15
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.8
Blueprint label
  • «lem:integral-bound»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
AL∃∀Nused by 1

Evaluate a(0) exactly.

Code for Lemma8.15●1 definition, incomplete
  • axiom 
    MagicFunction.a.SpecialValues.a_zero : PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

Extract the constant term from the convergent integral representation.

Definition8.16
Group: Auxiliary forms and integral formulas defining <missing> . (4)
Hover another entry in this group to preview it.
Preview
Definition 8.17
Blueprint label
  • «def:psiI-psiT-psiS»
Group
  • Auxiliary forms and integral formulas defining <missing> .
XL∃∀Nused by 0

Define the intermediate modular expression h used to build \psi_I,\psi_T,\psi_S.

Proof

Direct algebraic definition.

Definition8.17
Group: Auxiliary forms and integral formulas defining <missing> . (4)
Hover another entry in this group to preview it.
Preview
Definition 8.16
Blueprint label
  • «def:h»
Group
  • Auxiliary forms and integral formulas defining <missing> .
XL∃∀Nused by 0

Define \psi_I,\psi_T,\psi_S via slash-operator combinations of h.

Proof

Direct from slash-action formulas.

Lemma8.18
Group: Auxiliary forms and integral formulas defining <missing> . (4)
Hover another entry in this group to preview it.
Preview
Definition 8.16
Blueprint label
  • «def:h»
Group
  • Auxiliary forms and integral formulas defining <missing> .
XL∃∀Nused by 1

Explicit closed forms for \psi_I,\psi_T,\psi_S in terms of H_2,H_3,H_4,\Delta.

Proof

Algebraic elimination using theta identities.

Lemma8.19
Group: Auxiliary forms and integral formulas defining <missing> . (4)
Hover another entry in this group to preview it.
Preview
Definition 8.16
Blueprint label
  • «def:h»
Group
  • Auxiliary forms and integral formulas defining <missing> .
XL∃∀Nused by 0

Leading Fourier terms for \psi_I and \psi_T.

Proof

Expand the explicit formulas from Lemma 8.18.

Definition8.20
Group: Auxiliary forms and integral formulas defining <missing> . (4)
Hover another entry in this group to preview it.
Preview
Definition 8.16
Blueprint label
  • «def:h»
Group
  • Auxiliary forms and integral formulas defining <missing> .
XL∃∀Nused by 0

Define b via six contour integrals built from \psi_I,\psi_T,\psi_S.

Proof

Direct integral definition.

Lemma8.21
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.22
Blueprint label
  • «lemma:bound-J1-J3-J5»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
XL∃∀N
Used by 3
Hover a use site to preview it.
Preview
Lemma 8.22
Blueprint label
  • «lemma:bound-J1-J3-J5»
Uses target in
  • proof

Exponential growth/decay bounds for \psi_I,\psi_T,\psi_S on the relevant contours.

Proof

From q-expansions and transformation formulas.

Lemma8.22
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.21
Blueprint label
  • «lemma:psi-bound»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
XL∃∀Nused by 0

Bounds for J_1,J_3,J_5.

Proof

Apply Lemma 8.21 and contour estimates.

Lemma8.23
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.21
Blueprint label
  • «lemma:psi-bound»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
XL∃∀Nused by 0

Bounds for J_2,J_4,J_6.

Proof

Apply Lemma 8.21 and contour estimates.

Lemma8.24
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.21
Blueprint label
  • «lemma:psi-bound»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
AL∃∀Nused by 0

b is a radial Schwartz function.

Code for Lemma8.24●1 definition, incomplete
  • axiom 
    MagicFunction.FourierEigenfunctions.b : PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

Use the J_j bounds and Theorem 5.8.

Lemma8.25
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.21
Blueprint label
  • «lemma:psi-bound»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
AL∃∀Nused by 1

b is a Fourier eigenfunction with eigenvalue -1.

Code for Lemma8.25●1 definition, incomplete
  • axiom 
    MagicFunction.b.Fourier.eig_b : PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

Contour deformation plus Gaussian transform identities.

Corollary8.26
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.21
Blueprint label
  • «lemma:psi-bound»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
XL∃∀Nused by 1

Asymptotic control of \psi_I(it) near zero and infinity.

Proof

Derive from Lemma 8.21 and transformation formulas.

Lemma8.27
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.21
Blueprint label
  • «lemma:psi-bound»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
XL∃∀Nused by 1

b has double zeroes at lattice vectors with norm larger than \sqrt{2}.

Proof

Use Corollary 8.26 and the alternative integral expression.

Lemma8.28
Group: Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> . (7)
Hover another entry in this group to preview it.
Preview
Lemma 8.21
Blueprint label
  • «lemma:psi-bound»
Group
  • Schwartz, Fourier-eigenfunction, and double-zero properties of <missing> .
AL∃∀Nused by 1

Evaluate b(0) exactly.

Code for Lemma8.28●1 definition, incomplete
  • axiom 
    MagicFunction.b.SpecialValues.b_zero : PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

Read the constant term from the convergent integral form.