Sphere Packing in R^8

6. Cohn-Elkies Bounds🔗

In 2003 Cohn and Elkies developed linear programming bounds that apply directly to sphere packings; see Cohn and Elkies (2003). The goal of this section is to formalize the Cohn-Elkies linear programming bound.

The following theorem is the key result of Cohn and Elkies (2003). Note that the original theorem is stated for a class of functions more general then Schwartz functions.

Theorem6.1
✓L∃∀Nused by 1

Let X\subset\mathbb{R}^d be a discrete subset such that \|x-y\|\geq 1 for any distinct x,y\in X. Suppose that X is \Lambda-periodic with respect to some lattice \Lambda\subset\mathbb{R}^d. Let f:\R^d\to\R be a Schwartz function that is not identically zero and satisfies f(x)\leq 0 for \|x\|\geq 1 and \widehat{f}(x)\geq0 for all x\in\R^d. Then the density of any \Lambda-periodic sphere packing is bounded above by \frac{f(0)}{\widehat{f}(0)}\cdot \mathrm{vol}(B_d(0,1/2)). This uses Definition 5.1 and Definition 2.4.

Lean code for Theorem6.1●1 theorem
  • theorem LinearProgrammingBound' {dℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  {fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ : SchwartzMapSchwartzMap.{u_5, u_6} (E : Type u_5) (F : Type u_6) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F]
  [NormedSpace ℝ F] : Type (max u_5 u_6)A function is a Schwartz function if it is smooth and all derivatives decay faster than
