Probability

Motivation

Training a model in machine learning means minimizing an expected loss over a data distribution, using a finite sample from it. Two families of methods dominate. Stochastic gradient methods step along the gradient of the loss at one data point: each step is cheap, but the noise forces small steps and many sequential iterations. Batch methods average the gradient over a large set of points: each step is accurate and parallelizes well, but costs a pass over the data. Bottou and Bousquet (The tradeoffs of large scale learning, NIPS 2007) compared the two by the total work needed to reach accuracy $\epsilon$ and concluded that stochastic gradient descent is preferable in large-scale learning.

Byrd, Chin, Nocedal and Wu (Sample size selection in optimization methods for machine learning, Math. Program. 2012) analyse a third option: a dynamic batch method, which takes gradient steps on mini-batches whose size grows over the run. A small batch makes early progress cheap; a large batch later makes the steps accurate. Their Theorem 4.2 shows that when the batch size grows geometrically, steepest descent with a fixed step converges linearly in expectation, and their Corollary 4.3 derives from it a total work bound of the same order as stochastic gradient descent. The analysis underlies a line of work on adaptive sampling and variance-controlled batch methods (for example Friedlander and Schmidt, Hybrid deterministic-stochastic methods for data fitting, SIAM J. Sci. Comput. 2012; Bottou, Curtis and Nocedal, Optimization methods for large-scale machine learning, SIAM Review 2018, §5.2).

Setting

Let $(Z,P)$ be a probability space of data points $z$; in the paper $z=(x,y)$ is an input–output pair with distribution $P(x,y)$. The parameter is $w\in\mathbb R^m$ ($m$ is the number of variables). A per-sample loss $\ell(w;z)$ is given with gradient $\nabla\ell(w;z)$ in $w$, and the objective is the expected loss (2.1)

$$J(w)=\int\ell(w;z)\,dP(z).$$

The gradient of the objective is the expected per-sample gradient, $\nabla J(w)=\int\nabla\ell(w;z)\,dP(z)$.

Uniform convexity (4.2): $J$ is twice continuously differentiable and there are constants $0<\lambda<L$ with

$$\lambda\|d\|_2^2\le d^T\nabla^2J(w)\,d\le L\|d\|_2^2\qquad\text{for all } w,d .$$

Then $J$ has a unique minimizer $w^*$.

For a random vector $X\in\mathbb R^m$, $\|\mathrm{Var}(X)\|_1=\mathbb E\|X-\mathbb EX\|_2^2$ is the sum of its componentwise variances. The variance bound (4.22) asks for a constant $\omega$ with

$$\|\mathrm{Var}(\nabla\ell(w;\cdot))\|_1\le\omega\qquad\text{for all } w .$$

The algorithm. Fix sample sizes $n_k\ge1$ and a starting point $w_0$. At iteration $k$ draw a batch $S_k$ of $n_k$ points, independently with law $P$ and independently of earlier batches, form the batch gradient (4.19)

$$g_k=\frac1{n_k}\sum_{i\in S_k}\nabla\ell(w_k;i),$$

and take the dynamic batch steepest descent step (4.24)

$$w_{k+1}=w_k-\frac1L\,g_k .$$

The iterates $w_k$ are random, and expectations below are over all batches.

Formalization targets

Goal: Theorem 4.2

If $n_k\ge a^k$ for all $k$, for some $a>1$, and (4.22) holds, then

$$\mathbb E[J(w_k)-J(w^*)]\le C\rho^k\quad\text{for all }k,\qquad \rho=\max\{1-\lambda/(4L),\,1/a\}<1,\quad C=\max\{J(w_0)-J(w^*),\,2\omega/\lambda\}.$$

The constants are the paper's. The goal also asserts that $J(w_k)$ is integrable for every $k$.

Milestones, in the order the proof uses them

1. (4.5), p. 8: $\nabla J(w)^T\nabla J(w)\ge\lambda[J(w)-J(w^*)]$ for every $w$.
2. Taylor bound, p. 11: $J(w-\frac1Lg)\le J(w)-\frac1L\nabla J(w)^Tg+\frac1{2L}\|g\|^2$ for every $w$ and $g$.
3. (4.25), p. 11: at a fixed point $w$, with $g$ the batch gradient of $n$ i.i.d. draws,

$$\mathbb E[J(w-\tfrac1Lg)]\le J(w)-\tfrac1L\|\nabla J(w)\|^2+\tfrac1{2L}\mathbb E\|g\|^2,\qquad \mathbb E\|g\|^2=\|\nabla J(w)\|^2+\|\mathrm{Var}(g)\|_1 .$$

4. Variance of the batch gradient, p. 12: $\|\mathrm{Var}(g)\|_1\le\|\mathrm{Var}(\nabla\ell(w;\cdot))\|_1/n$.
5. (4.26), p. 12: $\mathbb E[J(w-\tfrac1Lg)]\le J(w)-\tfrac1{2L}\|\nabla J(w)\|^2+\tfrac1{2Ln}\|\mathrm{Var}(\nabla\ell(w;\cdot))\|_1$.
6. (4.27), p. 12: $\mathbb E[J(w-\tfrac1Lg)-J(w^*)]\le(1-\tfrac{\lambda}{2L})(J(w)-J(w^*))+\tfrac{\omega}{2Ln}$.

Milestones 3–6 are the paper's conditional expectations given $w_k$, stated at a fixed point $w$ with the batch drawn afresh.

Significance

Theorem 4.2 is the convergence guarantee of the dynamic sampling strategy: it says that the noise of a mini-batch gradient does not destroy the linear rate of steepest descent, provided the batch grows geometrically. The rate $\rho$ makes the trade-off explicit: the optimization contracts by $1-\lambda/(4L)$ per step, the noise by $1/a$, and the slower of the two governs. From it the paper's Corollary 4.3 bounds the total number of sample-gradient evaluations to reach $\mathbb E[J(w_k)-J(w^*)]\le\epsilon$ by $O(L/(\lambda\epsilon))$, which places dynamic batch methods on the same footing as stochastic gradient descent in the Bottou–Bousquet comparison, while keeping the parallelism of batch methods.

