Sphere Packing in R^8

5. Fourier Analysis🔗

Definition5.1
Group: Fourier transform and Schwartz-space preliminaries. (3)
Hover another entry in this group to preview it.
Preview
Lemma 5.2
Blueprint label
  • «lemma:Gaussian-Fourier»
Group
  • Fourier transform and Schwartz-space preliminaries.
AL∃∀Nused by 0

Define the Fourier transform on Euclidean space with the normalization used by the Cohn-Elkies bound.

Code for Definition5.1●1 definition, incomplete
  • axiom 
    Real.fourierIntegral : PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

Direct analytic definition.

Lemma5.2
Group: Fourier transform and Schwartz-space preliminaries. (3)
Hover another entry in this group to preview it.
Preview
Definition 5.1
Blueprint label
  • «def:Fourier-Transform»
Group
  • Fourier transform and Schwartz-space preliminaries.
XL∃∀Nused by 0

The Fourier transform of a Gaussian is an explicit Gaussian.

Proof

Classical calculation.

Definition5.3
Group: Fourier transform and Schwartz-space preliminaries. (3)
Hover another entry in this group to preview it.
Preview
Definition 5.1
Blueprint label
  • «def:Fourier-Transform»
Group
  • Fourier transform and Schwartz-space preliminaries.
AL∃∀Nused by 0

Define Schwartz functions as smooth functions with rapid decay of all derivatives.

Code for Definition5.3●1 definition, incomplete
  • axiom 
    SchwartzMap : PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

Direct functional-analytic definition.

Lemma5.4
Group: Fourier transform and Schwartz-space preliminaries. (3)
Hover another entry in this group to preview it.
Preview
Definition 5.1
Blueprint label
  • «def:Fourier-Transform»
Group
  • Fourier transform and Schwartz-space preliminaries.
AL∃∀Nused by 0

Fourier transform is an automorphism of Schwartz space.

Code for Lemma5.4●1 definition, incomplete
  • axiom 
    SchwartzMap.fourierTransformCLM : PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

Standard Schwartz-space Fourier theory.

Lemma5.5
Group: Summability lemmas and Poisson summation over lattices. (3)
Hover another entry in this group to preview it.
Preview
Lemma 5.6
Blueprint label
  • «lemma:Schwartz-summable»
Group
  • Summability lemmas and Poisson summation over lattices.
XL∃∀Nused by 1

Inverse power tails are summable in the range needed for lattice summation arguments.

Proof

By comparison with convergent p-series.

Lemma5.6
Group: Summability lemmas and Poisson summation over lattices. (3)
Hover another entry in this group to preview it.
Preview
Lemma 5.5
Blueprint label
  • «lemma:inv-power-summable»
Group
  • Summability lemmas and Poisson summation over lattices.
XL∃∀Nused by 0

Summing Schwartz functions over lattices is absolutely convergent.

Proof

Use rapid decay together with Lemma 5.5.

Theorem5.7
Group: Summability lemmas and Poisson summation over lattices. (3)
Hover another entry in this group to preview it.
Preview
Lemma 5.5
Blueprint label
  • «lemma:inv-power-summable»
Group
  • Summability lemmas and Poisson summation over lattices.
AL∃∀Nused by 1

Poisson summation holds for Schwartz functions on lattices.

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

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

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

Apply the Schwartz summability lemmas and Fourier inversion machinery.

Theorem5.8
Group: Summability lemmas and Poisson summation over lattices. (3)
Hover another entry in this group to preview it.
Preview
Lemma 5.5
Blueprint label
  • «lemma:inv-power-summable»
Group
  • Summability lemmas and Poisson summation over lattices.
XL∃∀N
Used by 2
Hover a use site to preview it.
Preview
Lemma 8.11
Blueprint label
  • «prop:a-schwartz»
Uses target in
  • proof

Smooth functions with sufficiently fast derivative decay belong to Schwartz space.

Proof

Direct from the defining seminorm bounds.