Proposition 2, p. 10 — DFO: F(β⁽ᵐ⁾) decreases to some F* ≥ 0, and min_{m≤M} ‖β⁽ᵐ⁺¹⁾ − β⁽ᵐ⁾‖² ≤ 2(F(β⁽¹⁾) − F*)/(M(L − L₀))

Let $f:\mathbb R^p\to\mathbb R$ be a nonnegative, differentiable, convex function whose gradient is $L_0$-Lipschitz,

with $L_0\ge0$. Let $\lambda\ge0$, $q\in\{1,2\}$, $k\ge1$, $L>0$, and put $F(\beta)=f(\beta)+\lambda\|\beta\|_q$. Let $\beta^{(1)},\beta^{(2)},\dots$ be any sequence generated by the DFO algorithm: $\beta^{(1)}$ is $k$-sparse and $\beta^{(m+1)}\in\mathrm S\big(\beta^{(m)}-\tfrac1L\nabla f(\beta^{(m)});k;\tfrac\lambda L\ell_q\big)$ for $m\ge1$. Then:

1. if $L\ge L_0$, the sequence $\big(F(\beta^{(m)})\big)_{m\ge1}$ is non-increasing and converges to some $F^*\ge0$;
2. if $L>L_0$, its limit $F^*$ satisfies, for every $M\ge1$,

The DFO method is thus a descent method for the $\ell_0$-constrained, $\ell_q$-penalized problem (7), and the squared length of its shortest step among the first $M$ is $O(1/M)$; in the terminology of Definition 1 of the paper, it reaches an $\epsilon$-accurate first-order stationary point in $O(\epsilon^{-1})$ iterations.

Formalization Note Three hypotheses are added to the printed statement (slip 7 of the planning notes). The paper's proof uses "$F(\beta)\ge0$", which holds for $f(\beta)=\tfrac12\|y-X\beta\|_2^2$ but not for every $L_0$-smooth convex $f$ (for $f(\beta)=-\beta_1$ the values can tend to $-\infty$), so $f\ge0$ and $\lambda\ge0$ are assumed. The update divides by $L$, and $L\ge L_0$ allows $L=0$ when $L_0=0$, so $L>0$ is assumed. "Decreasing" is read as non-increasing, since (22) gives only $\le$ at $L=L_0$. Part 2 is stated for every real limit of the sequence, which is the $F^*$ of part 1 because limits in $\mathbb R$ are unique. The minimum is Finset.inf' over Finset.Icc 1 M. The sequence is any choice from the possibly set-valued operator $\mathrm S$; its index $0$ is unused.