The result is proved in the paper; to our knowledge no machine-checked proof exists. A formalization produces a reusable account of the one-iteration analysis of a mini-batch gradient step (descent lemma, variance of an i.i.d. sample mean of random vectors, conditional expectation over a fresh batch), and of the passage from a conditional one-step recursion to an unconditional bound over a run driven by an infinite i.i.d. array. Corollary 4.3 is not part of this mission: it involves $O(\cdot)$ bounds, a cost model for gradient evaluations and an iteration count treated as a real number.

Difficulty

The arithmetic of the induction on p. 12 is short. The difficulty is in making the probability rigorous. The iterate $w_k$ is random, and the paper's one-step bound (4.27) is a conditional expectation given $w_k$, with $J(w_k)$ on the right-hand side. Turning it into an unconditional recursion requires that the batch of iteration $k$ be independent of $w_k$, that $w_k$ be a measurable function of the earlier batches, and that $J(w_k)$ and $\|g_k\|^2$ be integrable at every step, none of which is automatic for a run driven by an infinite array of draws. A naive formalization that treats $w_k$ as a fixed point, or $g_k$ as an abstract random vector with a postulated variance bound, skips exactly this content.

The variance identity for a sample mean of random vectors in $\mathbb R^m$ and the bound $\|\nabla J(w)\|\le L\|w-w^*\|$ from (4.2) are standard but not packaged in this form in Mathlib.

Formalization scope

• The space is EuclideanSpace ℝ (Fin m). The paper's $\lambda$ is written lam (λ is a Lean keyword). (4.2) is ContDiff ℝ 2 J, 0 < lam < L, and the two-sided bound on fderiv ℝ (fderiv ℝ J) w d d.
• $J$ is defined as the Bochner integral $\int\ell(w;z)\,dP(z)$ for a general per-sample loss $\ell$; the paper's linear predictor $f(w;x)=w^Tx$ and convex loss $l$ are not used by the theorem and are not assumed. The model assumes: $\ell(w;\cdot)$ integrable; $\nabla\ell(w;z)$ the gradient of $\ell(\cdot;z)$ at $w$; $(w,z)\mapsto\nabla\ell(w;z)$ jointly measurable; $\nabla\ell(w;\cdot)$ square-integrable; and $\nabla J(w)=\int\nabla\ell(w;z)\,dP(z)$ (differentiation under the integral, which the paper uses without proof).
• Sampling with replacement. The paper's (3.5) is sampling without replacement from $N$ points; it takes $N\to\infty$ on p. 5, which "also corresponds to the case of sampling with replacement". The formalization draws every point i.i.d. from $P$: draw $i$ of iteration $k$ is $\xi_{k,i}$ and the law of the whole array is Measure.infinitePi over $\mathbb N\times\mathbb N$. The finite-population factor $(N-n_k)/(N-1)$ is not modelled.
• $w^*$ is a given minimizer of $J$; $n_k$ are natural numbers with $a^k\le n_k$ (real powers of a real $a>1$); $\omega$ is a real number.
• The goal asserts integrability of $J(w_k)$ together with the bound, so the inequality cannot be met by the Bochner integral's value $0$ on a non-integrable function. The batch gradient is the mean over $n_k$ draws at the current iterate, and $w_k$ is the random run: a goal with an abstract random $g_k$ satisfying a postulated variance bound, or with $w_k$ a deterministic sequence, would not be this theorem.
• Welcome contributions: the variance of an i.i.d. mean of $\mathbb R^m$-valued random vectors; the descent lemma and gradient-dominance inequality from Hessian bounds; measurability and independence lemmas for processes driven by Measure.infinitePi. All three are reusable beyond this mission.

Selected references

• R. H. Byrd, G. M. Chin, J. Nocedal, Y. Wu, Sample size selection in optimization methods for machine learning, Mathematical Programming 134 (2012) 127–155. https://doi.org/10.1007/s10107-012-0572-5
• L. Bottou, O. Bousquet, The tradeoffs of large scale learning, NIPS 2007. https://papers.nips.cc/paper/3323-the-tradeoffs-of-large-scale-learning
• M. P. Friedlander, M. Schmidt, Hybrid deterministic-stochastic methods for data fitting, SIAM J. Sci. Comput. 34 (2012) A1380–A1405. https://doi.org/10.1137/110830629
• L. Bottou, F. E. Curtis, J. Nocedal, Optimization methods for large-scale machine learning, SIAM Review 60 (2018) 223–311. https://doi.org/10.1137/16M1080173

Motivation

Barak, Goldreich, Impagliazzo, Rudich, Sahai, Vadhan and Yang proved that general-purpose program obfuscation in the virtual black-box sense is impossible (J. ACM 59(2), 2012). A natural question is whether the impossibility proof relativizes, that is, whether it survives when every party gets access to the same oracle. Proposition 4.14 of the paper shows that it does not: there is an oracle relative to which efficient circuit obfuscators exist. This is evidence that the impossibility results are not formal consequences of black-box reasoning, and a further example that relativization is a poor guide to what can be proved.

The construction obfuscates a circuit $C$ by publishing a random image $O_k(C,r)$, and its security comes down to one information-theoretic statement, Claim 4.14.2, restated and proved in Appendix B as Lemma B.1. A random injective function is a pseudorandom generator even against distinguishers that may query the function itself. The proof is a counting (compression) argument in the style of Gennaro and Trevisan's proof that a random permutation is one-way against nonuniform adversaries (FOCS 2000). Arguments of this kind recur in lower bounds for black-box constructions and in the theory of random oracles.

Setting

Fix natural numbers $K$ and $L$ and finite sets $[K]$, $[L]$ of these sizes. A distinguisher $D$ receives an element $y\in[L]$ and may ask an oracle $G:[K]\to[L]$ for values $G(z)$, choosing each query point adaptively from the input and the answers so far; finally it outputs a bit. Formally $D$ is a family $(D_y)_{y\in[L]}$ of query trees: a leaf carries an output bit, and an internal node carries a query point $z\in[K]$ and one subtree for each possible answer in $[L]$. Running $D_y$ against $G$ follows the branch labelled $G(z)$ at each node; $D^G(y)$ is the bit at the leaf reached. The query complexity of $D$ is the largest depth of its trees. Nothing restricts the computation between queries.

