Definitions

Convention: align with Mathlib

We adopt Mathlib's conventions throughout:

• Circle: AddCircle (2*π) with normalized Haar measure (probability measure). Fourier monomials fourier n are orthonormal w.r.t. this measure.
• Polar coordinates: Mathlib's polarCoord with angular range (-π, π).
• Complex plane: ℂ ≃ ℝ². Lebesgue measure on ℂ is volume.

noncomputable def FockSPR.T : ℝ

The two-pi period, as a convenient abbreviation.

Equations

• FockSPR.T = 2 * Real.pi

theorem FockSPR.T_pos : 0 < T

instance FockSPR.instFactLtRealOfNatT : Fact (0 < T)

Def 1.1: The function rho

noncomputable def FockSPR.rho (w : ℂ) : ℝ

rho(w) = | ‖1 + w‖ - 1 | where ‖·‖ is the complex modulus.

Equations

• FockSPR.rho w = |‖1 + w‖ - 1|

Def 1.2: Polynomial evaluation

def FockSPR.polyEval {D : ℕ} (a : Fin D → ℂ) (z : ℂ) : ℂ

For a : Fin D → ℂ representing coefficients a₁, …, a_D, the polynomial U(z) = ∑_{n=1}^D aₙ zⁿ with U(0) = 0.

Equations

• FockSPR.polyEval a z = ∑ k : Fin D, a k * z ^ (↑k + 1)

Def 1.3: Polynomial evaluation on a circle (via AddCircle)

noncomputable def FockSPR.polyEvalCircle {D : ℕ} (a : Fin D → ℂ) (r : ℝ) : AddCircle T → ℂ

Restriction of the polynomial to |z| = r, viewed as a function on AddCircle T. polyEvalCircle a r t = ∑_k a(k) * r^{k+1} * fourier(k+1)(t).

Equations

• FockSPR.polyEvalCircle a r t = ∑ k : Fin D, a k * ↑r ^ (↑k + 1) * (fourier ↑(↑k + 1)) t

Def 1.4: Fock norm squared (finite)

noncomputable def FockSPR.fockNormSq {D : ℕ} (a : Fin D → ℂ) : ℝ

‖U‖_F² = ∑_{n=1}^D |aₙ|² n! — the Fock-space norm squared as a finite sum.

Equations

• FockSPR.fockNormSq a = ∑ k : Fin D, ‖a k‖ ^ 2 * ↑(↑k + 1).factorial

Def 1.5: Rho-Fock norm squared (finite)

noncomputable def FockSPR.rhoFockNormSq {D : ℕ} (a : Fin D → ℂ) : ℝ

The RHS of the main inequality: (1/π) ∫_ℂ ρ(U(z))² exp(−|z|²) dm(z).

Equations

• FockSPR.rhoFockNormSq a = 1 / Real.pi * ∫ (z : ℂ), FockSPR.rho (FockSPR.polyEval a z) ^ 2 * Real.exp (-‖z‖ ^ 2)

Def 1.6: Circle L² norm squared

noncomputable def FockSPR.circleNormSq (f : AddCircle T → ℂ) : ℝ

‖f‖²_{L²(S¹)} = ∫ |f(t)|² d(haar) w.r.t. normalized Haar measure on AddCircle T.

Equations

• FockSPR.circleNormSq f = ∫ (t : AddCircle FockSPR.T), ‖f t‖ ^ 2 ∂AddCircle.haarAddCircle

Helper lemmas

Helper: Norm bound and integrability for polar-coordinate integrands

Lemma 1.7: Polar-coordinate decomposition of the Fock norm

theorem FockSPR.polar_coord_fock {D : ℕ} (a : Fin D → ℂ) : rhoFockNormSq a = 2 * ∫ (r : ℝ) in Set.Ioi 0, r * Real.exp (-r ^ 2) * ∫ (t : AddCircle T), rho (polyEvalCircle a r t) ^ 2 ∂AddCircle.haarAddCircle

Lemma 1.8: Fock norm equals Gaussian integral

theorem FockSPR.fockNorm_eq_gaussian_integral {D : ℕ} (a : Fin D → ℂ) : 1 / Real.pi * ∫ (z : ℂ), ‖polyEval a z‖ ^ 2 * Real.exp (-‖z‖ ^ 2) = fockNormSq a