Prove2Me

Theorem 4 — exact smooth strongly convex interpolation

Proved
TaylorHG.PEP.theorem_4

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

first-order-methodsinterpolationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1performance-estimationsemidefinite-programmingsmooth-strongly-convex

For finite triples (xi,gi,fi)(x_i,g_i,f_i) and 0≤μ<L≤∞0\leq\mu<L\leq\infty, interpolation by Fμ,L\mathcal F_{\mu,L} is equivalent to every ordered pair satisfying

fi−fj−⟨gj,xi−xj⟩≥1L∥gi−gj∥2+μ∥xi−xj∥2−2μL⟨gj−gi,xj−xi⟩2(1−μ/L).f_i-f_j-\langle g_j,x_i-x_j\rangle\geq\frac{\frac1L\|g_i-g_j\|^2+\mu\|x_i-x_j\|^2-\frac{2\mu}{L}\langle g_j-g_i,x_j-x_i\rangle}{2(1-\mu/L)}.

This necessary and sufficient criterion is the paper's bridge from functions to finite data.

Formalization Note The data index is finite, interpolants are real-valued, and 1/∞=01/\infty=0.

Preamble
import Mathlib
import Definitions.Def_TaylorHG_PEP_Interp
Formal statement
namespace TaylorHG.PEP

theorem theorem_4 {d : ℕ} {ι : Type*} [Fintype ι]
    (μ : NNReal) (L : ENNReal) (hμL : (μ : ENNReal) < L)
    (x g : ι → EuclideanSpace ℝ (Fin d)) (fv : ι → ℝ) :
    Interpolable μ L x g fv ↔ ∀ i j, InterpIneq μ L x g fv i j := by sorry

end TaylorHG.PEP
Source
Taylor, Hendrickx & Glineur, arXiv:1502.05666v6, p. 10, Theorem 4 and (4)
Human review

  • Endorsed by Shuze Chen · Oct 8, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 8, 2026

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

View graph