Prove2Me

§5.3.2, proof of Theorem 5.3, p. 321 — ∇²f(x_k)(x_{k+1} − x*) = ∫₀¹ [∇²f(x_k) − ∇²f(x* + s(x_k − x*))](x_k − x*) ds

Open
ConvexOptAlg.Newton.error_representation

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

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

Let f:Rn→Rf:\mathbb R^n\to\mathbb R be a C2C^2 function with gradient ∇f\nabla f and Hessian ∇2f\nabla^2 f, and let x∗x^* be a local minimum of ff, so that ∇f(x∗)=0\nabla f(x^*)=0. Let y∈Rny\in\mathbb R^n. Then

  1. the gradient at yy is
∇f(y)=∫01∇2f(x∗+s(y−x∗)) (y−x∗) ds;\nabla f(y)=\int_0^1\nabla^2 f\big(x^*+s(y-x^*)\big)\,(y-x^*)\,ds;
  1. if y+y^+ is obtained from yy by a Newton step, i.e. ∇2f(y) (y−y+)=∇f(y)\nabla^2 f(y)\,(y-y^+)=\nabla f(y), then
∇2f(y) (y+−x∗)=∫01[∇2f(y)−∇2f(x∗+s(y−x∗))](y−x∗) ds.\nabla^2 f(y)\,(y^+-x^*)=\int_0^1\Big[\nabla^2 f(y)-\nabla^2 f\big(x^*+s(y-x^*)\big)\Big](y-x^*)\,ds.

With y=xky=x_k and y+=xk+1y^+=x_{k+1} this is the representation of the error of one Newton step from which the quadratic rate is read off.

Formalization Note The book writes part 2 as xk+1−x∗=[∇2f(xk)]−1∫01[… ](xk−x∗) dsx_{k+1}-x^*=[\nabla^2 f(x_k)]^{-1}\int_0^1[\dots](x_k-x^*)\,ds. Here both sides are multiplied by ∇2f(y)\nabla^2 f(y), so no inverse is taken; when ∇2f(y)\nabla^2 f(y) is invertible the two forms are equivalent. The statement is for any point yy and any Newton step y+y^+ from it, not only for iterates of a run. Integrals are Bochner integrals over [0,1][0,1] of Rn\mathbb R^n-valued maps.

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

/-- The error representation in the proof of Theorem 5.3 (Bubeck, arXiv:1405.4980v2, §5.3.2,
p. 321, second and third displays of the proof). Let `f : ℝⁿ → ℝ` be C² with gradient map `g` and
Hessian map `H`, and let `x∗` be a local minimum of `f` (so `∇f(x∗) = 0`). For every point `y`:
(1) `∇f(y) = ∫₀¹ ∇²f(x∗ + s(y − x∗)) (y − x∗) ds`; and
(2) if `y⁺` is a Newton step from `y`, i.e. `∇²f(y)(y − y⁺) = ∇f(y)`, then
`∇²f(y)(y⁺ − x∗) = ∫₀¹ [∇²f(y) − ∇²f(x∗ + s(y − x∗))] (y − x∗) ds`.
Part (2) is the page's last line `x_{k+1} − x∗ = [∇²f(x_k)]⁻¹ ∫₀¹ […] (x_k − x∗) ds` with both
sides multiplied by `∇²f(x_k)`, which avoids inverting a possibly singular operator; for the
book's iterate (`y = x_k`, `y⁺ = x_{k+1}`, `∇²f(x_k)` invertible) the two forms are equivalent. -/
theorem error_representation {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (g : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (H : EuclideanSpace ℝ (Fin n) → (EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)))
    (hfgH : IsC2GradHess f g H) (xstar : EuclideanSpace ℝ (Fin n)) (hmin : IsLocalMin f xstar)
    (y yplus : EuclideanSpace ℝ (Fin n)) (hstep : H y (y - yplus) = g y) :
    g y = (∫ s in (0 : ℝ)..1, H (xstar + s • (y - xstar)) (y - xstar)) ∧
    H y (yplus - xstar) =
      ∫ s in (0 : ℝ)..1, (H y - H (xstar + s • (y - xstar))) (y - xstar) := by sorry

end ConvexOptAlg.Newton
Source
Bubeck, arXiv:1405.4980v2, §5.3.2, proof of Theorem 5.3, p. 321, second and third displays

View graph