Conclusion

Sharp radial and unrestricted sphere-packing conclusions.

theorem PackingBounds.PackingBridge.sphere_packing_sharp_asymptotic_upper : ∃ (e : ℕ → ℝ), (e =o[Filter.atTop] fun (x : ℕ) => 1) ∧ ∀ (d : ℕ), 0 < d → SpherePackingConstant d ≤ ENNReal.ofReal ((√(Real.exp 1 / (2 * Real.pi)) + e d) ^ d)

structure PackingBounds.FullAdmissible (d : ℕ) : Type

An unrestricted Cohn--Elkies auxiliary function in dimension d.

• function : CohnElkies.TestFunction d

  The Schwartz auxiliary function.

• real (x : CohnElkies.Euclidean d) : (self.function x).im = 0

  The auxiliary function is real-valued.

• fourier_real (x : CohnElkies.Euclidean d) : ((FourierTransform.fourier self.function) x).im = 0

  Its Fourier transform is real-valued.

• fourier_nonneg (x : CohnElkies.Euclidean d) : 0 ≤ ((FourierTransform.fourier self.function) x).re

  Its Fourier transform is nonnegative.

• fourier_zero_pos : 0 < ((FourierTransform.fourier self.function) 0).re

  Its Fourier transform is positive at the origin.

• outside_nonpos (x : CohnElkies.Euclidean d) : 1 ≤ ‖x‖ → (self.function x).re ≤ 0

  The auxiliary function is nonpositive outside the unit ball.

noncomputable def PackingBounds.fullQuotient {d : ℕ} (f : FullAdmissible d) : ℝ

The Cohn--Elkies quotient of an unrestricted admissible function.

Equations

• PackingBounds.fullQuotient f = (f.function 0).re / ((FourierTransform.fourier f.function) 0).re

noncomputable def PackingBounds.fullLinearProgram (d : ℕ) : ℝ

The unrestricted Cohn--Elkies linear program in dimension d.

Equations

• PackingBounds.fullLinearProgram d = CohnElkies.unitBallVolume d / 2 ^ d * sInf (PackingBounds.fullQuotientSet✝ d)

theorem PackingBounds.FullMain.exact_limit : Filter.Tendsto (fun (d : ℕ) => fullLinearProgram d ^ (↑d)⁻¹) Filter.atTop (nhds √(Real.exp 1 / (2 * Real.pi)))

theorem PackingBounds.FullMain.exact_binary_exponent : Filter.Tendsto (fun (d : ℕ) => Real.logb 2 (fullLinearProgram d) / ↑d) Filter.atTop (nhds (-(1 / 2) * Real.logb 2 (2 * Real.pi / Real.exp 1)))

structure PackingBounds.SharpFullCohnElkiesManuscriptConclusions : Prop

The complete sharp asymptotic conclusions for the unrestricted program.

• root_before_infimum : Filter.Tendsto (fun (d : ℕ) => sInf {q : ℝ | ∃ (f : FullAdmissible d), fullQuotient f ^ (↑d)⁻¹ = q} / √↑d) Filter.atTop (nhds (1 / Real.pi))

  The normalized infimum of pointwise quotient roots tends to 1 / π.

• root_before_infimum_vanishing_error : ∃ (err : ℕ → ℝ), Filter.Tendsto err Filter.atTop (nhds 0) ∧ ∀ (d : ℕ), 0 < d → sInf {q : ℝ | ∃ (f : FullAdmissible d), fullQuotient f ^ (↑d)⁻¹ = q} = (1 / Real.pi + err d) * √↑d

  The quotient-root infimum has a vanishing additive error.

• linear_program_root : Filter.Tendsto (fun (d : ℕ) => fullLinearProgram d ^ (↑d)⁻¹) Filter.atTop (nhds √(Real.exp 1 / (2 * Real.pi)))

  The linear-program root has the sharp Cohn--Elkies limit.

• natural_logarithmic_rate : Filter.Tendsto (fun (d : ℕ) => Real.log (fullLinearProgram d) / ↑d) Filter.atTop (nhds (1 / 2 * Real.log (Real.exp 1 / (2 * Real.pi))))

  The natural-logarithmic rate has its sharp limit.

• natural_vanishing_exponential_error : ∃ (err : ℕ → ℝ), Filter.Tendsto err Filter.atTop (nhds 0) ∧ ∀ᶠ (d : ℕ) in Filter.atTop, fullLinearProgram d = (√(Real.exp 1 / (2 * Real.pi)) + err d) ^ d

  The linear program admits a vanishing root-error expansion.

• universal_nonnegative_delta : ∃ (δ : ℕ → ℝ), Filter.Tendsto δ Filter.atTop (nhds 0) ∧ (∀ (d : ℕ), 0 ≤ δ d) ∧ ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (f : FullAdmissible d), 2 ^ d / CohnElkies.unitBallVolume d * (√(Real.exp 1 / (2 * Real.pi)) - δ d) ^ d ≤ fullQuotient f

  Every admissible function obeys a universal vanishing-error lower bound.

• base_two_exponent_positive : 0 < 1 / 2 * Real.logb 2 (2 * Real.pi / Real.exp 1)

  The sharp base-two exponent is positive.

• base_two_decimal_certificate : 1 / 2 * Real.logb 2 (2 * Real.pi / Real.exp 1) ∈ Set.Ioo 0.604400544291677695341677307053 0.604400544291677695341677307054

  A certified narrow decimal interval contains the base-two exponent.

• base_two_logarithmic_rate : Filter.Tendsto (fun (d : ℕ) => Real.logb 2 (fullLinearProgram d) / ↑d) Filter.atTop (nhds (-(1 / 2 * Real.logb 2 (2 * Real.pi / Real.exp 1))))

  The base-two logarithmic rate has its sharp limit.

• base_two_vanishing_exponential_error : ∃ (err : ℕ → ℝ), Filter.Tendsto err Filter.atTop (nhds 0) ∧ ∀ᶠ (d : ℕ) in Filter.atTop, fullLinearProgram d = 2 ^ (-(1 / 2 * Real.logb 2 (2 * Real.pi / Real.exp 1) + err d) * ↑d)

  The linear program admits a vanishing base-two exponent error.

theorem PackingBounds.sharpFullCohnElkiesManuscriptConclusions : SharpFullCohnElkiesManuscriptConclusions