The kernel gradient is Fréchet differentiable at the origin with zero derivative.

theorem V7.Stage5AboveTwoLower.S5AFinalRepair.lpNorm_powerDualityMap {r : ℝ} (hr : 1 < r) {d : ℕ} (x : Point d) : O3.lpNorm (O3.conjugateExponent r) (O3.powerDualityMap r x) = O3.lpNorm r x ^ (r - 1)

Dependency-pure copy of the exact dual norm calculation for the power duality map. This uses only the shared Stage-2 geometry, not an obsolete above-two trial or machine.

theorem V7.Stage5AboveTwoLower.S5AFinalRepair.norm_apply_le_lpNorm {s : ℝ} (hs : 1 ≤ s) {d : ℕ} (x : Point d) (i : Fin d) : |x i| ≤ O3.lpNorm s x

Every coordinate is bounded by the literal finite-dimensional ell_s norm.

theorem V7.Stage5AboveTwoLower.S5AFinalRepair.norm_le_lpNorm {s : ℝ} (hs : 1 ≤ s) {d : ℕ} (x : Point d) : ‖x‖ ≤ O3.lpNorm s x

The ambient product norm is bounded by the literal finite-dimensional ell_s norm.

noncomputable def V7.Stage5AboveTwoLower.S5AFinalRepair.lpAmbientConstant (s : ℝ) (d : ℕ) : ℝ

Explicit finite-dimensional comparison constant between the ambient product norm and the literal ell_s norm.

Equations

• V7.Stage5AboveTwoLower.S5AFinalRepair.lpAmbientConstant s d = ↑((↑d).rpow (1 / ENNReal.ofReal s).toReal)

theorem V7.Stage5AboveTwoLower.S5AFinalRepair.lpAmbientConstant_nonneg (s : ℝ) (d : ℕ) : 0 ≤ lpAmbientConstant s d

theorem V7.Stage5AboveTwoLower.S5AFinalRepair.lpNorm_le_ambientConstant {s : ℝ} (hs : 1 ≤ s) {d : ℕ} (x : Point d) : O3.lpNorm s x ≤ lpAmbientConstant s d * ‖x‖

The literal ell_s norm is bounded by a fixed multiple of the ambient product norm. The multiplier is the explicit Lipschitz constant of the canonical finite-dimensional PiLp transport.

theorem V7.Stage5AboveTwoLower.S5AFinalRepair.lpNorm_kernelGradientVector {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) {d : ℕ} (x : Point d) : O3.lpNorm (O3.conjugateExponent r) (S5ARepair.kernelGradientVector r theta x) = 4 * theta * O3.lpNorm r x ^ (2 * theta - 1)

Exact dual norm of the concrete kernel gradient.

theorem V7.Stage5AboveTwoLower.S5AFinalRepair.norm_kernelGradientVector_le {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) {d : ℕ} (x : Point d) : ‖S5ARepair.kernelGradientVector r theta x‖ ≤ 4 * theta * O3.lpNorm r x ^ (2 * theta - 1)

Uniform ambient growth of the kernel gradient. The negative-looking power of lpPower has disappeared before this estimate is used at the origin.

theorem V7.Stage5AboveTwoLower.S5AFinalRepair.norm_rpow_isLittleO_id {E : Type u_1} [NormedAddCommGroup E] {a : ℝ} (ha : 1 < a) : (fun (x : E) => ‖x‖ ^ a) =o[nhds 0] fun (x : E) => x

For any normed real vector space, a real power of the norm with exponent strictly larger than one is little-o of the identity at the origin.

theorem V7.Stage5AboveTwoLower.S5AFinalRepair.hasFDerivAt_kernelGradientVector_zero {r theta : ℝ} (hr : 2 < r) (htheta : 1 < theta) (htr : 2 * theta < r) {d : ℕ} : HasFDerivAt (S5ARepair.kernelGradientVector r theta) (S5ARepair.kernelHessian r theta 0) 0

The gradient is genuinely Fréchet differentiable at the origin with zero derivative. This is the first hard gate of the final S5-A repair.