Symmetry, positivity, and Cauchy-Schwarz estimates for the kernel Hessian.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.kernelHessian_pairing_symmetric {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} (x e f : Point d) : O3.pairing e ((Stage5AboveTwoLower.S5ARepair.kernelHessian r theta x) f) = O3.pairing f ((Stage5AboveTwoLower.S5ARepair.kernelHessian r theta x) e)

Symmetry of the concrete Hessian, obtained from the actual second Fréchet derivative rather than from an asserted matrix property.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.kernelHessian_quadratic_nonneg {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} (x e : Point d) : 0 ≤ O3.pairing e ((Stage5AboveTwoLower.S5ARepair.kernelHessian r theta x) e)

Positive semidefiniteness of the concrete Hessian. Convexity makes the first derivative along every affine line monotone; differentiating that monotone scalar function gives the Hessian quadratic form.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.psd_pairing_cauchy_schwarz {d : ℕ} (H : Point d →L[ℝ] Point d) (hsymm : ∀ (e : O3.Point d) (f : Point d), O3.pairing e (H f) = O3.pairing f (H e)) (hpos : ∀ (e : O3.Point d), 0 ≤ O3.pairing e (H e)) (e f : Point d) : O3.pairing e (H f) ^ 2 ≤ O3.pairing e (H e) * O3.pairing f (H f)

Cauchy--Schwarz for a symmetric positive-semidefinite Hessian form. This is the local algebraic wheel needed to retain the exact Banach-space constant without passing through the ambient Euclidean operator norm.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.kernelHessian_cauchy_schwarz {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} (x e f : Point d) : O3.pairing e ((Stage5AboveTwoLower.S5ARepair.kernelHessian r theta x) f) ^ 2 ≤ O3.pairing e ((Stage5AboveTwoLower.S5ARepair.kernelHessian r theta x) e) * O3.pairing f ((Stage5AboveTwoLower.S5ARepair.kernelHessian r theta x) f)

Pointwise Hessian Cauchy--Schwarz for the concrete kernel.