Let $G$ be uniformly random among the injective functions $[K]\to[L]$. For a distinguisher $D$ the two acceptance probabilities are

$$p_X(D,G)=\Pr_{x\in[K]}\big[D^G(G(x))=1\big],\qquad p_Y(D,G)=\Pr_{y\in[L]}\big[D^G(y)=1\big],$$

where $x$ and $y$ are uniform. $D$ tries to tell the output $G(x)$ of a random seed from a uniform element of $[L]$ while it may query $G$.

Formalization targets

Goal: Lemma B.1 (Claim 4.14.2)

There is a constant $\delta>0$ such that for all sufficiently large $K$, all $L\ge K^2$, and every $D$ making at most $K^\delta$ oracle queries,

$$\Pr_G\Big[\,\big|p_X(D,G)-p_Y(D,G)\big|\le \tfrac{1}{K^\delta}\Big]\ \ge\ 1-2^{-K^\delta}.$$

The constant $\delta$ is left unspecified, as in the paper; the threshold for $K$ may depend on $\delta$ only.

Milestones

The milestones follow the proof on pp. A:43–A:45, for small $\delta$ and $\gamma=K^{-3\delta}$:

1. an averaging bound: for most sets $S\subseteq[K]$ of size $K^{1-5\delta}$, few runs $D^G(G(x))$, $x\in S$, query $S\setminus\{x\}$;
2. a sampling bound: a random such $S$ estimates $p_X$ within $\frac1{4K^\delta}$;
3. the triangle-inequality chain that turns a violation of the goal into a gap $>\frac1{2K^\delta}$ between $S_G$ and $L_G=[L]\setminus G([K]\setminus S_G)$;
4. inequality (8): a simulator $M$ that reads $G$ only off $S_G$ keeps that gap;
5. the Chernoff count of subsets $T$ that overestimate a Boolean average;
6. Claim B.1.2 in counting form: the $G$ admitting a good $S_G$ inside a fixed $S$ number at most $B\cdot2^{-cK^{1-7\delta}}$, where $B$ is the number of injections;
7. the closing density bound: the bad $G$ have density below $K^{-\delta}$.

Significance

Lemma B.1 is the step that makes Proposition 4.14 work. Once the oracle is fixed everywhere except at the values $O_k(C,\cdot)$, the simulator's only dependence on the remaining randomness is through queries to $G$, and Lemma B.1 says that such a simulator cannot distinguish $G$'s outputs from uniform except with probability $2^{-K^\delta}$ over the oracle. A union bound over circuits and adversaries of bounded description then yields the obfuscator relative to the oracle. More broadly, the lemma is a clean instance of the principle that a random function is pseudorandom against adversaries with few queries to it, which is used in random-oracle and black-box separation arguments.

The paper gives only a sketch, and formalizing it adds more than a check. The sketch proves the density bound $K^{-\delta}$ but asserts $2^{-K^\delta}$; the counting bound supports the stronger statement, but the step is not written. More seriously, Property 2 of Claim B.1.1 as printed (no query of $D^G(G(x))$ lands in $S_G$, including at $x$ itself) cannot be met: a one-query distinguisher that inverts $G$ makes every bad $G$ violate it, so Claim B.1.1 is false as stated and the proof needs repair. As far as the platform's records show, no part of the argument has been machine-checked.

Difficulty

The naive attempt is a union bound: fix $D$, compute the expected gap over $G$, and apply a concentration inequality over $G$. This fails because $D$ queries $G$, so the events "$D^G(G(x))=1$" for different $x$ are correlated through $G$ in ways that depend on $D$'s adaptive strategy. Neither independence nor a bounded-differences argument applies directly, since changing one value of $G$ can change many runs.

The compression argument avoids this, but each of its steps needs care. The set on which $D$'s runs are "independent" must be chosen from a fixed $S$ so that it is cheap to describe. The simulator must answer queries without the part of $G$ being described. The saving from the Chernoff count must exceed the cost of describing $S_G$ inside $S$. Queries a run makes at its own preimage $x$ must be handled separately, which is where the printed argument breaks.

Formalization scope

The query trees are an inductive type QTree K L with constructors out : Bool → QTree K L and query : Fin K → (Fin L → QTree K L) → QTree K L, and $[K]$, $[L]$ are Fin K, Fin L. A distinguisher is D : Fin L → QTree K L, and "at most $K^\delta$ queries" means every D y has depth at most $K^\delta$ (a real power). Distinguishers are deterministic: the probabilities in the goal are over $x$, $y$ and $G$ only. Randomized distinguishers, averaged over their coins, are not covered, and the paper's application fixes the simulator's coins.

Every probability is a counting fraction over a finite uniform sample space: Fin K, Fin L, the embeddings Fin K ↪ Fin L, or the subsets of a given size (Finset.powersetCard). Sizes the paper writes as non-integers are floors or inequalities: $|S|=\lfloor K^{1-5\delta}\rfloor$ and $|S_G|\ge(1-\gamma)|S|$. Each $\Omega(\cdot)$ is an explicit constant $c>0$ that depends only on $\delta$. "Sufficiently small $\delta$" is either an explicit range $0<\delta\le1/100$ (for the elementary steps) or an existential $\delta_0>0$ (for the counting steps), and "sufficiently large $K$" is an explicit threshold $K_0$.

The goal quantifies $\exists\delta>0\ \exists K_0\ \forall K\ge K_0\ \forall L\ge K^2\ \forall D$, so $\delta$ cannot depend on $K$ or $D$. The probability over $G$ is taken outside the absolute value: averaging the gap over $G$ would give a much weaker statement and is ruled out. Non-adaptive distinguishers or a fixed query set would also weaken the goal and are not used.

Milestone 1 is stated in a corrected form: it excludes the query at $x$ itself and reads the misprint $4/K^{-4\delta}$ as $4K^{-4\delta}$. Claim B.1.1 is not a milestone because it is false as printed. Milestones 4 and 6 use the printed Property 2. Contributions repairing the link between the corrected averaging step and the compression step are welcome, as are sorry-free proofs of the generic concentration milestones (2 and 5), which are reusable beyond this mission.

Selected references

