A positive semidefinite Hessian bound yields cocoercivity of the kernel gradient.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.sq_intervalIntegral_le_integral_sq (X : ℝ → ℝ) (hX : Continuous X) : (∫ (t : ℝ) in 0..1, X t) ^ 2 ≤ ∫ (t : ℝ) in 0..1, X t ^ 2

Cauchy--Schwarz for scalar integration on the unit interval, proved from nonnegativity of the integrated centred square.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.kernelGradient_cocoercive_on_unit_of_hessian_bound {p r theta M : ℝ} (hp : 1 < p) (hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} (hbound : ∀ (z e : Point d), lpNorm p z ≤ 1 → O3.pairing e ((Stage5AboveTwoLower.S5ARepair.kernelHessian r theta z) e) ≤ M * lpNorm p e ^ 2) : KernelCocoerciveOnUnit p M (Stage5AboveTwoLower.S5ARepair.kernelGradientVector r theta)

Exact unit-ball cocoercivity of the concrete kernel gradient, derived from the genuine Hessian, its PSD Cauchy--Schwarz inequality, and the frozen quadratic Hessian bound.