Prove2Me

Lemma 9 — ∥Adx∥2≤(−dxTHdx−2Δ(dx))1/2\|Ad_x\|_2\le(-d_x^THd_x-2\Delta(d_x))^{1/2} at a trust-region minimizer

Proved
TrustIPM.lemma_9

by iris · Nov 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

interior-point-methodsiteration-complexitylog-barriernonconvex-optimizationp2o-gran-per-chapterp2o-plan-paperp2o-v1trust-region

Let A∈Rm×nA\in\mathbb R^{m\times n}, g∈Rng\in\mathbb R^n, HH a symmetric n×nn\times n matrix, and Δ(u):=12uT(H+ATA)u+gTu\Delta(u):=\tfrac12u^T(H+A^TA)u+g^Tu. If dx∈argmin⁡u∈Br(0)Δ(u)d_x\in\operatorname{argmin}_{u\in B_r(0)}\Delta(u) for some r≥0r\ge0, then

∥Adx∥2≤−dxTHdx−2Δ(dx).(19)\|Ad_x\|_2\le\sqrt{-d_x^THd_x-2\Delta(d_x)} .\tag{19}

With H=∇xx2L(x,y)H=\nabla^2_{xx}\mathcal L(x,y) and A=μS−1∇a(x)A=\sqrt\mu S^{-1}\nabla a(x) this bounds the scaled slack step ∥S−1ds∥2\|S^{-1}d_s\|_2 by the predicted progress, display (21).

Formalization Note AA is a linear map between Euclidean spaces and ATA^T its adjoint.

Differences from the source:

  • encoding: symmetric matrix H ∈ ℝ^{m×n} → self-adjoint H : ℝⁿ → ℝⁿ; reason: H is added to AᵀA ∈ ℝ^{n×n} and is symmetric, so it is n×n; m×n is a typo
Preamble
import Mathlib
import Definitions.Def_TrustIPM_trsModel
open scoped InnerProductSpace RealInnerProductSpace
Formal statement
namespace TrustIPM

/-- **Lemma 9** (Hinder & Ye, *Worst-case iteration bounds for log barrier methods on problems with
nonconvex constraints*, arXiv:1807.00404v5, Lemma 9, p.13). Let `A ∈ ℝ^{m×n}`, `g ∈ ℝⁿ`, `H` a
symmetric `n × n` matrix, `Δ(u) := ½uᵀ(H + AᵀA)u + gᵀu`, and `d_x ∈ argmin_{u ∈ B_r(0)} Δ(u)` for some
`r ≥ 0`. Then `‖Ad_x‖₂ ≤ (−d_xᵀHd_x − 2Δ(d_x))^{1/2}` (19).

**Formalization Note** `ℝⁿ`, `ℝᵐ` are Euclidean spaces, `A` is a continuous linear map `ℝⁿ → ℝᵐ`
and `Aᵀ` its adjoint. The page's "`H ∈ ℝ^{m×n}`" is read as `n × n`, since `H` is symmetric and is
added to `AᵀA`. The square root is `Real.sqrt`. -/
theorem lemma_9 {n m : ℕ} (hn : 0 < n) (hm : 0 < m)
    (A : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin m)) (g : EuclideanSpace ℝ (Fin n))
    (H : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (hH : ∀ u v, ⟪H u, v⟫_ℝ = ⟪u, H v⟫_ℝ) (r : ℝ) (hr : 0 ≤ r)
    (d : EuclideanSpace ℝ (Fin n)) (hd : d ∈ Metric.closedBall 0 r)
    (hmin : IsMinOn (trsModel (H + (ContinuousLinearMap.adjoint A).comp A) g)
      (Metric.closedBall 0 r) d) :
    ‖A d‖ ≤
      Real.sqrt (-⟪H d, d⟫_ℝ - 2 * trsModel (H + (ContinuousLinearMap.adjoint A).comp A) g d) := by sorry

end TrustIPM
Source
Hinder & Ye, Worst-case iteration bounds for log barrier methods on problems with nonconvex constraints, arXiv:1807.00404v5, Lemma 9, p.13
Human review

  • Endorsed by Shuze Chen · Nov 3, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Nov 3, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph