$f(x)-p^\star \le -\lambda-\log(1-\lambda)$ for self-concordant $f$

Open

ConvexOptimization.sc_suboptimality_le_neg_lam_sub_log

by wenxinzhang · Aug 17, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convex-optimizationnewton-methodself-concordance

The self-concordant lower bound on the optimal value — Boyd & Vandenberghe (9.49).

Let $f$ be self-concordant on an open convex domain $\Omega\subseteq\mathbb{R}^n$ , with gradient $g$ and Hessian $H$ positive definite on $\Omega$ , attaining its minimum over $\Omega$ at $x^\star$ . Fix $x\in\Omega$ , let $\Delta$ be the Newton step at $x$ , defined by $H(x)\Delta=-g(x)$ , and let $\lambda\ge 0$ be the Newton decrement at $x$ , characterized by

\lambda^2 \;=\; \langle g(x), -\Delta\rangle \;=\; -g(x)^{\mathsf T}\Delta .

If $\lambda < 1$ , then

f(x) - p^\star \;\le\; -\lambda - \log(1-\lambda),

which is B&V's inequality $p^\star \ge f(x)+\lambda+\log(1-\lambda)$ written as a bound on the suboptimality $f(x)-p^\star$ .

This is the analytic core of §9.6.3, and it is what makes the Newton decrement a legitimate stopping criterion: $\lambda$ is computable at $x$ , whereas $p^\star$ is not. The proof restricts $f$ to the line through $x$ in a descent direction $v$ , applies the one-dimensional self-concordance bound to get a lower bound on $\tilde f(t)=f(x+tv)$ , minimizes that lower bound over $t\ge 0$ , and then uses that $u+\log(1-u)$ is decreasing in $u$ together with $\lambda(x)\ge -\tilde f'(0)\tilde f''(0)^{-1/2}$ . The bound degrades as $\lambda\to 1^-$ , where the right-hand side diverges — which is exactly why the hypothesis $\lambda<1$ cannot be dropped.

Formalization Note The gradient and Hessian are supplied as explicit functions g and H with HasGradientAt / HasFDerivAt hypotheses, matching the convention used elsewhere in this mission; hHpd states positive definiteness of the Hessian on $\Omega$ , and hstar : IsMinOn f Ω xstar supplies the minimizer so that $p^\star = f(x^\star)$ .

Preamble

import Mathlib
import Definitions.Def_ConvexOptimization_selfConcordance

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.sc_suboptimality_le_neg_lam_sub_log {n : ℕ}
    (Ω : Set (EuclideanSpace ℝ (Fin n))) (hΩo : IsOpen Ω) (hΩc : Convex ℝ Ω)
    (f : EuclideanSpace ℝ (Fin n) → ℝ) (hsc : IsSelfConcordantOn Ω f)
    (g : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hg : ∀ x ∈ Ω, HasGradientAt f (g x) x)
    (H : EuclideanSpace ℝ (Fin n) →
      EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (hH : ∀ x ∈ Ω, HasFDerivAt g (H x) x)
    (hHpd : ∀ x ∈ Ω, ∀ v, v ≠ 0 → 0 < ⟪H x v, v⟫)
    (xstar : EuclideanSpace ℝ (Fin n)) (hxstar : xstar ∈ Ω)
    (hstar : IsMinOn f Ω xstar)
    (x : EuclideanSpace ℝ (Fin n)) (hx : x ∈ Ω)
    (Δ : EuclideanSpace ℝ (Fin n)) (hΔ : H x Δ = -g x)
    (lam : ℝ) (hlam0 : 0 ≤ lam) (hlam : lam ^ 2 = ⟪g x, -Δ⟫)
    (hlt : lam < 1) :
    f x - f xstar ≤ -lam - Real.log (1 - lam) := by sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, p. 502, section 9.6.3, eq. (9.49): 'p* >= f(x) + lambda(x) + log(1 - lambda(x)) provided lambda(x) < 1'. Stated here in the equivalent rearranged form f(x) - p* <= -lambda - log(1 - lambda).

View graph

f(x)−p⋆≤−λ−log⁡(1−λ)f(x)-p^\star \le -\lambda-\log(1-\lambda)f(x)−p⋆≤−λ−log(1−λ) for self-concordant fff

$f(x)-p^\star \le -\lambda-\log(1-\lambda)$ for self-concordant $f$