Machine Learning

Motivation

Gradient descent on a smooth function $f:\mathbb R^d\to\mathbb R$ converges at a linear rate (the optimality gap shrinks by a constant factor each step) under strong convexity. Many problems in machine learning and statistics are not strongly convex: least squares with a rank-deficient design, logistic regression on separable or degenerate data, and some non-convex objectives. Over roughly 25 years several weaker conditions were proposed that still give linear convergence. Examples are the error bound of Luo and Tseng, restricted strong convexity, essential strong convexity, weak strong convexity, and quadratic growth (also called optimal or semi-strong convexity). Each came with its own proof, usually assuming convexity. How these conditions relate to one another was rarely made explicit.

Karimi, Nutini and Schmidt (arXiv:1608.04636, ECML PKDD 2016) put the Polyak–Łojasiewicz (PL) inequality (Polyak, 1963) at the centre. Their Theorem 2 orders seven conditions by strength for functions with a Lipschitz gradient, without convexity. It shows that PL is equivalent to the error bound and implies quadratic growth. For convex functions it shows that the four weakest conditions coincide. The equivalence of EB and PL is a special case of a result of Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234, Theorem 5). Zhang (arXiv:1606.00269) independently related RSI, EB, PL and QG.

Setting

Let $f:\mathbb R^d\to\mathbb R$ be differentiable with gradient $\nabla f$. The paper's standing assumptions (§2, p. 2) are:

1. $\nabla f$ is $L$-Lipschitz: $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for all $x,y$, with $L>0$;
2. the solution set $\mathcal X^*=\{x:\ f(x)\le f(y)\ \forall y\}$ is non-empty. Write $f^*$ for the optimal value.

For every $x$, $x_p$ denotes a projection of $x$ onto $\mathcal X^*$: a point of $\mathcal X^*$ at distance $\operatorname{dist}(x,\mathcal X^*)$ from $x$. Each of the following conditions involves a constant $\mu>0$, which may differ between conditions (Appendix A, pp. 11–12):

• SC (strong convexity): $f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle+\frac\mu2\|y-x\|^2$ for all $x,y$.
• ESC (essential strong convexity): the same inequality for all $x,y$ with $x_p=y_p$.
• WSC (weak strong convexity): $f^*\ge f(x)+\langle\nabla f(x),x_p-x\rangle+\frac\mu2\|x_p-x\|^2$ for all $x$.
• RSI (restricted secant inequality): $\langle\nabla f(x),x-x_p\rangle\ge\mu\|x_p-x\|^2$ for all $x$.
• EB (error bound): $\|\nabla f(x)\|\ge\mu\|x_p-x\|$ for all $x$.
• PL (Polyak–Łojasiewicz): $\frac12\|\nabla f(x)\|^2\ge\mu(f(x)-f^*)$ for all $x$.
• QG (quadratic growth): $f(x)-f^*\ge\frac\mu2\|x_p-x\|^2$ for all $x$.

Formalization targets

Goal: Theorem 2 (p. 3)

Read each condition as "it holds for some $\mu>0$". For $f$ with a Lipschitz-continuous gradient,

$$(SC)\to(ESC)\to(WSC)\to(RSI)\to(EB)\equiv(PL)\to(QG),$$

and if $f$ is also convex,

$$(RSI)\equiv(EB)\equiv(PL)\equiv(QG).$$

The goal states no constants, because the constant may change along the chain.

Milestones: the implications of Appendix A, with their constants

The appendix proves a subset of the arrows, each with an explicit constant. The rest follow by transitivity.

$$\text{SC}(\mu)\Rightarrow\text{ESC}(\mu),\quad \text{ESC}(\mu)\Rightarrow\text{WSC}(\mu),\quad \text{WSC}(\mu)\Rightarrow\text{RSI}(\mu/2),\quad \text{RSI}(\mu)\Rightarrow\text{EB}(\mu),$$ $$\text{EB}(\mu)\Rightarrow\text{PL}(\mu^2/L),\quad \text{PL}(\mu)\Rightarrow\text{QG}(\mu),\quad \text{PL}(\mu)\Rightarrow\text{EB}(\mu),\quad \text{QG}(\mu)+\text{convex}\Rightarrow\text{RSI}(\mu/2).$$

One further milestone is display (20). Under PL, $g=\sqrt{f-f^*}$ satisfies $\|\nabla g(x)\|\ge\sqrt{\mu/2}$ at every $x\notin\mathcal X^*$.

Significance

The result. Theorem 2 shows that QG is the weakest of the seven conditions. QG alone does not rule out non-global local minima, so it cannot guarantee that gradient descent reaches a global minimizer. Among the conditions considered, PL and the equivalent EB are therefore the most general that still give linear convergence to a global minimum. The paper's Theorem 1 gives that rate under PL with a one-paragraph proof. For convex $f$, RSI (there called restricted strong convexity), EB, PL and QG are one condition. A rate proved under any of them transfers to the others, up to the constants of the milestones.

Formalizing it. The result is proved on paper, and the arrows of Appendix A are short, except PL → QG. A machine-checked version adds three things. It fixes a precise meaning for $x_p$ when $\mathcal X^*$ is not convex and a nearest point is not unique. It records the correct constant in EB → PL: the printed text says $\mu/L$, while the displayed argument yields $\mu^2/L$. It puts PL → QG for non-convex $f$ on a checked footing; the acknowledgments note an earlier error in this proof. No formalization of these implications is known to be on the platform or in Mathlib.

Difficulty

Most arrows are one-line rearrangements or the Cauchy–Schwarz inequality. EB → PL also needs the quadratic upper bound implied by the Lipschitz gradient, and $\nabla f(x_p)=0$ at a global minimizer.

The obstacle is PL → QG without convexity. The natural first idea fails. Integrating along the segment from $x$ to $x_p$ uses no information from PL, because the gradient along that segment is unrelated to the gap $f-f^*$. The implication is global: it converts a pointwise bound on the gradient into a lower bound on $f$ in terms of the distance to a possibly non-convex set $\mathcal X^*$. Any proof has to bound the distance to $\mathcal X^*$ by the length of some path into it that is controlled by $f$. Building such a path in Lean, with its existence, its arrival at $\mathcal X^*$ in finite time and a bound on its length, needs analysis that is not yet assembled in Mathlib for this purpose.

Formalization scope

• Space. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d), abbreviated E d. Gradients are Mathlib's gradient. The Lipschitz gradient is the literal hypothesis ∀ x y, ‖gradient f x - gradient f y‖ ≤ L * ‖x - y‖ with 0 < L, together with Differentiable ℝ f.
• Solution set. Non-emptiness is carried by a global minimizer xstar with ∀ y, f xstar ≤ f y, and $f^*$ is f xstar. In WSC, $f^*$ is written $f(x_p)$.
• Projection. $x_p$ is an explicit map p with IsProjSel f p: p x lies in $\mathcal X^*$ and ‖x - p x‖ = Metric.infDist x X*. Every condition, and Theorem 2, refers to an arbitrary such selection. ESC's "$x_p=y_p$" is p x = p y for that same selection. No Classical.choose is used.
• PL is the published predicate ShiOptRates.PolyakLojasiewicz f (gradient f) μ fstar (definition ShiOptrates_FunctionClass), i.e. $2\mu(f(x)-f^*)\le\|\nabla f(x)\|^2$. This is the paper's (3) multiplied by 2.
• Constants. Each milestone carries the constant of its appendix bullet and the hypothesis $\mu>0$. The goal uses Holds C := ∃ μ, 0 < μ ∧ C μ independently on each side of every arrow. Convexity is ConvexOn ℝ Set.univ f.
• Dropped standing hypotheses. Milestones whose argument does not use the Lipschitz gradient omit it: SC → ESC, ESC → WSC, WSC → RSI, RSI → EB, QG + convex → RSI, and (20). Each is then a slightly stronger statement.
• Corrected constant. EB → PL is stated with $\mu^2/L$, which is what the paper's displayed argument proves. The quoted milestone text keeps the printed "$\mu/L$".
• No trivialization. Every condition is quantified over all $x$ (and $y$). The selection p is constrained by IsProjSel, not free, and the goal's hypotheses are satisfiable: $f(x)=\frac12\|x\|^2$ with $p\equiv0$, $L=1$ satisfies all of them and SC with $\mu=1$. A formalization that fixed one $\mu$ for the whole chain, or replaced $x_p$ by an unconstrained map, would be a different theorem.
• Reuse. The condition predicates and the projection selection are reusable by any development on linear convergence without strong convexity. A general "PL implies QG" lemma via gradient flow is reusable beyond this mission. Contributions toward the ODE and arc-length infrastructure are welcome.

