Round-six lemma `chirpA_err8`
ProvedJ6A.chirpA_err8An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.
The following holds (Lean statement, in the scope of module Solutions.J6AMath8):
theorem J6A.chirpA_err8 (P σ W s t α H p ex k : ℕ) (he : 8 * ex ≤ p) (hs : 0 < s) (hst : s ≤ t) (hα : 2 ≤ α)
(hαp : α ^ 2 ≤ p) (hH : 1 ≤ H) (hW : H + sWidth p α + 3 ≤ W) (hP : 2 ≤ P) (hσP : σ ≤ 2 * P)
(hσ : Real.exp (Real.pi * (s * (t - s) * H ^ 2 : ℕ) / ((t ^ 2 * α ^ 2 : ℕ) : ℝ)) ≤ 2 ^ σ)
(U : ℕ → ℤ × ℤ) (hU : ∀ i, ‖toC (U i)‖ ≤ 2 ^ p * 2 ^ ex) :
‖toC (chirpA P σ W s t α H U k) - 2 ^ p * Sexact s t α (fun i => toC (U i) / 2 ^ p) k‖
≤ 2 * W * (6 * 2 ^ (2 * P) * (2 ^ p * 2 ^ ex) / 2 ^ (3 * P - σ)) + 2
Context. A lines (PR #5 block chirp), part 2: the error of chirpA
chirpA_err8: chirpA_err (J6AMath2) for inputs in the larger disc ‖U_i‖ ≤ 2^p 2^ex
(8 ex ≤ p): ‖chirpA U k - 2^p S'(U/2^p)_k‖ ≤ 2W · 6 · 2^{2P} · 2^p 2^ex / 2^{3P-σ} + 2.
(window part: per-term weight error weight_err; one final rounding ≤ 3/2; Gaussian tail
outside the window ≤ 1/2 as in Sapprox_bound.)
Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction. import Definitions.Def_IntMul_Kappa_R6_Defs60 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6A open Complex open IntMul.HvdH IntMul.HvdH.SPf
theorem J6A.chirpA_err8 (P σ W s t α H p ex k : ℕ) (he : 8 * ex ≤ p) (hs : 0 < s) (hst : s ≤ t) (hα : 2 ≤ α)
(hαp : α ^ 2 ≤ p) (hH : 1 ≤ H) (hW : H + sWidth p α + 3 ≤ W) (hP : 2 ≤ P) (hσP : σ ≤ 2 * P)
(hσ : Real.exp (Real.pi * (s * (t - s) * H ^ 2 : ℕ) / ((t ^ 2 * α ^ 2 : ℕ) : ℝ)) ≤ 2 ^ σ)
(U : ℕ → ℤ × ℤ) (hU : ∀ i, ‖toC (U i)‖ ≤ 2 ^ p * 2 ^ ex) :
‖toC (chirpA P σ W s t α H U k) - 2 ^ p * Sexact s t α (fun i => toC (U i) / 2 ^ p) k‖
≤ 2 * W * (6 * 2 ^ (2 * P) * (2 ^ p * 2 ^ ex) / 2 ^ (3 * P - σ)) + 2 := by sorry