Stage 2 route D: finite-sum and duality identities

This probe-local module develops native identities needed by a direct Bregman proof. It contains no target-shaped hypothesis.

theorem O3.Stage2RouteD.pairing_add_left {d : ℕ} (x y z : Point d) : pairing (x + y) z = pairing x z + pairing y z

theorem O3.Stage2RouteD.pairing_add_right {d : ℕ} (x y z : Point d) : pairing x (y + z) = pairing x y + pairing x z

theorem O3.Stage2RouteD.pairing_smul_left {d : ℕ} (a : ℝ) (x y : Point d) : pairing (a • x) y = a * pairing x y

theorem O3.Stage2RouteD.pairing_smul_right {d : ℕ} (a : ℝ) (x y : Point d) : pairing x (a • y) = a * pairing x y

theorem O3.Stage2RouteD.scalar_powerDuality_self {p u : ℝ} (hp : 1 < p) : |u| ^ (p - 2) * u * u = |u| ^ p

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

theorem O3.Stage2RouteD.lpNorm_rpow_p {p : ℝ} (hp : 1 < p) {d : ℕ} (u : Point d) : lpNorm p u ^ p = lpPower p u

@[simp]

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

theorem O3.Stage2RouteD.dualityMap_of_ne {p : ℝ} (hp : 0 < p) {d : ℕ} {u : Point d} (hu : u ≠ 0) : dualityMap p u = fun (i : Fin d) => lpNorm p u ^ (2 - p) * (|u i| ^ (p - 2) * u i)

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

noncomputable def O3.Stage2RouteD.weightVector (q : ℝ) {d : ℕ} (z : Point d) : Point d

Coordinate weights with exponent q - 2 in the squared norm Hessian estimate.

Equations

• O3.Stage2RouteD.weightVector q z i = |z i| ^ (q - 2)

noncomputable def O3.Stage2RouteD.squareVector {d : ℕ} (h : Point d) : Point d

The coordinatewise square of a direction vector.

Equations

• O3.Stage2RouteD.squareVector h i = h i ^ 2

theorem O3.Stage2RouteD.lpNorm_weightVector {q : ℝ} (hq : 2 < q) {d : ℕ} (z : Point d) : lpNorm (q / (q - 2)) (weightVector q z) = lpNorm q z ^ (q - 2)

theorem O3.Stage2RouteD.lpNorm_squareVector {q : ℝ} (hq : 0 < q) {d : ℕ} (h : Point d) : lpNorm (q / 2) (squareVector h) = lpNorm q h ^ 2

theorem O3.Stage2RouteD.weightedHolder_upper {q : ℝ} (hq : 2 < q) {d : ℕ} (z h : Point d) (hz : z ≠ 0) : lpNorm q z ^ (2 - q) * ∑ i : Fin d, |z i| ^ (q - 2) * h i ^ 2 ≤ lpNorm q h ^ 2

The exact weighted Holder estimate in the nonsingular q > 2 Hessian. This is the analytic core of the conjugate-smoothness route.

theorem O3.Stage2RouteD.lpPower_factor_eq_lpNorm {q : ℝ} (hq : 0 < q) {d : ℕ} {z : Point d} (hz : z ≠ 0) : lpPower q z ^ (2 / q - 1) = lpNorm q z ^ (2 - q)

theorem O3.Stage2RouteD.weightedHolder_upper_power {q : ℝ} (hq : 2 < q) {d : ℕ} (z h : Point d) (hz : z ≠ 0) : lpPower q z ^ (2 / q - 1) * ∑ i : Fin d, |z i| ^ (q - 2) * h i ^ 2 ≤ lpNorm q h ^ 2

theorem O3.Stage2RouteD.quadratic_fenchel_lower {p q : ℝ} (hpq : p.HolderConjugate q) {d : ℕ} (y w : Point d) : pairing w y - quadraticRegularizer q 0 w ≤ quadraticRegularizer p 0 y

Exact quadratic Fenchel--Young lower bound for the literal conjugate O3 norms. This is the algebraic entry point for the dual smoothness proof.

theorem O3.Stage2RouteD.fenchel_smoothness_algebra {p q σ : ℝ} (hpq : p.HolderConjugate q) {d : ℕ} (x h a c : Point d) (_hσ : 0 ≤ σ) (hconst : (q - 1) * σ = 1) (hfenchelX : pairing a x - quadraticRegularizer q 0 a = quadraticRegularizer p 0 x) (hpairC : pairing c h = lpNorm p h ^ 2) (hnormStep : lpNorm q (σ • c) = σ * lpNorm p h) (hsmooth : quadraticRegularizer q 0 (a + σ • c) ≤ quadraticRegularizer q 0 a + pairing x (σ • c) + (q - 1) / 2 * lpNorm q (σ • c) ^ 2) : quadraticRegularizer p 0 (x + h) ≥ quadraticRegularizer p 0 x + pairing a h + σ / 2 * lpNorm p h ^ 2

Pure algebra behind the conjugate-smoothness pivot. Once the native duality identities and the q-smoothness estimate supply these hypotheses, the source-exact coefficient σ/2 follows without loss.