Local

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

theorem FockSPR.LocalFockSPR_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)