(23) and the next display, p. 35 — summed decrease: F(β⁽¹⁾) − F(β⁽ᴹ⁺¹⁾) ≥ M(L − L₀)/2 · min ‖β⁽ᵐ⁺¹⁾ − β⁽ᵐ⁾‖²

Proved

SubsetShrink.DFO.eq_23

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

convergence-ratefirst-order-methodsp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $f:\mathbb R^p\to\mathbb R$ be differentiable and convex with $L_0$ -Lipschitz gradient, $L_0\ge0$ , let $L>L_0$ , $\lambda\in\mathbb R$ , $q\in\{1,2\}$ , $k\ge1$ , put $F(\beta)=f(\beta)+\lambda\|\beta\|_q$ , and let $\beta^{(1)},\beta^{(2)},\dots$ be a sequence generated by the DFO algorithm (14). Then for every $M\ge1$ ,

\sum_{m=1}^M\big(F(\beta^{(m)})-F(\beta^{(m+1)})\big)\ge\frac{L-L_0}2\sum_{m=1}^M\|\beta^{(m+1)}-\beta^{(m)}\|_2^2 \tag{23}

and

F(\beta^{(1)})-F(\beta^{(M+1)})\ge\frac{M(L-L_0)}2\min_{m=1,\dots,M}\|\beta^{(m+1)}-\beta^{(m)}\|_2^2 .

These two displays turn the one-step decrease (22) into the finite-time rate of Proposition 2(b).

Formalization Note The minimum over $m=1,\dots,M$ is Finset.inf' over Finset.Icc 1 M, which is nonempty because $M\ge1$ .

Preamble

import Mathlib
import Definitions.Def_SubsetShrink_DFO_Model

Formal statement

namespace SubsetShrink.DFO

/-- (23) and the display after it, p. 35 (Mazumder, Radchenko & Dedieu, arXiv:1708.03288v4).
Let `f : ℝᵖ → ℝ` be differentiable and convex with `L₀`-Lipschitz gradient ((8)), `L > L₀`,
`L > 0`, `q ∈ {1, 2}`, `k ≥ 1`, and let `β⁽¹⁾, β⁽²⁾, …` be a sequence generated by the DFO
algorithm. For every `M ≥ 1`,
`∑_{m=1}^M (F(β⁽ᵐ⁾) − F(β⁽ᵐ⁺¹⁾)) ≥ ((L − L₀)/2) ∑_{m=1}^M ‖β⁽ᵐ⁺¹⁾ − β⁽ᵐ⁾‖₂²` and
`F(β⁽¹⁾) − F(β⁽ᴹ⁺¹⁾) ≥ (M(L − L₀)/2) min_{m=1,…,M} ‖β⁽ᵐ⁺¹⁾ − β⁽ᵐ⁾‖₂²`. -/
theorem eq_23 {p : ℕ} (f : E p → ℝ) (L0 L lam : ℝ) (q k : ℕ)
    (hq : q = 1 ∨ q = 2) (hk : 1 ≤ k)
    (hdiff : Differentiable ℝ f) (hconv : ConvexOn ℝ Set.univ f) (hL0nn : 0 ≤ L0)
    (hL0 : ∀ β α : E p, ‖gradient f β - gradient f α‖ ≤ L0 * ‖β - α‖)
    (hL : L0 < L) (hLpos : 0 < L)
    (β : ℕ → E p) (hrun : IsDFORun f L lam q k β)
    (M : ℕ) (hM : 1 ≤ M) :
    (L - L0) / 2 * ∑ m ∈ Finset.Icc 1 M, ‖β (m + 1) - β m‖ ^ 2 ≤
        ∑ m ∈ Finset.Icc 1 M, (F f lam q (β m) - F f lam q (β (m + 1))) ∧
    (M : ℝ) * (L - L0) / 2 *
        (Finset.Icc 1 M).inf' (Finset.nonempty_Icc.2 hM) (fun m => ‖β (m + 1) - β m‖ ^ 2) ≤
      F f lam q (β 1) - F f lam q (β (M + 1)) := by sorry

end SubsetShrink.DFO

Source

Mazumder, Radchenko & Dedieu, Subset Selection with Shrinkage, arXiv:1708.03288v4, p. 35, proof of Proposition 2(b) (A.1), (23) and the display after it

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