proofs
Provedadcgssupportingquadratic-step

The clipped Frank–Wolfe scalar step minimizes the quadratic model on the unit interval

For all h,d∈R\htmlData{mx=1}{h, d \in \htmlData{mx=0}{\mathbb{R}}}, if 0≤h0 \mathrel{\htmlData{mx=1}{\leq}} \htmlData{mx=0}{h} and 0<d0 \mathrel{\htmlData{mx=1}{<}} \htmlData{mx=0}{d}, then

0≤min⁡(1,hd)∧min⁡(1,hd)≤1∧∀t∈R,0≤t  ⟹  t≤1  ⟹  −h⋅min⁡(1,hd)+d2⋅(min⁡(1,hd))2≤−h⋅t+d2⋅t2\begin{aligned} & 0 \mathrel{\htmlData{mx=5}{\leq}} \htmlData{mx=4}{\min(1, \htmlData{mx=3}{\frac{\htmlData{mx=1}{h}}{\htmlData{mx=2}{d}}})} \\ & \htmlData{mx=0}{\land} \htmlData{mx=9}{\min(1, \htmlData{mx=8}{\frac{\htmlData{mx=6}{h}}{\htmlData{mx=7}{d}}})} \mathrel{\htmlData{mx=10}{\leq}} 1 \\ & \htmlData{mx=0}{\land} \htmlData{mx=11}{\forall} t \in \htmlData{mx=12}{\mathbb{R}}, \\ & \quad 0 \mathrel{\htmlData{mx=15}{\leq}} \htmlData{mx=14}{t} \\ & \quad \htmlData{mx=13}{\implies} \htmlData{mx=16}{t} \mathrel{\htmlData{mx=17}{\leq}} 1 \\ & \quad \htmlData{mx=13}{\implies} \htmlData{mx=34}{\htmlData{mx=25}{\htmlData{mx=20}{-\htmlData{mx=19}{h}} \cdot \htmlData{mx=24}{\min(1, \htmlData{mx=23}{\frac{\htmlData{mx=21}{h}}{\htmlData{mx=22}{d}}})}} + \htmlData{mx=33}{\htmlData{mx=27}{\frac{\htmlData{mx=26}{d}}{2}} \cdot \htmlData{mx=32}{\left(\htmlData{mx=31}{\min(1, \htmlData{mx=30}{\frac{\htmlData{mx=28}{h}}{\htmlData{mx=29}{d}}})}\right)^{2}}}} \\ & \quad \quad \htmlData{mx=18}{\leq} \htmlData{mx=44}{\htmlData{mx=38}{\htmlData{mx=36}{-\htmlData{mx=35}{h}} \cdot \htmlData{mx=37}{t}} + \htmlData{mx=43}{\htmlData{mx=40}{\frac{\htmlData{mx=39}{d}}{2}} \cdot \htmlData{mx=42}{\htmlData{mx=41}{t}^{2}}}} \end{aligned}
What the notation means · or point at any symbol
RReal numbers
The real numbers: every point on the number line. (ℝ)
x ∈ TVariables
h, d range over real numbers: the statement must hold for every choice. ((h d : ℝ))
≤At most
0 is less than or equal to h. (0 ≤ h)
<Less than
0 is strictly smaller than d. (0 < d)
minMinimum
The smaller of 1 and h/d. (min 1 (h / d))
a/bDivision
h divided by d. In Lean, dividing by 0 gives 0. (h / d)
∧And
Both hold: min(1, h/d) ≤ 1, and ∀ t, 0 ≤ t → (t ≤ 1 → −h · min(1, h/d) + d/2 · min(1, h/d)…. (min 1 (h / d) ≤ 1 ∧ ∀ t : ℝ, 0 ≤ t → t …)
∀For all
The statement after the comma holds for every t. (∀ t : ℝ, 0 ≤ t → t ≤ 1 → -h * min 1 (h …)
⟹Implies
If t ≤ 1, then −h · min(1, h/d) + d/2 · min(1, h/d)^2 ≤ −h · t + d/2 · t^2. (Between types, A → B is the type of functions from A to B.) (t ≤ 1 → -h * min 1 (h / d) + d / 2 * (m…)
−xNegation
The negative of h. (-h)
·Multiplication
−h times min(1, h/d). (-h * min 1 (h / d))
+Addition
−h · min(1, h/d) plus d/2 · min(1, h/d)^2. (-h * min 1 (h / d) + d / 2 * (min 1 (h …)
aᵇPower
min(1, h/d) raised to the power 2. ((min 1 (h / d)) ^ 2)

Algorithm 1 line 17 and Appendix A.1 scalar line minimization. Here h is the nonnegative FW gap and d=||v-u||^2/eta is positive on a continuing nonzero inner step. The target proves interval feasibility and global minimization of q(t)=-ht+dt^2/2 over 0<=t<=1, not a complete convergence result. It is the literal scalar quadratic underlying the vector subproblem; d=0/stopping is a separate case.

How it was proved

Proved
30 September 2026
By
Ajax
Checked by
Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms
Classical.choice, Quot.sound, propext
Proof
33 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements