theorem
f_nonneg_at_zero
{d : ℕ}
{f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ}
(hCohnElkies₂ : ∀ (x : EuclideanSpace ℝ (Fin d)), (Real.fourierIntegral (⇑f) x).re ≥ 0)
:
theorem
f_zero_pos
{d : ℕ}
{f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ}
(hne_zero : f ≠ 0)
(hReal : ∀ (x : EuclideanSpace ℝ (Fin d)), ↑(f x).re = f x)
(hRealFourier : ∀ (x : EuclideanSpace ℝ (Fin d)), ↑(Real.fourierIntegral (⇑f) x).re = Real.fourierIntegral (⇑f) x)
(hCohnElkies₂ : ∀ (x : EuclideanSpace ℝ (Fin d)), (Real.fourierIntegral (⇑f) x).re ≥ 0)
:
theorem
LinearProgrammingBound'
{d : ℕ}
{f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ}
(hne_zero : f ≠ 0)
(hReal : ∀ (x : EuclideanSpace ℝ (Fin d)), ↑(f x).re = f x)
(hRealFourier : ∀ (x : EuclideanSpace ℝ (Fin d)), ↑(Real.fourierIntegral (⇑f) x).re = Real.fourierIntegral (⇑f) x)
(hCohnElkies₁ : ∀ (x : EuclideanSpace ℝ (Fin d)), ‖x‖ ≥ 1 → (f x).re ≤ 0)
(hCohnElkies₂ : ∀ (x : EuclideanSpace ℝ (Fin d)), (Real.fourierIntegral (⇑f) x).re ≥ 0)
{P : PeriodicSpherePacking d}
(hP : P.separation = 1)
[Nonempty ↑P.centers]
{D : Set (EuclideanSpace ℝ (Fin d))}
(hD_isBounded : Bornology.IsBounded D)
(hD_unique_covers : ∀ (x : EuclideanSpace ℝ (Fin d)), ∃! g : ↥P.lattice, g +ᵥ x ∈ D)
(hd : 0 < d)
:
P.density ≤ ↑(f 0).re.toNNReal / ↑(Real.fourierIntegral (⇑f) 0).re.toNNReal * MeasureTheory.volume (Metric.ball 0 (1 / 2))
theorem
LinearProgrammingBound
{d : ℕ}
{f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ}
(hne_zero : f ≠ 0)
(hReal : ∀ (x : EuclideanSpace ℝ (Fin d)), ↑(f x).re = f x)
(hRealFourier : ∀ (x : EuclideanSpace ℝ (Fin d)), ↑(Real.fourierIntegral (⇑f) x).re = Real.fourierIntegral (⇑f) x)
(hCohnElkies₁ : ∀ (x : EuclideanSpace ℝ (Fin d)), ‖x‖ ≥ 1 → (f x).re ≤ 0)
(hCohnElkies₂ : ∀ (x : EuclideanSpace ℝ (Fin d)), (Real.fourierIntegral (⇑f) x).re ≥ 0)
(hd : 0 < d)
:
SpherePackingConstant d ≤ ↑(f 0).re.toNNReal / ↑(Real.fourierIntegral (⇑f) 0).re.toNNReal * MeasureTheory.volume (Metric.ball 0 (1 / 2))