Selected references

• H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition, ECML PKDD 2016; arXiv:1608.04636v4 (2020). https://arxiv.org/abs/1608.04636
• B. T. Polyak, Gradient methods for minimizing functionals, Zh. Vychisl. Mat. Mat. Fiz. 3(4):643–653, 1963 (English translation: USSR Comput. Math. Math. Phys. 3(4):864–878). https://doi.org/10.1016/0041-5553(63)90382-3
• J. Bolte, T. P. Nguyen, J. Peypouquet, B. W. Suter, From error bounds to the complexity of first-order descent methods for convex functions, Math. Program. 165, 2017. https://arxiv.org/abs/1510.08234
• H. Zhang, The restricted strong convexity revisited: analysis of equivalence to error bound and quadratic growth, Optim. Lett. 11, 2017. https://arxiv.org/abs/1511.01635
• H. Zhang, New analysis of linear convergence of gradient-type methods via unifying error bound conditions, Math. Program. 180, 2020. https://arxiv.org/abs/1606.00269
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46, 1993. https://doi.org/10.1007/BF02096261

Motivation

Gradient descent is often introduced with strong convexity as the condition that gives a geometric reduction in objective error. That condition excludes useful smooth objectives whose minimizer is not unique and some nonconvex objectives. Karimi, Nutini, and Schmidt place the Polyak–Łojasiewicz inequality at the center of a more general account: it controls the objective gap using the squared gradient norm without requiring convexity. Their paper uses it to analyze gradient, coordinate, stochastic, and proximal gradient methods, and identifies settings including least squares and logistic regression in which the condition is useful. Karimi, Nutini, and Schmidt, §1–2

This mission isolates the paper's first rate theorem and its immediate analytic setting. The question is whether the ordinary gradient step with length $1/L$ has a global geometric rate when the objective has a Lipschitz gradient, attains its minimum, and satisfies the PL inequality. The claim applies to every initial point, even when the function is nonconvex. It also gives a precise test case for deciding which properties of smoothness and optimality must be represented explicitly in Lean. Karimi, Nutini, and Schmidt, Theorem 1, p. 2

Setting

Let $d$ be a natural number and let $f:\mathbb R^d\to\mathbb R$ be a differentiable objective. Its gradient at $x$ is $\nabla f(x)$, with the Euclidean norm and inner product denoted by $\|\cdot\|$ and $\langle\cdot,\cdot\rangle$. An $L$-Lipschitz gradient means that $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for every $x,y$, with $L>0$. The corresponding quadratic upper bound is the paper's inequality (2):

$$f(y)\le f(x)+\langle\nabla f(x),y-x\rangle+\frac L2\|y-x\|^2.$$

The optimization problem is unconstrained. It has a nonempty set of solutions: choose a global minimizer $x^*$, so $f(x^*)\le f(y)$ for every $y$, and write $f^*=f(x^*)$. This notation ties the reference value to an attained optimum. The PL inequality with constant $\mu>0$ is

$$\frac12\|\nabla f(x)\|^2\ge\mu\bigl(f(x)-f^*\bigr) \qquad\text{for every }x\in\mathbb R^d.$$

Given any starting point $x_0$, the gradient descent run is the sequence specified by $x_{k+1}=x_k-L^{-1}\nabla f(x_k)$. The term “linear convergence” here refers to a geometric bound on the difference in objective values, not to a claim that the points $x_k$ approach a particular minimizer. Multiple minimizers are allowed. These conventions are those of §2 and Theorem 1 of the source. Karimi, Nutini, and Schmidt, p. 2

Formalization targets

Gradient descent at step size $1/L$

The mission goal is the paper's Theorem 1. For every starting point and every $k\in\mathbb N$,

$$f(x_k)-f^*\le\left(1-\frac\mu L\right)^k\bigl(f(x_0)-f^*\bigr).$$

The target includes the gradient update itself. Its three milestones record the source's analytic path: the quadratic upper bound (2) from the Lipschitz gradient assumption, the one-step decrease displayed in the proof, and the one-step PL contraction displayed immediately afterwards. The latter two are linked to proved platform theorems whose exact-gradient specializations give the source's displays. Karimi, Nutini, and Schmidt, Theorem 1 and proof, p. 2

Nearby consequences

The mission also states the paper's observation that an exact line search over all real step sizes has the same function-value rate. Two companion claims record that a stationary point under PL is a global minimizer, and that $\mu$-strong convexity implies PL with the same $\mu$. These claims locate the rate theorem among the conditions discussed in §2.2 and Appendix B; they are separate from the goal and its milestone list. Karimi, Nutini, and Schmidt, pp. 3, 14

Significance

The rate bounds the objective error at each finite iteration, with an explicit factor $1-\mu/L$. It explains why uniqueness of the minimizer and convexity are not prerequisites for this particular function-value guarantee. It does not by itself assert a rate for the distance to the solution set, a rate for individual iterates, or convergence to a uniquely determined point. The strong-convexity companion shows that the classical strongly convex case fits inside the same PL framework. Karimi, Nutini, and Schmidt, §§2–2.2 and Appendix B

For formalization, the mission adds the precise bridge from a literal Lipschitz-gradient hypothesis to the quadratic upper-bound form used by the existing step results. It also states the complete source theorem with an attained optimum, a genuine gradient, and the update rule, rather than treating any reference value or gradient-like map as interchangeable with those objects. The two published one-step theorems are already machine checked on Prove2Me; the five source-specific draft statements in this proposal remain targets until their proofs are supplied and verified. This distinction matters because the previously published geometric-rate theorem assumes $\mu\le L$, while Theorem 1 does not state that restriction.

Difficulty

Smoothness controls the change in $f$ during a gradient step through the size of the gradient. A geometric rate needs the change to be related to the remaining objective gap. That relation does not follow from smoothness alone; the PL inequality supplies the additional control. Another issue is that the factor $1-\mu/L$ may be negative if $\mu>L$. The source does not exclude that parameter range, so the formal theorem must handle it without inserting an extra hypothesis. An exact line search raises a distinct issue: its asserted minimum along a line must be attained, and the chosen next iterate must be a point realizing it. Karimi, Nutini, and Schmidt, Theorem 1 and following paragraph, pp. 2–3

Formalization scope

Lean represents $\mathbb R^d$ as EuclideanSpace ℝ (Fin d), so $d=0$ is included and denotes a one-point space. It uses Mathlib's gradient on an explicitly differentiable $f$, ordinary real scalars and norms, and a sequence indexed by natural numbers. The fixed step is written with $1/L$ and requires $L>0$. The minimizer witness $x^*$ and its global-minimality property are explicit; the PL predicate uses exactly $f(x^*)$ as its reference value. The PL inequality is represented in the equivalent form $2\mu(f(x)-f(x^*))\le\|\nabla f(x)\|^2$. The goal assumes the literal Lipschitz bound on gradients; equation (2) is a milestone conclusion. No convexity and no condition $\mu\le L$ are added.

The exact line-search companion quantifies over every real step size and requires an attained minimizing iterate. The stationary-point consequence retains differentiability but does not need the $L$-Lipschitz gradient bound. The strong-convexity companion uses the first inequality in Appendix A and the implication in Appendix B, with the same $\mu$ on both sides. The shared ShiOptRates predicates for the quadratic upper bound and PL inequality are referenced as published definitions. Useful contributions include proofs of the Lipschitz-to-quadratic-bound bridge and the paper-specific results, as well as reusable facts about gradients on Euclidean spaces. A freely chosen $f^*$ or a default value of gradient at a nondifferentiable point would change the mathematical claim; the goal excludes both.

Selected references

• H. Karimi, J. Nutini, and M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak–Łojasiewicz Condition, ECML PKDD, 2016; arXiv:1608.04636v4. This mission cites the pinned preprint's pp. 2–3, 11, and 14.

Motivation

Stochastic gradient (SG) methods are the default algorithms for training machine-learning models: when an objective is an average over a very large number of training examples, computing its full gradient even a few times is infeasible, while the gradient of a single randomly chosen example is cheap. The classical convergence theory of SG rates its expected suboptimality under strong convexity — the $O(1/k)$ rate of Nemirovski, Juditsky, Lan and Shapiro (2009) — yet common models such as least squares with a rank-deficient design and logistic regression are convex but not strongly convex.

Karimi, Nutini and Schmidt (2016) observed that the much older Polyak–Łojasiewicz (PL) inequality of Polyak (1963) is enough to recover linear rates for gradient descent and its variants without any convexity. Their Theorem 4 transfers this observation to SG: under PL alone, SG with a decreasing step attains the $O(1/k)$ rate known from the strongly convex case, and SG with a constant step converges linearly to a neighbourhood of the optimum whose size is proportional to the step. This mission formalizes that theorem.

