The ambient Fréchet derivative and coordinate gradient of the power kernel away from zero.

noncomputable def V7.Stage5AboveTwoLower.S5ARepair.pairingCLM {d : ℕ} (g : Point d) : Point d →L[ℝ] ℝ

The continuous linear functional given by pairing with a fixed vector.

Equations

• V7.Stage5AboveTwoLower.S5ARepair.pairingCLM g = ∑ i : Fin d, g i • ContinuousLinearMap.proj i

@[simp]

theorem V7.Stage5AboveTwoLower.S5ARepair.pairingCLM_apply {d : ℕ} (g h : Point d) : (pairingCLM g) h = O3.pairing g h

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

The Fréchet derivative formula for the sum of coordinate absolute powers.

Equations

• V7.Stage5AboveTwoLower.S5ARepair.lpPowerFDeriv r x = r • V7.Stage5AboveTwoLower.S5ARepair.pairingCLM (O3.powerDualityMap r x)

theorem V7.Stage5AboveTwoLower.S5ARepair.hasFDerivAt_lpPower {d : ℕ} {r : ℝ} (hr : 1 < r) (x : Point d) : HasFDerivAt (O3.lpPower r) (lpPowerFDeriv r x) x

noncomputable def V7.Stage5AboveTwoLower.S5ARepair.kernelGradientVector {d : ℕ} (r theta : ℝ) (x : Point d) : Point d

The explicit coordinate gradient of the power smoothing kernel.

Equations

• V7.Stage5AboveTwoLower.S5ARepair.kernelGradientVector r theta x = (4 * theta * O3.lpPower r x ^ (2 * theta / r - 1)) • O3.powerDualityMap r x

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

The kernel gradient represented as a continuous linear functional.

Equations

• V7.Stage5AboveTwoLower.S5ARepair.kernelFDeriv r theta x = V7.Stage5AboveTwoLower.S5ARepair.pairingCLM (V7.Stage5AboveTwoLower.S5ARepair.kernelGradientVector r theta x)

theorem V7.Stage5AboveTwoLower.S5ARepair.hasFDerivAt_lowerKernelPhi_of_ne_zero {d : ℕ} {r theta : ℝ} (hr : 1 < r) (x : Point d) (hx : x ≠ 0) : HasFDerivAt (lowerKernelPhi r theta) (kernelFDeriv r theta x) x

theorem V7.Stage5AboveTwoLower.S5ARepair.lowerKernelPhi_coordinate_gradient_of_ne_zero {d : ℕ} {r theta : ℝ} (hr : 1 < r) (x : Point d) (hx : x ≠ 0) : fderiv ℝ (lowerKernelPhi r theta) x = kernelFDeriv r theta x