First and second derivatives of the power kernel restricted to affine lines.

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

The concrete smoothing kernel restricted to an affine line.

Equations

• V7.Stage5AboveTwoLower.S5ARepair.kernelLine r theta x h t = V7.lowerKernelPhi r theta (x + t • h)

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

The exact first directional derivative away from the unique whole-vector origin. Coordinate zeroes are allowed.

Equations

• V7.Stage5AboveTwoLower.S5ARepair.kernelLineGradient r theta x h t = 4 * theta * O3.Stage2RouteA.linePower r x h t ^ (2 * theta / r - 1) * O3.Stage2RouteA.linePowerPair r x h t

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

The exact second directional derivative away from the whole-vector origin. The coordinatewise derivative is nevertheless valid at zero coordinates because r > 2.

Equations

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

theorem V7.Stage5AboveTwoLower.S5ARepair.kernelLine_eq_linePower {d : ℕ} (r theta : ℝ) (x h : Point d) (t : ℝ) : kernelLine r theta x h t = 2 * O3.Stage2RouteA.linePower r x h t ^ (2 * theta / r)

theorem V7.Stage5AboveTwoLower.S5ARepair.hasDerivAt_kernelLine_of_ne_zero {d : ℕ} {r theta : ℝ} (hr : 1 < r) (x h : Point d) (t : ℝ) (hz : x + t • h ≠ 0) : HasDerivAt (kernelLine r theta x h) (kernelLineGradient r theta x h t) t

theorem V7.Stage5AboveTwoLower.S5ARepair.hasDerivAt_kernelLineGradient_of_ne_zero {d : ℕ} {r theta : ℝ} (hr : 2 < r) (x h : Point d) (t : ℝ) (hz : x + t • h ≠ 0) : HasDerivAt (kernelLineGradient r theta x h) (kernelLineHessian r theta x h t) t

theorem V7.Stage5AboveTwoLower.S5ARepair.kernelLine_twice_differentiable_of_ne_zero {d : ℕ} {r theta : ℝ} (hr : 2 < r) (x h : Point d) (t : ℝ) (hz : x + t • h ≠ 0) : HasDerivAt (kernelLine r theta x h) (kernelLineGradient r theta x h t) t ∧ HasDerivAt (kernelLineGradient r theta x h) (kernelLineHessian r theta x h t) t

theorem V7.Stage5AboveTwoLower.S5ARepair.kernelLine_eq_radial_of_eq_zero {d : ℕ} {r theta : ℝ} (hr : 1 ≤ r) (x h : Point d) (t : ℝ) (hz : x + t • h = 0) : kernelLine r theta x h = fun (s : ℝ) => 2 * lpNorm r h ^ (2 * theta) * |s - t| ^ (2 * theta)

Along a line passing through the whole-vector origin, the kernel is an exact scalar homogeneous power. This is the form used to treat the origin without differentiating a negative power of the power sum there.

theorem V7.Stage5AboveTwoLower.S5ARepair.hasDerivAt_kernelLine_at_zero {d : ℕ} {r theta : ℝ} (hr : 1 ≤ r) (htheta : 1 < theta) (x h : Point d) (t : ℝ) (hz : x + t • h = 0) : HasDerivAt (kernelLine r theta x h) 0 t

The first derivative at the whole-vector origin is zero by homogeneous growth of degree 2 * theta > 2.

theorem V7.Stage5AboveTwoLower.S5ARepair.hasDerivAt_kernelLine_radialGradient_at_zero {d : ℕ} {r theta : ℝ} (htheta : 1 < theta) (h : Point d) (t : ℝ) : HasDerivAt (fun (s : ℝ) => 4 * theta * lpNorm r h ^ (2 * theta) * O3.Experimental.scalarJ (2 * theta) (s - t)) 0 t

The derivative of the scalar radial model has derivative zero at the origin when the homogeneous degree is strictly above two. This is the second origin calculation needed for the continuous Hessian extension.