Setting

Let $d\ge0$ and let $\mathbb R^d$ carry the Euclidean norm $\|\cdot\|$. An index $i$ ranges over a measurable space $I$ with a probability measure $\nu$, and each index has a differentiable component function $f_i:\mathbb R^d\to\mathbb R$. The stochastic optimization problem (7) is to minimize

$$f(x) = \mathbb E_{i\sim\nu}[f_i(x)],$$

of which the finite sum $f = \frac1n\sum_{i=1}^n f_i$ (8) is the case of the uniform distribution on $n$ indices. The component gradients are unbiased: $\mathbb E_{i\sim\nu}[\nabla f_i(x)] = \nabla f(x)$ for every $x$.

The SG method (9) starts from a point $x_0$ and, given step sizes $\alpha_k>0$ and indices $i_0,i_1,\dots$ drawn independently from $\nu$, iterates

$$x_{k+1} = x_k - \alpha_k\nabla f_{i_k}(x_k).$$

The iterate $x_k$ is a random vector, a function of $i_0,\dots,i_{k-1}$.

The standing assumptions on $f$ (§2 of the paper) are:

1. $\nabla f$ is $L$-Lipschitz: $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for all $x,y$, with $L>0$;
2. the solution set is non-empty: some $x^*$ minimizes $f$, and $f^* = f(x^*)$;
3. the PL inequality (3) with constant $\mu>0$: $\tfrac12\|\nabla f(x)\|^2\ge\mu\,(f(x)-f^*)$ for all $x$.

Theorem 4 adds a second-moment bound along the iterates: $\mathbb E_{i\sim\nu}\big[\|\nabla f_i(x_k)\|^2\big]\le C^2$ for every iterate $x_k$.

Formalization targets

Goal: Theorem 4 (p. 6)

Under the assumptions above,

1. with the decreasing step $\alpha_k = \dfrac{2k+1}{2\mu(k+1)^2}$,

$$\mathbb E[f(x_k)-f^*]\le\frac{LC^2}{2k\mu^2}\qquad(k\ge1);$$

2. with a constant step $\alpha_k=\alpha$, $0<\alpha<\dfrac1{2\mu}$,

$$\mathbb E[f(x_k)-f^*]\le(1-2\mu\alpha)^k\,[f(x_0)-f^*]+\frac{LC^2\alpha}{4\mu}\qquad(k\ge0).$$

The second-moment bound is assumed separately for the run of each scheme, with the same constant $C$.

Milestones (proof of Theorem 4, p. 7)

1. One-step bound. For any point $x$ with $\mathbb E_i\|\nabla f_i(x)\|^2\le C^2$ and any step $a$,

$$\mathbb E_i[f(x-a\nabla f_i(x))]\le f(x)-a\|\nabla f(x)\|^2+\frac{LC^2a^2}{2}.$$

2. Recursion (10). Along the run, whenever $\alpha_k\ge0$,

$$\mathbb E[f(x_{k+1})-f^*]\le(1-2\alpha_k\mu)\,\mathbb E[f(x_k)-f^*]+\frac{LC^2\alpha_k^2}{2}.$$

3. Decreasing step rate, the first half of the goal.
4. Constant step rate, the second half of the goal.

Significance

The result. Theorem 4 places SG under PL on the same footing as SG under strong convexity: the same $O(1/k)$ rate, with constants depending on $L$, $\mu$ and $C$ only, and no convexity. Since PL holds for least squares with any design matrix and, over any compact set, for logistic regression (§2.3 of the paper), the theorem gives explicit SG rates for these models. The constant-step bound quantifies the practitioners' rule of halving the step when progress stalls: halving $\alpha$ at least halves the noise floor $LC^2\alpha/(4\mu)$.

Formalizing it. The result is proved, in a short argument, in the paper. To our knowledge no machine-checked proof exists: the existing Lean formalizations of SG rates on Prove2Me concern stationarity of non-convex objectives under a variance bound, a different noise model with a different conclusion. The remaining work is to formalize the paper's proof, which requires a usable treatment of expectations over an i.i.d. index sequence (conditioning the step from $x_k$ on the past) — infrastructure that every later analysis of a stochastic first-order method can reuse.

Difficulty

The deterministic content is elementary: the descent lemma, unbiasedness, the PL inequality, a telescoping sum and a geometric series. The difficulty is probabilistic bookkeeping. Recursion (10) takes the expectation of a one-step inequality with respect to $i_k$ alone, holding $x_k$ fixed; this is legitimate because $i_k$ is independent of $i_0,\dots,i_{k-1}$, of which $x_k$ is a function. Making this precise requires measurability of the iterates in the sample path and a Fubini-type decomposition of the product law into the first $k$ coordinates, the $k$-th coordinate and the rest. A second subtlety is that the second-moment bound holds only at the iterates, not at every point, so the one-step bound must be applied pointwise in the path, on a set of full measure, rather than once and for all.

Formalization scope

The space is EuclideanSpace ℝ (Fin d) and $\nabla$ is Mathlib's gradient. The index law is an arbitrary probability measure $\nu$ on a measurable space, and the path law is the infinite product Measure.infinitePi (fun _ => ν); the run is a deterministic function sgRun of the path. The Lipschitz-gradient assumption is stated literally on $\nabla f$; the PL inequality is the published predicate ShiOptRates.PolyakLojasiewicz f (gradient f) μ (f xstar) (inequality (3) multiplied by 2); the solution set is a point xstar with ∀ y, f xstar ≤ f y, and $f^*$ is f xstar, never a free real.

Every expectation of a gap is a lower Lebesgue integral of $\max(f(x_k)-f^*,0)$ with values in $[0,\infty]$, which equals $\mathbb E[f(x_k)-f^*]$ because $f^*$ is the minimum; no integrability side condition can make a bound hold by default. The second-moment bound is the lower Lebesgue integral of $\|\nabla f_i(x_k)\|^2$, required for almost every path and every $k$. Unbiasedness and problem (7) carry explicit integrability, so a non-integrable gradient cannot turn them into trivialities.

The second-moment bound is deliberately not imposed at every point $x$. With the bound at every point, $\|\nabla f\|\le C$ everywhere, so $f-f^*\le C^2/(2\mu)$ by PL, while along the gradient-ascent flow $f-f^*$ grows exponentially unless it vanishes; hence $f$ would be constant and the theorem vacuous. Along the iterates the hypothesis is met by non-constant objectives such as $f(x)=\tfrac12\|x\|^2$.

Additions relative to the page, all disclosed in the statements: each $f_i$ is differentiable; $(i,x)\mapsto\nabla f_i(x)$ is jointly measurable, so that the iterates are random variables; the constant step is positive; the decreasing-step rate is stated for $k\ge1$; and "each $f$ has an $L$-Lipschitz continuous gradient" is read as a condition on $f$, the only one the proof uses. The page's proof of the constant-step bound writes the exponent $k$ where $k+1$ is meant; the statements follow the theorem's (correct) form.

Contributions welcome: the measurability of the run, the conditioning step for infinitePi, the deterministic one-step bound, and the two scalar recursions, each of which is reusable for other SG analyses.

Selected references

• H. Karimi, J. Nutini, M. Schmidt, Linear Convergence of Gradient and Proximal-Gradient Methods Under the Polyak-Łojasiewicz Condition, ECML PKDD 2016; arXiv:1608.04636v4, 2020. https://arxiv.org/abs/1608.04636
• B. T. Polyak, Gradient methods for minimizing functionals, USSR Computational Mathematics and Mathematical Physics 3(4), 1963. https://doi.org/10.1016/0041-5553(63)90382-3
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19(4), 2009. https://doi.org/10.1137/070704277
• F. Bach, E. Moulines, Non-strongly-convex smooth stochastic approximation with convergence rate O(1/n), NeurIPS 2013. https://arxiv.org/abs/1306.2119

Why an explicit exploration policy matters

In episodic reinforcement learning, an agent learns the rewards and dynamics of a system while choosing actions that determine which states it observes. A bound on the number of states and actions alone does not prescribe how to explore: a policy can be valuable because it earns reward, because it visits an uncertain state-action pair, or both. Foster, Kakade, Qian, and Rakhlin introduced the decision-estimation coefficient (DEC) to measure this trade-off in interactive decision problems. Their tabular reinforcement learning example gives an explicit policy distribution with a bound depending on the horizon and the sizes of the state and action sets Foster et al., §5.2.

