LocalCore

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

theorem FockSPR.LocalFockSPR_of_small_norm (p : Polynomial ℂ) (hp_real : (Polynomial.eval 0 p).im = 0) (hsmall : 1 / Real.pi * ∫ (z : ℂ), ‖Polynomial.eval z p‖ ^ 2 * Real.exp (-‖z‖ ^ 2) ≤ (1 / 4601) ^ 2) : ∫ (z : ℂ), ‖Polynomial.eval z p‖ ^ 2 * Real.exp (-‖z‖ ^ 2) ≤ 23003 ^ 2 * ∫ (z : ℂ), |‖1 + Polynomial.eval z p‖ - 1| ^ 2 * Real.exp (-‖z‖ ^ 2)