All missions

Motivation

The proximal algorithm is the basic implicit scheme for minimizing a function $f$: from the current point $x^k$ it moves to a minimizer of $f$ plus a quadratic penalty on the distance travelled. For convex $f$ its convergence theory is classical (Martinet 1970, Rockafellar 1976). For nonconvex, nonsmooth $f$ the situation is different: descent and boundedness give only that limit points are critical, and the whole sequence may fail to converge even for smooth $f$ (Palis–de Melo; Absil, Mahony and Andrews, SIAM J. Optim. 2005).

Attouch and Bolte (Math. Program. 116, 2009, online 2007; author's version hal-00803898) showed that the Łojasiewicz inequality, which holds for real-analytic functions and for continuous subanalytic functions, restores convergence of the whole sequence for the nonsmooth proximal algorithm, together with explicit rates. The argument is Łojasiewicz's original gradient-flow idea transferred to a discrete, nonsmooth setting. It became the template for the later convergence analyses of proximal alternating minimization, forward–backward splitting and PALM under the Kurdyka–Łojasiewicz property, which are used throughout nonconvex optimization, signal processing and machine learning.

Timeline:

• 1963: Łojasiewicz proves his gradient inequality for real-analytic functions and deduces convergence of bounded gradient trajectories.
• 2005: Absil, Mahony and Andrews prove convergence of descent methods for analytic cost functions.
• 2007: Bolte, Daniilidis and Lewis extend the inequality to nonsmooth subanalytic functions with the limiting subdifferential (SIAM J. Optim. 17).
• 2007/2009: Attouch and Bolte prove the result of this mission for the proximal algorithm.

Setting

Points live in $\mathbb R^n$ with the Euclidean norm $|\cdot|$. Let $f:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ be proper (never $-\infty$, finite somewhere) and lower semicontinuous, with domain $\operatorname{dom} f=\{x: f(x)<+\infty\}$.

The limiting subdifferential $\partial f(x)$ is the set of limits $x^*$ of Fréchet subgradients $x_j^*\in\hat\partial f(x_j)$ along sequences $x_j\to x$ with $f(x_j)\to f(x)$. A point with $0\in\partial f(x)$ is critical, and the set of critical points is $\operatorname{crit} f$.

Fix $0<\lambda_-<\lambda_+<+\infty$ and step sizes $\lambda_k\in(\lambda_-,\lambda_+)$. From an arbitrary $x^0$ the proximal algorithm produces

$$x^{k+1}\in\operatorname{argmin}\Big\{f(u)+\frac{1}{2\lambda_k}|u-x^k|^2 : u\in\mathbb R^n\Big\}.\qquad(2)$$

Any minimizer may be selected. The standing hypotheses are

• (H1) $\inf_{\mathbb R^n} f>-\infty$;
• (H2) the restriction of $f$ to $\operatorname{dom} f$ is continuous;
• (H3) the Łojasiewicz property: for every critical point $\hat x$ there are $C,\varepsilon>0$ and $\theta\in[0,1)$ with

$$|f(x)-f(\hat x)|^\theta\le C|x^*|\qquad\forall x\in B(\hat x,\varepsilon),\ \forall x^*\in\partial f(x),\qquad(5)$$

with the convention $0^0=0$ (Remark 4). The number $\theta$ in (5) at a point is a Łojasiewicz exponent of that point.

$\omega(x^0)$ denotes the set of limit points of $(x^k)$.

Formalization targets

Goal: Theorem 4 (convergence)

Under (H1), (H2), (H3), if $(x^k)$ is bounded then

$$\sum_{k=0}^{\infty}|x^{k+1}-x^k|<+\infty\quad\text{and}\quad x^k\to x^\infty\in\operatorname{crit} f.$$

It fixes no constants and holds for every admissible step sequence and every selection in (2).

Milestones

• (3): $x^{k+1}=x^k-\lambda_k g^{k+1}$ with $g^{k+1}\in\partial f(x^{k+1})$.
• Proposition 2 (i)–(ii): $f(x^k)$ is nonincreasing and $\sum|x^{k+1}-x^k|^2<\infty$.
• Proposition 2 (iii): $\omega(x^0)\subset\operatorname{crit} f$ under (H2).
• Proposition 2 (iv): for bounded $(x^k)$, $\omega(x^0)$ is nonempty, compact and connected, and $d(x^k,\omega(x^0))\to0$.
• Lemma 3 (i): $f$ is constant on a connected set of critical points.
• Lemma 3 (ii): (5) holds with common constants on $\{x: d(x,K)\le\varepsilon\}$ for compact connected $K\subset\operatorname{crit} f$.
• (8) and (9), the one-step and summed length estimates of the proof.

Further statements

Theorem 5 (rates): with $\theta$ a Łojasiewicz exponent of $x^\infty$, $\theta=0$ gives finite termination, $\theta\in(0,\frac12]$ gives $|x^k-x^\infty|\le cQ^k$ with $Q\in[0,1)$, and $\theta\in(\frac12,1)$ gives $|x^k-x^\infty|\le c\,k^{-(1-\theta)/(2\theta-1)}$. Also: well-posedness of (2) under (H1), Proposition 2 (v), and Remark 2.

Significance

The theorem turns subsequential convergence into convergence of the whole sequence, with finite length, for a class that includes semi-algebraic, real-analytic and continuous subanalytic functions. Finite length is the property later used to analyse splitting and alternating schemes under the Kurdyka–Łojasiewicz property, and Theorem 5 is the first rate classification by the Łojasiewicz exponent for a nonsmooth algorithm.

The results are proved on paper. No machine-checked proof of Theorem 4 or Theorem 5 is known to exist. A formalization adds a checked convergence theorem for the nonsmooth proximal algorithm with extended-real-valued $f$, and a reusable set of descent, limit-set and uniformization lemmas that apply to other Łojasiewicz-type analyses.

Difficulty

Descent and $\sum|x^{k+1}-x^k|^2<\infty$ give only $|x^{k+1}-x^k|\to0$, which does not imply convergence: the iterates can circle a continuum of critical points with square-summable but non-summable steps, as in the counterexamples for smooth functions. The step that must be supplied is summability of $|x^{k+1}-x^k|$ itself. The local inequality (5) holds only near one critical point with its own constants, while the iterates approach a whole compact set $\omega(x^0)$, so the local constants first have to be made uniform near that set. The nonsmooth setting adds two difficulties: $f$ takes the value $+\infty$, and subgradients are limits of Fréchet subgradients, so their closure properties have to be established for this subdifferential.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n); $n=0$ is allowed. $f$ is EReal-valued and proper means never $\bot$ and somewhere not $\top$. Lower semicontinuity is Mathlib's LowerSemicontinuous. (H2) is ContinuousOn f {x | f x ≠ ⊤}. The limiting subdifferential and $\operatorname{crit} f$ are the published platform definitions NonconvexSplitting.Shared.LimitingSubdiff and NonsmoothLojasiewicz.Continuous.crit. Algorithm (2) is a predicate on a sequence (every step is some minimizer), not a proximal map. Limit points are cluster points of the sequence. The power in (5) is lojPow θ s = if s = 0 then 0 else s ^ θ, which implements $0^0=0$; real values of $f$ are used only where $f$ is finite.

