Prove2Me

(9), p. 8 — an L₀-smooth f lies below its quadratic model Q_L(β; α) for every L ≥ L₀

Proved
SubsetShrink.DFO.eq_9

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

descent-lemmafirst-order-methodsp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let f:Rp→Rf:\mathbb R^p\to\mathbb R be a differentiable convex function whose gradient is L0L_0-Lipschitz, with L0≥0L_0\ge0:

∥∇f(β)−∇f(α)∥2≤L0∥β−α∥2∀ β,α∈Rp.\|\nabla f(\beta)-\nabla f(\alpha)\|_2\le L_0\|\beta-\alpha\|_2\qquad\forall\,\beta,\alpha\in\mathbb R^p .

Then for every L≥L0L\ge L_0 and all α,β∈Rp\alpha,\beta\in\mathbb R^p,

f(β)≤f(α)+⟨∇f(α),β−α⟩+L2∥β−α∥22=QL(β;α).f(\beta)\le f(\alpha)+\langle\nabla f(\alpha),\beta-\alpha\rangle+\frac L2\|\beta-\alpha\|_2^2=Q_L(\beta;\alpha).

This is the quadratic upper bound (the "descent lemma") that the DFO method minimizes in place of ff at each step; it is the first ingredient of the proof of Proposition 2.

Formalization Note Convexity is part of the setting of (7)–(8) ("an L0L_0-smooth convex function") and is kept as a hypothesis as printed. The gradient is Mathlib's gradient f.

Preamble
import Mathlib
import Definitions.Def_SubsetShrink_DFO_Model
Formal statement
namespace SubsetShrink.DFO

/-- (9), p. 8 (Mazumder, Radchenko & Dedieu, arXiv:1708.03288v4): if `f : ℝᵖ → ℝ` is a
differentiable convex function whose gradient is `L₀`-Lipschitz ((8)), then for every
`L ≥ L₀` and all `α, β ∈ ℝᵖ`,
`f(β) ≤ f(α) + ⟨∇f(α), β − α⟩ + (L/2)‖β − α‖₂² = Q_L(β; α)`. -/
theorem eq_9 {p : ℕ} (f : E p → ℝ) (L0 L : ℝ)
    (hdiff : Differentiable ℝ f) (hconv : ConvexOn ℝ Set.univ f) (hL0nn : 0 ≤ L0)
    (hL0 : ∀ β α : E p, ‖gradient f β - gradient f α‖ ≤ L0 * ‖β - α‖)
    (hL : L0 ≤ L) :
    ∀ β α : E p, f β ≤ QL f L β α := by sorry

end SubsetShrink.DFO
Source
Mazumder, Radchenko & Dedieu, Subset Selection with Shrinkage, arXiv:1708.03288v4, p. 8, (8)–(9)
Human review

  • Endorsed by Shuze Chen · Oct 15, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 15, 2026

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

View graph