Dimension-dependent norm comparisons yield the kernel Hessian and cocoercivity bounds.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.lpAmbientConstant_eq_rpow {s : ℝ} (hs : 0 < s) {d : ℕ} : Stage5AboveTwoLower.S5AFinalRepair.lpAmbientConstant s d = ↑d ^ (1 / s)

The explicit ambient comparison constant is the expected real power.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.lpNorm_kernelR0_le_exp_mul_lpNorm {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) (hregime : ¬p ≤ 3 * Real.log ↑d) (x : Point d) : lpNorm (Stage5AboveTwoLower.kernelR0 p d) x ≤ Real.exp (1 / 3) * lpNorm p x

In the logarithmic regime the finite-dimensional norm conversion costs only the fixed factor exp (1/3).

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repair_logarithmic_hessian_scalar_bound {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) (hregime : ¬p ≤ 3 * Real.log ↑d) : 4 * Stage5AboveTwoLower.S5ARepair.repairTheta p d * (Stage5AboveTwoLower.kernelR0 p d - 1) * Real.exp (2 * Stage5AboveTwoLower.S5ARepair.repairTheta p d / 3) ≤ 15 * Real.exp (2 / 3) * Real.log ↑d

The repaired parameter leaves enough slack to absorb both occurrences of the logarithmic-regime finite-dimensional norm conversion.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repair_kernelHessian_unit_bound {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) (z e : Point d) (hz : lpNorm p z ≤ 1) : O3.pairing e ((Stage5AboveTwoLower.S5ARepair.kernelHessian (Stage5AboveTwoLower.kernelR0 p d) (Stage5AboveTwoLower.S5ARepair.repairTheta p d) z) e) ≤ (if p ≤ 3 * Real.log ↑d then 5 * p else 15 * Real.exp (2 / 3) * Real.log ↑d) * lpNorm p e ^ 2

The literal repaired kernel Hessian obeys the exact frozen two-regime constant on the physical unit ell_p ball.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.repair_kernelGradient_cocoercive {p : ℝ} {d : ℕ} (hp : 2 < p) (hd : 2 ≤ d) : KernelCocoerciveOnUnit p (if p ≤ 3 * Real.log ↑d then 5 * p else 15 * Real.exp (2 / 3) * Real.log ↑d) (Stage5AboveTwoLower.S5ARepair.kernelGradientVector (Stage5AboveTwoLower.kernelR0 p d) (Stage5AboveTwoLower.S5ARepair.repairTheta p d))

Exact cocoercivity with the frozen two-regime Mpd.