Standing assumptions carried by the goal and Theorem 5: $f$ proper and lower semicontinuous, (H1), (H2), (H3), $0<\lambda_-<\lambda_+$ with $\lambda_k\in(\lambda_-,\lambda_+)$, a sequence complying with (2), and boundedness of its range. Milestones drop the assumptions their claims do not use. The milestones (8) and (9) also assume $x^{k+1}\ne x^k$ for all $k$ and use $\ell=\inf_k f(x^k)$. Both come from the proof's normalization. This reduction is not a hypothesis of Theorem 4: a goal that assumed it, mentioned the constants $\theta,M,N_0,r$, or assumed (8) would not be the paper's theorem.

The development needs the closure properties of the limiting subdifferential, the Fermat rule for proximal steps, and compactness and connectedness of limit sets of sequences with vanishing steps. These are reusable for every Łojasiewicz-type convergence proof. Proofs of individual milestones, of the rate lemmas in the proof of Theorem 5, and of the example $f(x)=|x|^2/2$ are welcome.

Selected references

• H. Attouch, J. Bolte, On the convergence of the proximal algorithm for nonsmooth functions involving analytic features, Math. Program. 116(1–2):5–16, 2009. https://doi.org/10.1007/s10107-007-0133-5 (author's version: https://hal.science/hal-00803898v1)
• J. Bolte, A. Daniilidis, A. Lewis, The Łojasiewicz inequality for nonsmooth subanalytic functions with applications to subgradient dynamical systems, SIAM J. Optim. 17(4):1205–1223, 2007. https://doi.org/10.1137/050644641
• P.-A. Absil, R. Mahony, B. Andrews, Convergence of the iterates of descent methods for analytic cost functions, SIAM J. Optim. 16(2):531–547, 2005. https://doi.org/10.1137/040605266
• R. T. Rockafellar, R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3
• S. Łojasiewicz, Une propriété topologique des sous-ensembles analytiques réels, in Les Équations aux Dérivées Partielles, CNRS, Paris, 1963, pp. 87–89.

Motivation

A sparse graph that approximates a dense one, in the sense that both have nearly the same Laplacian quadratic form, can stand in for it in every algorithm that only reads cuts or solves Laplacian linear systems. Spielman and Teng introduced such spectral sparsifiers and built them in nearly linear time; the construction is the sparsification step of their nearly-linear-time Laplacian solver (arXiv:0808.4134, SIAM J. Comput. 40(4), 2011).

Sampling edges at random works well only inside a graph of high conductance, where no vertex set is separated from the rest by few edges. A general graph is therefore first cut into pieces of high conductance, with few edges running between the pieces. Section 7 of the paper proves that such a decomposition always exists. A similar result was obtained independently by Trevisan (2005). The decomposition theorem, together with the sampling theorem of §6, already shows that every graph has a spectral sparsifier with $O(n\log^7 n)$ edges; the algorithmic decomposition of §8, which the fast algorithm uses, is an approximate version of it, and its analysis rests on the same certificate lemma.

Setting

Let $G=(V,E)$ be a finite simple undirected graph with $m=|E|$ edges, and write $d_i$ for the degree of vertex $i$. For disjoint $S,T\subseteq V$, $E(S,T)$ is the set of edges with one end in $S$ and one in $T$. The volume of $S\subseteq V$ is $\operatorname{Vol}(S)=\sum_{i\in S}d_i$; in particular $\operatorname{Vol}(V)=2m$.

For a vertex set $B\subseteq V$ and $S\subseteq B$, the conductance of $S$ inside $B$ is

$$\Phi^G_B(S)=\frac{|E(S,B-S)|}{\min\big(\operatorname{Vol}(S),\operatorname{Vol}(B-S)\big)},\qquad \Phi^G_B(\emptyset)=1,$$

and the conductance of $B$ is $\Phi^G_B=\min_{S\subset B}\Phi^G_B(S)$ over proper subsets, with $\Phi^G_B=1$ when $|B|=1$. Volumes are always measured with the degrees of $G$, never with the degrees inside the induced subgraph $G(B)$; consequently $\Phi^G_B$ is at most the usual conductance of $G(B)$, and lower bounds on $\Phi^G_B$ transfer to it.

A decomposition of $G$ is a partition $(A_1,\dots,A_k)$ of $V$. It is a $\varphi$-decomposition if $\Phi^G_{A_i}\ge\varphi$ for all $i$, and its boundary is the set of edges between different parts,

$$\partial(A_1,\dots,A_k)=E\cap\bigcup_{i\neq j}(A_i\times A_j).$$

In Lean: vol G S, cutEdges G S T $=|E(S,T)|$, condRel G B S $=\Phi^G_B(S)$, cond G B $=\Phi^G_B$, and decompBoundary G P $=\partial(A_1,\dots,A_k)$ for a Finpartition P of the vertex set, all in the namespace SpectralSparsify.Decomp.

Formalization targets

Goal: Theorem 7.1 (p. 17)

Every graph $G$ without isolated vertices has a decomposition $(A_1,\dots,A_k)$ with

$$\Phi^G_{A_i}\ \ge\ \big(6\log_{4/3}2m\big)^{-1}\quad\text{for all } i,\qquad |\partial(A_1,\dots,A_k)|\ \le\ \frac{|E|}{2}.$$

The constants are the paper's. Both conditions must hold for one and the same partition.

Milestones

1. (12), first inequality (p. 18): for $S\subseteq B$, $R\subseteq B-S$, $T=R\cup S$, $|E(T,B-T)|\le|E(S,B-S)|+|E(R,B-S-R)|$.
2. The volume bound proving (13) (p. 19): if $\operatorname{Vol}(R)\le\frac12\operatorname{Vol}(B-S)$ and $\operatorname{Vol}(S)=\alpha\operatorname{Vol}(B)$, then $\operatorname{Vol}(R\cup S)\le\frac{1+\alpha}{2}\operatorname{Vol}(B)$.
3. Lemma 7.2, Sparsest Cuts as Certificates (p. 18): let $\varphi\le1$, and let $S\subset B$ maximize $\operatorname{Vol}(S)$ subject to (C.1) $\operatorname{Vol}(S)\le\operatorname{Vol}(B)/2$ and (C.2) $\Phi^G_B(S)\le\varphi$. If $\operatorname{Vol}(S)=\alpha\operatorname{Vol}(B)$ with $\alpha\le1/3$, then

$$\Phi^G_{B-S}\ \ge\ \varphi\,\frac{1-3\alpha}{1-\alpha}.$$

4. The $\varphi/3$ step (proof of Theorem 7.1, p. 19): under the hypotheses of Lemma 7.2 with $\operatorname{Vol}(S)\le\operatorname{Vol}(B)/4$, $\Phi^G_{B-S}\ge\varphi/3$.
5. The per-level cut bound (proof of Theorem 7.1, p. 19): for pairwise disjoint $B_1,\dots,B_r$ and $S_j\subset B_j$ satisfying (C.1) and (C.2) in $B_j$ with $\varphi\ge0$, $\sum_j|E(S_j,B_j-S_j)|\le\varphi|E|$.

Significance

The theorem says that every graph is, after removing at most half of its edges, a disjoint union of pieces of conductance $\Omega(1/\log m)$. By Cheeger's inequality each piece then has normalized spectral gap $\Omega(1/\log^2 m)$, which is the hypothesis under which the random sampling of §6 produces a spectral approximation; applying the theorem recursively to the removed edges gives the existence of spectral sparsifiers with $O(n\log^7 n)$ edges (§7.2). Decompositions of this kind, now called expander decompositions, have become a standard tool in graph algorithms.