• B. Barak, O. Goldreich, R. Impagliazzo, S. Rudich, A. Sahai, S. Vadhan, K. Yang, On the (Im)possibility of Obfuscating Programs, Journal of the ACM 59(2), 2012. https://doi.org/10.1145/2160158.2160159
• R. Gennaro, L. Trevisan, Lower bounds on the efficiency of generic cryptographic constructions, FOCS 2000. https://doi.org/10.1109/SFCS.2000.892119
• W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58(301), 1963. https://doi.org/10.1080/01621459.1963.10500830

Motivation

Multistage stochastic linear programs model sequential decisions under uncertainty: capacity and reservoir planning, hydro-thermal scheduling, inventory and asset–liability management. When the data process is stagewise independent, the problem decomposes by dynamic programming into one linear program per stage, coupled through expected cost-to-go functions. These functions are convex and piecewise linear, and the stochastic dual dynamic programming (SDDP) method of Pereira and Pinto (1991) approximates them from below by cutting planes. SDDP is the standard solution method in the long-term planning of hydro-dominated power systems, and its convergence theory determines what the bounds it reports actually mean.

Shapiro's paper (Optimization Online 2009/12/2509; European J. Oper. Res. 209(1), 2011, doi:10.1016/j.ejor.2010.08.007) analyses SDDP applied to a sample average approximation (SAA) of the true problem, with all of the data $(c_t, A_t, B_t, b_t)$ random. Its convergence result, Proposition 3.1, asserts finite convergence with probability one when the forward scenarios are subsampled independently. A related almost-sure finite convergence theorem for a different algorithm (DOASA, with randomness only in the right-hand sides and cut sharing across outcomes) is due to Philpott and Guan (2008); it is posed as a separate mission on this platform and is not restated here.

Setting

There are $T\ge 2$ stages. The decision $x_t\in\mathbb R^{n_t}$ satisfies $x_t\ge 0$ and, at the first stage, $A_1x_1=b_1$ with deterministic data $(c_1,A_1,b_1)$. For $t=2,\dots,T$ the data are replaced by a sample $\tilde\xi_t^j=(\tilde c_{tj},\tilde A_{tj},\tilde B_{tj},\tilde b_{tj})$, $j=1,\dots,N_t$, each with probability $1/N_t$, independently across stages, and the stage-$t$ constraint is $\tilde B_{tj}x_{t-1}+\tilde A_{tj}x_t=\tilde b_{tj}$. The SAA cost-to-go functions are defined backwards from $\widetilde{\mathcal Q}_{T+1}\equiv 0$:

$$\widetilde Q_{tj}(x_{t-1})=\inf_{x_t\ge0}\big\{\tilde c_{tj}^\top x_t+\widetilde{\mathcal Q}_{t+1}(x_t):\tilde B_{tj}x_{t-1}+\tilde A_{tj}x_t=\tilde b_{tj}\big\},\qquad \widetilde{\mathcal Q}_t=\frac1{N_t}\sum_{j=1}^{N_t}\widetilde Q_{tj}.$$

A scenario is a choice $(j_2,\dots,j_T)$; there are $N=\prod_t N_t$ of them, each of probability $1/N$. A policy $\bar x_t=\bar x_t(\tilde\xi_{[t]})$ depends only on the outcomes up to stage $t$; it is optimal for the SAA problem if it is feasible on every scenario and its expected cost $\frac1N\sum_{\text{scenarios}}\sum_t\tilde c_t^\top\bar x_t$ is minimal.

SDDP keeps, for each stage, a finite set of cuts $\alpha+\beta^\top x$ whose maximum $\mathfrak Q_{t+1}$ lies below $\widetilde{\mathcal Q}_{t+1}$. An iteration has a forward step: $M$ scenarios are sampled, and along each of them the decisions $\bar x_t$ solve the stage problems with $\mathfrak Q_{t+1}$ in place of $\widetilde{\mathcal Q}_{t+1}$, (3.13)–(3.14). It also has a backward step: from $t=T-1$ down to $1$, at each trial point $\bar x_t$ the stage-$(t+1)$ problems with the current cuts are solved for all $N_{t+1}$ outcomes, and the cut (3.17) $\ell(x)=\underline{\widetilde{\mathcal Q}}_{t+1}(\bar x_t)+\tilde g^\top(x-\bar x_t)$ is added, where $\tilde g$ averages $-\tilde B^\top\pi$ over basic optimal (extreme-point) dual solutions $\pi$.

Formalization targets

Goal: Proposition 3.1

Suppose the forward scenarios are drawn independently and uniformly from the SAA scenarios, (A1) holds ((3.13) and (3.14) have finite optimal values for every scenario at every iteration), and the backward steps use basic optimal dual solutions. Then

$$P\Big(\exists K\ \forall k\ge K:\ \text{the forward policy defined by }\mathfrak Q^k_2,\dots,\mathfrak Q^k_{T}\text{ is optimal for the SAA problem}\Big)=1 .$$

The goal fixes no iteration count, no rate and no number of forward scenarios $M\ge1$.

Milestones, in attack order

1. Attainment: an LP of the form (3.13)/(3.14) with finite optimal value has an optimal solution.
2. Cut validity: every cut lies below $\widetilde{\mathcal Q}_{t+1}$ on reachable decisions, and $\underline{\widetilde Q}_{tj}\le\widetilde Q_{tj}$.
3. Lower bound: the optimal value $\underline\vartheta_k$ of (3.13) is at most the SAA optimal value.
4. Finitely many cutting planes (3.17) for a fixed next-stage cut set, uniformly in the trial point.
5. Finitely many realizations of the $\mathfrak Q_t$ and of first-stage solutions; along each run the cut sets are eventually constant.
6. A policy is optimal for the SAA problem if and only if it satisfies the dynamic programming conditions (3.18) on every scenario.
7. With probability one every SAA scenario is drawn at infinitely many iterations.

Significance

The result separates SDDP's sampling from its convergence: on a finite scenario tree, independent subsampling of forward paths suffices for the method to stop at an optimal policy, without ever enumerating the tree. It explains why the lower bound $\underline\vartheta_k$ eventually equals the SAA optimal value, which is what makes the gap-based stopping rules of the paper (§3, Remarks 4–6) meaningful. The paper's closing remark stresses that without independence of the forward scenarios there is no guarantee of convergence.

