Ambient norm estimates imply continuity of the kernel Hessian at the origin.

theorem V7.Stage5AboveTwoLower.S5AHessianContinuity.kernelHessian_zero {r theta : ℝ} (_hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} : S5ARepair.kernelHessian r theta 0 = 0

theorem V7.Stage5AboveTwoLower.S5AHessianContinuity.lpPower_rpow_eq_lpNorm_rpow_of_ne_zero {r a : ℝ} (hr : r ≠ 0) {d : ℕ} (x : Point d) (hx : x ≠ 0) : O3.lpPower r x ^ a = O3.lpNorm r x ^ (r * a)

theorem V7.Stage5AboveTwoLower.S5AHessianContinuity.abs_scalarJ_eq {r a : ℝ} (hr : 1 < r) : |O3.Experimental.scalarJ r a| = |a| ^ (r - 1)

theorem V7.Stage5AboveTwoLower.S5AHessianContinuity.abs_lpPowerFDeriv_apply_le {r : ℝ} (hr : 2 < r) {d : ℕ} (x h : Point d) : |(S5ARepair.lpPowerFDeriv r x) h| ≤ r * O3.lpNorm r x ^ (r - 1) * S5AFinalRepair.lpAmbientConstant r d * ‖h‖

noncomputable def V7.Stage5AboveTwoLower.S5AHessianContinuity.hessianCoordConstant (r theta : ℝ) (d : ℕ) : ℝ

The coefficient in the coordinatewise bound for the kernel Hessian.

Equations

• V7.Stage5AboveTwoLower.S5AHessianContinuity.hessianCoordConstant r theta d = 4 * theta * (|2 * theta / r - 1| * r * V7.Stage5AboveTwoLower.S5AFinalRepair.lpAmbientConstant r d + (r - 1))

theorem V7.Stage5AboveTwoLower.S5AHessianContinuity.hessianCoordConstant_nonneg {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) {d : ℕ} : 0 ≤ hessianCoordConstant r theta d

theorem V7.Stage5AboveTwoLower.S5AHessianContinuity.abs_kernelHessianCoord_first_apply_le {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) {d : ℕ} (x h : Point d) (hx : x ≠ 0) (i : Fin d) : |((4 * theta * O3.Experimental.scalarJ r (x i)) • ((2 * theta / r - 1) * O3.lpPower r x ^ (2 * theta / r - 2)) • S5ARepair.lpPowerFDeriv r x) h| ≤ 4 * theta * |2 * theta / r - 1| * r * S5AFinalRepair.lpAmbientConstant r d * O3.lpNorm r x ^ (2 * theta - 2) * ‖h‖

theorem V7.Stage5AboveTwoLower.S5AHessianContinuity.abs_kernelHessianCoord_second_apply_le {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) {d : ℕ} (x h : Point d) (hx : x ≠ 0) (i : Fin d) : |((4 * theta * O3.lpPower r x ^ (2 * theta / r - 1)) • ((r - 1) * |x i| ^ (r - 2)) • ContinuousLinearMap.proj i) h| ≤ 4 * theta * (r - 1) * O3.lpNorm r x ^ (2 * theta - 2) * ‖h‖

theorem V7.Stage5AboveTwoLower.S5AHessianContinuity.abs_kernelHessianCoord_apply_le {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) {d : ℕ} (x h : Point d) (hx : x ≠ 0) (i : Fin d) : |(S5ARepair.kernelHessianCoord r theta x i) h| ≤ hessianCoordConstant r theta d * O3.lpNorm r x ^ (2 * theta - 2) * ‖h‖

theorem V7.Stage5AboveTwoLower.S5AHessianContinuity.norm_kernelHessian_le_lpNorm_rpow {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} (x : Point d) : ‖S5ARepair.kernelHessian r theta x‖ ≤ hessianCoordConstant r theta d * O3.lpNorm r x ^ (2 * theta - 2)

noncomputable def V7.Stage5AboveTwoLower.S5AHessianContinuity.hessianAmbientConstant (r theta : ℝ) (d : ℕ) : ℝ

The coefficient in the ambient norm bound for the kernel Hessian.

Equations

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

theorem V7.Stage5AboveTwoLower.S5AHessianContinuity.hessianAmbientConstant_nonneg {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) {d : ℕ} : 0 ≤ hessianAmbientConstant r theta d

theorem V7.Stage5AboveTwoLower.S5AHessianContinuity.norm_kernelHessian_le_ambient_rpow {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} (x : Point d) : ‖S5ARepair.kernelHessian r theta x‖ ≤ hessianAmbientConstant r theta d * ‖x‖ ^ (2 * theta - 2)

theorem V7.Stage5AboveTwoLower.S5AHessianContinuity.continuousAt_kernelHessian_zero {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} : ContinuousAt (S5ARepair.kernelHessian r theta) 0

The exact narrow-repair gate: the concrete ambient Hessian converges to zero in continuous-linear-map operator norm at the origin.