The theorem is proved in the paper; to the knowledge of this mission it has no machine-checked proof. What the mission produces is a formal proof of the existence statement with the paper's explicit constant, a formal Lemma 7.2 (the certificate lemma that also drives the approximate version, Theorem 8.1), and reusable Lean definitions of volume, relative conductance $\Phi^G_B$ and decomposition boundary for finite simple graphs.

Difficulty

The obvious argument, cutting along any sparse set until no sparse set is left, controls the conductance of the final parts but not the number of edges cut: a long sequence of small sparse cuts can remove far more than half of the edges. The difficulty is to show that one well-chosen cut leaves a remainder whose conductance is certified without further search, which is the content of Lemma 7.2. Its hypothesis is a maximality condition over all subsets of $B$, and its conclusion concerns all subsets of $B-S$, a different set measured with the same ambient degrees, so the two cannot be compared directly. The existence statement then needs a well-founded description of the recursion, a bound on its depth, and an accounting of the cut edges level by level, all against the explicit constant $(6\log_{4/3}2m)^{-1}$.

Formalization scope

Graphs are SimpleGraph V on a finite vertex type with decidable adjacency; vertex sets are Finset V; volumes, conductances and the bound on $|\partial|$ are real numbers; decompositions are Finpartition (Finset.univ : Finset V); $\log_{4/3}$ is Real.logb (4/3).

Hypotheses made explicit:

