The explicit ambient Hessian of the power kernel away from the origin.

noncomputable def V7.Stage5AboveTwoLower.S5ARepair.kernelHessianCoord {d : ℕ} (r theta : ℝ) (x : Point d) (i : Fin d) : Point d →L[ℝ] ℝ

One coordinate of the explicit kernel Hessian as a continuous linear functional.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def V7.Stage5AboveTwoLower.S5ARepair.kernelHessian {d : ℕ} (r theta : ℝ) (x : Point d) : Point d →L[ℝ] Point d

The explicit kernel Hessian assembled from its coordinate functionals.

Equations

• V7.Stage5AboveTwoLower.S5ARepair.kernelHessian r theta x = ContinuousLinearMap.pi fun (i : Fin d) => V7.Stage5AboveTwoLower.S5ARepair.kernelHessianCoord r theta x i

@[simp]

theorem V7.Stage5AboveTwoLower.S5ARepair.kernelHessian_apply {d : ℕ} (r theta : ℝ) (x h : Point d) (i : Fin d) : (kernelHessian r theta x) h i = (kernelHessianCoord r theta x i) h

theorem V7.Stage5AboveTwoLower.S5ARepair.hasFDerivAt_kernelGradientVector_of_ne_zero {d : ℕ} {r theta : ℝ} (hr : 2 < r) (x : Point d) (hx : x ≠ 0) : HasFDerivAt (kernelGradientVector r theta) (kernelHessian r theta x) x

theorem V7.Stage5AboveTwoLower.S5ARepair.kernelGradientVector_fderiv_of_ne_zero {d : ℕ} {r theta : ℝ} (hr : 2 < r) (x : Point d) (hx : x ≠ 0) : fderiv ℝ (kernelGradientVector r theta) x = kernelHessian r theta x