The proposition is proved in the paper. No machine-checked proof of it, or of any SDDP convergence theorem, exists to our knowledge. Formalizing it requires a precise account of what the method is: which dual solutions, which forward solutions, which order of updates. Several of these points are left implicit on the page.

Difficulty

Finiteness of the cut universe (milestones 4–5) is a statement about extreme points of dual polyhedra whose dimension grows with the cut sets of the next stage, so it must be organized stage by stage from $T$ down. The central difficulty is the last step of the argument. Once the approximations have stopped changing, one must show that the stable cuts are exact where the forward policy goes, so that the forward policy satisfies (3.18). The obvious argument, "if (3.18) fails at the last stage where it fails, the next cut there increases $\mathfrak Q$", does not work as printed: (3.18) holding at later stages does not by itself make the next-stage approximation exact at the trial point. Closing this step is where the conventions on forward solutions and on sampling listed below become essential.

Formalization scope

The Lean development is in the namespace ShapiroSDDP.Convergence. Stages are numbered $1,\dots,T$; the data of stage $t+1$ are stored under index $t$ (the coupling matrix is indexed by the decision it multiplies); V t is $\widetilde{\mathcal Q}_{t+1}$, with V t ≡ 0 for $t\ge T$. Cost-to-go values are real infima, used only on reachable decisions. The explicit readings are:

• cost-to-go functions finite valued on reachable decisions (the paper: everywhere; weaker);
• initial cut sets: a parameter, nonempty and valid on reachable decisions, with $\{(0,0)\}$ at stage $T$;
• forward solutions from a deterministic oracle that reads the cut set and returns an optimal solution whenever one exists; the goal holds for every such oracle;
• basic optimal duals: extreme points of the dual feasible region, chosen arbitrarily; the goal holds for every run;
• (A1) as a hypothesis on the run; $M\ge1$ forward scenarios per iteration, i.i.d. uniform (independence via iIndepFun);
• forward step before backward step within an iteration, with cuts at that iteration's trial points.

Optimality of a policy is defined by expected cost, never by (3.18), so that milestone 6 is not definitional. Sampling is stated as i.i.d. uniform draws, not as "every scenario recurs", which is milestone 7. All of $c,A,B,b$ depend on the outcome. If some $\tilde A_{tj}$ lacks full row rank, no basic dual solution exists and no run exists; a sorry-free witness instance shows that all hypotheses of the goal can hold together.

Useful infrastructure: LP weak and strong duality (LinearOptimization.lp_weak_duality, LinearOptimization.lp_strong_duality exist on the platform in their own encoding), finiteness of extreme points of polyhedra, attainment for polyhedral objectives, and the second Borel–Cantelli lemma (ProbabilityTheory.measure_limsup_eq_one). Proofs of any milestone, and reusable lemmas on LPs with cut epigraphs, are welcome.

Selected references

• A. Shapiro, Analysis of Stochastic Dual Dynamic Programming Method, Optimization Online preprint 2009/12/2509; European Journal of Operational Research 209(1):63–72, 2011. https://optimization-online.org/2009/12/2509/ · https://doi.org/10.1016/j.ejor.2010.08.007
• M. V. F. Pereira, L. M. V. G. Pinto, Multi-stage stochastic optimization applied to energy planning, Mathematical Programming 52:359–375, 1991. https://doi.org/10.1007/BF01582895
• A. B. Philpott, Z. Guan, On the convergence of stochastic dual dynamic programming and related methods, Operations Research Letters 36(4):450–455, 2008. https://doi.org/10.1016/j.orl.2008.01.013
• J. E. Kelley, The cutting-plane method for solving convex programs, J. SIAM 8(4):703–712, 1960. https://doi.org/10.1137/0108053
• A. Shapiro, D. Dentcheva, A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751

Motivation

Many graph algorithms run in time proportional to the number of edges. A sparsifier of a weighted graph $G$ is a graph $H$ on the same vertices with far fewer edges that approximates $G$ for the purpose at hand, so that the algorithm can be run on $H$ instead. Benczúr and Karger (1996) showed that every graph has a sparsifier with $O(n\log n/\varepsilon^2)$ edges preserving the weight of every cut up to a factor $1\pm\varepsilon$. Spielman and Teng (2004) introduced the stronger spectral notion, in which the Laplacian quadratic form is preserved for every real vector, not only for cut indicators; their sparsifiers had $O(n\log^c n)$ edges for a large constant $c$ and were the first step of their nearly-linear-time solvers for symmetric diagonally dominant linear systems.

Spielman and Srivastava (arXiv:0803.0929, STOC 2008, SIAM J. Comput. 2011) proved that independent sampling of $O(n\log n/\varepsilon^2)$ edges, each edge with probability proportional to its weight times its effective resistance, yields a spectral sparsifier. The result improved both earlier bounds, replaced a recursive partitioning construction by a one-line sampling rule, and made effective resistance a standard tool in graph algorithms. Batson, Spielman and Srivastava (arXiv:0808.0163) later obtained $O(n/\varepsilon^2)$ edges deterministically, by a slower method built on the same matrix $\Pi$.

Setting

Let $G=(V,E,w)$ be a connected weighted undirected graph with $n=|V|$ vertices, $m=|E|$ edges and weights $w_e>0$. Orient every edge arbitrarily, so that it has a head and a tail (distinct vertices).

