7.6. Theorem 1.1: the two halves are fused
The report proves Theorem 1.1 by combining the lower bound (28) with the upper bound (86) and
Stirling's formula. The formalization does not expose the limit superior half as a separate
theorem; instead it isolates an abstract sandwich argument on the normalized program
\inf_{f \in \mathcal{A}_d}(f(0)/\widehat f(0))^{1/d}/\sqrt d.
Suppose that (a) for every c < 1/\pi and all sufficiently large d, every
f \in \mathcal{A}_d (Definition 1.1.4) has normalized cost
(f(0)/\widehat f(0))^{1/d}/\sqrt d \ge c, and
(b) there is an ordered \epsilon-construction as in Theorem 5.5.6:
\epsilon_0 > 0, radii with R_{\epsilon,d}/\sqrt d \to \alpha_\epsilon as d \to \infty and
\alpha_\epsilon \to 1/\pi as \epsilon \downarrow 0, and for every 0 < \epsilon < \epsilon_0
and all large d an admissible function of normalized cost at most R_{\epsilon,d}/\sqrt d.
Then
\inf_{f \in \mathcal{A}_d^{\mathrm{rad}}}(f(0)/\widehat f(0))^{1/d}/\sqrt d \to 1/\pi,
and consequently, with Definition 1.1.6, \mathrm{LP}_d^{1/d} \to \sqrt{e/(2\pi)}.
Lean code for Theorem7.6.1●1 theorem
Associated Lean declarations
-
theoremdefined in CohnElkies/Asymptotics/Framework.leancomplete
theorem CohnElkies.sharpQuotient_of_uniform_lower_and_ordered_upper (hlower : CohnElkies.UniformAdmissibleLowerBound) (construction : CohnElkies.OrderedEpsilonUpperConstruction) : CohnElkies.SharpQuotientAsymptotic
theorem CohnElkies.sharpQuotient_of_uniform_lower_and_ordered_upper (hlower : CohnElkies.UniformAdmissibleLowerBound) (construction : CohnElkies.OrderedEpsilonUpperConstruction) : CohnElkies.SharpQuotientAsymptotic
Theorem 1.1 of the report: a uniform lower bound plus an ordered `ε`-construction give the sharp asymptotics of the normalized program.
Write \nu_d for the normalized program. Fix c > 1/\pi. By (b) choose \epsilon with
\alpha_\epsilon < c; for all large d we have R_{\epsilon,d}/\sqrt d < c and an admissible
function of cost at most R_{\epsilon,d}/\sqrt d, so \nu_d \le c
(CohnElkies.ConstructivePrimalUpperBound). Fix c < 1/\pi; by (a), \nu_d \ge c for all large
d. Since the order topology of \mathbb{R} is generated by such rays, \nu_d \to 1/\pi
(CohnElkies.sharpQuotient_of_uniform_lower_and_constructive_upper). Finally
\mathrm{LP}_d^{1/d} = (v_d/2^d)^{1/d}\sqrt d\cdot\nu_d
(CohnElkies.linearProgram_root_eq_geometric_mul_normalizedProgram, using
Lemma 1.1.7), and (v_d/2^d)^{1/d}\sqrt d \to \sqrt{2\pi e}/2 by
Lemma 3.1.8, so
\mathrm{LP}_d^{1/d} \to \sqrt{2\pi e}/(2\pi) = \sqrt{e/(2\pi)}.
The hypothesis (a) is the content of Theorem 4.2.2 before Stirling's formula is applied.