The power smoothing kernel is twice continuously Fréchet differentiable globally.

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

The derivative of the kernel's Fréchet derivative, obtained from its Hessian.

Equations

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

theorem V7.Stage5AboveTwoLower.S5AGlobalC2.continuous_kernelFDerivDerivative {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} : Continuous (kernelFDerivDerivative r theta)

theorem V7.Stage5AboveTwoLower.S5AGlobalC2.hasFDerivAt_kernelFDeriv {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} (x : Point d) : HasFDerivAt (S5ARepair.kernelFDeriv r theta) (kernelFDerivDerivative r theta x) x

theorem V7.Stage5AboveTwoLower.S5AGlobalC2.contDiff_one_kernelFDeriv {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} : ContDiff ℝ 1 (S5ARepair.kernelFDeriv r theta)

theorem V7.Stage5AboveTwoLower.S5AGlobalC2.contDiff_two_lowerKernelPhi {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} : ContDiff ℝ 2 (lowerKernelPhi r theta)

Genuine global C² closure for the fixed scalar smoothing kernel.