• The incidence matrix $B\in\mathbb R^{m\times n}$ has $B(e,v)=1$ if $v$ is the head of $e$, $-1$ if $v$ is its tail, and $0$ otherwise; $b_e$ denotes its row for $e$. $W$ is the diagonal $m\times m$ matrix with $W(e,e)=w_e$.
• The Laplacian is $L=B^{\mathsf T}WB$, with quadratic form $x^{\mathsf T}Lx=\sum_e w_e\,(x(\mathrm{head}\,e)-x(\mathrm{tail}\,e))^2$.
• $L^{+}$ is the Moore–Penrose pseudoinverse of $L$: if $L=\sum_{i=1}^{n-1}\lambda_iu_iu_i^{\mathsf T}$ over its nonzero eigenvalues, then $L^{+}=\sum_{i=1}^{n-1}\lambda_i^{-1}u_iu_i^{\mathsf T}$.
• The effective resistance of the edge $e$ is $R_e=b_eL^{+}b_e^{\mathsf T}$: the potential difference across $e$ when a unit current enters at one end and leaves at the other, the edges being resistors of conductance $w_e$.
• $\Pi=W^{1/2}BL^{+}B^{\mathsf T}W^{1/2}$ is an $m\times m$ matrix with $\Pi(e,e)=w_eR_e$.
• Sparsify$(G,q)$ draws $q$ edges independently with replacement, the edge $e$ with probability $p_e=w_eR_e/\sum_f w_fR_f$, and gives $e$ the weight $w_e/(qp_e)$ for each time it is drawn. Its output $H$ has Laplacian $\tilde L=B^{\mathsf T}W^{1/2}SW^{1/2}B$, where $S$ is the random diagonal matrix with $S(e,e)=\#\{\text{draws of }e\}/(qp_e)$.

Formalization targets

Goal: Theorem 1

There are an absolute constant $C$ and a threshold $N_0$ such that, for every $n\ge N_0$, every connected weighted graph on $n$ vertices and every $1/\sqrt n<\varepsilon\le1$, with $q=\lceil 9C^2n\log n/\varepsilon^2\rceil$, with probability at least $1/2$

$$\forall x\in\mathbb R^n:\qquad (1-\varepsilon)\,x^{\mathsf T}Lx\;\le\;x^{\mathsf T}\tilde Lx\;\le\;(1+\varepsilon)\,x^{\mathsf T}Lx .$$

The constant $C$ is left unfixed; the statement asserts the shape $q=O(n\log n/\varepsilon^2)$ with the paper's explicit dependence on $C$.

Milestones

1. Lemma 3 (four parts): $\Pi$ is an orthogonal projection; $\operatorname{im}\Pi=\operatorname{im}W^{1/2}B$; the eigenvalues of $\Pi$ are $1$ with multiplicity $n-1$ and $0$ with multiplicity $m-n+1$; $\Pi(e,e)=\|\Pi(\cdot,e)\|^2$.
2. Lemma 4: for a nonnegative diagonal $S$, $\|\Pi S\Pi-\Pi\Pi\|_2\le\varepsilon$ implies $(1-\varepsilon)x^{\mathsf T}Lx\le x^{\mathsf T}B^{\mathsf T}W^{1/2}SW^{1/2}Bx\le(1+\varepsilon)x^{\mathsf T}Lx$ for all $x$.
3. Lemma 5 (Rudelson–Vershynin): for independent samples $y_1,\dots,y_q$ of a random vector with $\|y\|_2\le M$ and $\|\mathbb E\,yy^{\mathsf T}\|_2\le1$, and $q\ge2$,

$$\mathbb E\Big\|\frac1q\sum_{j=1}^q y_jy_j^{\mathsf T}-\mathbb E\,yy^{\mathsf T}\Big\|_2\le CM\sqrt{\frac{\log q}{q}}\quad\text{whenever the right side is }<1.$$

Significance

Theorem 1 says that every weighted graph is spectrally approximated by a reweighted subgraph with $O(n\log n/\varepsilon^2)$ edges. A spectral approximation preserves cut weights, the eigenvalues of the Laplacian up to $1\pm\varepsilon$, effective resistances, and the condition number of $L$ as a preconditioner, so any algorithm whose output depends on these quantities can run on $H$. Combined with fast approximate computation of effective resistances (the second mission of this series), it gives a nearly-linear-time construction, and it is the sampling step used in Laplacian solvers, in sparsification of sums of rank-one matrices, and in leverage-score sampling for regression, where $w_eR_e$ is exactly the statistical leverage of a row.

The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission formalizes the statement and the paper's proof structure: the linear algebra of $\Pi$ (Lemma 3), the deterministic reduction from quadratic forms to a spectral-norm bound (Lemma 4), and the matrix concentration inequality (Lemma 5), which is the substantive analytic input and is itself a reusable result about sums of independent rank-one matrices.

Difficulty

The deterministic part is linear algebra over the pseudoinverse. The obstacle is concentration: the expected Laplacian of $H$ equals $L$, but bounding the deviation uniformly over all $x\in\mathbb R^n$ is a statement about the spectral norm of a random matrix, and a union bound over a net of directions costs a factor of $n$ in the sample count rather than $\log n$. Scalar Chernoff bounds per cut, which suffice for cut sparsifiers, do not give the spectral statement. Lemma 5 is the matrix inequality that removes this loss, and no inequality of this kind (a concentration bound for the spectral norm of a sum of independent random matrices) is in Mathlib.

Formalization scope

All declarations sit in the namespace EffResSparsify.Sampling.

• Graphs. A structure WGraph V E with orientation maps head, tail : E → V, weights w : E → ℝ, and the fields head e ≠ tail e (no loops) and 0 < w e. Parallel edges are allowed; nothing in §3 uses simplicity. Connectivity is a separate hypothesis on the underlying simple graph and includes $V\ne\emptyset$. In Theorem 1 the vertex type is Fin n; the edge type is an arbitrary finite type.
• Pseudoinverse. $L^{+}$ is the matrix of the published Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv of $x\mapsto Lx$ on Euclidean $\mathbb R^V$; it equals the spectral formula above and is the gauge-fixed inverse, never "some solution of $Lx=y$".
• Sampling. $p_e$ is defined as $w_eR_e/\sum_f w_fR_f$; the identity $\sum_f w_fR_f=n-1$ is part of the proof. An outcome of Sparsify is a sequence in $E^q$ with probability $\prod_i p_{s_i}$, and probabilities and expectations are finite sums over $E^q$, with no measure theory.
• Norms and logarithms. $\|\cdot\|_2$ is the $\ell_2$ operator norm on matrices (Matrix.Norms.L2Operator); vector norms in Lemma 5 are Euclidean; $\log$ is natural (the base is absorbed into $C$).
• Constants. In Theorem 1, $\exists C>0,\ \exists N_0,\ \forall n\ge N_0$ precede the graph and $\varepsilon$; the sample count is $\lceil 9C^2n\log n/\varepsilon^2\rceil$, rounded up because the printed value is not an integer. In Lemma 5, $\exists C>0$ precedes the dimension, the distribution, $M$ and $q$.
• Corrected statement. Lemma 5 as printed, with right side $\min(CM\sqrt{\log q/q},1)$, is false (at $q=1$ the bound is $0$). The formal milestone is Rudelson and Vershynin's own Theorem 3.1: $q\ge2$, and the bound $a=CM\sqrt{\log q/q}$ holds when $a<1$. It is stated for finitely supported distributions, which is all Theorem 1 uses. Theorem 1 applies it with $a\le\varepsilon/2$, so the correction does not affect the goal.
• Not a trivialization. Theorem 1 does not take Lemma 5, a bound on $\mathbb E\|\Pi S\Pi-\Pi\|_2$, or a free sample count as a hypothesis; a statement with any of these, or with "$\exists q$" in place of $\lceil 9C^2n\log n/\varepsilon^2\rceil$, is a different theorem.

