Prove2Me

Theorem 1 — convex interpolation

Proved
TaylorHG.PEP.theorem_1

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

A finite family of triples (xi,gi,fi)(x_i,g_i,f_i) is interpolable by a convex function if and only if every ordered pair satisfies

fi≥fj+⟨gj,xi−xj⟩.f_i\geq f_j+\langle g_j,x_i-x_j\rangle.

This is the base interpolation criterion from which the smooth strongly convex condition is developed.

Formalization Note Interpolating functions are real-valued, and the index type is finite.

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

theorem theorem_1 {d : ℕ} {ι : Type*} [Fintype ι]
    (x g : ι → EuclideanSpace ℝ (Fin d)) (fv : ι → ℝ) :
    Interpolable 0 ⊤ x g fv ↔
      ∀ i j, fv j + inner ℝ (g j) (x i - x j) ≤ fv i := by sorry

end TaylorHG.PEP
Source
Taylor, Hendrickx & Glineur, arXiv:1502.05666v6, p. 7, Theorem 1
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