The target is Proposition 5.6 of that paper. Its policy-cover inverse gap weighting strategy, or PC-IGW, places weight on policies that cover state-action pairs under an estimated model, while accounting for their estimated loss in reward. The paper also gives a posterior-sampling bound for a dual DEC in Proposition 5.4. PC-IGW addresses the frequentist coefficient with an explicit distribution and the constant $95$ Foster et al., Propositions 5.4 and 5.6.

Tabular models and the policy cover

A tabular Markov decision process has a finite state set $S$, a finite action set $A$, and $H\ge1$ decision layers. At layer $h$, state $s$, and action $a$, a model $M$ supplies a transition distribution $P_h^M(\cdot\mid s,a)$ and a reward distribution $R_h^M(\cdot\mid s,a)$. Every model shares the initial state distribution $d_1$. A randomized nonstationary policy $\pi$ supplies an action distribution $\pi_h(\cdot\mid s)$ for each layer and state; all such policies form $\Pi_{\mathrm{RNS}}$ Foster et al., Example 1.2.

The trajectory law $M(\pi)$ records the sequence of states, actions, and rewards generated by $M$ and $\pi$. The final transition reaches a deterministic terminal state and contributes no model-dependent factor to this law. The policy's value is $f^M(\pi)=\mathbb E^{M,\pi}[\sum_{h=1}^H r_h]$. Write $\pi_M$ for any value-maximizing policy and $d_h^{M,\pi}(s,a)$ for the probability of visiting $(s,a)$ at layer $h$. The squared Hellinger distance between two trajectory laws has the normalization $D_H^2(P,Q)=\sum_x(\sqrt{P(x)}-\sqrt{Q(x)})^2$, with no factor $1/2$ Foster et al., §2, Eq. (5).

Given an estimated model $\bar M$ and $\eta>0$, Algorithm 4 chooses, for each $(h,s,a)$, a policy $\pi_{h,s,a}$ that maximizes

$$\frac{d_h^{\bar M,\pi}(s,a)}{2HSA+\eta\bigl(f^{\bar M}(\pi_{\bar M})-f^{\bar M}(\pi)\bigr)} \quad\text{over }\pi\in\Pi_{\mathrm{RNS}}.$$

Let $\Psi$ be the resulting set of distinct cover policies. The PC-IGW distribution gives each $\pi\in\Psi\cup\{\pi_{\bar M}\}$ weight $p(\pi)=1/[\lambda+\eta(f^{\bar M}(\pi_{\bar M})-f^{\bar M}(\pi))]$, where $\lambda$ makes the weights sum to one. Proposition 5.7 states that this positive normalizer is unique and lies in $[1,2HSA]$ Foster et al., Algorithm 4 and Proposition 5.7.

Formalization targets

The main target is the explicit-policy inequality of Proposition 5.6. For $\gamma>0$ and $\eta=\gamma/(21H^2)$, the distribution from Algorithm 4 satisfies, for every normalized tabular model $M$,

$$\mathbb E_{\pi\sim p}\!\left[ f^M(\pi_M)-f^M(\pi)-\gamma D_H^2(M(\pi),\bar M(\pi)) \right]\le\frac{95H^3SA}{\gamma}.$$

The uniform quantifier over $M$ is the paper's supremum over its model class. Because this is a bound for a particular distribution $p$, it certifies the stated DEC bound. The Lean goal expresses that explicit distribution and its inequality directly; it does not introduce a separate supremum over all models and infimum over all distributions. The milestone list records the unique normalizer, the exploration-bias display (59), the cover comparison (61), the local and global simulation estimates, the Hellinger information inequalities, and Lemma 5.2's change of measure Foster et al., pp. 36–38 and Appendices A.2, F.1.

What the bound contributes

The result controls the cost of exploration for a finite-horizon model class by $H^3SA/\gamma$ with a specified constant. Its importance is the constructive policy distribution: the bound applies to the strategy returned by Algorithm 4, rather than asserting only that some distribution exists. In the paper, this bound combines with estimation and the general DEC-to-regret result to obtain a tabular regret guarantee; the authors also use the policy-cover idea as a starting point for their bilinear-class treatment Foster et al., §§5.2.2–5.2.3 and 7.

The paper result is proved. This mission asks for machine-checked proofs of its finite-alphabet statements; the draft theorems currently carry sorry. Its MDP interface includes reward distributions, full trajectory laws, occupancy probabilities, backward values, and local divergences. Those definitions can be reused for other tabular DEC results. Published FoundationsRL definitions already provide the discrete Hellinger and total-variation distances and a proved comparison between them. A separate published MDP interface records reward means, which cannot represent the reward-kernel Hellinger terms in this result Foster and Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making.

Where the difficulty lies

The cover is chosen using occupancies under $\bar M$, while the regret is evaluated under any $M$ in the class. An ordinary value bound for one fixed policy does not by itself control this mismatch. The page's intermediate expressions also divide by an average occupancy that may be zero. A formal statement must still cover state-action pairs that the policy distribution never visits, without assigning meaning to a zero-denominator ratio. The final inequality uses Hellinger distance between whole trajectories even though local simulation estimates are expressed through transition and reward kernels. Keeping those two levels of comparison aligned is the main mathematical burden Foster et al., pp. 37–38.

There is also a reward-bound issue in the appendix. Lemma F.3 uses continuation values in $[0,1]$ at states visited under $\bar M$, including states that may be unreachable under $M$ from the shared initial law. The paper states an almost-sure bound on total episode reward, but that statement alone does not control every such continuation value Foster et al., Lemma F.3, p. 107.

Formalization scope

State, action, and reward alphabets are finite and nonempty. Probability laws and expectations are finite vectors and sums. Policies may randomize; the cover condition compares its choice against every valid randomized nonstationary policy. Layers use zero-based Fin H indices, while the paper uses $1,\ldots,H$. All models share $d_1$. The terminal transition is omitted from the trajectory law and from one-step divergence sums. Duplicate cover policies are merged, as required by the paper's set $\Psi\cup\{\pi_{\bar M}\}$. The selector $\pi_M$ must maximize value over valid policies, and the algorithm's weights must sum to one; these conditions exclude a free policy choice or an unnormalized pseudo-law.

The paper assumes $\sum_h r_h\in[0,1]$ almost surely. The local simulation lemma's stated bound needs two disclosed additions here: nonnegative stage rewards, and the same total-reward bound on every supported suffix started from any state. RewardsNormalized records them. The change-of-measure and global-simulation milestones use the weaker episode-only condition where sufficient. The cover comparison is cross-multiplied so it remains meaningful when an occupancy is zero. The goal's right side is a real number with $\gamma>0$, $H\ge1$, and nonempty $S,A$, so its divisions and size factors have the intended meaning.

A complete development needs the finite trajectory law, the policy-cover normalizer, occupancy bounds, the two simulation lemmas, Hellinger comparison inequalities, and the change-of-measure result. Contributions to these foundations, to the exact constant in Proposition 5.6, and to later generalizations of the cover are within scope. The abstract DEC infimum over all randomized policies is a later interface target; this mission's goal is the stronger, explicit-strategy certificate printed first in the proposition.

Selected references

• Dylan J. Foster, Sham M. Kakade, Jian Qian, and Alexander Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, version 3, 2023. arXiv:2112.13487v3.
• Dylan J. Foster and Alexander Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, arXiv preprint, 2023. arXiv:2312.16730.

Why tabular reinforcement learning needs a decision-estimation bound

In episodic reinforcement learning, an agent acts repeatedly in an unknown system and must learn which policy earns the largest expected reward. Even when states and actions are finite, the agent's choices change which data it observes. Foster, Kakade, Qian, and Rakhlin use the decision-estimation coefficient (DEC) to connect this information constraint to regret across interactive decision problems. Their tabular example asks for an explicit bound in terms of the horizon, the numbers of states and actions, and an information penalty Foster et al., §5.2.

The result here is the posterior-sampling bound of Proposition 5.4. It gives a uniform constant, rather than a rate stated only with asymptotic notation. Its role is to show that a policy drawn from a distribution of model-optimal policies controls the Bayesian or dual DEC in a tabular class. The same article also studies a frequentist policy-cover strategy with a different coefficient; this mission isolates the posterior-sampling argument and the information inequalities it needs Foster et al., Propositions 5.4 and 5.6.

Models, policies, and trajectory laws

