Construction of the smoothing kernel with its explicit regularity and curvature guarantees.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairMpd_pos {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : 0 < repairMpd p d

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairMpd_universal_bound {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : repairMpd p d ≤ 15 * Real.exp (2 / 3) * min p (Real.log ↑d)

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairKernel_assumptions {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : SmoothingKernelAssumptions (repairKernel p d)

Every frozen clause except no clause: the concrete repaired data now satisfies the full SmoothingKernelAssumptions carrier.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repairKernel_raw_hessian_bound {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) (x e : Point d) : pairing e (((repairKernel p d).hessian x) e) ≤ 4 * Stage5AboveTwoLower.S5ARepair.repairTheta p d * (Stage5AboveTwoLower.kernelR0 p d - 1) * lpNorm (Stage5AboveTwoLower.kernelR0 p d) x ^ (2 * Stage5AboveTwoLower.S5ARepair.repairTheta p d - 2) * lpNorm (Stage5AboveTwoLower.kernelR0 p d) e ^ 2

The exact raw Hessian formula exported by the construction.

theorem V7.smoothingKernelConstruction : SmoothingKernelConstructionStatement

Full Stage-5 S5-A kernel construction.