any power of `‖x‖`.  (EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)) ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. } (hne_zerof ≠ 0 : fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. 0)
  (hReal∀ (x : EuclideanSpace ℝ (Fin d)), ↑(f x).re = f x : ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)), ↑(fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ xEuclideanSpace ℝ (Fin d))
  (hRealFourier∀ (x : EuclideanSpace ℝ (Fin d)), ↑((FourierTransform.fourier f) x).re = (FourierTransform.fourier f) x :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)),
      ↑((FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
        (FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) xEuclideanSpace ℝ (Fin d))
  (hCohnElkies₁∀ (x : EuclideanSpace ℝ (Fin d)), ‖x‖ ≥ 1 → (f x).re ≤ 0 :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)), ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. xEuclideanSpace ℝ (Fin d)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≥GE.ge.{u} {α : Type u} [LE α] (a b : α) : Prop`a ≥ b` is an abbreviation for `b ≤ a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `≥` in identifiers is `ge`.

 * The recommended spelling of `>=` in identifiers is `ge` (prefer `≥` over `>=`). 1 → (fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`). 0)
  (hCohnElkies₂∀ (x : EuclideanSpace ℝ (Fin d)), ((FourierTransform.fourier f) x).re ≥ 0 :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)),
      ((FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  ≥GE.ge.{u} {α : Type u} [LE α] (a b : α) : Prop`a ≥ b` is an abbreviation for `b ≤ a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `≥` in identifiers is `ge`.

 * The recommended spelling of `>=` in identifiers is `ge` (prefer `≥` over `>=`). 0)
  {PPeriodicSpherePacking d : PeriodicSpherePackingPeriodicSpherePacking (d : ℕ) : Type dℕ} (hPP.separation = 1 : PPeriodicSpherePacking d.separationSpherePacking.separation {d : ℕ} (self : SpherePacking d) : ℝ =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1)
  [NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
 ↑PPeriodicSpherePacking d.centersSpherePacking.centers {d : ℕ} (self : SpherePacking d) : Set (EuclideanSpace ℝ (Fin d))] {DSet (EuclideanSpace ℝ (Fin d)) : SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.
 (EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ))}
  (hD_isBoundedBornology.IsBounded D : Bornology.IsBoundedBornology.IsBounded.{u_2} {α : Type u_2} [Bornology α] (s : Set α) : Prop`IsBounded` is the predicate that `s` is bounded relative to the ambient bornology on `α`.  DSet (EuclideanSpace ℝ (Fin d)))
  (hD_unique_covers∀ (x : EuclideanSpace ℝ (Fin d)), ∃! g, g +ᵥ x ∈ D :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)), ∃!ExistsUnique.{u_1} {α : Sort u_1} (p : α → Prop) : PropFor `p : α → Prop`, `ExistsUnique p` means that there exists a unique `x : α` with `p x`.  g↥P.lattice,ExistsUnique.{u_1} {α : Sort u_1} (p : α → Prop) : PropFor `p : α → Prop`, `ExistsUnique p` means that there exists a unique `x : α` with `p x`.  g↥P.lattice +ᵥHVAdd.hVAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HVAdd α β γ] : α → β → γ`a +ᵥ b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+ᵥ` in identifiers is `vadd`. xEuclideanSpace ℝ (Fin d) ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. DSet (EuclideanSpace ℝ (Fin d)))
  (hd0 < d : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. dℕ) (hfSummable ⇑f : SummableSummable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α)
  (L : SummationFilter β := SummationFilter.unconditional β) : Prop`Summable f` means that `f` has some (infinite) sum with respect to `L`. Use `tsum` to get the
value.  ⇑fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) :
  PPeriodicSpherePacking d.densitySpherePacking.density {d : ℕ} (S : SpherePacking d) : ENNReal ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).
    ↑(fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ 0).reComplex.re (self : ℂ) : ℝThe real part of a complex number. .toNNRealReal.toNNReal (r : ℝ) : NNRealReinterpret a real number `r` as a non-negative real number. Returns `0` if `r < 0`.  /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`. ↑((FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) 0).reComplex.re (self : ℂ) : ℝThe real part of a complex number. .toNNRealReal.toNNReal (r : ℝ) : NNRealReinterpret a real number `r` as a non-negative real number. Returns `0` if `r < 0`.  *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`.  (Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 (1 / 2))
    theorem LinearProgrammingBound' {dℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  {fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ :
    SchwartzMapSchwartzMap.{u_5, u_6} (E : Type u_5) (F : Type u_6) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F]
  [NormedSpace ℝ F] : Type (max u_5 u_6)A function is a Schwartz function if it is smooth and all derivatives decay faster than
any power of `‖x‖`.  (EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ))
      ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. }
  (hne_zerof ≠ 0 : fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. 0)
  (hReal∀ (x : EuclideanSpace ℝ (Fin d)), ↑(f x).re = f x :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)),
      ↑(fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ xEuclideanSpace ℝ (Fin d))
  (hRealFourier∀ (x : EuclideanSpace ℝ (Fin d)), ↑((FourierTransform.fourier f) x).re = (FourierTransform.fourier f) x :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)),
      ↑((FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ)
              xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
        (FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) xEuclideanSpace ℝ (Fin d))
  (hCohnElkies₁∀ (x : EuclideanSpace ℝ (Fin d)), ‖x‖ ≥ 1 → (f x).re ≤ 0 :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)),
      ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. xEuclideanSpace ℝ (Fin d)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≥GE.ge.{u} {α : Type u} [LE α] (a b : α) : Prop`a ≥ b` is an abbreviation for `b ≤ a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `≥` in identifiers is `ge`.

 * The recommended spelling of `>=` in identifiers is `ge` (prefer `≥` over `>=`). 1 → (fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`). 0)
  (hCohnElkies₂∀ (x : EuclideanSpace ℝ (Fin d)), ((FourierTransform.fourier f) x).re ≥ 0 :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)),
      ((FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ)
            xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  ≥GE.ge.{u} {α : Type u} [LE α] (a b : α) : Prop`a ≥ b` is an abbreviation for `b ≤ a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `≥` in identifiers is `ge`.

 * The recommended spelling of `>=` in identifiers is `ge` (prefer `≥` over `>=`).
        0)
  {PPeriodicSpherePacking d : PeriodicSpherePackingPeriodicSpherePacking (d : ℕ) : Type dℕ}
  (hPP.separation = 1 : PPeriodicSpherePacking d.separationSpherePacking.separation {d : ℕ} (self : SpherePacking d) : ℝ =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. 1)
  [NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
 ↑PPeriodicSpherePacking d.centersSpherePacking.centers {d : ℕ} (self : SpherePacking d) : Set (EuclideanSpace ℝ (Fin d))]
  {DSet (EuclideanSpace ℝ (Fin d)) : SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`.

Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be
relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets
and predicates.
 (EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ))}
  (hD_isBoundedBornology.IsBounded D : Bornology.IsBoundedBornology.IsBounded.{u_2} {α : Type u_2} [Bornology α] (s : Set α) : Prop`IsBounded` is the predicate that `s` is bounded relative to the ambient bornology on `α`.  DSet (EuclideanSpace ℝ (Fin d)))
  (hD_unique_covers∀ (x : EuclideanSpace ℝ (Fin d)), ∃! g, g +ᵥ x ∈ D :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)),
      ∃!ExistsUnique.{u_1} {α : Sort u_1} (p : α → Prop) : PropFor `p : α → Prop`, `ExistsUnique p` means that there exists a unique `x : α` with `p x`.  g↥P.lattice,ExistsUnique.{u_1} {α : Sort u_1} (p : α → Prop) : PropFor `p : α → Prop`, `ExistsUnique p` means that there exists a unique `x : α` with `p x`.  g↥P.lattice +ᵥHVAdd.hVAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HVAdd α β γ] : α → β → γ`a +ᵥ b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+ᵥ` in identifiers is `vadd`. xEuclideanSpace ℝ (Fin d) ∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∈` in identifiers is `mem`. DSet (EuclideanSpace ℝ (Fin d)))
  (hd0 < d : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. dℕ) (hfSummable ⇑f : SummableSummable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α)
  (L : SummationFilter β := SummationFilter.unconditional β) : Prop`Summable f` means that `f` has some (infinite) sum with respect to `L`. Use `tsum` to get the
value.  ⇑fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) :
  PPeriodicSpherePacking d.densitySpherePacking.density {d : ℕ} (S : SpherePacking d) : ENNReal ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).
    ↑(fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ 0).reComplex.re (self : ℂ) : ℝThe real part of a complex number. .toNNRealReal.toNNReal (r : ℝ) : NNRealReinterpret a real number `r` as a non-negative real number. Returns `0` if `r < 0`.  /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`.
        ↑((FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ)
                0).reComplex.re (self : ℂ) : ℝThe real part of a complex number. .toNNRealReal.toNNReal (r : ℝ) : NNRealReinterpret a real number `r` as a non-negative real number. Returns `0` if `r < 0`.  *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. 
        (Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 (1 / 2))
    complete
Proof

Here we reproduce the proof given in Cohn and Elkies (2003). Uses Theorem 5.7. The inequality \sharp (X/\Lambda)\cdot f(0)\geq \sum_{x\in X}\sum_{y\in X/\Lambda}f(x-y)=\sum_{x\in X/\Lambda}\sum_{y\in X/\Lambda}\sum_{\ell\in \Lambda}f(x-y+l) follows from the first Cohn-Elkies condition of the theorem and the assumption on the distances between points in X. /- -/ The equality \sum_{x\in X/\Lambda}\sum_{y\in X/\Lambda}\sum_{\ell\in \Lambda}f(x-y+l)=\sum_{x\in X/\Lambda}\sum_{y\in X/\Lambda}\frac{1}{\mathrm{vol}(\mathbb{R}^d/\Lambda)}\,\sum_{m\in \Lambda^*} \widehat{f}(m)\,e^{2\pi i m(x-y)} follows from the Poisson summation formula. /- -/ The right-hand side of the above equation can be written as \sum_{x\in X/\Lambda}\sum_{y\in X/\Lambda}\frac{1}{\mathrm{vol}(\mathbb{R}^d/\Lambda)}\,\sum_{m\in \Lambda^*} \widehat{f}(m)\,e^{2\pi i m(x-y)}=\frac{1}{\mathrm{vol}(\mathbb{R}^d/\Lambda)}\,\sum_{m\in \Lambda^*} \widehat{f}(m)\cdot\big|\sum_{x\in X/\Lambda}e^{2\pi i m x}\big|^2. Note that \big|\sum_{x\in X/\Lambda}e^{2\pi i m x}\big|^2\geq0 for all m\in\Lambda^*. Moreover, the term corresponding to m=0 satisfies \big|\sum_{x\in X/\Lambda}e^{2\pi i 0 x}\big|^2=\sharp (X/\Lambda)^2. /- -/ Now we use the second Cohn-Elkies condition and estimate \frac{1}{\mathrm{vol}(\mathbb{R}^d/\Lambda)}\,\sum_{m\in \Lambda^*} \widehat{f}(m)\cdot\big|\sum_{x\in X/\Lambda}e^{2\pi i m(x-y)}\big|^2 \geq \frac{\sharp (X/\Lambda)^2}{\mathrm{vol}(\mathbb{R}^d/\Lambda)}\cdot \widehat{f}(0). Comparing inequalities, we arrive at \frac{\sharp (X/\Lambda)}{\mathrm{vol}(\mathbb{R}^d/\Lambda)}\leq \frac{f(0)}{\widehat{f}(0)}. Now we see that the density of the periodic packing \mathcal{P}_X with balls of radius 1/2 is bounded by \Delta(\mathcal{P}_X)=\frac{\sharp (X/\Lambda)}{\mathrm{vol}(\mathbb{R}^d/\Lambda)}\cdot{\mathrm{vol}(B_d(0,1/2))}\leq \frac{f(0)}{\widehat{f}(0)}\cdot \mathrm{vol}(B_d(0,1/2)). This finishes the proof of the theorem for periodic packings.

Theorem6.2
✓L∃∀Nused by 1

Let f:\R^d\to\R be a Schwartz function that is not identically zero and satisfies Cohn-Elkies condition 1 and Cohn-Elkies condition 2 above. Then the density of any \Lambda-periodic sphere packing is bounded above by \frac{f(0)}{\widehat{f}(0)}\cdot \mathrm{vol}(B_d(0,1/2)).

Lean code for Theorem6.2●1 theorem
  • theorem LinearProgrammingBound {dℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  {fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ : SchwartzMapSchwartzMap.{u_5, u_6} (E : Type u_5) (F : Type u_6) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F]
  [NormedSpace ℝ F] : Type (max u_5 u_6)A function is a Schwartz function if it is smooth and all derivatives decay faster than
any power of `‖x‖`.  (EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)) ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. } (hne_zerof ≠ 0 : fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. 0)
  (hReal∀ (x : EuclideanSpace ℝ (Fin d)), ↑(f x).re = f x : ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)), ↑(fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ xEuclideanSpace ℝ (Fin d))
  (hRealFourier∀ (x : EuclideanSpace ℝ (Fin d)), ↑((FourierTransform.fourier f) x).re = (FourierTransform.fourier f) x :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)),
      ↑((FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
        (FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) xEuclideanSpace ℝ (Fin d))
  (hCohnElkies₁∀ (x : EuclideanSpace ℝ (Fin d)), ‖x‖ ≥ 1 → (f x).re ≤ 0 :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)), ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. xEuclideanSpace ℝ (Fin d)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≥GE.ge.{u} {α : Type u} [LE α] (a b : α) : Prop`a ≥ b` is an abbreviation for `b ≤ a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `≥` in identifiers is `ge`.

 * The recommended spelling of `>=` in identifiers is `ge` (prefer `≥` over `>=`). 1 → (fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`). 0)
  (hCohnElkies₂∀ (x : EuclideanSpace ℝ (Fin d)), ((FourierTransform.fourier f) x).re ≥ 0 :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)),
      ((FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  ≥GE.ge.{u} {α : Type u} [LE α] (a b : α) : Prop`a ≥ b` is an abbreviation for `b ≤ a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `≥` in identifiers is `ge`.

 * The recommended spelling of `>=` in identifiers is `ge` (prefer `≥` over `>=`). 0)
  (hd0 < d : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. dℕ) (hfSummable ⇑f : SummableSummable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α)
  (L : SummationFilter β := SummationFilter.unconditional β) : Prop`Summable f` means that `f` has some (infinite) sum with respect to `L`. Use `tsum` to get the
