Prerequisites for the Cohn–Elkies Bound

Auxiliary results on Schwartz functions used in the proof of the Cohn–Elkies bound.

instance instNonemptyFin {d : ℕ} [Fact (0 < d)] : Nonempty (Fin d)

def PSF_Conditions {d : ℕ} (f : EuclideanSpace ℝ (Fin d) → ℂ) : Prop

Equations

• PSF_Conditions f = (Summable f ∧ sorry)

theorem PSF_L {d : ℕ} [Fact (0 < d)] (Λ : Submodule ℤ (EuclideanSpace ℝ (Fin d))) [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] {f : EuclideanSpace ℝ (Fin d) → ℂ} (hf : PSF_Conditions f) (v : EuclideanSpace ℝ (Fin d)) : ∑' (ℓ : ↥Λ), f (v + ↑ℓ) = 1 / ↑(ZLattice.covolume Λ MeasureTheory.volume) * ∑' (m : ↥(LinearMap.BilinForm.dualSubmodule (innerₗ (EuclideanSpace ℝ (Fin d))) Λ)), FourierTransform.fourier f ↑m * Complex.exp (2 * ↑Real.pi * Complex.I * ↑⟪v.ofLp, (↑m).ofLp⟫_[ℝ])

theorem PSF_L' {d : ℕ} [Fact (0 < d)] (Λ : Submodule ℤ (EuclideanSpace ℝ (Fin d))) [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] {f : EuclideanSpace ℝ (Fin d) → ℂ} (hf : PSF_Conditions f) : ∑' (ℓ : ↥Λ), f ↑ℓ = 1 / ↑(ZLattice.covolume Λ MeasureTheory.volume) * ∑' (m : ↥(LinearMap.BilinForm.dualSubmodule (innerₗ (EuclideanSpace ℝ (Fin d))) Λ)), FourierTransform.fourier f ↑m

theorem SchwartzMap.PoissonSummation_Lattices {d : ℕ} [Fact (0 < d)] (Λ : Submodule ℤ (EuclideanSpace ℝ (Fin d))) [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] (f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℂ) (v : EuclideanSpace ℝ (Fin d)) : ∑' (ℓ : ↥Λ), f (v + ↑ℓ) = 1 / ↑(ZLattice.covolume Λ MeasureTheory.volume) * ∑' (m : ↥(LinearMap.BilinForm.dualSubmodule (innerₗ (EuclideanSpace ℝ (Fin d))) Λ)), FourierTransform.fourier ⇑f ↑m * Complex.exp (2 * ↑Real.pi * Complex.I * ↑⟪v.ofLp, (↑m).ofLp⟫_[ℝ])

theorem Continuous.pos_iff_exists_nhd_pos {E : Type u_1} [TopologicalSpace E] {f : E → ℝ} (hf₁ : Continuous f) (x : E) : 0 < f x ↔ ∃ U ∈ nhds x, ∀ y ∈ U, 0 < f y

theorem Continuous.pos_iff_exists_measurable_nhd_pos {E : Type u_1} [TopologicalSpace E] [MeasureTheory.MeasureSpace E] [BorelSpace E] {f : E → ℝ} (hf₁ : Continuous f) (x : E) : 0 < f x ↔ ∃ U ∈ nhds x, MeasurableSet U ∧ ∀ y ∈ U, 0 < f y

instance instIsOpenPosMeasureVolume_spherePacking {E : Type u_1} [NormedAddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [MeasureTheory.volume.IsAddLeftInvariant] [MeasureTheory.volume.Regular] [NeZero MeasureTheory.volume] : MeasureTheory.volume.IsOpenPosMeasure

theorem Continuous.integral_zero_iff_zero_of_nonneg {E : Type u_1} [NormedAddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [MeasureTheory.MeasureSpace E] [BorelSpace E] [MeasureTheory.volume.IsAddLeftInvariant] [MeasureTheory.volume.Regular] [NeZero MeasureTheory.volume] {f : E → ℝ} (hf₁ : Continuous f) (hf₂ : MeasureTheory.Integrable f MeasureTheory.volume) (hnn : ∀ (x : E), 0 ≤ f x) : ∫ (v : E), f v = 0 ↔ f = 0

theorem SchwartzMap.toFun_eq_zero_iff_zero {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : SchwartzMap E F) : ⇑f = 0 ↔ f = 0

theorem SchwartzMap.integral_zero_iff_zero_of_nonneg {d : ℕ} {f : SchwartzMap (EuclideanSpace ℝ (Fin d)) ℝ} (hnn : ∀ (x : EuclideanSpace ℝ (Fin d)), 0 ≤ f x) : ∫ (v : EuclideanSpace ℝ (Fin d)), f v = 0 ↔ f = 0

@[instance_reducible]

noncomputable instance instDecidableEqEuclideanSpaceRealFinOfNat_spherePacking {d : ℕ} (v : EuclideanSpace ℝ (Fin d)) : Decidable (v = 0)

Equations

• instDecidableEqEuclideanSpaceRealFinOfNat_spherePacking v = Classical.propDecidable (v = 0)

@[instance_reducible]

noncomputable instance instDecidableEqEuclideanSpaceRealFin_spherePacking {d : ℕ} : DecidableEq (EuclideanSpace ℝ (Fin d))

Equations

• instDecidableEqEuclideanSpaceRealFin_spherePacking = Classical.typeDecidableEq (EuclideanSpace ℝ (Fin d))

theorem Complex.exp_neg_real_I_eq_conj {d : ℕ} (x m : EuclideanSpace ℝ (Fin d)) : exp (-(2 * ↑Real.pi * I * ↑⟪x.ofLp, m.ofLp⟫_[ℝ])) = (starRingEnd ℂ) (exp (2 * ↑Real.pi * I * ↑⟪x.ofLp, m.ofLp⟫_[ℝ]))