Stage 3: exact ell_p -> ell_q descent lemma

The scalar line restriction is differentiated using the frozen IsCoordinateGradient interface. After subtracting the exact quadratic model, its derivative is nonpositive on [0,1]; this yields the coefficient L/2, rather than the weaker coefficient obtainable from two convexity inequalities alone.

noncomputable def O3.Stage3Anchor.objectiveLine {d : ℕ} (f : Vec d → ℝ) (x y : Vec d) (t : ℝ) : ℝ

The objective restricted to the affine line from x to y.

Equations

• O3.Stage3Anchor.objectiveLine f x y t = f ((AffineMap.lineMap x y) t)

theorem O3.Stage3Anchor.hasDerivAt_objectiveLine {d : ℕ} {f : Vec d → ℝ} {grad : Vec d → Vec d} (hgrad : IsCoordinateGradient f grad) (x y : Vec d) (t : ℝ) : HasDerivAt (objectiveLine f x y) (pairing (grad ((AffineMap.lineMap x y) t)) (y - x)) t

theorem O3.Stage3Anchor.firstOrderConvex_of_coordinateGradient {d : ℕ} {f : Vec d → ℝ} {grad : Vec d → Vec d} (hconv : IsConvexObjective f) (hgrad : IsCoordinateGradient f grad) : FirstOrderConvex f grad

Source first-order convexity, derived from convexity and the actual coordinate representation of the Frechet derivative.

noncomputable def O3.Stage3Anchor.smoothPathRemainder {d : ℕ} (p L : ℝ) (f : Vec d → ℝ) (grad : Vec d → Vec d) (x y : Vec d) (t : ℝ) : ℝ

The objective along a line after subtracting its initial linear model and smoothness quadratic.

Equations

• O3.Stage3Anchor.smoothPathRemainder p L f grad x y t = O3.Stage3Anchor.objectiveLine f x y t - t * O3.pairing (grad x) (y - x) - L / 2 * t ^ 2 * O3.lpNorm p (y - x) ^ 2

noncomputable def O3.Stage3Anchor.smoothPathRemainderDeriv {d : ℕ} (p L : ℝ) (grad : Vec d → Vec d) (x y : Vec d) (t : ℝ) : ℝ

The directional derivative of the objective's smoothness remainder.

Equations

• O3.Stage3Anchor.smoothPathRemainderDeriv p L grad x y t = O3.pairing (grad ((AffineMap.lineMap x y) t)) (y - x) - O3.pairing (grad x) (y - x) - L * t * O3.lpNorm p (y - x) ^ 2

theorem O3.Stage3Anchor.hasDerivAt_smoothPathRemainder {d : ℕ} {p L : ℝ} {f : Vec d → ℝ} {grad : Vec d → Vec d} (hgrad : IsCoordinateGradient f grad) (x y : Vec d) (t : ℝ) : HasDerivAt (smoothPathRemainder p L f grad x y) (smoothPathRemainderDeriv p L grad x y t) t

theorem O3.Stage3Anchor.smoothPathRemainderDeriv_nonpos {d : ℕ} {p q L t : ℝ} {grad : Vec d → Vec d} (hp : 1 < p) (hpq : p.HolderConjugate q) (hsmooth : IsLpSmooth p q L grad) (x y : Vec d) (ht0 : 0 ≤ t) : smoothPathRemainderDeriv p L grad x y t ≤ 0

theorem O3.Stage3Anchor.smooth_descent_lp {d : ℕ} {p q L : ℝ} {f : Vec d → ℝ} {grad : Vec d → Vec d} (hp : 1 < p) (hpq : p.HolderConjugate q) (hgrad : IsCoordinateGradient f grad) (hsmooth : IsLpSmooth p q L grad) (x y : Vec d) : f y ≤ f x + pairing (grad x) (y - x) + L / 2 * lpNorm p (y - x) ^ 2

Exact source descent lemma with coefficient L/2.