The output bound of the `J` kernel (round six, `jKer_out_bnd`)
ProvedJ6Seg.JK.jKer_out_bndThe output bound of the J kernel (one part).
The following holds (Lean statement, in the scope of module Solutions.J6SegJPre8):
theorem J6Seg.JK.jKer_out_bnd (h : SegReg P R s t lam w α) (hG : (LJ s t lam w).length ≤ G)
(v : List ℤ) (hv : v.length = G) (hvb : Bnd Bv v) :
∀ y ∈ jKer P R s t lam w α K G v, |y| ≤ jWb P w K Bv
Context. J kernel precondition (JPre), part 8: the output bound of the J kernel
jKer_out_bnd: in the regime SegReg, with |LJ| ≤ G, for every row part v of length G
with Bnd Bv v, every entry of jKer P R s t λ w α K G v is bounded by
jWb P w K Bv = 11 (2K+1)(2w+1) 2^{max Bv P} (the window coefficients are ≤ (2w+1)(2^P+1),
the capacitance solution ≤ 4·2^{Bv} + 2^P). jKerG_out_bnd: the same for both parts of a
GI row through liftG.
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_Defs67
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg J6Seg.JK
open Finset
open IntMul NLogN NLogN.KIL NLogN.KFB Function
variable {P R s t lam w α K G Bv : ℕ}
theorem J6Seg.JK.jKer_out_bnd (h : SegReg P R s t lam w α) (hG : (LJ s t lam w).length ≤ G)
(v : List ℤ) (hv : v.length = G) (hvb : Bnd Bv v) :
∀ y ∈ jKer P R s t lam w α K G v, |y| ≤ jWb P w K Bv := by sorry