value.  ⇑fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) :
  SpherePackingConstantSpherePackingConstant (d : ℕ) : ENNRealThe `SpherePackingConstant` in dimension d is the supremum of the density of all packings. See
also `<TODO>` for specifying the separation radius of the packings.  dℕ ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).
    ↑(fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ 0).reComplex.re (self : ℂ) : ℝThe real part of a complex number. .toNNRealReal.toNNReal (r : ℝ) : NNRealReinterpret a real number `r` as a non-negative real number. Returns `0` if `r < 0`.  /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`.
        ↑(FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  (⇑fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) 0).reComplex.re (self : ℂ) : ℝThe real part of a complex number. .toNNRealReal.toNNReal (r : ℝ) : NNRealReinterpret a real number `r` as a non-negative real number. Returns `0` if `r < 0`.  *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`.  (Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 (1 / 2))
    theorem LinearProgrammingBound {dℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
}
  {fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ :
    SchwartzMapSchwartzMap.{u_5, u_6} (E : Type u_5) (F : Type u_6) [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F]
  [NormedSpace ℝ F] : Type (max u_5 u_6)A function is a Schwartz function if it is smooth and all derivatives decay faster than
any power of `‖x‖`.  (EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ))
      ℂComplex : TypeComplex numbers consist of two `Real`s: a real part `re` and an imaginary part `im`. }
  (hne_zerof ≠ 0 : fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. 0)
  (hReal∀ (x : EuclideanSpace ℝ (Fin d)), ↑(f x).re = f x :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)),
      ↑(fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ xEuclideanSpace ℝ (Fin d))
  (hRealFourier∀ (x : EuclideanSpace ℝ (Fin d)), ↑((FourierTransform.fourier f) x).re = (FourierTransform.fourier f) x :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)),
      ↑((FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ)
              xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`.
        (FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) xEuclideanSpace ℝ (Fin d))
  (hCohnElkies₁∀ (x : EuclideanSpace ℝ (Fin d)), ‖x‖ ≥ 1 → (f x).re ≤ 0 :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)),
      ‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function. xEuclideanSpace ℝ (Fin d)‖Norm.norm.{u_8} {E : Type u_8} [self : Norm E] : E → ℝthe `ℝ`-valued norm function.  ≥GE.ge.{u} {α : Type u} [LE α] (a b : α) : Prop`a ≥ b` is an abbreviation for `b ≤ a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `≥` in identifiers is `ge`.

 * The recommended spelling of `>=` in identifiers is `ge` (prefer `≥` over `>=`). 1 → (fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`). 0)
  (hCohnElkies₂∀ (x : EuclideanSpace ℝ (Fin d)), ((FourierTransform.fourier f) x).re ≥ 0 :
    ∀ (xEuclideanSpace ℝ (Fin d) : EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
space use `EuclideanSpace 𝕜 (Fin n)`.

For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type,
analogous to `![x, y, ...]` notation.  ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.  (FinFin (n : ℕ) : TypeNatural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 dℕ)),
      ((FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ)
            xEuclideanSpace ℝ (Fin d)).reComplex.re (self : ℂ) : ℝThe real part of a complex number.  ≥GE.ge.{u} {α : Type u} [LE α] (a b : α) : Prop`a ≥ b` is an abbreviation for `b ≤ a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `≥` in identifiers is `ge`.

 * The recommended spelling of `>=` in identifiers is `ge` (prefer `≥` over `>=`).
        0)
  (hd0 < d : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. dℕ) (hfSummable ⇑f : SummableSummable.{u_1, u_2} {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α)
  (L : SummationFilter β := SummationFilter.unconditional β) : Prop`Summable f` means that `f` has some (infinite) sum with respect to `L`. Use `tsum` to get the
value.  ⇑fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) :
  SpherePackingConstantSpherePackingConstant (d : ℕ) : ENNRealThe `SpherePackingConstant` in dimension d is the supremum of the density of all packings. See
also `<TODO>` for specifying the separation radius of the packings.  dℕ ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

 * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).
    ↑(fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ 0).reComplex.re (self : ℂ) : ℝThe real part of a complex number. .toNNRealReal.toNNReal (r : ℝ) : NNRealReinterpret a real number `r` as a non-negative real number. Returns `0` if `r < 0`.  /HDiv.hDiv.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HDiv α β γ] : α → β → γ`a / b` computes the result of dividing `a` by `b`.