• No isolated vertices (∀ v, 0 < G.degree v) in Theorem 7.1, Lemma 7.2 and the milestones that divide by a volume. The paper leaves it implicit: $\Phi^G_B(S)$ is $0/0$ for sets of isolated vertices, and with Lean's $0/0=0$ Lemma 7.2 would be false (one edge plus two isolated vertices is a counterexample). Under the hypothesis $m=0$ forces $V=\emptyset$, and Theorem 7.1 is then trivially true.
• $B$ nonempty in Lemma 7.2 and the $\varphi/3$ step, so that $\alpha=\operatorname{Vol}(S)/\operatorname{Vol}(B)$ is determined.
• $\varphi\ge0$ in the per-level bound (the paper's $\varphi$ is positive).

Conventions: $\Phi^G_B$ is the minimum over proper subsets, the empty set contributing $1$; $\Phi^G_B=1$ for $|B|\le1$; $|E(S,T)|$ counts ordered adjacent pairs in $S\times T$, which is the edge count for disjoint sets. Neither conclusion of Theorem 7.1 may be dropped: the partition into singletons satisfies the conductance bound and the partition into one part satisfies the boundary bound, so a formalization keeping only one conclusion is trivial.

Not formalized: idealDecomp as an object (step 2 involves a choice, so it is a relation rather than a function; the goal is the existence statement), its termination and depth bound as separate items, the λ-spectral decomposition remark via Cheeger's inequality, the existence sketch for sparsifiers in §7.2, and the algorithmic analogue of §8. Contributions welcome: proofs of the milestones, a formal recursion for idealDecomp, and lemmas on volume and edge-boundary arithmetic that other graph-partitioning missions can reuse.

Selected references

• D. A. Spielman, S.-H. Teng, Spectral Sparsification of Graphs, arXiv:0808.4134v3, 2010; SIAM J. Comput. 40(4), 2011. https://arxiv.org/abs/0808.4134
• L. Trevisan, Approximation algorithms for unique games, FOCS 2005, pp. 197–205; journal version Theory of Computing 4 (2008) 111–128. https://doi.org/10.4086/toc.2008.v004a005
• D. A. Spielman, S.-H. Teng, Nearly-linear time algorithms for graph partitioning, graph sparsification, and solving linear systems, STOC 2004, pp. 81–90. https://doi.org/10.1145/1007352.1007372

Motivation

Many classical search algorithms are random walks: a Markov chain $P$ on a finite state space $X$ is run until it hits a marked state. Szegedy (2004) attached to every such chain a unitary quantum walk $W(P)$, and Magniez, Nayak, Roland and Santha (SIAM J. Comput. 2011, arXiv:quant-ph/0608026) used it to search quadratically faster than the classical walk for every reversible ergodic chain. The search runs Grover-style rotations, and each rotation needs the reflection $\mathrm{ref}(\pi)$ about the stationary state $|\pi\rangle$. Preparing $|\pi\rangle$ exactly can cost far more than one step of the walk, so the paper builds an approximate reflection $R(P)$ from the walk alone, by phase estimation. Theorem 6 of the paper is the guarantee for that circuit, and this mission formalizes it.

Timeline:

• Jordan, 1875. Two subspaces of a Euclidean space decompose it into one- and two-dimensional invariant pieces ("principal angles").
• Cleve, Ekert, Macchiavello and Mosca, 1998 (Proc. R. Soc. A). The phase-estimation circuit $C(U)$ and its output distribution (Theorem 5 of the paper).
• Szegedy, 2004. The walk $W(P)$, and its spectrum in terms of the singular values of the discriminant matrix (Theorem 4 of the paper).
• Magniez, Nayak, Roland and Santha, 2007/2011. The circuit $R(P)$ and Theorem 6, the search algorithm (Theorem 7), and the bound $\Delta(P)\ge2\sqrt{\delta(P)}$ relating the phase gap to the eigenvalue gap.

Setting

$X$ is a finite set of size $n$. A Markov chain is a row-stochastic matrix $P=(p_{xy})_{x,y\in X}$. It is ergodic if some power of $P$ has all entries positive. A stationary distribution $\pi$ satisfies $\pi_x>0$, $\sum_x\pi_x=1$ and $\sum_x\pi_xp_{xy}=\pi_y$. The time-reversed chain $P^*$ is defined by $\pi_xp_{xy}=\pi_yp^*_{yx}$, and $P$ is reversible if $P^*=P$.

The space is $\mathcal H=\mathbb C^{X\times X}$ with basis $|x\rangle|y\rangle$. Put $|p_x\rangle=\sum_y\sqrt{p_{xy}}\,|y\rangle$ and $|p^*_y\rangle=\sum_x\sqrt{p^*_{yx}}\,|x\rangle$, and

$$\mathcal A=\mathrm{Span}(|x\rangle|p_x\rangle:x\in X),\qquad \mathcal B=\mathrm{Span}(|p^*_y\rangle|y\rangle:y\in X).$$

For a subspace $\mathcal K$, $\mathrm{ref}(\mathcal K)=2\Pi_{\mathcal K}-\mathrm{Id}$, where $\Pi_{\mathcal K}$ is the orthogonal projector onto $\mathcal K$. The quantum walk is $W(P)=\mathrm{ref}(\mathcal B)\cdot\mathrm{ref}(\mathcal A)$, and the stationary state is $|\pi\rangle=\sum_x\sqrt{\pi_x}\,|x\rangle|p_x\rangle$.

The discriminant matrix is $D(P)=(\sqrt{p_{xy}p^*_{yx}})_{x,y}$. Its singular values lie in $[0,1]$. The phase gap $\Delta(P)$ is $2\theta$, where $\theta$ is the smallest angle in $(0,\pi/2)$ such that $\cos\theta$ is a singular value of $D(P)$.

The phase-estimation circuit $C(U)$ acts on $\mathbb C^\iota\otimes\mathbb C^{2^s}$. It is

$$C(U)=(\mathrm{Id}\otimes F^\dagger)\Big(\sum_{j<2^s}U^j\otimes|j\rangle\langle j|\Big)(\mathrm{Id}\otimes H^{\otimes s}),$$

where $H^{\otimes s}$ is the Walsh–Hadamard matrix and $F$ is the $2^s$-point Fourier transform.

The circuit $R(P)$ uses $s=\lceil\log_2(2\pi/\Delta(P))\rceil$ and acts on $\mathcal H\otimes(\mathbb C^{2^s})^{\otimes k}$. It is built in three steps:

1. $V$ applies $C(W(P))$ $k$ times, each time to the system register and a fresh ancilla register.
2. $F_{\neq0}$ multiplies by $-1$ every basis state with a non-zero estimate in some register.
3. Then $R(P)=V^\dagger F_{\neq0}V$.

Formalization targets

Goal: Theorem 6, properties 2 and 3

For $P$ ergodic and reversible on $n\ge2$ states, and every integer $k\ge0$:

$$R(P)\,|\pi\rangle|0^{ks}\rangle=|\pi\rangle|0^{ks}\rangle,\qquad \big\|(R(P)+\mathrm{Id})\,|\psi\rangle|0^{ks}\rangle\big\|\le2^{1-k}\|\psi\|\quad(\psi\in\mathcal A+\mathcal B,\ \psi\perp|\pi\rangle).$$

Milestones

The milestones follow the order in which the paper's proof uses them:

1. Theorem 4 (Szegedy). The spectrum of $W(P)$ on $\mathcal A+\mathcal B$. On that space $W(P)$ has the eigenvalues $1$ (on $\mathcal A\cap\mathcal B$), $-1$, and $e^{\pm2i\theta}$ for $\cos\theta$ a singular value of $D(P)$ in $(0,1)$, with matching multiplicities. The mission has two items for it: the full statement, and the direction the proof uses.
2. §3.2. For ergodic reversible $P$, $|\pi\rangle$ is the only $1$-eigenvector of $W(P)$ in $\mathcal A+\mathcal B$, up to scalars, and every other eigenvalue $\mu$ there satisfies $|1-\mu|\ge|1-e^{i\Delta(P)}|$.
3. Theorem 5, properties 2 and 3. $C(U)$ fixes $|\psi\rangle|0^s\rangle$ when $U\psi=\psi$. If $U\psi=e^{2i\theta}\psi$ with $\theta\in(0,\pi)$, it outputs $|\psi\rangle|\omega\rangle$ with $|\langle0^s|\omega\rangle|=|\sin(2^s\theta)|/(2^s\sin\theta)$.
4. Single-copy bound. For $\Delta/2\le\theta\le\pi-\Delta/2$ and the $s$ above, $|\sin(2^s\theta)|/(2^s\sin\theta)\le1/2$.
5. $k$-copy bound. For $\psi\in\mathcal A+\mathcal B$ with $\psi\perp|\pi\rangle$, the all-zero-estimate component $\psi_0$ of $V|\psi\rangle|0^{ks}\rangle$ has $\|\psi_0\|\le2^{-k}\|\psi\|$. For every $\psi$, $\|(R(P)+\mathrm{Id})|\psi\rangle|0^{ks}\rangle\|=2\|\psi_0\|$.

Significance

Theorem 6 replaces the reflection about $|\pi\rangle$ with a circuit that only calls the walk. Its cost scales as $1/\Delta(P)$ rather than as the cost of preparing $|\pi\rangle$. Combined with $\Delta(P)\ge2\sqrt{\delta(P)}$, where $\delta(P)$ is the eigenvalue gap, this gives the search cost $S+\frac1{\sqrt\varepsilon}\big(\frac1{\sqrt\delta}U+C\big)$ of Theorem 7, up to logarithmic factors. The same approximate-reflection device recurs in later quantum-walk and amplitude-amplification algorithms.

The results are proved in the paper, which takes Theorem 4 from Szegedy and Theorem 5 from Cleve et al. As far as the platform index shows, none of Theorems 4, 5 or 6 has a machine-checked proof. The mission produces three reusable components: a Lean definition of the Szegedy walk and of the phase-estimation circuit, a formal Jordan-type spectral theorem for products of two reflections, and the analysis of phase estimation on an eigenvector.

Difficulty

Most of the work is linear algebra. The proof of Theorem 6 has a short outline: expand $\psi$ in eigenvectors of $W(P)$, apply Theorem 5 to each, and bound each amplitude by $1/2$. Three steps carry the weight:

• Theorem 4. The eigen-decomposition of $W(P)$ on $\mathcal A+\mathcal B$ is Jordan's two-subspace decomposition, with the multiplicities read off the singular value decomposition of $D(P)$. The decomposition has to be built, and the cases at singular values $0$ and $1$ have to be handled separately.
• Uniqueness of $|\pi\rangle$. This step needs ergodicity, through Perron–Frobenius, and reversibility, because $D(P)$ is then symmetric and its singular values are the moduli of the eigenvalues of $P$. Without reversibility $D(P)$ can have the singular value $1$ twice, and property 3 then fails.
• Repetition. The $k$ phase estimations share one system register. Their product acts on an eigenvector as a tensor power on the ancillas. This needs the eigenvectors of the unitary $W(P)$ restricted to the invariant subspace $\mathcal A+\mathcal B$ to be orthogonal.

Formalization scope

• $\mathcal H$ is EuclideanSpace ℂ (X × X), with the first coordinate the first register.
• The ancilla register is indexed by Fin (2^s), and $k$ registers by Fin k → Fin (2^s); the all-zeros state is the zero index.
• $\mathrm{ref}(\mathcal K)$ is Mathlib's Submodule.reflection.
• The stationary distribution $\pi$ is passed as data with its defining hypotheses. "Ergodic" is Matrix.IsPrimitive.
• Singular values of the real matrix $D(P)$ are LinearMap.singularValues.
• When $D(P)$ has no singular value in $(0,1)$, the paper leaves $\Delta(P)$ undefined, and the formalization sets $\Delta(P)=\pi$.
• $\log_2$ is Real.logb 2 and the ceiling is Nat.ceil.

Deviations from the page.

• Reversibility, the standing assumption of §3.2, is a hypothesis of the goal.
• Property 3 is stated for vectors and is homogeneous in $\|\psi\|$.
• Theorem 5 is stated for any finite-dimensional unitary, not only $2^m\times2^m$, and with $|\sin(2^s\theta)|$, because the printed right-hand side can be negative.
• The single-copy bound also covers the eigenvalue $-1$.

Only exact statements are formalized. The cost halves (gate counts, calls to $c$-$W(P)$, "$s\in\log_2(1/\Delta)+O(1)$", the qubit count, uniformity) are out of scope.

The circuit $R(P)$ is the explicit composition above, built from $C(W(P))$. It is neither "some circuit with properties 2–3" nor anything defined through the projector onto $|\pi\rangle$, either of which would make the goal a tautology.

Contributions welcome: proofs of the milestones, Jordan's lemma for two subspaces as a standalone result, and the bound $\Delta(P)\ge2\sqrt{\delta(P)}$ of §3.3.

Selected references

• F. Magniez, A. Nayak, J. Roland, M. Santha, Search via Quantum Walk, SIAM J. Comput. 40(1), 2011. https://arxiv.org/abs/quant-ph/0608026 (v4), https://doi.org/10.1137/090745854
• M. Szegedy, Quantum speed-up of Markov chain based algorithms, FOCS 2004. https://doi.org/10.1109/FOCS.2004.53
• R. Cleve, A. Ekert, C. Macchiavello, M. Mosca, Quantum algorithms revisited, Proc. R. Soc. Lond. A 454, 1998. https://doi.org/10.1098/rspa.1998.0164
• C. Jordan, Essai sur la géométrie à n dimensions, Bull. Soc. Math. France 3, 1875. https://doi.org/10.24033/bsmf.90

Motivation

In an online linear decision problem a decision maker chooses, on each period $t = 1, 2, \dots$, a decision $d_t$ from a set $\mathcal D \subset \mathbb R^n$, and only then learns a state vector $s_t \in \mathcal S \subset \mathbb R^n$ and pays the cost $d_t \cdot s_t$. The online shortest path problem, the experts problem, online binary search trees and list update are all of this form. Kalai and Vempala showed that a single offline optimisation oracle $M(s) = \operatorname{arg\,min}_{d \in \mathcal D} d \cdot s$ is enough to compete with the best fixed decision in hindsight: Follow the Perturbed Leader plays the leader of a randomly perturbed history (Kalai & Vempala 2005; the idea goes back to Hannan 1957).

Each period of FPL calls the oracle once and may change the decision. When an oracle call is expensive, or when switching decisions carries a cost (rotating a search tree, re-routing traffic), this is wasteful. The same paper introduces Follow the Lazy Leader: versions FLL and FLL* of FPL and FPL* that correlate the perturbations across periods so that the decision rarely changes, while each single period is distributed exactly as before. Lemma 1.2 of the paper is the statement that this works, and it is the result of this mission.

Setting

Vectors are elements of $\mathbb R^n$; $|x|_1 = \sum_i |x_i|$, and $s_{1:t} = s_1 + \dots + s_t$ with $s_{1:0} = 0$.

• An argmin oracle for $\mathcal D$ is a map $M$ with $M(x) \in \mathcal D$ and $M(x) \cdot x \le d \cdot x$ for all $d \in \mathcal D$. The decisions are assumed to have $L^1$ diameter at most $D$, and the states satisfy $|s|_1 \le A$ for $s \in \mathcal S$.
• The states $s_1, s_2, \dots \in \mathcal S$ form a fixed sequence (an oblivious adversary).
• For $\varepsilon > 0$, $U$ is the uniform law on the cube $[0, 1/\varepsilon]^n$ and $\mu$ is the Laplace law with density $d\mu(x) = (\varepsilon/2)^n e^{-\varepsilon |x|_1}$.

The four algorithms, period $t$:

1. FPL($\varepsilon$) plays $M(s_{1:t-1} + p)$ with $p \sim U$; FPL*($\varepsilon$) does the same with $p \sim \mu$.
2. FLL($\varepsilon$) draws one offset $p \sim U$ at the start, which fixes the grid $G = \{p + \tfrac1\varepsilon z : z \in \mathbb Z^n\}$, and plays $M(g_{t-1})$, where the grid point $g_{t-1} = g(s_{1:t-1}, p)$ is the unique point of $G$ in $s_{1:t-1} + [0, 1/\varepsilon)^n$.
3. FLL*($\varepsilon$) draws $p_1 \sim \mu$, plays $M(s_{1:t-1} + p_t)$, and then sets $p_{t+1} = p_t - s_t$ with probability $\min\{1, d\mu(p_t - s_t)/d\mu(p_t)\}$ and $p_{t+1} = -p_t$ otherwise. Accepting keeps the evaluation point fixed: $s_{1:t} + p_{t+1} = s_{1:t-1} + p_t$. The law of $p_t$ is written $\nu_t$.

Formalization targets

Goal: Lemma 1.2 (p. 295)

For every period $t \ge 1$:

$$\mathbb E_{p\sim U}\big[s_t \cdot M(g(s_{1:t-1}, p))\big] = \mathbb E_{p\sim U}\big[s_t \cdot M(s_{1:t-1} + p)\big], \qquad \Pr_{p\sim U}[g_{t-1} \ne g_t] \le \varepsilon A,$$ $$\mathbb E_{p_t\sim \nu_t}\big[s_t \cdot M(s_{1:t-1} + p_t)\big] = \mathbb E_{p\sim \mu}\big[s_t \cdot M(s_{1:t-1} + p)\big], \qquad \Pr\big[s_{1:t} + p_{t+1} \ne s_{1:t-1} + p_t\big] \le \varepsilon A .$$

The first line is the FLL half, the second the FLL* half. The constant $\varepsilon A$ is the paper's.

Milestones

1. Lemma 3.2 (p. 300): $U(\{x : x - v \in [0,1/\varepsilon]^n\}) \ge 1 - \varepsilon |v|_1$.
2. The grid point is uniform (pp. 302–303): $g(x, p)$ with $p \sim U$ has the law of $x + p$.
3. FLL update bound (p. 303): $\Pr_{p\sim U}[g(x,p) \ne g(x+v,p)] \le \varepsilon |v|_1$.
4. Display (8) (p. 304): one FLL* update maps $\mu$ to $\mu$.
5. Induction (p. 304): $\nu_t = \mu$ for every $t \ge 1$.
6. Switching bound (p. 304): for any law of $p_t$, $\Pr[p_{t+1} \ne p_t - v] \le \varepsilon |v|_1$.

Significance

Lemma 1.2 transfers every guarantee proved for FPL and FPL* to FLL and FLL*: Theorem 1.1 of the paper bounds expected costs period by period, so equal per-period expectations give the same additive bound $\text{min-cost}_T + \varepsilon RAT + D/\varepsilon$ and the same multiplicative bound for the lazy algorithms. In addition, the expected number of oracle calls and decision changes over $T$ periods is at most $\varepsilon A T$, which is $O(\sqrt T)$ at the usual tuning $\varepsilon \sim 1/\sqrt T$. The paper uses this for online binary search trees with few rotations.

The result is proved in the paper. As far as is known there is no machine-checked proof of it. This mission produces a Lean statement of all four claims and of the six steps of the proof, against explicit Lean definitions of the grid point, the FLL* step and the law sequence $\nu_t$. The uniformity of a random-grid point and the invariance of a Laplace law under a Metropolis-type step are reusable facts beyond online learning.

Difficulty

The FLL half asks for the exact law of the grid point $g(x, p)$, a piecewise translation of $p$ whose pieces depend on $x$. The page settles it in one line ("by symmetry"); in Lean it is an equality of push-forward measures, and the obvious attempt, a single change of variables $p \mapsto p + c$, fails because the shift $c$ is different on different pieces of the cube.

The FLL* half is a statement about measures on $\mathbb R^n \times \mathbb R^n$ given as a mixture of point masses. The page argues with densities, pointwise in $x$; the formal statement is an equality of measures, with the update written as a Measure.bind against a kernel whose two branches move mass in different directions. The density computation of display (8) does not by itself give this equality.

Formalization scope

• Vectors are Fin n → ℝ, $d \cdot s$ is dotProduct, $|x|_1$ is written out as ∑ i, |x i|. States are indexed from 1; s 0 is unused.
• $s_{1:t}$ is prefixSum and $U$ is perturbLaw n ε from the published definition OracleRO.ApproxFPL.FPL. The oracle is the predicate IsArgminOracle Dset M, and every statement holds for every such $M$.
• The Laplace law laplaceLaw n ε carries its normalising constant $(\varepsilon/2)^n$, so it is a probability measure for $\varepsilon > 0$.
• The grid point fllGridPoint ε x p is the explicit formula $p_i + \lceil \varepsilon(x_i - p_i) \rceil / \varepsilon$. It is the unique grid point in the half-open cube for $\varepsilon > 0$, and it is measurable. The half-open and closed cubes differ by a null set, and the closed-cube law is used throughout.
• The FLL* update is the joint law fllStarJoint ε v ν of $(p_t, p_{t+1})$, built with Measure.bind and Measure.dirac. The acceptance probability is $\min\{1, e^{-\varepsilon(|p-v|_1 - |p|_1)}\}$. The law fllStarLaw ε s t is the recursion started at $\mu$, not $\mu$ itself.
• "Performing an update" on period $t$ means $g_{t-1} \ne g_t$ for FLL and $s_{1:t} + p_{t+1} \ne s_{1:t-1} + p_t$ for FLL*.
• Hypotheses not on the page: measurability of $M$ and $\varepsilon > 0$.

The formalization rules out the following trivializations:

• the grid point is not a Classical.choose;
• the integrands are bounded and measurable, because $M$ maps into a set of finite diameter, so the expectations are not the junk value $0$ of a non-integrable function;
• $\nu_t$ is defined by the chain and not as $\mu$, so claim 3 does not compare a law with itself;
• FLL's grid point is compared with FPL's point $s_{1:t-1} + p$, not with itself.

Welcome contributions:

• the uniformity of $x + ((p - x) \bmod L)$ under the uniform law on a box;
• Measure.bind lemmas for finite mixtures of Dirac kernels;
• the change of variables for the Laplace density under reflection and shift.

Selected references

• A. Kalai, S. Vempala, Efficient algorithms for online decision problems, Journal of Computer and System Sciences 71(3):291–307, 2005. https://doi.org/10.1016/j.jcss.2004.10.016
• J. Hannan, Approximation to Bayes risk in repeated play, Contributions to the Theory of Games III, Annals of Mathematics Studies 39, 97–139, 1957. https://doi.org/10.1515/9781400882151-005
• A. Ben-Tal, E. Hazan, T. Koren, S. Mannor, Oracle-based robust optimization via online learning, Operations Research 63(3):628–638, 2015. https://doi.org/10.1287/opre.2015.1374

Motivation

Many sequential decision problems have a combinatorial decision set and a linear cost: choosing a path in a graph whose edge delays change every day, choosing a binary search tree for a stream of requests, or choosing one of $n$ experts whose losses are revealed after each round. Classical weighted-majority algorithms keep one weight per decision, which is exponential in the size of a path or tree. Kalai and Vempala (J. Comput. System Sci. 71 (2005)) showed that one call per round to an offline optimiser, applied to the cumulative costs plus a random perturbation, already gives online guarantees comparable to those of the exponential-weights algorithms. The idea goes back to Hannan's perturbed algorithm (1957); the paper's contribution is a short, general analysis in the linear setting.

The paper proves two guarantees for Follow the Perturbed Leader. The additive one (Theorem 1.1(a), a sister mission) bounds the regret by a term growing like $\sqrt T$. This mission formalizes the multiplicative one, Theorem 1.1(b): for nonnegative costs, a variant with exponentially distributed perturbations pays at most a factor $1+\varepsilon$ more than the best fixed decision in hindsight, plus a term independent of the horizon. Such "small-loss" bounds matter when the best decision has small total cost, since the regret then scales with that cost rather than with $T$.

Setting

Fix a dimension $n$. A decision set $\mathcal D \subset \mathbb R^n$ and a state set $\mathcal S \subset \mathbb R^n$ are given; choosing $d\in\mathcal D$ in state $s\in\mathcal S$ costs $d\cdot s$. In this mission both sets are nonnegative: $\mathcal D, \mathcal S \subset \mathbb R^n_+$.

The decision set is accessed only through an argmin oracle $M:\mathbb R^n\to\mathcal D$ with

$$M(x)\cdot x \le d\cdot x \quad\text{for all } d\in\mathcal D,$$

i.e. $M(x)=\arg\min_{d\in\mathcal D} d\cdot x$ with arbitrary tie-breaking. For a state sequence $s_1,\dots,s_T\in\mathcal S$ write $s_{1:t}=s_1+\dots+s_t$; the benchmark is

$$\text{min-cost}_T=\min_{d\in\mathcal D}\sum_{t=1}^T d\cdot s_t = M(s_{1:T})\cdot s_{1:T}.$$

Two parameters measure the instance: the $\ell_1$-diameter $D\ge |d-d'|_1$ for $d,d'\in\mathcal D$, and the state size $A\ge |s|_1$ for $s\in\mathcal S$, where $|x|_1=\sum_i|x_i|$.

The algorithm FPL*($\varepsilon$) acts as follows on each period $t$: draw $p_t$ from the probability law $\mu_\varepsilon$ with density

$$\frac{d\mu_\varepsilon}{dx}(x)=\Big(\frac{\varepsilon}{2}\Big)^n e^{-\varepsilon|x|_1},$$

so each coordinate is $\pm r/\varepsilon$ with $r$ standard exponential, and play $M(s_{1:t-1}+p_t)$. Its expected cost against a fixed state sequence is

$$\mathbb E[\text{cost of FPL}^*(\varepsilon)]=\sum_{t=1}^T\int s_t\cdot M(s_{1:t-1}+p)\,d\mu_\varepsilon(p).$$

In Lean these are IsArgminOracle Dset M, laplaceLaw n ε and fplStarExpectedCost M s ε T; $s_{1:t}$ is the published OracleRO.ApproxFPL.prefixSum s t.

Formalization targets

Goal: Theorem 1.1(b)

For nonnegative $\mathcal D,\mathcal S$, $A>0$ and $0<\varepsilon\le 1$,

$$\mathbb E[\text{cost of FPL}^*(\varepsilon/2A)]\le(1+\varepsilon)\,\text{min-cost}_T+\frac{4AD(1+\ln n)}{\varepsilon}.$$

Intermediate statements (milestones, in attack order)

1. For any fixed $p_1$: $\sum_{t=1}^T M(s_{1:t}+p_1)\cdot s_t\le M(s_{1:T})\cdot s_{1:T}+D|p_1|_\infty$ (p. 303, by Lemma 3.1).
2. The expected maximum of $n$ independent standard exponentials is at most $\ln n+1$ (end of §2, p. 299).
3. $\mathbb E_{p\sim\mu_\varepsilon}|p|_\infty\le(1+\ln n)/\varepsilon$ (pp. 299, 303).
4. Equation (7): $\mathbb E[M(s_{1:t-1}+p)\cdot s_t]=\int (M(s_{1:t}+y)\cdot s_t)\,e^{-\varepsilon(|y+s_t|_1-|y|_1)}\,d\mu_\varepsilon(y)$.
5. Equation (6): $\mathbb E[M(s_{1:t-1}+p)\cdot s_t]\le e^{\varepsilon A}\,\mathbb E[M(s_{1:t}+p)\cdot s_t]$.
6. For $0<\varepsilon\le 1/A$: $e^{\varepsilon A}\le 1+2\varepsilon A$.
7. For $0<\varepsilon\le 1/A$: $\mathbb E[\text{cost of FPL}^*(\varepsilon)]\le(1+2\varepsilon A)\big(\text{min-cost}_T+D(1+\ln n)/\varepsilon\big)$.

Statement 7 is the bound for an arbitrary parameter; the goal is its evaluation at $\varepsilon/2A$.

Significance

The result is the first multiplicative guarantee for a perturbation algorithm that needs only an offline linear optimiser. With $\varepsilon$ tuned to $\text{min-cost}_T$ it gives $\mathbb E[\text{cost}]\le\text{min-cost}_T+4\sqrt{\text{min-cost}_T\,AD(1+\ln n)}+4AD(1+\ln n)$ (p. 294). The paper applies it to online shortest paths, to the tree-update problem (giving the first efficient $(1+\varepsilon)$-competitive algorithm there), and to adaptive Huffman coding. The lazy variant FLL* of the same paper, whose per-period behaviour coincides with FPL*, inherits the bound; that is the third mission of this series.

The theorem is proved in the paper; to our knowledge no machine-checked proof exists. This mission produces a formal proof of Theorem 1.1(b) as printed, together with the reusable ingredients: the multivariate Laplace law with its normalisation, its translation identity (7), and the expected maximum of i.i.d. exponentials. The paper's argument has small gaps that a formalization must close, notably the condition $\varepsilon\le 1$, which (b) omits but its proof uses.

Difficulty

The deterministic part is the be-the-leader argument with a shared perturbation; it is a finite-sum induction. The probabilistic part is where the work is. The obvious approach, bounding the difference between following and being the perturbed leader by the measure of a symmetric difference of translated sets as in the additive case, gives an additive term proportional to $T$ and cannot give a multiplicative factor. Instead (6) needs the density ratio of $\mu_\varepsilon$ under translation by $s_t$, which requires a change of variables against a density on $\mathbb R^n$, together with the nonnegativity of the integrand; without nonnegativity the inequality fails. The bound on $\mathbb E|p|_\infty$ requires the expected maximum of $n$ exponentials, which is not in Mathlib, and the identification of the coordinates of $\mu_\varepsilon$ as independent scaled Laplace variables, which requires factoring a product density.

Formalization scope

Vectors are Fin n → ℝ; $d\cdot s$ is ⬝ᵥ; $|x|_1$ is written $\sum_i|x_i|$; $|x|_\infty$ is the Lean norm ‖x‖, which on Fin n → ℝ is the sup norm. The decision set is Dset, the diameter Ddiam. States are indexed from $1$; s 0 is unused. The oracle is a hypothesis IsArgminOracle Dset M on an arbitrary function, so the theorems hold for every tie-breaking rule. The paper's parameters are hypotheses ∀ d d' ∈ Dset, ∑ i, |d i - d' i| ≤ Ddiam and ∀ x ∈ S, ∑ i, |x i| ≤ A. The bound $R\ge|d\cdot s|$ of the paper is not used by part (b) and is omitted.

Hypotheses added to the page, each necessary: measurability of $M$ (the expectations presuppose it); $\varepsilon>0$; $A>0$ (the parameter $\varepsilon/2A$ presupposes it); $\varepsilon\le1$ in the goal (used by the proof, p. 303); and $n\ge1$ only in the statement about a maximum over $n$ variables. Two printed slips are corrected, not copied: "exponential distributions with mean $\varepsilon$" (rate $\varepsilon$ is meant) and "$|p_1|_\infty\le(1+\ln n)/\varepsilon$" (an expectation is meant).

Trivializing formalizations are ruled out as follows. The law $\mu_\varepsilon$ carries its normalising constant $(\varepsilon/2)^n$ and is shown to be a probability measure in a sorry-free sanity file; it is not the uniform law of FPL. The cost uses $M(s_{1:t-1}+p)$, not the be-the-leader $M(s_{1:t}+p)$. The oracle is not built with Classical.epsilon. All integrands are measurable and bounded (because $\mathcal D$ has finite diameter), so no integral vanishes for lack of integrability; the sanity file checks this on a two-expert instance that satisfies every hypothesis.

A complete development needs Lebesgue change of variables under translation for densities on Fin n → ℝ, Fubini for product densities, the tail-integral formula for expectations, and a union bound. The Laplace law, its translation identity, and the expected maximum of exponentials are reusable beyond this mission; contributions of those as standalone lemmas are welcome.

Selected references

• A. Kalai and S. Vempala, Efficient algorithms for online decision problems, J. Comput. System Sci. 71(3):291–307, 2005. https://doi.org/10.1016/j.jcss.2004.10.016
• J. Hannan, Approximation to Bayes risk in repeated plays, in Contributions to the Theory of Games III, Ann. of Math. Studies 39, Princeton University Press, 1957, pp. 97–139 (reference [14] of Kalai and Vempala).

Motivation

In an online decision problem a decision maker chooses actions one period at a time, and only after each choice learns what that choice cost. The classical instance is prediction with expert advice: each day one of $n$ experts is followed, and afterwards every expert's loss is revealed. The goal is a strategy whose total cost is close to that of the best single fixed action in hindsight, whatever the sequence of costs.

Many structured problems have exponentially many actions, such as paths in a graph whose edge delays change daily. Weighted-majority methods keep one weight per action and are then inefficient. A. Kalai and S. Vempala (J. Comput. System Sci. 71 (2005) 291–307) showed that it suffices to be able to solve the offline problem: given total costs, find the best single action. Their algorithm, Follow the Perturbed Leader (FPL), adds a random perturbation to the accumulated costs and calls the offline solver once per period. The idea goes back to J. Hannan (1957); the paper's analysis made it short and broadly applicable, and FPL has since become a standard tool in online learning and online combinatorial optimization.

Timeline.

• 1957: Hannan introduces perturbed play, with perturbations growing like $\sqrt t$, and obtains additive bounds for finitely many actions.
• 2005: Kalai and Vempala analyse FPL for linear costs over an arbitrary decision set with an offline oracle: an additive bound (Theorem 1.1(a), the goal here), a multiplicative bound (Theorem 1.1(b)), and lazy variants.

Setting

Decisions and states are vectors in $\mathbb R^n$. The decision set is a possibly infinite set $\mathcal D \subset \mathbb R^n$ and the state set is $\mathcal S \subset \mathbb R^n$. In period $t = 1, 2, \dots$ the decision maker picks $d_t \in \mathcal D$, then the state $s_t \in \mathcal S$ is revealed, and the cost is the dot product $d_t \cdot s_t$. The state sequence is fixed in advance (an oblivious adversary).

Write $s_{1:t} = s_1 + \dots + s_t$, with $s_{1:0} = 0$. The offline oracle is a map $M : \mathbb R^n \to \mathcal D$ with

$$M(s) \in \operatorname*{arg\,min}_{d \in \mathcal D} d \cdot s .$$

Because costs are linear, the best fixed decision after $T$ periods has cost

$$\text{min-cost}_T = \min_{d \in \mathcal D} \sum_{t=1}^T d \cdot s_t = M(s_{1:T}) \cdot s_{1:T}.$$

Three parameters measure an instance, with $|x|_1 = \sum_i |x_i|$:

• the diameter $D \ge |d - d'|_1$ for all $d, d' \in \mathcal D$;
• the cost bound $R \ge |d \cdot s|$ for all $d \in \mathcal D$, $s \in \mathcal S$;
• the state size $A \ge |s|_1$ for all $s \in \mathcal S$.

FPL($\varepsilon$), for a parameter $\varepsilon > 0$: in each period $t$, draw $p_t$ uniformly at random from the cube $[0, 1/\varepsilon]^n$ and play $M(s_{1:t-1} + p_t)$. Its expected cost is $\mathbb E[\text{cost of FPL}(\varepsilon)] = \sum_{t=1}^T \mathbb E\,[M(s_{1:t-1} + p_t) \cdot s_t]$.

Hannan($\delta$): the same rule with $p_t$ uniform on $[0, \sqrt t/\delta]^n$.

Formalization targets

Goal: Theorem 1.1(a)

For every state sequence $s_1, \dots, s_T \in \mathcal S$ and every $0 < \varepsilon \le 1$,

$$\mathbb E[\text{cost of FPL}(\varepsilon)] \le \text{min-cost}_T + \varepsilon R A T + \frac{D}{\varepsilon}.$$

The constants are the paper's. With $\varepsilon = \sqrt{D/(RAT)}$ the expected regret is at most $2\sqrt{DRAT}$.

Milestones (the paper's proof path)

1. Display (4), "be the leader": $\sum_{t=1}^T M(s_{1:t}) \cdot s_t \le M(s_{1:T}) \cdot s_{1:T}$.
2. Lemma 3.1: for any $T > 0$ and vectors $p_0 = 0, p_1, \dots, p_T$,

$$\sum_{t=1}^T M(s_{1:t} + p_t) \cdot s_t \le M(s_{1:T}) \cdot s_{1:T} + D \sum_{t=1}^T |p_t - p_{t-1}|_\infty .$$

3. Display (5): for $p_1 \in [0, 1/\varepsilon]^n$, $\sum_t M(s_{1:t} + p_1) \cdot s_t \le M(s_{1:T}) \cdot s_{1:T} + D|p_1|_\infty \le M(s_{1:T}) \cdot s_{1:T} + D/\varepsilon$.
4. Lemma 3.2: the cubes $[0, 1/\varepsilon]^n$ and $v + [0, 1/\varepsilon]^n$ overlap in at least a $(1 - \varepsilon |v|_1)$ fraction.

Companion: Theorem 3.3

For any state sequence in $\mathcal S$, any $\delta > 0$ and any $T > 0$,

$$\mathbb E[\text{cost of Hannan}(\delta)] \le M(s_{1:T}) \cdot s_{1:T} + 2\delta R A \sqrt T + \frac{D\sqrt T}{\delta}.$$

This bound needs no knowledge of $T$. It is included as a separate theorem, not a milestone of the goal.

Significance

The result. Theorem 1.1(a) reduces online linear optimization over any decision set to its offline counterpart, at the price of one oracle call per period and regret $O(\sqrt{DRAT})$. Applied to online shortest paths, spanning trees and other combinatorial problems it gives efficient algorithms where weighted majority would maintain exponentially many weights. Later uses of FPL (approximate oracles, robust optimization via online learning) start from this bound.

Formalizing it. The theorem has been proved in print for twenty years; it has no machine-checked proof that we know of. The platform already holds a formalization of Ben-Tal, Hazan, Koren and Mannor's approximate-oracle variant (OracleRO.ApproxFPL), which takes a maximising oracle and an oscillation bound $R$ and therefore yields a weaker constant ($2\varepsilon RAT$) in this setting. This mission states the exact-oracle bound with the paper's constant $\varepsilon RAT$, where $R$ bounds $|d \cdot s|$ itself. A correct proof must handle that constant carefully; see the next section.

Difficulty

Display (4), Lemma 3.1 and display (5) are finite-sum arguments from the defining property of $M$. Lemma 3.2 is a statement about Lebesgue measure of a cube and its translate.

The central difficulty is the stability step: bounding, period by period, how much worse it is to play $M(s_{1:t-1} + p_t)$ than $M(s_{1:t} + p_t)$. The obvious argument says that the two perturbed points have laws that agree on a $(1 - \varepsilon|s_t|_1)$ fraction, and on the rest "one can only be $R$ larger". Under the printed definition of $R$ the difference of two costs $d \cdot s_t - d' \cdot s_t$ can be as large as $2R$, so this per-period bound fails for costs of mixed sign: with $n = 1$, $\mathcal D = \{-1, 1\}$ and suitable $s_{1:t-1}$, the per-period difference is $2\varepsilon s_t^2$, while $\varepsilon R A = \varepsilon s_t^2$. The theorem itself, with $\varepsilon RAT$, remains true, but a proof cannot proceed by the per-period comparison as written. Proving the goal with the stated constant, rather than $2\varepsilon RAT$, is the substantive part of the mission.

Formalization scope

• Vectors are Fin n → ℝ; $d \cdot s$ is dotProduct (⬝ᵥ); $|x|_1$ is written out as $\sum_i |x_i|$; $|x|_\infty$ is the Lean norm ‖x‖, which on Fin n → ℝ is the sup norm. The sets are Dset and S; the diameter is Ddiam.
• States are a sequence s : ℕ → Fin n → ℝ indexed from $1$ (s 0 is unused); the hypothesis $s_t \in \mathcal S$ is imposed for $1 \le t \le T$.
• The oracle is the predicate IsArgminOracle Dset M: $M(x) \in \mathcal D$ and $M(x) \cdot x \le d \cdot x$ for all $d \in \mathcal D$. Every theorem quantifies over all such $M$; the oracle is never a chosen Classical.epsilon minimiser.
• Parameters $D$, $R$, $A$ are hypotheses over the sets exactly as printed on p. 294 (not the weaker "reasonable decisions" variant of the paper's footnote 4). Each statement takes only the parameters it uses.
• Shared definitions come from the published OracleRO.ApproxFPL.FPL: prefixSum s t $= s_{1:t}$; perturbLaw n ε, the uniform law on $[0, 1/\varepsilon]^n$; and fplExpectedReward M s ε T $= \sum_{t=1}^T \int s_t \cdot M(s_{1:t-1} + p)\, dU(p)$, which with an argmin oracle is the expected cost of FPL($\varepsilon$) (its name reflects a maximisation source). Using one integral per period is the paper's own observation that fresh and shared perturbations give the same expectation.
• Added hypotheses, each disclosed in the item: $\varepsilon > 0$ and $\delta > 0$ (the page divides by them); measurability of $M$ (the expectations require it). With $R$ bounding $|d \cdot s|$ and $M(x) \in \mathcal D$, every integrand is bounded and measurable, so every expectation is a genuine integral and no bound holds vacuously. The page's $\varepsilon \le 1$ is kept in the goal although the bound does not use it. $T$ is unrestricted where the page allows it.
• Not a trivialization. The expected cost uses $M(s_{1:t-1} + p)$, the decision available before $s_t$ is seen; replacing it by the "be the leader" decision $M(s_{1:t} + p)$ would make the goal follow from display (5) alone. The uniform law is normalised (a probability measure for $\varepsilon > 0$).
• Corrected reading. Display (5) on the page prints $M(s_t + p_1)$; the statement uses $M(s_{1:t} + p_1)$, which is what Lemma 3.1 gives and what the text says it applies.
• Not included. The per-period stability inequality of the printed proof, which is false for costs of mixed sign.

Contributions welcome: proofs of the milestones, the goal and Theorem 3.3, and reusable lemmas on uniform laws over translated cubes.

Selected references

• A. Kalai, S. Vempala, Efficient algorithms for online decision problems, J. Comput. System Sci. 71(3) (2005) 291–307. https://doi.org/10.1016/j.jcss.2004.10.016
• J. Hannan, Approximation to Bayes risk in repeated plays, in: Contributions to the Theory of Games, vol. 3, Princeton University Press, 1957, pp. 97–139 (reference [14] of Kalai–Vempala, https://doi.org/10.1016/j.jcss.2004.10.016).
• A. Ben-Tal, E. Hazan, T. Koren, S. Mannor, Oracle-based robust optimization via online learning, Oper. Res. 63(3) (2015) 628–638. https://doi.org/10.1287/opre.2015.1374