Lemma 10 — Follow the Leader is no worse than Be the Leader (index corrected)

Proved

LogRegretOCO.FTAL.ftl_be_the_leader

by mikedeng1 · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

online-convex-optimizationonline-learningp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1regret

Let $f_1, f_2, \dots$ be cost functions on $\mathbb{R}^n$ and let $x_1, x_2, \dots$ be a run of Follow the Leader over $P$ , i.e. $x_t \in \arg\min_{x \in P} \sum_{\tau=1}^{t-1} f_\tau(x)$ for every $t \ge 1$ . Then for every $T$ and every $u \in P$ ,

\sum_{t=1}^T f_t(x_t) - \sum_{t=1}^T f_t(u) \le \sum_{t=1}^T f_t(x_t) - \sum_{t=1}^T f_t(x_{t+1}).

Equivalently, the "Be the Leader" sequence, which plays in round $t$ the minimiser $x_{t+1}$ of the costs up to and including round $t$ , has cost at most that of the best fixed point in hindsight. The lemma reduces bounding the regret of FTL to bounding how much consecutive leaders differ.

Formalization Note The paper prints $x_t = \arg\min_{x \in P} \sum_{\tau=1}^{t} f_\tau(x)$ . With that index the lemma is false already for $T = 1$ (take $P = [0,1]$ , $f_1(x) = x$ , $f_2(x) = -2x$ : then $x_2 = 1$ and $f_1(x_2) = 1 > 0 = \min f_1$ ). The paper's proof ("for $T = 1$ the two are equal by definition") and every use of the lemma (Theorem 5) need $x_t = \arg\min_{x\in P}\sum_{\tau=1}^{t-1} f_\tau(x)$ , the Follow the Leader rule, which is what is stated here. The paper's " $-\min_{x \in P}$ " is encoded as "for every comparator $u \in P$ ".

Preamble

import Mathlib
import Definitions.Def_LogRegretOCO_FTAL_IsFTLRun

Formal statement

namespace LogRegretOCO.FTAL
theorem ftl_be_the_leader {n : ℕ} (P : Set (EuclideanSpace ℝ (Fin n)))
    (f : ℕ → EuclideanSpace ℝ (Fin n) → ℝ) (x : ℕ → EuclideanSpace ℝ (Fin n))
    (hx : IsFTLRun P f x) (T : ℕ) :
    ∀ u ∈ P,
      ∑ t ∈ Finset.Icc 1 T, f t (x t) - ∑ t ∈ Finset.Icc 1 T, f t u
        ≤ ∑ t ∈ Finset.Icc 1 T, f t (x t) - ∑ t ∈ Finset.Icc 1 T, f t (x (t + 1)) := by sorry
end LogRegretOCO.FTAL

Source

Hazan, Agarwal, Kale, Logarithmic regret algorithms for online convex optimization, Mach Learn 69 (2007), p. 190, Lemma 10 (Appendix 1)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. Let $n \in \mathbb{N}$ , $P \subseteq \mathbb{R}^n$ , functions $f_t : \mathbb{R}^n \to \mathbb{R}$ for $t \in \mathbb{N}$ , and points $x_t \in \mathbb{R}^n$ .

Hypothesis. $x$ is a Follow-the-Leader run for $f$ on $P$ . That is, for every $t \ge 1$ :

$x_t \in P$ ;
for every $y \in P$ , $\sum_{\tau=1}^{t-1} f_\tau(x_t) \le \sum_{\tau=1}^{t-1} f_\tau(y)$ .

Conclusion. For every horizon $T \in \mathbb{N}$ and every $u \in P$ ,

\sum_{t=1}^{T} f_t(x_t) - \sum_{t=1}^{T} f_t(u) \;\le\; \sum_{t=1}^{T} f_t(x_t) - \sum_{t=1}^{T} f_t(x_{t+1}).

This is equivalent to $\sum_{t=1}^T f_t(x_{t+1}) \le \sum_{t=1}^T f_t(u)$ . The right-hand side involves $x_{T+1}$ , which the hypothesis also constrains. No convexity, continuity or other regularity is assumed of $P$ or of any $f_t$ .

Degenerate cases.

$T = 0$ . All sums are empty, and the conclusion is $0 \le 0$ .
$P = \emptyset$ . The hypothesis cannot be satisfied, so the statement is vacuous. It is also vacuous if some cumulative cost has no minimiser on $P$ , since no run then exists.
Unused indices. $x_0$ and $f_0$ play no role.
$n = 0$ . Every point is the same, and both sides of the inequality are equal.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph