LocalHelpers

noncomputable def FockSPR.phaseDistanceSq (p : Polynomial ℂ) (lam : ℂ) : ℝ

Gaussian L² distance from 1 + p to the unit phase lam.

Equations

• FockSPR.phaseDistanceSq p lam = ∫ (z : ℂ), ‖1 + Polynomial.eval z p - lam‖ ^ 2 * Real.exp (-‖z‖ ^ 2)

noncomputable def FockSPR.phaseDistanceSqNorm (p : Polynomial ℂ) (lam : ℂ) : ℝ

Normalized Gaussian L² distance from 1 + p to the unit phase lam.

Equations

• FockSPR.phaseDistanceSqNorm p lam = 1 / Real.pi * FockSPR.phaseDistanceSq p lam

theorem FockSPR.LocalFockSPR_of_small_norm_exists_phase (p : Polynomial ℂ) (hsmall : 1 / Real.pi * ∫ (z : ℂ), ‖Polynomial.eval z p‖ ^ 2 * Real.exp (-‖z‖ ^ 2) ≤ (1 / 4601) ^ 2) : ∃ (w : ℂ), ‖w‖ = 1 ∧ ∫ (z : ℂ), ‖w * (1 + Polynomial.eval z p) - 1‖ ^ 2 * Real.exp (-‖z‖ ^ 2) ≤ 23003 ^ 2 * ∫ (z : ℂ), |‖1 + Polynomial.eval z p‖ - 1| ^ 2 * Real.exp (-‖z‖ ^ 2)