LaplaceFactorial

Definitions

noncomputable def FockSPR.rStar (n : ℕ) : ℝ

r_n = √(n + 1/2), the saddle point of φ_n.

Equations

• FockSPR.rStar n = √(↑n + 1 / 2)

noncomputable def FockSPR.phiFunc (n : ℕ) (r : ℝ) : ℝ

φ_n(r) = (2n + 1) log(r) − r² for r > 0. Note: r^{2n+1} exp(−r²) = exp(φ_n(r)).

Equations

• FockSPR.phiFunc n r = (2 * ↑n + 1) * Real.log r - r ^ 2

Private lemmas

Theorem 2.7: Concavity of φ_n

φ_n''(r) = −(2n+1)/r² − 2 ≤ −2 for r > 0. In particular, φ_n is strictly concave on (0, ∞).

theorem FockSPR.phiFunc_concavity {n : ℕ} (hn : 1 ≤ n) : StrictConcaveOn ℝ (Set.Ioi 0) (phiFunc n)

Theorem 2.8: Quadratic upper bound

φ_n(r) ≤ φ_n(r_n) − (r − r_n)² for all n ≥ 1, r > 0.

Proof: Define h(r) = φ_n(r) + (r − r_n)². Then h'(r) = (2n+1)/r − 2r_n, which is strictly decreasing and vanishes at r_n. By concavity of h, h(r) ≤ h(r_n) = φ_n(r_n) for all r > 0.

theorem FockSPR.phiFunc_quad_bound {n : ℕ} (hn : 1 ≤ n) {r : ℝ} (hr : 0 < r) : phiFunc n r ≤ phiFunc n (rStar n) - (r - rStar n) ^ 2

Theorem 2.9: Factorial upper bound on exp(φ_n(r_n))

exp(φ_n(r_n)) ≤ exp(1/4) * n! / 2 for all n ≥ 1.

Proof (via Stirling's lower bound): We show φ_n(r_n) ≤ log(n!) − log 2 + 1/4 by combining:

1. φ_n(r_n) = (n+1/2) log(n+1/2) − (n+1/2) ≤ n log n + (1/2) log n − n + 1/4 (using log(1+x) ≤ x and n ≥ 1)
2. Stirling: n log n − n + (1/2) log n + (1/2) log(2π) ≤ log(n!)
3. (1/2) log(2π) ≥ log 2 (since π ≥ 2)

theorem FockSPR.exp_phi_le_factorial {n : ℕ} (hn : 1 ≤ n) : Real.exp (phiFunc n (rStar n)) ≤ Real.exp (1 / 4) * ↑n.factorial / 2

Corollary 2.10: Monomial integral upper bound

For n ≥ 1 and integer j ≥ 0: ∫_j^{j+1} r^{2n+1} exp(−r²) dr ≤ (exp(1/4) * n!/2) * exp(−dist(r_n, [j, j+1])²)

where dist(r_n, [j, j+1]) = max(j − r_n, r_n − (j+1), 0).

Proof: By Theorem 2.8: r^{2n+1} exp(−r²) = exp(φ_n(r)) ≤ exp(φ_n(r_n)) exp(−(r−r_n)²). For r ∈ [j, j+1]: |r − r_n| ≥ dist(r_n, [j,j+1]), so exp(−(r−r_n)²) ≤ exp(−dist(…)²). Integrating over an interval of length 1 and applying Theorem 2.9.

def FockSPR.distToInterval (x : ℝ) (j : ℕ) : ℝ

Distance from a point to a closed interval [j, j+1].

Equations

• FockSPR.distToInterval x j = max (max (↑j - x) (x - (↑j + 1))) 0

theorem FockSPR.monomial_integral_bound {n : ℕ} (hn : 1 ≤ n) (j : ℕ) : ∫ (r : ℝ) in ↑j..↑j + 1, r ^ (2 * n + 1) * Real.exp (-r ^ 2) ≤ Real.exp (1 / 4) * ↑n.factorial / 2 * Real.exp (-distToInterval (rStar n) j ^ 2)