A tabular Markov decision process has a finite state set $S$, a finite action set $A$, and $H\ge1$ decision layers. At layer $h$, state $s$, and action $a$, the model $M$ supplies a transition distribution $P_h^M(\cdot\mid s,a)$ and a reward distribution $R_h^M(\cdot\mid s,a)$. Every model has the same initial state distribution $d_1$. A randomized nonstationary policy $\pi$ supplies an action distribution $\pi_h(\cdot\mid s)$ at each layer and state. This is the policy class $\Pi_{\mathrm{RNS}}$ used in Example 1.2, including genuinely randomized policies Foster et al., Example 1.2.

The trajectory law $M(\pi)$ records states, actions, and realized rewards over one episode. Its weight on a trajectory is the product of the shared initial probability, the policy probabilities, reward-kernel probabilities, and transitions between consecutive decision layers. The state after layer $H$ is a deterministic terminal state. Therefore the last model transition contributes no factor to the recorded law. The reward value of an outcome is given by a fixed map $r$, and the value of a policy is $f^M(\pi)=\mathbb E^{M,\pi}[\sum_{h=1}^{H}r_h]$. The occupancy $d_h^{M,\pi}(s,a)$ is the probability of visiting state-action pair $(s,a)$ at layer $h$ Foster et al., §2.

For each model, $\pi_M$ denotes a policy maximizing $f^M$ over $\Pi_{\mathrm{RNS}}$. Let $\mu$ be a prior on models. Posterior sampling here means drawing a model $M'\sim\mu$ and using $\pi_{M'}$. The model whose performance is evaluated is a separate draw $M\sim\mu$; these two draws must remain independent. The reference model is denoted $\bar M$. Squared Hellinger distance has the paper's normalization $D_H^2(P,Q)=\sum_x(\sqrt{P(x)}-\sqrt{Q(x)})^2$, with no factor of one half Foster et al., Eq. (5).

Formalization targets

The main target is the policy-specific inequality of Proposition 5.4. For $\gamma>0$, it asserts