Reusable beyond this mission: the weighted Laplacian with its pseudoinverse and effective resistances, and Lemma 5, which applies to any sampling scheme for sums of rank-one matrices (leverage-score sampling, column subset selection). Contributions toward a matrix Chernoff or Rudelson-type inequality in Mathlib are welcome.

Selected references

• D. A. Spielman, N. Srivastava, Graph Sparsification by Effective Resistances, arXiv:0803.0929v4, 2009; SIAM J. Comput. 40(6), 2011. https://arxiv.org/abs/0803.0929, https://doi.org/10.1137/080734029
• M. Rudelson, R. Vershynin, Sampling from large matrices: an approach through geometric functional analysis, J. ACM 54(4), 2007. https://doi.org/10.1145/1255443.1255449
• M. Rudelson, Random vectors in the isotropic position, J. Funct. Anal. 164(1), 1999. https://doi.org/10.1006/jfan.1998.3384
• A. A. Benczúr, D. R. Karger, Approximating s-t minimum cuts in Õ(n²) time, STOC 1996. https://doi.org/10.1145/237814.237827
• D. A. Spielman, S.-H. Teng, Spectral sparsification of graphs, SIAM J. Comput. 40(4), 2011 (arXiv:0808.4134). https://arxiv.org/abs/0808.4134
• J. Batson, D. A. Spielman, N. Srivastava, Twice-Ramanujan sparsifiers, SIAM J. Comput. 41(6), 2012 (arXiv:0808.0163). https://arxiv.org/abs/0808.0163

Motivation

Markov decision processes model sequential decisions under uncertainty, and their optimal policies are computed from transition probabilities that in practice are estimated from data. Optimal policies can be sensitive to estimation error in those probabilities. Robust dynamic programming replaces each transition law by a set of plausible laws and evaluates a policy by its worst-case expected reward over that set. Garud Iyengar's Robust dynamic programming (CORC Tech Report TR-2002-07, 2002, rev. 2004; Mathematics of Operations Research 30(2), 2005) set up this theory for countable state spaces and history-dependent policies. It isolated the Rectangularity assumption under which the robust problem keeps a Bellman equation. In the same period, Nilim and El Ghaoui studied robust control of Markov decision processes with finite state spaces.

Timeline:

• 1968, 1973. Satia (PhD thesis) and Satia and Lave (Operations Research 21) treat finite-state, finite-action Markov decision processes with uncertain transition probabilities. They state the max–min optimality equation and the optimality of stationary policies, assuming convex uncertainty sets, and do not prove that the solution of the equation is the robust value function.
• 2001. Bagnell, Ng and Schneider analyse robust policies when the decision maker is restricted to stationary policies.
• 2002–2005. Iyengar (this paper) and Nilim and El Ghaoui (Operations Research 53, 2005) give the rectangular theory. Iyengar proves the discounted robust Bellman equation for countable state spaces, against history-dependent randomized policies and an adversary that may change the law at every visit.

Setting

