Stage 2, route B: the normalized duality map

This file is an isolated exploration of the strong-monotonicity route to O3.belowGeometry. It contains only native consequences of the current explicit finite-dimensional definitions. In particular, it does not assume strong convexity or the frozen target.

theorem O3.Stage2RouteB.lpNorm_rpow_eq_lpPower {p : ℝ} (hp : p ≠ 0) {d : ℕ} (x : Point d) : lpNorm p x ^ p = lpPower p x

theorem O3.Stage2RouteB.coordinate_power_identity {p a : ℝ} (hp : 1 < p) : |a| ^ (p - 2) * a * a = |a| ^ p

theorem O3.Stage2RouteB.pairing_powerDualityMap_self {p : ℝ} (hp : 1 < p) {d : ℕ} (x : Point d) : pairing (powerDualityMap p x) x = lpPower p x

theorem O3.Stage2RouteB.pairing_dualityMap_self {p : ℝ} (hp : 1 < p) {d : ℕ} (x : Point d) : pairing (dualityMap p x) x = lpNorm p x ^ 2

theorem O3.Stage2RouteB.dualityMap_zero {p : ℝ} (hp : 0 < p) {d : ℕ} : dualityMap p 0 = 0

noncomputable def O3.Stage2RouteB.squaredLpEnergy (p : ℝ) {d : ℕ} (x : Point d) : ℝ

The scalar energy written directly in terms of the finite power sum.

Equations

• O3.Stage2RouteB.squaredLpEnergy p x = 1 / 2 * O3.lpPower p x ^ (2 / p)

theorem O3.Stage2RouteB.squaredLpEnergy_eq_quadraticRegularizer {p : ℝ} (_hp : 0 < p) {d : ℕ} (x : Point d) : squaredLpEnergy p x = quadraticRegularizer p 0 x

theorem O3.Stage2RouteB.deriv_lpPower_line {p : ℝ} (hp : 1 < p) {d : ℕ} (x h : Point d) (t : ℝ) : deriv (fun (s : ℝ) => lpPower p fun (i : Fin d) => x i + s * h i) t = p * pairing (powerDualityMap p fun (i : Fin d) => x i + t * h i) h

theorem O3.Stage2RouteB.lpPower_pos_of_point_ne_zero {p : ℝ} {d : ℕ} {x : Point d} (hx : x ≠ 0) : 0 < lpPower p x

theorem O3.Stage2RouteB.powerSum_factor_eq_norm_factor {p : ℝ} (hp : 0 < p) {d : ℕ} {x : Point d} (hx : x ≠ 0) : lpPower p x ^ (2 / p - 1) = lpNorm p x ^ (2 - p)

theorem O3.Stage2RouteB.pairing_dualityMap_eq_powerSum_factor {p : ℝ} (hp : 0 < p) {d : ℕ} {z : Point d} (hz : z ≠ 0) (h : Point d) : pairing (dualityMap p z) h = lpPower p z ^ (2 / p - 1) * pairing (powerDualityMap p z) h

theorem O3.Stage2RouteB.deriv_squaredLpEnergy_line_of_ne {p : ℝ} (hp : 1 < p) {d : ℕ} (x h : Point d) (t : ℝ) (hxt : (fun (i : Fin d) => x i + t * h i) ≠ 0) : deriv (fun (s : ℝ) => squaredLpEnergy p fun (i : Fin d) => x i + s * h i) t = pairing (dualityMap p fun (i : Fin d) => x i + t * h i) h

Route B reaches the exact gradient formula away from the unique possible origin crossing of an affine line.

theorem O3.Stage2RouteB.lpPower_scalar_mul {p a : ℝ} {d : ℕ} (h : Point d) : (lpPower p fun (i : Fin d) => a * h i) = |a| ^ p * lpPower p h

theorem O3.Stage2RouteB.squaredLpEnergy_scalar_mul {p a : ℝ} (hp : 0 < p) {d : ℕ} (h : Point d) : (squaredLpEnergy p fun (i : Fin d) => a * h i) = a ^ 2 * squaredLpEnergy p h

theorem O3.Stage2RouteB.deriv_squaredLpEnergy_line_of_eq_zero {p : ℝ} (hp : 1 < p) {d : ℕ} (x h : Point d) (t : ℝ) (hxt : (fun (i : Fin d) => x i + t * h i) = 0) : deriv (fun (s : ℝ) => squaredLpEnergy p fun (i : Fin d) => x i + s * h i) t = pairing (dualityMap p fun (i : Fin d) => x i + t * h i) h

The same gradient identity at an origin crossing. Here the affine line is exactly a scalar multiple of its direction, so the squared norm is a genuine quadratic and has derivative zero at the crossing.

theorem O3.Stage2RouteB.deriv_squaredLpEnergy_line {p : ℝ} (hp : 1 < p) {d : ℕ} (x h : Point d) (t : ℝ) : deriv (fun (s : ℝ) => squaredLpEnergy p fun (i : Fin d) => x i + s * h i) t = pairing (dualityMap p fun (i : Fin d) => x i + t * h i) h

The explicit finite-dimensional squared ell_p energy has normalized duality-map directional derivative everywhere, including zero coordinates and the origin.

Conjugate-smoothness pivot