$$\mathbb E_{M\sim\mu,\,\pi\sim p} \left[f^M(\pi_M)-f^M(\pi)-\gamma D_H^2(M(\pi),\bar M(\pi))\right] \le \frac{26H^2SA}{\gamma}, \qquad p=\operatorname{Law}(\pi_{M'}),\ M'\sim\mu.$$

The claim holds for each finitely supported prior $\mu$ in the finite-alphabet representation. It directly gives the same upper bound when the dual DEC is defined as the supremum over such priors and the infimum over policy distributions. The Lean goal states the inequality for posterior sampling itself; no real supremum is needed to express that stronger, explicit claim. The reference model belongs to the normalized tabular class, which is the case actually proved in §5.2.1. The printed proposition also names reference models outside the class and points to the later general result Foster et al., p. 33.

The milestones are the conditional-to-joint Hellinger inequality of Lemma A.9, both inequalities of Lemma A.11, the global and local simulation lemmas F.2 and F.3, the change-of-measure statement in Lemma 5.2, and the unnumbered posterior-sampling decoupling inequality on pp. 34–35. Together they identify the stated estimates on which the proposition rests Foster et al., Appendices A.2 and F.1.

What the result contributes

The $26H^2SA/\gamma$ bound quantifies the price of learning the dynamics and rewards while selecting policies. Its explicit dependence on $S$ and $A$ is linear, and its dependence on the horizon is quadratic. In the paper, this estimate feeds the DEC-based analysis of tabular reinforcement learning and provides a comparison point for the policy-cover bound and later extensions beyond tabular models Foster et al., §5.2.

This formalization supplies a reusable interface for tabular MDPs with reward distributions: a full trajectory law, policy value, occupancy, backward values, and local divergences. The published FoundationsRL divergence definitions and a proved TV–Hellinger comparison can be reused. None of the seven statements has a machine-checked proof yet. A finite-horizon MDP object already published elsewhere records deterministic reward means and does not express the reward-kernel Hellinger distances required here.

Where the difficulty lies

A value difference is controlled by total variation between complete trajectory laws, but the proposed bound is expressed through local transition and reward discrepancies and ultimately through squared Hellinger distance between whole trajectories. These quantities average under different model-policy laws. Moving between them while retaining the exact constants in Lemma 5.2 is the central obstacle. A direct bound for a policy paired with the same model does not supply the double expectation in the target: the performance model and the policy-generating model are independent under posterior sampling.

The reward convention adds a second obstacle. Section 5.2 sets the reward space to $[0,1]$ and also assumes that total episode reward lies in $[0,1]$ almost surely. A model's continuation values at states it cannot reach from $d_1$ are not controlled by the episode condition. The local simulation bound is nevertheless asserted under the reference model's occupancy, which may visit such states.

Formalization scope

State, action, and reward alphabets are finite; reward distributions are finite probability vectors. The paper allows general measurable reward spaces, so the finite reward alphabet is a declared scope restriction. Layers are indexed by Fin H, starting at zero, while the source labels them $1,\ldots,H$. The terminal transition is omitted from trajectory products and local discrepancy sums. The initial distribution is a separate parameter shared by all models. Priors and policy laws have finite support, as in the paper's discrete-topology convention for model distributions. Every policy quantified in a theorem is checked to be a probability kernel, and each selected $\pi_M$ is checked to maximize value over valid randomized policies.

RewardsNormalized expresses both standing conditions of §5.2: reward values lie in $[0,1]$, and under every randomized policy every trajectory of positive probability has total reward $\sum_{h=1}^{H}r_h\in[0,1]$. The proposition and its decoupling milestone use it. The Appendix F simulation lemmas and Lemma 5.2 use EpisodeTotalInUnitInterval, which expresses only the total-reward condition stated in those lemmas.

The target uses the full trajectory law $M(\pi)$ in $D_H^2(M(\pi),\bar M(\pi))$. Replacing it with one-step kernel distances would change Proposition 5.4. A valid model is a family of probability kernels, a valid policy is a family of action distributions, and the model selector must really choose an optimum; these checks prevent the expected inequality from becoming true through zero-weight pseudo-laws or a free, suboptimal policy selector. The definition and Hellinger lemmas can support later tabular DEC missions as well.

Selected references

• Dylan J. Foster, Sham M. Kakade, Jian Qian, and Alexander Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, version 3, 2023. arXiv:2112.13487v3.
• Dylan J. Foster and Alexander Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, arXiv preprint, 2023. arXiv:2312.16730.

Motivation

Interactive decision methods often need an estimate of an unknown outcome law after each round. A learner can be good at decisions only if its model of the observations is accurate where future decisions will sample. Foster, Kakade, Qian and Rakhlin measure this accuracy by a cumulative squared Hellinger distance and use it in their regret bounds for decision making with structured observations. They connect that estimation quantity to online log-loss regret, a standard objective for sequential probability prediction. The connection lets a regret guarantee for a density predictor supply the estimation guarantee needed by a decision method. Foster et al., Appendix A.3 and §4.1.1.

This mission isolates the online estimation result, Lemma A.14, from the rest of the paper. It addresses a learner that predicts a conditional outcome distribution before the next covariate and outcome are revealed. The covariates may respond to the entire preceding history. This matters in interactive decision making, where the learner's earlier choices change what it observes next. Foster et al., pp. 75–76.

Setting

There are $T$ rounds. At round $t$, the learner has a history $H_{<t}=((x_s,y_s))_{s<t}$ of past covariates and outcomes. It predicts a probability distribution $\widehat g_t(\cdot\mid x;H_{<t})$ for every possible next covariate $x$. Nature draws $x_t$ from a history-dependent distribution $c_t(\cdot\mid H_{<t})$, then draws $y_t$ from the conditional law of a distinguished true expert $i^\star$. An expert class indexed by $I$ supplies laws $g_{i,t}(\cdot\mid x;H_{<t})$; realizability means $g_{i^\star,t}$ is the actual outcome law at every round. The prediction $\widehat g_t$ is selected from the past history, before $x_t$ is observed. Foster et al., Assumption A.1, p. 76.

For a predicted distribution $q$, the log loss on observation $y$ is $-\log q(y)$. The learner's log-loss regret $\mathrm{Reg}_{\mathrm{KL}}$ is its cumulative log loss minus the smallest cumulative loss of an expert in $I$. This is a realized quantity: both sums use the covariates and outcomes that actually occurred. The squared Hellinger distance is

$$D_{\mathrm H}^2(P,Q)=\sum_y\bigl(\sqrt{P(y)}-\sqrt{Q(y)}\bigr)^2.$$

The Hellinger estimation error $\mathrm{Est}_{\mathrm H}$ is different from a sum evaluated only at realized covariates. At each round it averages $D_{\mathrm H}^2(\widehat g_t(\cdot\mid x),g_{i^\star,t}(\cdot\mid x))$ over the conditional law of the next covariate $x$, given $H_{<t}$, then sums these conditional errors. Thus the error measures prediction quality in the distribution the learner is about to face. Foster et al., (99)–(100), pp. 75–76.

Formalization targets

Main high-probability bound

The main target is Lemma A.14 (102): for every $\delta\in(0,1)$,

$$\Pr\!\left\{\mathrm{Est}_{\mathrm H} \le \mathrm{Reg}_{\mathrm{KL}}+2\log(1/\delta)\right\}\ge 1-\delta.$$

The coefficient $2$ and the absence of a factor $1/2$ in $D_{\mathrm H}^2$ are part of the claim. The probability is under the complete history law generated by the adaptive covariate process and the true expert. Foster et al., Lemma A.14, p. 76.

Supporting results

The first milestone is Lemma A.4, an anytime conditional exponential-moment bound. It controls one event on which an adapted inequality fails at any horizon through $T$, without replacing it by a single fixed-horizon claim. The second milestone is the affinity identity used in the proof of Lemma A.14:

$$\sum_y\sqrt{P(y)Q(y)}=1-\tfrac12D_{\mathrm H}^2(P,Q).$$

The proposal also states the expectation clause $\mathbb E[\mathrm{Est}_{\mathrm H}]\le\mathbb E[\mathrm{Reg}_{\mathrm{KL}}]$ from (101) and the predictable-mask clause (103), which bounds error accumulated only on rounds selected from the past. Foster et al., pp. 70, 76, 79.

Significance

The high-probability bound lets an online density estimator serve as an estimation oracle for the paper's interactive decision bounds. A user can choose a predictor because it has a log-loss regret guarantee, then obtain control of Hellinger estimation error under adaptive observations. The expectation clause supplies the corresponding average guarantee. The masked clause handles applications that evaluate accuracy only on rounds selected before the current observation. Foster et al., Proposition 4.1 and Lemma A.14.

The result is already proved in the source paper. This mission asks for machine-checked proofs of the finite-alphabet statements and a reusable interface for sequential probability kernels, conditional error and log-loss regret. The published FoundationsRL Hellinger definition supplies the same normalization used by the paper; the mission does not propose a new distance. These items have no machine-checked proof in this proposal yet. The source also gives Vovk's aggregation guarantee for finite expert classes, but that algorithmic bound is outside the current item list. Foster et al., Lemma A.15, p. 76.

Difficulty

The quantity to be bounded is conditional on the past. A pathwise distance at the observed $x_t$ is a different random quantity and does not give (102). Adaptive covariates add another dependence on history, while the learner must choose its prediction before seeing $x_t$. A fixed covariate law would therefore omit a central feature of the theorem. The anytime milestone likewise concerns all prefixes of one process at once; separate claims at each fixed horizon do not preserve its statement. Foster et al., pp. 70, 75–79.

The log-loss formula also has a boundary. A zero predicted probability gives infinite loss in the paper, whereas Lean's real logarithm returns a finite default at zero. The formal statements must keep that default from affecting a positive-probability observation. Squared Hellinger distance has its own normalization convention, so the affinity identity checks the factor needed in the high-probability constant.

Formalization scope

The paper uses measurable covariate and outcome spaces and regular conditional densities. This mission specializes to finite covariates $X$, finite outcomes $Y$, and a finite nonempty expert class $I$. Each kernel is represented by a nonnegative vector summing to one. Complete histories are finite sequences, and the probability of a history is the product of its covariate and true-expert outcome probabilities. Expectations and event probabilities are finite sums. Time is indexed from zero; round $t$ in Lean corresponds to round $t+1$ in the paper.

The learner, experts and covariate kernel may all depend on preceding history. The learner and experts predict a law for every possible covariate while seeing only that history. A Boolean mask for (103) has the same information restriction. The Hellinger error sums conditional averages over the next covariate, and the probability guarantee is expressed as a bound on the total mass of histories where the displayed inequality fails.

The real-valued log loss requires one additional condition: on every complete history of positive probability, the learner and every expert give the observed outcome positive probability at every round. The condition is imposed only where the history law has support. It excludes Lean's default value for $\log 0$; it is a scope restriction from the paper's extended-valued formulation. A normalized history law and a distinguished true expert are explicit, so the probability statement cannot be discharged by an empty event space or an unnormalized zero law. The sequential-kernel definitions can be reused in other finite online learning results, and the probability, affinity, expectation and masked bounds are separate proof targets.

Selected references

• Dylan J. Foster, Sham M. Kakade, Jian Qian, Alexander Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint arXiv:2112.13487v3, 2023. arXiv.

Motivation

Lower bounds for interactive decision making (bandits, reinforcement learning, and the general decision making with structured observations framework of Foster, Kakade, Qian and Rakhlin, arXiv:2112.13487) compare what a learner observes under two different environments. A learner's whole interaction history is generated one step at a time: each observation is drawn from a conditional law that depends on everything seen before. Statistical estimation guarantees, by contrast, are stated one step at a time, as bounds on the divergence between the conditional laws at each round. Passing from the per-step guarantees to a statement about the laws of entire histories requires a chain rule for the divergence in use.

For the Kullback–Leibler divergence the chain rule is an identity. The paper's guarantees, however, are stated in the squared Hellinger distance, which is bounded, symmetric, and the natural loss for density estimation with the logarithmic loss. Hellinger distance has no exact chain rule. Lemma A.13 of the paper (App. A.2, p. 73) supplies an approximate one, losing a factor logarithmic in the number of steps, and the paper uses it in the proof of its main regret lower bound (Theorem 3.2, via App. C.1.3).

Setting

Fix $n \in \mathbb N$ and finite sets $\mathcal X_1, \dots, \mathcal X_n$. A sequence is $x = (x_1, \dots, x_n)$ with $x_i \in \mathcal X_i$, and $x_{1:i-1} = (x_1, \dots, x_{i-1})$ denotes its prefix; $\mathcal X^{(i-1)} = \prod_{t=1}^{i-1} \mathcal X_t$.

For probability distributions $p, q$ on a finite set, the squared Hellinger distance, the Hellinger distance and the Kullback–Leibler divergence are

$$D^2_{\mathrm H}(p, q) = \sum_a \big(\sqrt{p(a)} - \sqrt{q(a)}\big)^2, \qquad D_{\mathrm H} = \sqrt{D^2_{\mathrm H}}, \qquad D_{\mathrm{KL}}(p\,\|\,q) = \sum_a p(a) \log\frac{p(a)}{q(a)},$$

the last one set to $+\infty$ when $p$ charges a point that $q$ does not. Note that the paper's $D^2_{\mathrm H}$ carries no factor $\tfrac12$, so $0 \le D^2_{\mathrm H} \le 2$.

A family of sequential kernels $P = (P^{(i)})_{i=1}^n$ assigns to each $i$ and each prefix $x_{1:i-1}$ a probability distribution $P^{(i)}(\cdot \mid x_{1:i-1})$ on $\mathcal X_i$. Its sequential law is the law of $X_1, \dots, X_n$ under $X_i \sim P^{(i)}(\cdot \mid X_{1:i-1})$:

$$\mathbb P(x) = \prod_{i=1}^n P^{(i)}(x_i \mid x_{1:i-1}).$$

For a second family $Q$ with law $\mathbb Q$, the quantity controlled by per-step estimation is

$$\mathbb E_{\mathbb P}\Big[\sum_{i=1}^n D^2_{\mathrm H}\big(P^{(i)}(\cdot \mid X_{1:i-1}), Q^{(i)}(\cdot \mid X_{1:i-1})\big)\Big].$$

In Lean these are IsSeqKernel, seqLaw and condHellingerSum, with hellingerSq and klDivDiscrete the published discrete divergences.

Formalization targets

Goal: Lemma A.13, (97), for $n \ge 2$

$$D^2_{\mathrm H}(\mathbb P, \mathbb Q) \le 10^2 \log(n) \cdot \mathbb E_{\mathbb P}\Big[\sum_{i=1}^n D^2_{\mathrm H}\big(P^{(i)}(\cdot \mid X_{1:i-1}), Q^{(i)}(\cdot \mid X_{1:i-1})\big)\Big].$$

The constant $10^2$ is the paper's; the shape that matters downstream is the logarithmic dependence on $n$ with no assumption on the kernels beyond their being probability kernels.

Companion: Lemma A.13, (98)

If $V \ge e$ and $P^{(i)}(A \mid x_{1:i-1}) \le V\, Q^{(i)}(A \mid x_{1:i-1})$ for every $i$, prefix and event $A$, then $D^2_{\mathrm H}(\mathbb P, \mathbb Q) \le 3\log(V) \cdot \mathbb E_{\mathbb P}[\sum_i D^2_{\mathrm H}(P^{(i)}, Q^{(i)})]$.

Milestones

1. Lemma A.10 (p. 72): $D_{\mathrm{KL}}(p\,\|\,q) \le (2 + \log V)\, D^2_{\mathrm H}(p, q)$ under a likelihood-ratio bound $V$ (referenced, finite case).
2. Lemma A.5 (p. 71): $D^2_{\mathrm{TV}} \le D^2_{\mathrm H} \le D_{\mathrm{KL}}$ (referenced, finite case).
3. The triangle inequality for $D_{\mathrm H}$ (proof of Lemma A.13, p. 73).
4. The chain rule $D_{\mathrm{KL}}(\mathbb Q\,\|\,\mathbb P) = \mathbb E_{\mathbb Q}[\sum_i D_{\mathrm{KL}}(Q^{(i)}\,\|\,P^{(i)})]$ for sequential laws (p. 73).
5. Convexity of $D^2_{\mathrm H}$ in its second argument (p. 74).
6. Lemma A.11 (p. 72), the multiplicative Pinsker-type inequality: $|\mathbb E_P h - \mathbb E_Q h| \le \sqrt{2R(\mathbb E_P h + \mathbb E_Q h) D^2_{\mathrm H}(P, Q)}$ and $\mathbb E_P h \le 3\mathbb E_Q h + 4R\, D^2_{\mathrm H}(P, Q)$ for $0 \le h \le R$.

Significance

The result. Inequality (97) converts per-round Hellinger estimation error into a bound on the Hellinger distance between the laws of complete interaction histories, under no boundedness assumption on likelihood ratios. In the paper this is the step that lets the lower bound of Theorem 3.2 relate any algorithm's behaviour under a reference model to its behaviour under alternatives, and hence express the minimax regret through the decision-estimation coefficient. Without it, only the KL chain rule is available, which requires bounded likelihood ratios (the situation of (98)) or loses more than a logarithmic factor. Lemma A.11, a milestone here, is used independently in the same lower bound and in the paper's tabular reinforcement learning analysis.

Formalizing it. The lemma is proved in the paper; no machine-checked proof exists. The published layer on the platform has the discrete divergences and the comparisons of Lemmas A.5 and A.10; the sequential-law objects, the triangle inequality, the convexity of $D^2_{\mathrm H}$, the discrete chain rule and Lemma A.11 are new. A completed development gives a reusable chain-rule toolkit for any later formalization of lower bounds over adaptive interaction histories.

Difficulty

The squared Hellinger distance does not tensorize along adaptive sequences: the natural attempt to write $1 - \tfrac12 D^2_{\mathrm H}(\mathbb P, \mathbb Q)$ as a product of conditional affinities fails because the conditional affinities are random, depending on the prefix, and their expectation does not factor. Bounding $D^2_{\mathrm H}$ by $D_{\mathrm{KL}}$ and applying the KL chain rule fails in the other direction: the conditional KL divergences are not controlled by the conditional Hellinger distances unless the likelihood ratios are bounded, and in (97) they are not. The difficulty is to obtain a bound that pays only $\log n$ for an unbounded ratio, with explicit constants that survive the final numerical comparison.

Formalization scope

• Finite alphabets. The paper works over measurable spaces. This mission formalizes the finite-alphabet case, as the published FoundationsRL divergence layer does: each $\mathcal X_i$ is a Fintype, distributions are probability vectors, expectations are finite sums. Coordinates are indexed by Fin n (0-based) and the alphabets may differ from coordinate to coordinate.
• Kernels. A kernel family is a function P i x of the whole sequence that is a probability vector and depends only on the coordinates j < i; this is what makes seqLaw P the law the paper describes.
• Added hypothesis $n \ge 2$ in (97). The paper states (97) for every $n$; at $n = 1$ the right side vanishes because $\log 1 = 0$ while the left side is positive whenever $P^{(1)} \ne Q^{(1)}$, and the proof's last step $2(6\log(96n) + \tfrac{18}{96n}) \le 10^2\log n$ holds only for $n \ge 2$. The goal is stated for $n \ge 2$, with the constant unchanged.
• Likelihood ratios are stated multiplicatively, $P(A) \le V\,Q(A)$, so that a zero denominator does not make a hypothesis vacuous; KL divergences are compared to Hellinger distances in $[0, \infty]$.
• Lemma A.11 holds "almost surely under $P$ and $Q$", which becomes: $0 \le h \le R$ at every point charged by $P$ or $Q$.
• Ruling out trivial forms. The goal's hypotheses are satisfiable with $\mathbb P \ne \mathbb Q$ and $n \ge 2$ (checked in a sanity file). A formalization in which the kernels may read coordinates beyond the prefix, in which $\log$ is applied to $n \le 1$, or in which the ratio bound of (98) is checked through a quotient that is vacuous at zero denominators, is not the paper's statement.

Contributions welcome: proofs of any milestone and of the fact that seqLaw is a probability vector.

Selected references

• D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv:2112.13487v3, 2023. https://arxiv.org/abs/2112.13487
• Y. Yang, A. Barron, An asymptotic property of model selection criteria, IEEE Transactions on Information Theory 44(1), 1998. https://doi.org/10.1109/18.650993
• Y. Polyanskiy, Y. Wu, Lecture Notes on Information Theory, 2014. https://people.lids.mit.edu/yp/homepage/data/itlectures_v5.pdf
• D. J. Foster, A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, arXiv:2312.16730v1, 2023. https://arxiv.org/abs/2312.16730

Motivation

Neural networks trained by empirical risk minimization are sensitive to small, deliberately chosen perturbations of their inputs ("adversarial examples"). A standard defence is adversarial training: at each step, perturb the training example to increase the loss, then take a gradient step at the perturbed point. Sinha, Namkoong, Volpi and Duchi (arXiv:1710.10571, ICLR 2018) recast adversarial training as distributionally robust optimization over a Wasserstein ball around the data distribution, and replaced the hard ball constraint by a Lagrangian penalty. The resulting procedure perturbs each example by solving a penalized inner maximization, and the paper shows that, when the penalty is large enough relative to the smoothness of the loss, this inner problem is strongly concave and therefore tractable.

This mission formalizes the paper's computational guarantee, Theorem 2: stochastic gradient descent on the penalized robust objective, with an inexact adversary, reaches an approximate stationary point at the rate of smooth nonconvex stochastic optimization. The analysis follows Ghadimi and Lan's argument for nonconvex SGD (arXiv:1309.5549), adapted to a gradient oracle that is biased by the inexact inner maximization.

Setting

Parameters $\theta$ live in $\Theta=\mathbb R^d$ and data in a set $Z\subseteq\mathbb R^m$; both spaces carry the Euclidean norm $\|\cdot\|_2$. Data are drawn from a probability distribution $P_0$ on $Z$.

A transportation cost $c:Z\times Z\to[0,\infty)$ measures how expensive it is to move a data point $z_0$ to $z$. Assumption A: $c$ is continuous, $c(z,z)=0$, and for each $z_0\in Z$ the map $z\mapsto c(z,z_0)$ is $1$-strongly convex. The canonical example is $c(z,z_0)=\tfrac12\|z-z_0\|_2^2$.

A loss $\ell(\theta;z)$ has partial gradients $\nabla_\theta\ell$ and $\nabla_z\ell$. Assumption B: these gradients are Lipschitz in each argument,

$$\|\nabla_\theta\ell(\theta;z)-\nabla_\theta\ell(\theta';z)\|\le L_{\theta\theta}\|\theta-\theta'\|,\quad \|\nabla_z\ell(\theta;z)-\nabla_z\ell(\theta;z')\|\le L_{zz}\|z-z'\|,$$ $$\|\nabla_\theta\ell(\theta;z)-\nabla_\theta\ell(\theta;z')\|\le L_{\theta z}\|z-z'\|,\quad \|\nabla_z\ell(\theta;z)-\nabla_z\ell(\theta';z)\|\le L_{z\theta}\|\theta-\theta'\|.$$

For a penalty $\gamma>0$, the robust surrogate and the robust objective are

$$\varphi_\gamma(\theta;z_0)=\sup_{z\in Z}\{\ell(\theta;z)-\gamma c(z,z_0)\},\qquad F(\theta)=\mathbb E_{P_0}[\varphi_\gamma(\theta;Z)].$$

By Wasserstein duality, $F(\theta)$ equals the worst-case expected loss over all distributions $P$, penalized by $\gamma$ times the transport distance from $P$ to $P_0$.

Algorithm 1 (with $\Theta=\mathbb R^d$ and constant stepsize $\alpha$): from $\theta^0$, for $t=0,\dots,T-1$, draw $z^t\sim P_0$ independently, find an $\epsilon$-approximate maximizer $\hat z^t\in Z$, meaning $\ell(\theta^t;\hat z^t)-\gamma c(\hat z^t,z^t)\ge\varphi_\gamma(\theta^t;z^t)-\epsilon$, and set $\theta^{t+1}=\theta^t-\alpha\nabla_\theta\ell(\theta^t;\hat z^t)$.

Formalization targets

Goal: Theorem 2 (p. 6)

Let $\gamma>L_{zz}$, $L_\varphi=L_{\theta\theta}+L_{\theta z}L_{z\theta}/(\gamma-L_{zz})$, $\Delta_F\ge F(\theta^0)-\inf_\theta F(\theta)$, and assume $\mathbb E\|\nabla F(\theta)-\nabla_\theta\varphi_\gamma(\theta;Z)\|_2^2\le\sigma^2$ for all $\theta$. With $\alpha=\sqrt{\Delta_F/(L_\varphi T\sigma^2)}$ and $T\ge L_\varphi\Delta_F/\sigma^2$,

$$\frac1T\sum_{t=0}^{T-1}\mathbb E\big[\|\nabla F(\theta^t)\|_2^2\big]-\frac{4L_{\theta z}^2}{\gamma-L_{zz}}\,\epsilon\le4\sigma\sqrt{\frac{L_\varphi\Delta_F}{T}}.$$

Milestones

1. (4), p. 4: for $\gamma\ge L_{zz}$, $z\mapsto\ell(\theta;z)-\gamma c(z,z_0)$ is $(\gamma-L_{zz})$-strongly concave.
2. Lemma 1, p. 5: the supremum $\bar f(\theta)=\sup_{z\in Z}f(\theta,z)$ of a $\lambda$-strongly concave family satisfying Assumption B is differentiable, with $\nabla\bar f(\theta)=\nabla_\theta f(\theta,z_\star(\theta))$, a $(L_{z\theta}/\lambda)$-Lipschitz maximizer and a $(L_{\theta\theta}+L_{\theta z}L_{z\theta}/\lambda)$-Lipschitz gradient.
3. §2.1, p. 6: $\varphi_\gamma(\cdot;z_0)$ has $L_\varphi$-Lipschitz gradient $\nabla_\theta\varphi_\gamma(\theta;z_0)=\nabla_\theta\ell(\theta;z_\star(z_0,\theta))$.
4. (31) and (32), p. 40: the descent inequality for an $L_\varphi$-smooth objective, and its form with the bias $\delta=g-\nabla_\theta\varphi_\gamma$ separated, for $\alpha\le1/L_\varphi$.
5. The bias bound, p. 41: $\|\delta\|_2^2\le 2L_{\theta z}^2\epsilon/(\gamma-L_{zz})$.
6. The one-step bound in conditional expectation and the averaged bound, p. 41:

$$\frac1T\sum_{t<T}\mathbb E\|\nabla F(\theta^t)\|_2^2\le2\hat\epsilon+\frac{2\Delta_F}{\alpha T}+2L_\varphi\alpha\sigma^2,\qquad\hat\epsilon=\frac{2L_{\theta z}^2}{\gamma-L_{zz}}\epsilon,$$

for every constant stepsize $0<\alpha\le1/L_\varphi$. The goal is this bound at the balancing stepsize.

Significance

The result. Theorem 2 certifies that the robust training procedure is no harder, in iteration count, than ordinary nonconvex SGD: the stationarity measure decays as $T^{-1/2}$, and the inexactness of the adversary enters only as an additive term proportional to $\epsilon$, independent of $T$. This is what licenses running a few steps of gradient ascent for the inner problem rather than solving it exactly. It also explains the role of the penalty: the guarantee requires $\gamma>L_{zz}$, so smoothness of the loss in the data (smooth activations rather than ReLUs) is what makes the robust problem tractable.

Formalizing it. The result and its proof are published; nothing here is open. To our knowledge none of it is machine-checked. A formal proof would add a verified Danskin-type theorem for strongly concave suprema with explicit Lipschitz constants (Lemma 1), which is reusable well beyond this paper, and a verified nonconvex SGD analysis with a biased oracle, including the measure-theoretic bookkeeping (independence of the fresh sample from the current iterate, differentiation under the integral) that the paper's proof compresses into one line.

Difficulty

The deterministic inequalities (31), (32) and the bias bound are short. The weight sits elsewhere. First, Lemma 1 requires differentiability of a supremum over a possibly unbounded set, with the maximizer depending on $\theta$; the paper invokes a Danskin-type theorem that is not in Mathlib, and the cost $c$ is not assumed differentiable, so the first-order optimality conditions for the inner problem must be derived from strong convexity alone. Second, the expectation step uses $\mathbb E[\nabla_\theta\varphi_\gamma(\theta^t;z^t)\mid\theta^t]=\nabla F(\theta^t)$, which needs both differentiation under the integral sign for $F$ and the independence of $z^t$ from $\theta^t$ along the run. Third, finiteness of every expectation along the run is not assumed and must be propagated from step to step.

Formalization scope

Lean representation: $\Theta$ and $\mathbb R^m$ are EuclideanSpace ℝ (Fin d) and EuclideanSpace ℝ (Fin m); $Z$ is a set in the latter. The loss is a function on all of $\mathbb R^d\times\mathbb R^m$; its partial gradients are required at points of $Z$ and the Lipschitz conditions on $Z$ only. Strong convexity is Mathlib's StrongConvexOn, whose modulus convention matches the paper. Suprema are sSup over the image of $Z$. $F$ is a Bochner integral, and $\varphi_\gamma(\theta;\cdot)$ is assumed $P_0$-integrable for every $\theta$. The run is driven by $(z^0,\dots,z^{T-1})\sim P_0^{\otimes T}$ (Measure.pi). The expectations in the conclusion and in the variance hypothesis are lower Lebesgue integrals in $[0,\infty]$; the $\epsilon$-term of Theorem 2 is moved to the right-hand side.

Hypotheses made explicit that the paper leaves implicit: $\gamma>L_{zz}$ (the paper writes $\gamma\ge L_{zz}$ but divides by $\gamma-L_{zz}$); $Z$ nonempty, convex and closed; Lipschitz constants nonnegative; $\sigma>0$, $\Delta_F>0$, $T\ge1$, $\epsilon\ge0$; $F$ bounded below (so $\inf_\theta F$ is a real number); integrability of $\varphi_\gamma(\theta;\cdot)$; $P_0(Z)=1$; joint measurability of the oracle $(\theta,z_0)\mapsto\hat z(\theta,z_0)$; and, in (32) and the later milestones, $0<\alpha\le1/L_\varphi$, which the paper assumes "in the rest of the proof". Lemma 1 is specialized to the Euclidean norm, the case Theorem 2 uses. The cost $c$ is not assumed differentiable.

A trivializing formalization is ruled out: the run uses an oracle tied to $\varphi_\gamma$ by the $\epsilon$-gap and to $Z$ by membership, $\varphi_\gamma$ is the supremum of the penalized loss over $Z$, $F$ is its $P_0$-integral, and the hypotheses are satisfiable (for instance $\ell(\theta;z)=\tfrac12\|\theta\|^2$, $c(z,z_0)=\tfrac12\|z-z_0\|^2$, $Z=\mathbb R^m$, $P_0$ a point mass, $\epsilon=0$). Expectations as lower integrals prevent a non-integrable $\|\nabla F(\theta^t)\|^2$ from being read as $0$.

Infrastructure a complete development needs: the descent lemma for functions with Lipschitz gradient; first-order characterizations of strong concavity on a convex set; a Danskin/envelope theorem for strongly concave suprema; differentiation under the integral for $F$; and conditional-expectation bookkeeping for Markov-type recursions driven by i.i.d. samples on a finite product space. The first three are reusable in any minimax or bilevel analysis. Contributions to any milestone, or to these supporting facts as separate lemmas, are welcome.

Selected references

• A. Sinha, H. Namkoong, R. Volpi, J. Duchi, Certifying Some Distributional Robustness with Principled Adversarial Training, ICLR 2018; arXiv:1710.10571v5, 2020. https://arxiv.org/abs/1710.10571
• S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4), 2013. https://doi.org/10.1137/120880811
• J. F. Bonnans, A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
• R. Gao, A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, Mathematics of Operations Research 48(2), 2023; arXiv:1604.02199. https://arxiv.org/abs/1604.02199