A discounted ambiguous Markov decision process has a countable state set $\mathcal S$, for each state $s$ a nonempty set $\mathcal A(s)$ of admissible actions, for each admissible pair $(s,a)$ a nonempty set $\mathcal P(s,a)$ of probability measures on $\mathcal S$ (the ambiguity set), a bounded reward $r(s,a,s')$ and a discount factor $\lambda\in(0,1)$. Decisions are made at epochs $t=0,1,2,\dots$.

A policy $\pi=(d_0,d_1,\dots)$ maps each history $h_t=(s_0,a_0,\dots,s_t)$ to a probability measure on $\mathcal A(s_t)$. $\Pi$ is the set of all such policies. A deterministic Markov policy plays $d_t(s_t)$ for maps $d_t:\mathcal S\to\mathcal A$ with $d_t(s)\in\mathcal A(s)$. A stationary policy uses one such rule $d$ at every epoch.

Under Rectangularity, the adversary picks a law $p\in\mathcal P(s_t,a_t)$ separately at every epoch and history, and may pick a different law each time a state–action pair recurs. This is the dynamic model, and the set of path measures it generates is $\mathcal T^\pi$. In the static model the adversary fixes one $\bar p_{sa}\in\mathcal P(s,a)$ per pair. The robust value of a policy and the robust value function are

$$V^\pi_\lambda(s)=\inf_{\mathbf P\in\mathcal T^\pi}\mathbf E^{\mathbf P}\Big[\sum_{t=0}^\infty\lambda^t r(s_t,d_t(h_t),s_{t+1})\Big],\qquad V^*_\lambda(s)=\sup_{\pi\in\Pi}V^\pi_\lambda(s).$$

Let $\mathbf V$ be the bounded functions on $\mathcal S$ with $\|V\|=\sup_s|V(s)|$. For a set $\mathcal D$ of deterministic Markov rules, the robust Bellman operator is

$$\mathcal L_{\mathcal D}V(s)=\sup_{d\in\mathcal D}\ \inf_{p\in\mathcal P(s,d(s))}\mathbf E^p\big[r(s,d(s),s')+\lambda V(s')\big].$$

Formalization targets

Goal: Corollary 2(b)

$$V^*_\lambda(s)=\sup_{a\in\mathcal A(s)}\ \inf_{p\in\mathcal P(s,a)}\mathbf E^p\big[r(s,a,s')+\lambda V^*_\lambda(s')\big],\qquad s\in\mathcal S,$$

$V^*_\lambda$ is the only bounded solution of this equation, and for every $\epsilon>0$ some stationary deterministic policy $\pi^\epsilon$ has $V^{\pi^\epsilon}_\lambda\ge V^*_\lambda-\epsilon$.

Milestones

1. Theorem 5(a). $\mathcal L_{\mathcal D}$ maps $\mathbf V$ to $\mathbf V$ and $\|\mathcal L_{\mathcal D}U-\mathcal L_{\mathcal D}V\|\le\lambda\|U-V\|$.
2. Theorem 5(b). For $\mathcal D=\prod_s\mathcal D(s)$, the equation $\mathcal L_{\mathcal D}V=V$ has a unique bounded solution, equal to the robust value over deterministic Markov policies with rules in $\mathcal D$.
3. Corollary 2(a). The robust value of a stationary policy $(d,d,\dots)$ is the unique bounded solution of $V(s)=\inf_{p\in\mathcal P(s,d(s))}\mathbf E^p[r(s,d(s),s')+\lambda V(s')]$.
4. Theorem 4. $V^*_\lambda(s)=\sup_{\pi\in\Pi_{MD}}V^\pi_\lambda(s)$.
5. Lemma 3. For a stationary policy, the dynamic and static models give the same value.
6. Lemma 2. The value of a stationary policy is the optimal solution of the robust program (31).
7. Lemma 1, first claim. The output of robust value iteration is within $\epsilon/4$ of $V^*_\lambda$.

Significance

Corollary 2(b) justifies computing the robust value function by solving a state-wise max–min equation. Value iteration, policy iteration and their approximations all rely on that equation. It also shows that a decision maker facing a history-dependent adversary loses at most $\epsilon$ by committing to a stationary deterministic rule. Corollary 2(a) and Lemma 2 make robust policy evaluation a fixed point problem and a robust optimization problem. Lemma 3 shows that, for stationary policies, the dynamic model costs nothing relative to the static model, in which the true transition law is fixed but unknown.

The results are proved on paper. The page proves Theorem 4 only by citation to Puterman's non-robust arguments. No machine-checked proof of any of them is known. The platform has finite-state analogues posed by the Nilim–El Ghaoui and Satia–Lave missions, which compare only stationary or Markov controllers. This mission poses the countable, history-dependent version, and proving it would establish them in this generality.

Difficulty

The contraction property is a state-by-state $\epsilon$-argument. The hard step is to identify the fixed point with the value of the game against all history-dependent randomized policies. The adversary's choices at different epochs interact only through Rectangularity, so splitting the infimum over path measures into a first-step infimum and a continuation infimum must be justified for an infinite horizon, uncountably many adversary strategies and no attainment of the infima. The ambiguity sets need not be convex or closed. The naive route, "take the minimizing law at each state", is unavailable, and every bound must be carried with an $\epsilon$ slack. Truncating the infinite sum needs the uniform reward bound. Theorem 4 needs a separate argument that randomization and history dependence do not help the decision maker against the dynamic adversary.

Formalization scope

States and actions are countable Lean types; $\mathcal A(s)$ and $\mathcal P(s,a)$ are sets, assumed nonempty, with no convexity or closedness. Laws are PMFs and $\mathbf E^p[f]=\sum_x p(x)f(x)$ as a tsum. The rewards satisfy $|r(s,a,s')|\le R$ on admissible actions. This is the reading of the page's "$\sup r=R<\infty$", which its bounds $\pm R/(1-\lambda)$ require. The discount factor satisfies $0<\lambda<1$. Epochs start at $0$, so the first reward is undiscounted.

A policy maps $(n, h_n)$ to a PMF supported on $\mathcal A(s_n)$. The dynamic adversary maps $(n,h_n,a)$ to a law in $\mathcal P(s_n,a)$. The path law is built by PMF.bind, and the discounted reward is $\sum_t\lambda^t\mathbf E[r(s_t,a_t,s_{t+1})]$, which converges absolutely. Values are real infima and suprema over nonempty families bounded by $R/(1-\lambda)$, so no junk value arises. $\mathbf V$ is the predicate "bounded", and $\|\cdot\|$ is a supremum (the page writes max). All uniqueness claims are uniqueness among bounded functions.

$V^*_\lambda$ is a supremum over all history-dependent randomized policies. Defining it over deterministic Markov or stationary policies would make Theorem 4 trivial and weaken the goal, so it is ruled out. The adversary in $V^\pi_\lambda$ is the dynamic one; the static adversary appears only in Lemma 3.

The mission deviates from the page in three places:

• Theorem 5(b) is stated for product sets $\mathcal D=\prod_s\mathcal D(s)$. For an arbitrary $\mathcal D$ the printed statement fails, because its proof pastes $\epsilon$-greedy actions state by state. Both uses in Corollary 2 are products.
• Lemma 3 is stated for randomized Markov rules, which is the page's "any decision rule". The page proves it for deterministic rules.
• Lemma 2 adds $\sum_s\alpha(s)<\infty$ and restricts the program to bounded $V$.

Only the first claim of Lemma 1 is posed. Its second claim, that an $\epsilon/2$-greedy rule is $\epsilon$-optimal, is false as printed.

A complete development needs a general toolkit that is reusable beyond this mission: path laws of countable controlled processes with history-dependent policies, a uniform $\epsilon$-optimal selection argument for real infima over arbitrary sets, and the Banach fixed point theorem on bounded functions (Mathlib's ContractingWith). Proofs of individual milestones are welcome in any order. Theorem 5(a) is the natural entry point.

Selected references

• G. Iyengar, Robust dynamic programming, CORC Tech Report TR-2002-07, Columbia University, 2002 (rev. May 4, 2004); published in Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• A. Nilim and L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• J. K. Satia and R. E. Lave, Markovian decision processes with uncertain transition probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• J. A. Bagnell, A. Y. Ng and J. Schneider, Solving uncertain Markov decision problems, Tech. Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001. https://www.ri.cmu.edu/publications/solving-uncertain-markov-decision-problems/
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

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