For 1 < p ≤ 2, its conjugate exponent lies in the nonsingular range q ≥ 2. These exact arithmetic identities are the parameter bridge needed to turn a (q - 1) smoothness estimate into the desired (p - 1) strong convexity estimate without constant loss.

theorem O3.Stage2RouteB.two_le_conjugateExponent {p : ℝ} (hp : 1 < p) (hp2 : p ≤ 2) : 2 ≤ conjugateExponent p

theorem O3.Stage2RouteB.conjugateExponent_sub_one {p : ℝ} (hp : 1 < p) : conjugateExponent p - 1 = 1 / (p - 1)

theorem O3.Stage2RouteB.conjugate_constant_cancel {p : ℝ} (hp : 1 < p) : (conjugateExponent p - 1) * (p - 1) = 1

theorem O3.Stage2RouteB.mul_conjugateExponent_sub_one {p : ℝ} (hp : 1 < p) : (p - 1) * conjugateExponent p = p

theorem O3.Stage2RouteB.conjugateExponent_ne_zero {p : ℝ} (hp : 1 < p) : conjugateExponent p ≠ 0

theorem O3.Stage2RouteB.exponent_balance {p : ℝ} (hp : 1 < p) : (2 - p) * conjugateExponent p + p = conjugateExponent p

theorem O3.Stage2RouteB.abs_powerDuality_coordinate {p a : ℝ} (hp : 1 < p) : ||a| ^ (p - 2) * a| = |a| ^ (p - 1)

theorem O3.Stage2RouteB.abs_dualityMap_coordinate {p : ℝ} (hp : 1 < p) {d : ℕ} {x : Point d} (hx : x ≠ 0) (i : Fin d) : |dualityMap p x i| = lpNorm p x ^ (2 - p) * |x i| ^ (p - 1)

theorem O3.Stage2RouteB.lpPower_dualityMap {p : ℝ} (hp : 1 < p) {d : ℕ} (x : Point d) : lpPower (conjugateExponent p) (dualityMap p x) = lpNorm p x ^ conjugateExponent p

theorem O3.Stage2RouteB.lpNorm_dualityMap {p : ℝ} (hp : 1 < p) {d : ℕ} (x : Point d) : lpNorm (conjugateExponent p) (dualityMap p x) = lpNorm p x

theorem O3.Stage2RouteB.inner_comp_exponent {p : ℝ} (hp : 1 < p) : (p - 1) * (conjugateExponent p - 2) + (p - 2) = 0

theorem O3.Stage2RouteB.outer_comp_exponent {p : ℝ} (hp : 1 < p) : 2 - conjugateExponent p + (2 - p) * (conjugateExponent p - 1) = 0

theorem O3.Stage2RouteB.powerDuality_coordinate_comp {p a : ℝ} (hp : 1 < p) : ||a| ^ (p - 2) * a| ^ (conjugateExponent p - 2) * (|a| ^ (p - 2) * a) = a

theorem O3.Stage2RouteB.powerDuality_coordinate_scale {q c b : ℝ} (hc : 0 < c) : |c * b| ^ (q - 2) * (c * b) = c ^ (q - 1) * (|b| ^ (q - 2) * b)

theorem O3.Stage2RouteB.dualityMap_conjugate_comp {p : ℝ} (hp : 1 < p) {d : ℕ} (x : Point d) : dualityMap (conjugateExponent p) (dualityMap p x) = x

theorem O3.Stage2RouteB.lpNorm_scalar_mul {r a : ℝ} (hr : 0 < r) {d : ℕ} (z : Point d) : (lpNorm r fun (i : Fin d) => a * z i) = |a| * lpNorm r z

theorem O3.Stage2RouteB.squaredLpEnergy_dualityMap {p : ℝ} (hp : 1 < p) {d : ℕ} (x : Point d) : squaredLpEnergy (conjugateExponent p) (dualityMap p x) = squaredLpEnergy p x

theorem O3.Stage2RouteB.fenchelYoung_lower {p : ℝ} (hp : 1 < p) {d : ℕ} (w y : Point d) : pairing w y - squaredLpEnergy (conjugateExponent p) w ≤ squaredLpEnergy p y

noncomputable def O3.Stage2RouteB.ConjugateSmoothnessStatement : Prop

Exact dual-exponent smoothness interface. This is a reduction interface, not an assumed theorem in the target chain.

Equations

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

theorem O3.Stage2RouteB.pairing_add_left' {d : ℕ} (a b c : Point d) : pairing (a + b) c = pairing a c + pairing b c

theorem O3.Stage2RouteB.pairing_scalar_left {d : ℕ} (r : ℝ) (a b : Point d) : pairing (fun (i : Fin d) => r * a i) b = r * pairing a b

theorem O3.Stage2RouteB.pairing_add_right' {d : ℕ} (a b c : Point d) : pairing a (b + c) = pairing a b + pairing a c

theorem O3.Stage2RouteB.pairing_scalar_right {d : ℕ} (r : ℝ) (a b : Point d) : (pairing a fun (i : Fin d) => r * b i) = r * pairing a b

theorem O3.Stage2RouteB.conjugateSmoothness_implies_belowGeometry (hsmooth : ConjugateSmoothnessStatement) : BelowGeometryStatement