The meaning of this notation is type-dependent.
* For most types like `Nat`, `Int`, `Rat`, `Real`, `a / 0` is defined to be `0`.
* For `Nat`, `a / b` rounds downwards.
* For `Int`, `a / b` rounds downwards if `b` is positive or upwards if `b` is negative.
  It is implemented as `Int.ediv`, the unique function satisfying
  `a % b + b * (a / b) = a` and `0 ≤ a % b < natAbs b` for `b ≠ 0`.
  Other rounding conventions are available using the functions
  `Int.fdiv` (floor rounding) and `Int.tdiv` (truncation rounding).
* For `Float`, `a / 0` follows the IEEE 754 semantics for division,
  usually resulting in `inf` or `nan`. 

Conventions for notations in identifiers:

 * The recommended spelling of `/` in identifiers is `div`.
        ↑(FourierTransform.fourierFourierTransform.fourier.{u, v} {E : Type u} {F : outParam (Type v)} [self : FourierTransform E F] : E → F`𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  (⇑fSchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ)
                0).reComplex.re (self : ℂ) : ℝThe real part of a complex number. .toNNRealReal.toNNReal (r : ℝ) : NNRealReinterpret a real number `r` as a non-negative real number. Returns `0` if `r < 0`.  *HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `*` in identifiers is `mul`.
      MeasureTheory.volumeMeasureTheory.MeasureSpace.volume.{u_6} {α : Type u_6} [self : MeasureTheory.MeasureSpace α] : MeasureTheory.Measure α`volume` is the canonical measure on `α`. 
        (Metric.ballMetric.ball.{u} {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α`ball x ε` is the set of all points `y` with `dist y x < ε`  0 (1 / 2))
    complete
Proof

The result follows immediately from Theorem Theorem 2.14 and the Cohn-Elkies periodic theorem Theorem 6.1.

The main step in our proof of the main theorem is the explicit construction of an optimal function. It will be convenient for us to scale this function by \sqrt{2}.

Theorem6.3
XL∃∀Nused by 1

There exists a radial Schwartz function g:\R^8\to\R which satisfies: g(x)\leq 0\text{ for } \|x\|\geq \sqrt{2} \widehat{g}(x)\geq0\text{ for all } x\in\R^8 g(0)=\widehat{g}(0)=1. This uses Theorem 9.14.