Stage 2 closure: below-two geometry

This file combines the native conjugate-smoothness Hessian bound with the explicit duality/Fenchel reduction. The exported theorem is the frozen O3.BelowGeometryStatement without additional hypotheses.

theorem O3.Stage2Closure.dualityMap_two {d : ℕ} (u : Point d) : dualityMap 2 u = u

theorem O3.Stage2Closure.squaredLpEnergy_two_smooth {d : ℕ} (u v : Point d) : Stage2RouteB.squaredLpEnergy 2 v ≤ Stage2RouteB.squaredLpEnergy 2 u + pairing (dualityMap 2 u) (v - u) + (2 - 1) / 2 * lpNorm 2 (v - u) ^ 2

theorem O3.Stage2Closure.hasDerivAt_squaredLpEnergy_line {q : ℝ} (hq : 1 < q) {d : ℕ} (u h : Point d) (t : ℝ) : HasDerivAt (fun (s : ℝ) => Stage2RouteB.squaredLpEnergy q (u + s • h)) (pairing (dualityMap q (u + t • h)) h) t

noncomputable def O3.Stage2Closure.smoothRemainder (q : ℝ) {d : ℕ} (u h : Point d) (t : ℝ) : ℝ

The squared norm along a line after subtracting its smoothness quadratic.

Equations

• O3.Stage2Closure.smoothRemainder q u h t = O3.Stage2RouteB.squaredLpEnergy q (u + t • h) - (q - 1) / 2 * t ^ 2 * O3.lpNorm q h ^ 2

noncomputable def O3.Stage2Closure.smoothRemainderDeriv (q : ℝ) {d : ℕ} (u h : Point d) (t : ℝ) : ℝ

The directional derivative of the smoothness remainder along a line.

Equations

• O3.Stage2Closure.smoothRemainderDeriv q u h t = O3.pairing (O3.dualityMap q (u + t • h)) h - (q - 1) * t * O3.lpNorm q h ^ 2

theorem O3.Stage2Closure.hasDerivAt_smoothRemainder {q : ℝ} (hq : 1 < q) {d : ℕ} (u h : Point d) (t : ℝ) : HasDerivAt (smoothRemainder q u h) (smoothRemainderDeriv q u h t) t

theorem O3.Stage2Closure.exists_hasDerivAt_smoothRemainderDeriv_nonpos {q : ℝ} (hq : 2 < q) {d : ℕ} (u h : Point d) (t : ℝ) : ∃ (w : ℝ), HasDerivAt (smoothRemainderDeriv q u h) w t ∧ w ≤ 0

theorem O3.Stage2Closure.smoothRemainder_concave_above_two {q : ℝ} (hq : 2 < q) {d : ℕ} (u h : Point d) : ConcaveOn ℝ Set.univ (smoothRemainder q u h)

theorem O3.Stage2Closure.squaredLpEnergy_smooth_above_two {q : ℝ} (hq : 2 < q) {d : ℕ} (u v : Point d) : Stage2RouteB.squaredLpEnergy q v ≤ Stage2RouteB.squaredLpEnergy q u + pairing (dualityMap q u) (v - u) + (q - 1) / 2 * lpNorm q (v - u) ^ 2

theorem O3.Stage2Closure.conjugateSmoothness : Stage2RouteB.ConjugateSmoothnessStatement

theorem O3.belowGeometry : BelowGeometryStatement

Frozen Stage 2 target: exact strong convexity of the squared finite ell_p norm for every real 1 < p ≤ 2 and every finite dimension.