Prove2Me

§5.3.2, proof of Theorem 5.3, p. 321 — ∫₀¹ ‖∇²f(x_k) − ∇²f(x* + s(x_k − x*))‖ ds ≤ (M/2)‖x_k − x*‖

Open
ConvexOptAlg.Newton.lipschitz_integral_bound

by mikedeng1 · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

convex-optimizationhessiannewton-methodp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1

Let H:Rn→L(Rn,Rn)H:\mathbb R^n\to L(\mathbb R^n,\mathbb R^n) be MM-Lipschitz in operator norm, i.e. ∥H(x)−H(y)∥≤M∥x−y∥\|H(x)-H(y)\|\le M\|x-y\| for all x,yx,y (for instance, the Hessian H=∇2fH=\nabla^2 f of a function with MM-Lipschitz Hessian). Then for all x∗,y∈Rnx^*,y\in\mathbb R^n,

∫01∥H(y)−H(x∗+s(y−x∗))∥ ds≤M2 ∥y−x∗∥.\int_0^1\big\|H(y)-H\big(x^*+s(y-x^*)\big)\big\|\,ds\le\frac M2\,\|y-x^*\|.

In the analysis of Newton's method, with H=∇2fH=\nabla^2 f and y=xky=x_k, this bounds the integral in the error representation of a Newton step by M2∥xk−x∗∥\frac M2\|x_k-x^*\|, which produces the quadratic rate.

Formalization Note The book states the bound at an iterate xkx_k for the Hessian of ff; it uses only the Lipschitz property, so it is stated for any MM-Lipschitz map HH and any point yy. No sign condition on MM is needed (a negative MM makes the hypothesis unsatisfiable unless n=0n=0). Rn\mathbb R^n is EuclideanSpace ℝ (Fin n) and ∥⋅∥\|\cdot\| on linear maps is the operator norm.

Preamble
import Mathlib
import Definitions.Def_ConvexOptAlg_Newton_Defs
Formal statement
namespace ConvexOptAlg.Newton

/-- The Lipschitz integral bound in the proof of Theorem 5.3 (Bubeck, arXiv:1405.4980v2, §5.3.2,
p. 321, fifth display of the proof): if the Hessian map `H` is `M`-Lipschitz in operator norm, then
for all points `x∗, y ∈ ℝⁿ`,
`∫₀¹ ‖∇²f(y) − ∇²f(x∗ + s(y − x∗))‖ ds ≤ (M/2)‖y − x∗‖`.
The book states it at `y = x_k`; it uses only the Lipschitz property, so it is stated for any
`M`-Lipschitz map `H : ℝⁿ → L(ℝⁿ, ℝⁿ)` and any `y`. -/
theorem lipschitz_integral_bound {n : ℕ}
    (H : EuclideanSpace ℝ (Fin n) → (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)))
    (M : ℝ) (hHL : IsLipschitzHessian H M) (xstar y : EuclideanSpace ℝ (Fin n)) :
    ∫ s in (0 : ℝ)..1, ‖H y - H (xstar + s • (y - xstar))‖ ≤ M / 2 * ‖y - xstar‖ := by sorry

end ConvexOptAlg.Newton
Source
Bubeck, arXiv:1405.4980v2, §5.3.2, proof of Theorem 5.3, p. 321, fifth display

View graph