Machine Learning

Motivation

Many optimization problems are posed over a manifold rather than a vector space: orthogonality constraints (the Stiefel manifold), unit-norm constraints (the sphere), fixed-rank matrices. In some of them the objective can only be evaluated, not differentiated. Black-box adversarial attacks on a neural network with a norm-constrained perturbation, hyperparameter tuning and simulation-based objectives are examples, and in all of them each function value is also noisy. Zeroth-order (derivative-free) methods replace the gradient by a random finite-difference estimate built from function values alone.

In Euclidean space the analysis of such methods is well developed. Nesterov and Spokoiny (2017) analysed Gaussian-smoothing estimators for deterministic objectives, and Ghadimi and Lan (2013) gave the first non-asymptotic stationarity rates for stochastic nonconvex objectives (the RSGF method). Li, Balasubramanian and Ma (arXiv:2003.11238, published in Mathematics of Operations Research, 2023) carried this programme to embedded submanifolds. They estimate the Riemannian gradient by projecting a Gaussian vector onto the tangent space and moving along a retraction, and they prove convergence rates for the resulting methods. This mission formalizes their rate for the stochastic method, ZO-RSGD (Theorem 3.2).

Setting

Let $E$ be a finite-dimensional real inner product space (the paper's $\mathbb R^n$), and let $\mathcal M \subseteq E$ be a $C^1$ embedded submanifold of dimension $d$. The tangent space $T_x\mathcal M$ at $x \in \mathcal M$ is the linear span of the tangent cone of $\mathcal M$ at $x$. For a submanifold this is the set of velocities $\gamma'(0)$ of curves in $\mathcal M$ through $x$, and it is a subspace of dimension $d$. $\mathcal M$ carries the metric induced by the inner product of $E$, and $P_x$ denotes the orthogonal projection of $E$ onto $T_x\mathcal M$.

A retraction is a map $R$, $(x, \eta) \mapsto R_x(\eta)$. For every $x \in \mathcal M$ it sends all of $T_x\mathcal M$ into $\mathcal M$ and is smooth on $T_x\mathcal M$, with $R_x(0) = x$ and differential the identity at $0$. The Riemannian gradient of a differentiable $f$ is $\operatorname{grad} f(x) = P_x \nabla f(x)$.

The objective is stochastic, $f(x) = \mathbb E_\xi F(x, \xi)$, with noise $\xi$ distributed according to a probability measure $P_\xi$. Two assumptions are imposed:

• Assumption 2.1 ($L$-retraction-smoothness). For almost every $\xi$, $|F(R_x(\eta),\xi) - F(x,\xi) - \langle \operatorname{grad}F(x,\xi), \eta\rangle| \le \frac L2\|\eta\|^2$ for all $x \in \mathcal M$ and $\eta \in T_x\mathcal M$.
• Assumption 2.3 (unbiased oracle, bounded variance). For every $x \in \mathcal M$, $\mathbb E_\xi F(x,\xi) = f(x)$, $\mathbb E_\xi \operatorname{grad}F(x,\xi) = \operatorname{grad}f(x)$ and $\mathbb E_\xi\|\operatorname{grad}F(x,\xi) - \operatorname{grad}f(x)\|^2 \le \sigma^2$.

Given a smoothing parameter $\mu > 0$ and a batch size $m$, draw $m$ independent pairs $(u_{0,i}, \xi_i)$, each with $u_{0,i} \sim \mathcal N(0, I)$ independent of $\xi_i \sim P_\xi$, and put $u_i = P_x u_{0,i}$. The mini-batch zeroth-order Riemannian gradient is

$$\bar g_{\mu,\xi}(x) = \frac1m\sum_{i=1}^m \frac{F(R_x(\mu u_i), \xi_i) - F(x, \xi_i)}{\mu}\,u_i .$$

ZO-RSGD (Algorithm 2) starts at $x_0 \in \mathcal M$ and iterates $x_{k+1} = R_{x_k}(-\hat\eta\,\bar g_{\mu,\xi}(x_k))$ with step $\hat\eta = 1/L$ and a fresh batch at every step. $x^*$ denotes a minimizer of $f$ over $\mathcal M$.

Formalization targets

Goal: Theorem 3.2

If $m \ge 16(d+4)$, then for every $N$

$$\frac{1}{N+1}\sum_{k=0}^{N}\mathbb E\,\|\operatorname{grad} f(x_k)\|^2 \le 4L\,\frac{f(x_0) - f(x^*)}{N+1} + 2\mu^2L^2(d+6)^3 + \frac{16(d+4)}{m}\sigma^2 .$$

The constants are the paper's own. The goal states the rate for every $\mu$, $m$ and $N$. It does not state the parameter choices $\mu = O(\epsilon/d^{3/2})$, $m = O(d\sigma^2/\epsilon^2)$, $N = O(1/\epsilon^2)$ that follow from it.

Milestones

• Lemma 2.1. For a $d$-dimensional subspace $\mathcal X$ with projection $P$, $u = Pu_0$ and $x \in \mathcal X$: $\mathbb E\langle x,u\rangle u = x$ and $\mathbb E\langle x,u\rangle^2 = \|x\|^2$.
• Lemma 2.2 (Nesterov–Spokoiny). $\mathbb E\|u\|^p \le (n+p)^{p/2}$ for a standard Gaussian $u$ on $\mathbb R^n$ and $p \ge 2$. This is already proved on the platform and is reused.
• Corollary 2.1. $\mathbb E\|Pu_0\|^p \le (d+p)^{p/2}$.
• Proposition 2.1(a). $\|\mathbb E\,g_\mu(x) - \operatorname{grad}f(x)\| \le \frac{\mu L}{2}(d+3)^{3/2}$ for the single-sample estimator $g_\mu$.
• Lemma 3.1. $\mathbb E\|\bar g_{\mu,\xi}(x) - \operatorname{grad}f(x)\|^2 \le \mu^2L^2(d+6)^3 + \frac{8(d+4)}{m}\sigma^2 + \frac{8(d+4)}{m}\|\operatorname{grad}f(x)\|^2$.

Significance

Theorem 3.2 is the basic complexity result for derivative-free stochastic optimization on manifolds. With the parameter choices of (3.10) it gives an $\epsilon$-stationary point in expectation after $O(d/\epsilon^4)$ noisy function evaluations. The dependence is on the manifold dimension $d$, not on the ambient dimension $n$. This matches the Euclidean rate of Ghadimi and Lan with $n$ replaced by $d$, and it is what makes projected-Gaussian estimators attractive when $d \ll n$ (for example, low-dimensional Stiefel manifolds embedded in large matrix spaces).

The results are proved in the paper (main text, p. 17, and Appendix C) but, to our knowledge, none of them has been machine-checked. The Euclidean Gaussian moment bound (Lemma 2.2) is formalized on the platform. The Euclidean RSGF results of Ghadimi and Lan are stated on the platform, and they are different statements: they use $x + \mu u$ instead of a retraction, the full space instead of a tangent space, and a random output index. A complete formalization would also produce reusable infrastructure: Gaussian identities for orthogonal projections, the projected-Gaussian moment bound, and a template for proving stationarity rates of random iterates on a product probability space.

Difficulty

The Euclidean argument relies on a smoothed function $f_\mu(x) = \mathbb E f(x + \mu u)$ whose gradient is exactly the mean of the estimator. That identity has no Riemannian analogue: $R_x(\mu u)$ is not a translate, so $\mathbb E\,g_\mu(x)$ is not the gradient of any smoothed function. The bias in Proposition 2.1(a) has to be bounded directly from Assumption 2.1, and this is why the estimator is only approximately unbiased.

The convergence proof needs a one-step descent inequality conditioned on the past. The direction at step $k$ is projected onto $T_{x_k}\mathcal M$, which depends on all earlier draws, so the conditional bound of Lemma 3.1 must be integrated against the product law of the batches. A naive reading that samples every direction from one fixed subspace, or that treats the iterates as deterministic, does not describe the algorithm. A further subtlety is that the gradient term of Lemma 3.1 must be absorbed by the descent of one step. This requires the batch to be large compared with the dimension, $m \ge 16(d+4)$.

Formalization scope

• $E$ is any finite-dimensional real inner product space with its Borel σ-algebra. The Gaussian is Mathlib's stdGaussian E.
• $\mathcal M$ and its dimension are given by the published ProjLikeRetr.Retractor.IsSubmanifold 1 d M (a $C^1$ coordinate-slice submanifold), so $d$ is tied to $\mathcal M$ and is never a free number. $T_x\mathcal M$ is the published ProjLikeRetr.Retractor.tangentSpace M x, never an arbitrary subspace.
• The retraction is defined on all of each tangent space, as the paper requires (Assumption 2.1 holds "for all $\eta \in T_x\mathcal M$, i.e., $\rho_x = \infty$"). The objective $f$ and the samples $F(\cdot,\xi)$ are assumed differentiable rather than smooth, which is all the gradient formula (2.3) uses.
• Added hypotheses. The goal assumes $m \ge 16(d+4)$. The paper's proof assumes it explicitly, but the theorem statement omits it. The goal also assumes that $(x,\eta) \mapsto R_x(\eta)$ and $x \mapsto P_x$ are measurable, so that the iterates are random variables; this holds for closed $\mathcal M$ such as spheres and Stiefel manifolds. Lemma 3.1 is stated for every $m \ge 1$. The paper's last proof step uses $m \ge 2$, but the bound holds for $m = 1$ as well.
• The iterates are defined for every $k$ on the sequence space of i.i.d. batches (the algorithm without a stopping index), so $x_{N+1}$ exists.
• No junk expectations. Every expectation of a nonnegative quantity is a lower Lebesgue integral compared with ENNReal.ofReal of the bound. Every vector-valued expectation comes with an integrability conclusion, and Assumption 2.3 carries the integrability of $F(x,\cdot)$ and $\operatorname{grad}F(x,\cdot)$. So no statement can hold because a Bochner integral defaulted to $0$.
• The $O(\cdot)$ parameter choices (3.10) and the oracle complexity $mN = O(d/\epsilon^4)$ are not formalized.
• The development needs projections of Gaussian measures onto subspaces, moments of Gaussian norms, conditional expectation along an i.i.d. sequence of batches, and telescoping. Proofs of any milestone are welcome, as are general lemmas about the push-forward of stdGaussian under an orthogonal projection.

Selected references

• J. Li, K. Balasubramanian, S. Ma, Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization, Mathematics of Operations Research, 2023. Preprint arXiv:2003.11238v3. https://arxiv.org/abs/2003.11238
• Y. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17, 2017. https://doi.org/10.1007/s10208-015-9296-2
• S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4), 2013. https://arxiv.org/abs/1309.5549
• K. Balasubramanian, S. Ghadimi, Zeroth-Order Nonconvex Stochastic Optimization: Handling Constraints, High Dimensionality, and Saddle Points, Foundations of Computational Mathematics, 2022. https://arxiv.org/abs/1809.06474
• N. Boumal, P.-A. Absil, C. Cartis, Global Rates of Convergence for Nonconvex Optimization on Manifolds, IMA Journal of Numerical Analysis, 2019. https://arxiv.org/abs/1605.08101
• P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008.

Motivation

A generative model lets a planner request independent next-state samples for any state-action pair. This is a useful idealization for studying how many simulator calls are needed before a policy computed from an estimated model performs well in the true environment. Li, Wei, Chi, and Chen show that a small independent perturbation of the rewards lets a model-based planner meet a sample-size bound with cubic dependence on the effective horizon $1/(1-\gamma)$, while providing guarantees for both values and action values (Li et al., 2024). This mission isolates their perturbed-planning result and the source lemmas that support it.

Setting

A finite discounted Markov decision process consists of a state set $S$, an action set $A$, a transition probability $P(s'\mid s,a)$, an immediate reward $r(s,a)\in[0,1]$, and a discount factor $\gamma\in(0,1)$. A deterministic policy $\pi:S\to A$ chooses an action at each state. Its value $V^\pi(s)$ is the expected sum of rewards, discounted by $\gamma^t$, from state $s$. Its action value $Q^\pi(s,a)$ takes action $a$ first and follows $\pi$ thereafter. The optimal values $V^\star$ and $Q^\star$ are those of an optimal deterministic policy; equivalently, $Q^\star(s,a)=r(s,a)+\gamma\sum_{s'}P(s'\mid s,a)V^\star(s')$.

For each $(s,a)$, draw $N$ independent next states from $P(\cdot\mid s,a)$, independently across pairs. The empirical kernel $\widehat P$ is their frequency table. Independently draw one reward perturbation $\zeta(s,a)\sim\operatorname{Unif}(0,\xi)$ per pair and set $r_p=r+\zeta$. The planner returns an optimal deterministic policy $\widehat\pi_p^\star$ for the empirical MDP $(S,A,\widehat P,r_p,\gamma)$. The performance claim evaluates this policy under the original $P$ and $r$, so the perturbation changes policy selection but not the evaluation target.

Formalization targets

Perturbed model-based planning

Theorem 1 of Li et al. asserts that absolute constants $c_0,c_1>0$ can be chosen before $S$, $A$, $P$, $r$, $\gamma$, $\varepsilon$, and $\delta$. For $\delta>0$, $0<\varepsilon\le1/(1-\gamma)$, and $\xi=c_1(1-\gamma)\varepsilon/(|S|^5|A|^5)$, the sample-size condition is

$$N\ge\frac{c_0\log\!\bigl(|S||A|/((1-\gamma)\varepsilon\delta)\bigr)}{(1-\gamma)^3\varepsilon^2}.$$

With probability at least $1-\delta$ over both the samples and the perturbation, every optimal policy of the perturbed empirical MDP simultaneously satisfies

$$V^{\widehat\pi_p^\star}(s)\ge V^\star(s)-\varepsilon,\qquad Q^{\widehat\pi_p^\star}(s,a)\ge Q^\star(s,a)-\gamma\varepsilon\quad\text{for all }(s,a).$$

The milestone list follows the paper's numbered statements: fixed-policy and Bernstein-condition value bounds (Lemmas 1–2), calibrated state-action absorbing models and their finite reward grid (Lemma 3, (88), Lemma 4), planning under a separated optimum (Lemma 5), separation induced by random rewards (Lemma 6), and the reward-change bound before (49). The paper's additional claim about iteration counts for empirical QVI and PI is outside this target.

Significance

The theorem gives a policy guarantee from a finite number of calls to a generative model. It bounds the true value of the selected policy at every state and its true action value at every state-action pair, rather than only the empirical objective used to select the policy. Its $N$ is the number of samples per pair; the total number of transitions observed is $N|S||A|$. The statement is a theorem proved in the cited paper, not an open mathematical conjecture (Li et al., Theorem 1).

The formalization work is to turn the paper's probability experiment, policy choice, and linked inequalities into machine-checked statements and eventually machine-checked proofs. The published FoundationsML transition kernel and policy-value definitions provide reusable base objects. This mission adds a finite generative-sample law, the reward-perturbation law, and an absorbing-MDP interface. Those objects can support later formalizations of empirical planning and policy evaluation beyond this theorem. The goal and milestone proofs remain open in the present draft.

Difficulty

A fixed policy can be evaluated against an empirical transition kernel using concentration at that policy. The planner's policy depends on the same sampled kernel, so a fixed-policy bound cannot simply be applied to it. Small changes in transition frequencies may also switch the chosen optimal action when actions have nearly equal values. The paper's intermediate results specify the needed value-control and separation properties; a Lean proof must track their constants and their probability events without silently assuming that the data-dependent policy was fixed before sampling (Li et al., §§6.2–6.3).

Formalization scope

The Lean state and action types are finite, and both are nonempty where cardinalities occur in denominators. A transition kernel is a probability vector at each state-action pair. Policies are deterministic functions $S\to A$, embedded as point-mass stochastic policies for the published value definitions. $V^\star$ is the maximum over the finite set of deterministic policies; $Q^\star$ is $r+\gamma PV^\star$. Function norms are supremum norms. The empirical kernel is the frequency table of a finite array of samples, with $N>0$ in the goal because its formula divides by $N$. The independent perturbation is the uniform measure on the cube $[0,\xi]^{S\times A}$.

Probability claims bound the failure event. The data law is a finite product, and the auxiliary continuous draw is measured section by section. This formulation allows an outer measure for a section whose measurability is not already known; it does not let a nonmeasurable success event satisfy the result for free. The main theorem quantifies over every optimal policy of the empirical perturbed model, and its universal constants do not depend on the instance. These choices rule out treating the selected policy as arbitrary, fixing the perturbation in advance, or choosing constants after seeing the MDP.

The absorbing-MDP construction changes one transition row and one reward. The reward at that row may leave $[0,1]$, so the underlying value function accepts arbitrary real rewards even though the main MDP has normalized rewards. Lemma 5 is stated with normalized rewards as printed. Reusable contributions include basic properties of the sampling law, optimal-policy existence, the absorbing construction, and quantitative value stability; the milestone statements themselves are the intended proof targets.

Selected references

• G. Li, Y. Wei, Y. Chi, and Y. Chen, Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model, Operations Research, 2024; arXiv:2005.12900v8.

Motivation

Many optimization problems in statistics and machine learning constrain the variable to a smooth manifold: orthonormal frames in sparse PCA and dictionary learning (the Stiefel manifold), unit vectors in phase retrieval (the sphere), fixed-rank matrices in matrix completion. Riemannian optimization handles these problems directly on the manifold. A step is taken in the tangent space and mapped back to the manifold by a retraction.

In several applications the objective can be evaluated but not differentiated: black-box adversarial attacks, simulation-based models, and hyperparameter or policy tuning. Zeroth-order (derivative-free) methods replace the gradient by an estimator built from function values. In Euclidean space the standard construction is Gaussian smoothing, analysed by Nesterov and Spokoiny (2017) and Ghadimi and Lan (2013). Li, Balasubramanian and Ma (arXiv:2003.11238; Mathematics of Operations Research, 2023) carry the construction over to embedded submanifolds. They sample a Gaussian vector, project it onto the tangent space, and use the retraction in place of the straight line $x+\mu u$. This mission formalizes their first optimization guarantee: the convergence rate of zeroth-order Riemannian gradient descent (ZO-RGD).

Setting

Let $E$ be a finite-dimensional real inner product space (the ambient $\mathbb R^n$). Let $M\subseteq E$ be a $C^1$ embedded submanifold of dimension $d$. At each $x\in M$ the tangent space $T_xM$ is a $d$-dimensional linear subspace of $E$; let $P_x$ denote the orthogonal projection onto it. $M$ carries the metric induced by the inner product of $E$.

A retraction is a map $(x,\eta)\mapsto R_x(\eta)$ such that, for every $x\in M$, $R_x$ is smooth on $T_xM$, maps $T_xM$ into $M$, satisfies $R_x(0)=x$, and has the identity as its differential at $0$. In this mission $R_x$ is defined on all of $T_xM$.

For a differentiable $f:E\to\mathbb R$ the Riemannian gradient is $\operatorname{grad} f(x)=P_x\nabla f(x)$. Assumption 2.1 (retraction smoothness) asks for a constant $L\ge0$ such that

$$\big|f(R_x(\eta))-f(x)-\langle \operatorname{grad} f(x),\eta\rangle\big|\le \tfrac L2\|\eta\|^2\qquad(x\in M,\ \eta\in T_xM).$$

Given $\mu>0$ and a standard Gaussian vector $u_0\sim N(0,I_n)$ of $E$, set $u=P_xu_0$. The zeroth-order Riemannian gradient estimator is

$$g_\mu(x)=\frac{f(R_x(\mu u))-f(x)}{\mu}\,u .$$

ZO-RGD (Algorithm 1) starts at $x_0\in M$, draws independent Gaussian vectors $u_0^0,u_0^1,\dots$, and sets $x_{k+1}=R_{x_k}(-\hat\eta\, g_\mu(x_k))$, where $g_\mu(x_k)$ uses $u_k=P_{x_k}u_0^k$. The step size is $\hat\eta=1/(2(d+4)L)$. Let $x^*\in M$ be a minimizer of $f$ over $M$.

Formalization targets

Goal: Theorem 3.1

For every $N\ge0$,

$$\frac1{N+1}\sum_{k=0}^{N}\mathbb E\,\|\operatorname{grad} f(x_k)\|^2\le\frac4{\hat\eta}\left(\frac{f(x_0)-f(x^*)}{N+1}+C(\mu)\right),$$

where $4/\hat\eta=8(d+4)L$ and

$$C(\mu)=\frac{\mu^2L}{16}\frac{(d+3)^3}{d+4}+\frac{\mu^2L}{16}\frac{(d+6)^3}{d+4}+\frac{\mu^2L}{16}\frac{(d+6)^3}{(d+4)^2}.$$

Milestones

These are the paper's own intermediate results (§2.2, p. 8):

1. Lemma 2.1. For a subspace $\mathcal X$ with projection $P$, $u=Pu_0$ and $x\in\mathcal X$: $\mathbb E\langle x,u\rangle u=x$ and $\mathbb E\langle x,u\rangle^2=\|x\|^2$.
2. Lemma 2.2 (Nesterov–Spokoiny). $\mathbb E\|u\|^p\le(n+p)^{p/2}$ for $p\ge2$. This result is already on the platform as a proved theorem and is referenced.
3. Corollary 2.1. If $\dim\mathcal X=d$, then $\mathbb E\|Pu_0\|^p\le(d+p)^{p/2}$.
4. Proposition 2.1(a). $\|\mathbb E g_\mu(x)-\operatorname{grad} f(x)\|\le\frac{\mu L}{2}(d+3)^{3/2}$.
5. Proposition 2.1(b). $\|\operatorname{grad} f(x)\|^2\le2\|\mathbb E g_\mu(x)\|^2+\frac{\mu^2}{2}L^2(d+6)^3$.
6. Proposition 2.1(c). $\mathbb E\|g_\mu(x)\|^2\le\frac{\mu^2}{2}L^2(d+6)^3+2(d+4)\|\operatorname{grad} f(x)\|^2$.

Significance

Theorem 3.1 shows that ZO-RGD reaches an $\epsilon$-stationary point in expectation using $O(d/\epsilon^2)$ function evaluations, provided the smoothing parameter is of order $\epsilon/d^{3/2}$. The dimension that enters is the intrinsic dimension $d$ of the manifold, not the ambient dimension $n$. For the Stiefel manifold of $n\times p$ orthonormal frames this is the difference between $np-p(p+1)/2$ and $np$, and for the sphere between $n-1$ and $n$. More importantly, the estimator never explores normal directions. The three estimates of Proposition 2.1 are the toolkit that the paper reuses for its stochastic (ZO-RSGD), proximal (ZO-ManPG) and second-order variants.

The paper proves these results on paper; none of them has a machine-checked proof. The mission adds three things. It gives a precise model of a random iterate sequence on a submanifold, driven by the infinite product of Gaussian draws. It formalizes the projected-Gaussian identities, which are reusable for any method that samples in tangent spaces. And it pins down the constants. In checking the constants, the printed Proposition 2.1(b) turned out to be false for large $L$ (its proof yields $L^2$, not $L$), and the middle term of the printed $C(\mu)$ inherits that slip. The statements here carry the constants the proofs actually give.

Difficulty

In Euclidean space, $\mathbb E\,g_\mu(x)$ is exactly the gradient of the Gaussian-smoothed function $f_\mu(x)=\mathbb E f(x+\mu u)$, and the analysis runs on $f_\mu$. Once a retraction replaces $x+\mu u$, no smoothed function has $\mathbb E g_\mu$ as its gradient. The bias must be estimated directly from Assumption 2.1, which controls $f\circ R_x$ only along the tangent space. The moment bounds must then be taken for a Gaussian projected onto a subspace that changes with $x$.

In the descent argument, the direction $u_k$ is sampled in $T_{x_k}M$, which depends on all earlier draws. The expectation of step $k$ is therefore conditional on the past. Summing the one-step inequality requires conditional expectations on the product space, together with measurability of the iterate map. Finiteness of $\mathbb E f(x_k)$ is not given and must be handled as well.

Formalization scope

• Space. The ambient space is a finite-dimensional real inner product space $E$. The standard Gaussian is Mathlib's stdGaussian E, so $\kappa^{-1}\int\cdots e^{-\|u_0\|^2/2}du_0$ becomes integration against it.
• Manifold and tangent spaces. The manifold is given by the published coordinate-slice predicate ProjLikeRetr.Retractor.IsSubmanifold 1 d M, which ties $d$ to $M$. The tangent space is the published ProjLikeRetr.Retractor.tangentSpace M x, the span of Mathlib's tangent cone. Neither $d$ nor the tangent spaces are free parameters.
• Retraction. The retraction is global: Assumption 2.1 is required for every $\eta\in T_xM$ (the paper's "$\rho_x=\infty$"). "Smooth" means $C^\infty$, not analytic.
• Regularity of $f$. $f$ is assumed differentiable on $E$, which is what the definition $\operatorname{grad} f=P_x\nabla f$ needs. This is weaker than the paper's "smooth".
• Constants. The goal takes $L>0$, because the step size divides by $L$. The milestones take $L\ge0$ and $\mu>0$.
• Draws and iterates. The draws live on $E^{\mathbb N}$ with the infinite product of standard Gaussian measures. The iterates are defined for every $k$: the algorithm runs without a stopping time, so the sum over $k=0,\dots,N$ is meaningful.
• Minimizer. $x^*$ is an attained minimizer over $M$.
• Measurability. The goal adds two measurability hypotheses that make the iterates random variables: $(x,\eta)\mapsto R_x(\eta)$ is measurable and $x\mapsto P_x$ is measurable. Both hold for closed manifolds such as spheres and Stiefel manifolds.
• Corrected constants. Proposition 2.1(b) carries $L^2$, and the middle term of $C(\mu)$ carries $L$. The milestone texts keep the printed forms. Proposition 2.1(a) and (c) are as printed.
• Not formalized. The parameter choices $\mu=O(\epsilon/d^{3/2})$, $N=O(d/\epsilon^2)$ in the theorem's second sentence are an $O(\cdot)$ statement.

Several trivializing formalizations are ruled out. A Bochner integral of a non-integrable function is $0$, so every expectation in a conclusion is either a lower Lebesgue integral compared with a finite bound or paired with an integrability conjunct. The dimension $d$ comes from the manifold, not from a free natural number. The projection is onto $M$'s own tangent space, never onto an arbitrary subspace field.

A complete development needs the following infrastructure:

• the law of $P u_0$ (a standard Gaussian on the subspace);
• Gaussian moment bounds;
• conditional expectation along the product filtration;
• measurability of the iterate map.

The projected-Gaussian lemmas and the iterate model are reusable for the stochastic variant (ZO-RSGD) in the companion mission. Contributions of proofs for any milestone, and of general lemmas about Gaussian measures restricted to subspaces, are welcome.

Selected references

• J. Li, K. Balasubramanian, S. Ma, Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization, Mathematics of Operations Research, 2023; preprint arXiv:2003.11238v3, 2021. https://arxiv.org/abs/2003.11238
• Y. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17 (2017) 527–566. https://doi.org/10.1007/s10208-015-9296-2
• S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23 (2013) 2341–2368. https://doi.org/10.1137/120880811
• P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244

Motivation

Model-based reinforcement learning algorithms for Markov decision processes estimate each transition distribution $P_{s,a}$ from the transitions they have observed out of the state–action pair $(s,a)$. Their regret analyses then need to know how far the empirical distribution $\hat p$ can be from the true one $p$. The standard tool is an $\ell_1$ bound on $\hat p-p$, as in UCRL2 (Jaksch, Ortner and Auer, 2010), which costs a factor of order $\sqrt S$ in the number of states $S$. What the analysis actually uses, however, is the deviation along one direction: the projection $(\hat p-p)^Th$ onto a bias (or value) vector $h$ whose entries differ by at most the MDP's diameter $D$.

S. Agrawal and R. Jia (arXiv:1705.07041v3, published in Mathematics of Operations Research, 2023, as Optimistic Posterior Sampling for Reinforcement Learning: Worst-Case Regret Bounds) prove a worst-case regret bound of order $\tilde O(D\sqrt{SAT})$ for an optimistic variant of posterior sampling. One ingredient of that analysis is their Proposition 5.2: a Bernstein-type bound on $(\hat p-p)^Th$ whose leading term is governed by a variance of $h$ under $p$, written in stick-breaking form. This mission formalizes that proposition and the steps of its proof.

Setting

Fix a number of states $S$ and order them $1,\dots,S$. A probability vector $p\in\Delta^S$ has $p_i\ge0$ and $\sum_ip_i=1$. A multinoulli trial with parameter $p$ is a random state $X$ with $\mathbb P(X=i)=p_i$. Draw $n$ independent trials $X_1,\dots,X_n$ and let

$$\hat p_i=\frac{\#\{t: X_t=i\}}{n}$$

be the empirical probability vector, the average of the one-hot outcomes. For $p$ and a vector $h\in\mathbb R^S$ define the stick-breaking quantities

$$\gamma_i=\frac{p_i(p_{i+1}+\cdots+p_S)}{p_i+\cdots+p_S},\qquad H_{i+1}=\frac{1}{\sum_{j=i+1}^Sp_j}\sum_{j=i+1}^Sh_jp_j,\qquad c_i=h_i-H_{i+1}.$$

Thus $H_{i+1}$ is the mean of $h$ under $p$ conditioned on the states after $i$, and $c_i$ compares $h_i$ with it. The sum $\sum_{i<S}\gamma_ic_i^2$ equals the variance of $h(X)$ for $X\sim p$. In Lean these objects are gammaCoef p i, Hnext p h i, cCoef p h i, phat ω i, the law of one trial is cat p and the law of $n$ trials is trialsLaw n p, all in the namespace OptimisticPSRL.Concentration.

Formalization targets

Goal: Proposition 5.2 (p. 9)

Let $h\in\mathbb R^S$ satisfy $|h_i-h_{i'}|\le D$ for all $i,i'$, let $n\ge96$ and $\rho\in(0,1)$. Then, with probability at least $1-\rho$,

$$\big|(\hat p-p)^Th\big|\le2\sqrt{\log(n/\rho)\sum_{i<S}\frac{\gamma_ic_i^2}{n}}+3D\,\frac{\log(2/\rho)}{n}.$$

Milestones

1. Fact 1 (p. 17), a deterministic identity: for probability vectors $\tilde p,\bar p$ with stick-breaking ratios $\tilde y_i=\tilde p_i/(\tilde p_i+\cdots+\tilde p_S)$ and $\bar y_i$,

$$(\tilde p-\bar p)^Th=\sum_i(\tilde y_i-\bar y_i)(h_i-\tilde H_{i+1})(\bar p_i+\cdots+\bar p_S)=\sum_i(\tilde y_i-\bar y_i)(h_i-\bar H_{i+1})(\tilde p_i+\cdots+\tilde p_S).$$

2. The projection as a sum of martingale differences (proof, p. 21): with $Z_{t,i}=c_i\mathbb 1(X_t=i)-c_i\frac{p_i}{p_i+\cdots+p_S}\mathbb 1(X_t\ge i)$ and $Z_t=\sum_iZ_{t,i}$,

$$\frac1n\sum_{t=1}^nZ_t=(\hat p-p)^Th,$$

together with the two intermediate expressions of the page. 3. Uncorrelated coordinates (proof, p. 21): $\mathbb E[Z_{t,i}Z_{t,j}]=0$ for $i\ne j$. 4. The predictable variance (proof, p. 21): $\sum_{t=1}^n\mathbb E[Z_t^2]=\sum_ic_i^2\,n\,\gamma_i$. 5. Corollary B.1 (p. 26), Bernstein's inequality for bounded martingale differences with random predictable variance $V_n$: for $n\ge96$, $\delta\in(0,1)$, with probability greater than $1-\delta$,

$$|M_n|\le2\sqrt{V_n\ln(n/\delta)}+3K\ln(n/\delta).$$

Significance

The result. Proposition 5.2 is the concentration half of the optimism step of the paper (Lemma 5.3): combined with an anti-concentration bound for Dirichlet samples along the same direction (Proposition 5.1), it shows that some posterior sample is optimistic along $h$ with constant probability. Because the bound is stated along a single direction and is weighted by the variance of $h$ rather than by $D$ alone, it avoids the $\sqrt S$ loss that an $\ell_1$ bound would incur, which is part of how the paper's regret bound improves on UCRL2's $\tilde O(DS\sqrt{AT})$. The stick-breaking form of the variance is what lets the same quantity appear on both sides of the optimism argument, in the Dirichlet bound and in the empirical bound.

Formalizing it. The proposition and its proof steps are proved on paper; none of them has a machine-checked proof. The regret theorem of the paper (Theorem 1) is not posed: its constants are hidden in $O(\cdot)$ and its algorithm's parameters are given as $\Theta(\cdot)$. Proposition 5.2, by contrast, is fully explicit. Corollary B.1 is a reusable martingale inequality with explicit constants. The predictable-variance identity and Fact 1 are exact identities about stick-breaking coordinates that recur in analyses of Dirichlet and categorical models.

Difficulty

Two steps resist the obvious approach. First, the statement carries the variance in stick-breaking form, not as $\mathrm{Var}_p(h)$; linking the two needs the decomposition of Fact 1 and the identity for the predictable variance, which are exact algebraic identities whose bookkeeping of tails and empty tails is error-prone. Second, the paper's own route goes through Corollary B.1, a martingale Bernstein inequality with a random variance, which rests on a peeling argument over a grid of variance levels (Seldin et al., 2012); Mathlib has neither this inequality nor a Bernstein inequality with explicit constants for bounded variables.

A known subtlety: the paper's proof, through Corollary B.1, yields the second term $3D\log(n/\rho)/n$, while the statement prints the smaller $3D\log(2/\rho)/n$. The printed statement is still true for $n$ iid trials (the classical Bernstein inequality gives a bound below it), so the goal is posed as printed. The paper's own proof therefore does not establish the printed constant.

Formalization scope

• States are Fin S with its natural order, 0-based; the paper's range $i<S$ is every state but the last (belowLast S). Fact 1 holds for every ordering; the natural order covers this since states are labels.
• Probability vectors are p : Fin S → ℝ with IsProbVec p (nonnegative, summing to one). Zero entries are allowed. A ratio whose denominator is zero evaluates to $0$ (Lean's convention), which gives the values the identities need; no positivity of $p$ is assumed.
• One trial has law cat p $=\sum_ip_i\delta_i$; $n$ trials have the product law trialsLaw n p $=$ Measure.pi. The empirical vector phat ω is computed from the sample ω : Fin n → Fin S. "With probability $1-\rho$" is ENNReal.ofReal (1 - ρ) ≤ trialsLaw n p {good event}; Corollary B.1's "greater than $1-\delta$" is strict. $\log$ is Real.log.
• The proof displays (milestones 2–4) are stated in the iid reading of the proposition: the paper writes them for transitions of an MDP out of a fixed $(s,a)$, with an indicator $\mathbb 1(s_{t-1}=s,a_{t-1}=a)$ and a random count $\tau$; here the indicator is one and $\tau=n$, and the conditional expectations are expectations under one draw of law $p$. Milestone 2 assumes every drawn state has positive probability (true almost surely), which the page's intermediate sum over $i\le S-1$ needs.
• Corollary B.1 is posed for a general filtered probability space, with $Z_i$ $\mathcal F_i$-measurable, $|Z_i|\le K$ almost surely and $\mathbb E[Z_i\mid\mathcal F_{i-1}]=0$.

The goal cannot be satisfied by a degenerate reading: $\hat p$ is built from the sample, the measure is the $n$-fold product of the categorical law $p$, the event is the good event itself (not a complement bound), and the variance term is not identically zero (for $S=2$, $p=(\tfrac12,\tfrac12)$ it equals $(h_1-h_2)^2/4$).

Needed infrastructure: finite-sum manipulations over tails of Fin S; a Bernstein or Freedman inequality with explicit constants (for iid bounded variables for the goal, for martingale differences for Corollary B.1). Contributions of either inequality are reusable well beyond this mission and are welcome, as are alternative proofs of the goal that bypass Corollary B.1.

Selected references

• S. Agrawal and R. Jia, Posterior sampling for reinforcement learning: worst-case regret bounds, arXiv:1705.07041v3, 2020; published as Optimistic Posterior Sampling for Reinforcement Learning: Worst-Case Regret Bounds, Mathematics of Operations Research, 2023. https://arxiv.org/abs/1705.07041
• T. Jaksch, R. Ortner and P. Auer, Near-optimal regret bounds for reinforcement learning, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/jaksch10a.html
• Y. Seldin, F. Laviolette, N. Cesa-Bianchi, J. Shawe-Taylor and P. Auer, PAC-Bayesian inequalities for martingales, IEEE Transactions on Information Theory 58(12), 2012. https://doi.org/10.1109/TIT.2012.2211334

Motivation

In many sequential decision problems, playing one action reveals the outcome of other actions too. A bidder in a first-price auction who bids $b$ and sees the winning price learns whether every bid at or above that price would have won. A recommender that shows one item learns something about related items. Two kinds of side information recur. Graph feedback across actions: playing action $a$ also reveals the rewards of the out-neighbours of $a$ in a directed graph $G$ (Mannor and Shamir 2011; Alon, Cesa-Bianchi, Dekel and Koren 2015). Cross learning across contexts: the reward of the chosen action is revealed under every context, not only the current one (Balseiro, Golrezaei, Mahdian, Mirrokni and Schneider 2019).

Han, Zhou and Weissman (arXiv:2003.09795v7) reduce learning to bid in repeated first-price auctions to a contextual bandit with both structures. Their §3 starts from a simple arm-elimination algorithm that exploits graph feedback (Algorithm 1) and extends it to contexts with cross learning (Algorithm 2). This mission formalizes that layer: the algorithms, their concentration lemma, and their high-probability regret bounds (Theorems 3 and 4).

Timeline:

• 2011: Mannor and Shamir introduce bandits with side observations given by a graph.
• 2015: Alon, Cesa-Bianchi, Dekel and Koren show that for adversarial bandits with a directed feedback graph the minimax regret is $\tilde\Theta(\sqrt{\alpha T})$, with $\alpha$ the independence number; their Lemma 8 bounds the weak domination number by $50\alpha\log n$.
• 2016–2020: Cohen, Hazan and Koren, and Lykouris, Tardos and Wali, give elimination-type algorithms for stochastic bandits with graph feedback.
• 2019: Balseiro et al. introduce cross learning and obtain $\tilde O(\sqrt{KT})$ regret.
• 2020–2024: Han, Zhou and Weissman obtain $\tilde O(\sqrt{\min\{\alpha M, K\}T})$ for both structures together (this mission) and use it for first-price auctions.

Setting

A stochastic contextual bandit with graph feedback and cross learning (Definition 2) has a horizon $T$, contexts $\mathcal C = [M]$, actions $\mathcal A = [K]$, a joint reward law $P$ supported on $[0,1]^{M\times K}$ with mean rewards $R_{c,a}$, and a directed graph $G = (\mathcal A, E)$ without self-loops. In round $t$ a context $c_t$ is revealed, the learner picks $a_t$, nature draws $r_t = (r_{t,c,a})_{c,a}$ iid from $P$, and the learner observes $r_{t,c,a}$ for every $c \in \mathcal C$ and every $a \in I_t = \{a_t\}\cup\{a : (a_t,a)\in E\}$. The regret (5) is

$$R_T(\pi) = \sum_{t=1}^T\Big(\max_{a\in\mathcal A}R_{c_t,a} - R_{c_t,a_t}\Big).$$

Definition 1 is the case $M = 1$, with regret (4). The independence number $\alpha$ of $G$ is the largest size of a set of actions with no edge between any two of them.

Algorithm 2 keeps for each context $c$ an active set $\mathcal A_{\mathrm{act},c}$ and a minimum count $N_c$, and for each action $a$ a count $n_a$ shared by all contexts. In each round it plays an action of $\mathcal A_{0,c_t} = \{a\in\mathcal A_{\mathrm{act},c_t} : n_a = N_{c_t}\}$, either of largest out-degree in the graph restricted to $\mathcal A_{0,c_t}$ (Option I) or of in-degree zero there (Option II, for DAGs). When every active action of context $c$ has been observed more than $N_c$ times, the active set drops the actions whose empirical reward falls below the best by more than $6\sqrt{\log(2T)\log(MKT/\delta)/N_c}$. Algorithm 1 is the case $M = 1$.

Formalization targets

Goal: Theorem 4

With probability at least $1-\delta$, writing $L = \log(2T)\log(MKT/\delta)$,

$$R_T(\pi)\le T\wedge\big(K+24\sqrt{KTL}\big)\wedge\begin{cases}50\alpha M(\log K)^2+24\log K\sqrt{50\alpha MTL} & \text{Option I},\\ \alpha M+24\sqrt{\alpha MTL} & \text{Option II, }G\text{ a DAG,}\end{cases}$$

for every context sequence and every tie-breaking rule.

Milestones

• Lemma 1 (p. 13): with probability $1-\delta$, $|\bar r^t_a - R_a|\le 3\sqrt{\log(2T)\log(KT/\delta)/n^t_a}$ for all rounds and all observed actions of Algorithm 1.
• Lemma 10 (p. 35): a directed graph on $n\ge2$ vertices with independence number $\alpha$ has a weakly dominating set of size at most $50\alpha\log n$.
• Theorem 3 (p. 13): the one-context bound $T\wedge(50\alpha(\log K)^2+24\log K\sqrt{50\alpha T\log(2T)\log(KT/\delta)})$ (Option I), resp. $T\wedge(\alpha+24\sqrt{\alpha T\log(2T)\log(KT/\delta)})$ (Option II).
• Lemma 1, contextual form (p. 16): the same concentration for Algorithm 2, uniformly over contexts, with $\log(MKT/\delta)$.

Significance

Theorem 4 shows that one algorithm attains, up to logarithmic factors, the better of two regret rates: $\sqrt{KT}$, available from cross learning alone, and $\sqrt{\alpha MT}$, available from graph feedback alone. The paper then shows (Theorem 6) that with adversarial contexts nothing better than $\min\{\sqrt{\alpha MT},\sqrt{KT},T^{2/3}\}$ is possible, while with stochastic contexts and a partial order a variant reaches $\tilde O(\sqrt T)$ for first-price auctions. Algorithm 2 is the building block of that variant.

The results are proved in the paper; none is formalized. A formal development produces machine-checked versions of a concentration inequality with a random number of observations, of a domination bound for directed graphs, and of an elimination analysis with shared counts across contexts. Four printed statements need correction, and the formal statements record the corrected forms: the constant $3$ in Theorem 4's second bound (the printed proof gives $24$); Lemma 10, which is false for $n = 1$ and for edgeless graphs as worded; Lemma 1, which fails for $K = T = 1$ and $\delta$ close to $1$ (excluded by $KT \ge 2$); and the pseudocode of Algorithms 1–2, whose update $N_c \leftarrow N_c + 1$ can leave $\mathcal A_{0,c}$ empty after an elimination (the formalization keeps the text's invariant $N_c = \min_{a \in \mathcal A_{\mathrm{act},c}} n_a$, and coincides with the printed algorithm wherever the latter is defined).

Difficulty

The observations of an action are not a fixed sample: how often and when action $a$ is revealed depends on earlier rewards through the algorithm's choices. A union bound with Hoeffding's inequality at a fixed sample size does not apply directly, and Lemma 1 needs a self-normalized martingale inequality.

For Option I, the obvious bound on how long it takes to observe every least-pulled action once more is $|\mathcal A_0|$ rounds, which gives only $\sqrt{KT}$. Getting $\alpha$ instead of $K$ requires that a vertex of largest out-degree covers a $1/(50\alpha\log K)$ fraction of the remaining vertices; this is the content of Lemma 10, a probabilistic-method bound that is not in Mathlib. For contexts, the per-context analyses must be combined while counts are shared, and the bound in $K$ needs a per-action rather than a per-context accounting.

Formalization scope

• Actions Fin K, contexts Fin M, rounds Fin T; paper round $t$ is Lean index $t-1$. The feedback graph is a relation E with no self-loops; "independence number $\alpha$" is the hypothesis that every independent set has at most $\alpha$ elements (all bounds increase in $\alpha$).
• The reward law is a probability measure on Fin M → Fin K → ℝ carried by $[0,1]^{M\times K}$; rewards are iid across rounds (Measure.pi). The regret is the pseudo-regret with means $R_{c,a}=\int r_{c,a}\,dP$.
• "With probability at least $1-\delta$" is: the outer measure of the bad event under $P^{\otimes T}$ is at most $\delta$. The context sequence is fixed in advance (oblivious adversary); stochastic contexts independent of the rewards follow by conditioning.
• "Break ties arbitrarily" is a tie-breaking rule that sees the round, the algorithm's state (including the learner's whole observation history) and the context; the theorems hold for every rule that picks a member of every nonempty set.
• The minimum count $N_c$ follows the text's definition $N_c = \min_{a\in\mathcal A_{\mathrm{act},c}}n_a$. The printed update $N_c\leftarrow N_c+1$ can leave $\mathcal A_{0,c}$ empty after an elimination (for example with edges $a\to b$ and $c\to b$, when $a$ and $c$ are eliminated), where the printed algorithm is undefined. The formal algorithm agrees with the printed one wherever the latter is defined.
• Lemma 1 quantifies over $n^t_a\ge1$ and excludes $K = T = 1$, where it is false for $\delta$ close to $1$.
• Ruled out: replacing the three-way minimum by a single bound, restricting to a fixed tie-breaking rule, or to stochastic contexts.

Welcome contributions: the self-normalized inequality of de la Peña, Klass and Lai (Lemma 11), Lemma 10, invariants of Algorithm 2 (the active sets stay nonempty and contain an optimal action on the good event), and the deterministic regret accounting given the concentration event.

Selected references

• Y. Han, Z. Zhou, T. Weissman, Optimal No-regret Learning in Repeated First-price Auctions, arXiv:2003.09795v7, 2024; Operations Research, 2025. https://arxiv.org/abs/2003.09795
• N. Alon, N. Cesa-Bianchi, O. Dekel, T. Koren, Online Learning with Feedback Graphs: Beyond Bandits, COLT 2015. https://arxiv.org/abs/1502.07617
• S. Mannor, O. Shamir, From Bandits to Experts: On the Value of Side-Observations, NeurIPS 2011. https://arxiv.org/abs/1106.2436
• S. Balseiro, N. Golrezaei, M. Mahdian, V. Mirrokni, J. Schneider, Contextual Bandits with Cross-Learning, NeurIPS 2019. https://arxiv.org/abs/1809.09582
• V. H. de la Peña, M. J. Klass, T. L. Lai, Self-normalized processes: exponential inequalities, moment bounds and iterated logarithm laws, Annals of Probability 32(3A), 2004. https://doi.org/10.1214/009117904000000397

Motivation

Structural estimation of Markov decision processes recovers the parameters of an agent's reward from observed behavior, under the hypothesis that the agent acts optimally in a known dynamic environment. In econometrics this is the dynamic discrete choice model of Rust (Rust 1987); in artificial intelligence it is maximum-likelihood inverse reinforcement learning (ML-IRL). With Gumbel-distributed choice shocks the two coincide: the agent behaves like the optimal policy of an entropy-regularized MDP, and the reward parameter is estimated by maximizing the likelihood of the observed trajectories.

The classical estimators are nested: every evaluation of the likelihood solves the inner dynamic program to optimality (Rust's nested fixed-point algorithm), which is expensive when the state space is large. Zeng, Hong and Garcia (arXiv:2210.01282, Operations Research 2025) replace the nested loop by a single loop that alternates one approximate soft policy-iteration step with one stochastic gradient step on the reward parameter, and prove a finite-time guarantee for it. That guarantee, Theorem 1 of the paper, is the subject of this mission.

Setting

Let $\mathcal S$ and $\mathcal A$ be finite nonempty sets of states and actions, $P(s'\mid s,a)$ a transition kernel, $\rho$ an initial distribution on $\mathcal S$ and $\gamma\in[0,1)$ a discount factor. The reward $r(s,a;\theta)$ depends on a parameter $\theta\in\mathbb R^p$. A policy $\pi(a\mid s)$ is a distribution over actions at each state, with entropy $\mathcal H(\pi(\cdot\mid s))=-\sum_a\pi(a\mid s)\log\pi(a\mid s)$.

The soft Q-function of a pair $(\theta,\pi)$ is $Q(s,a)=r(s,a;\theta)+\gamma\,\mathbb E_{s'\sim P(\cdot\mid s,a)}[V(s')]$, where $V(s)$ is the expected discounted sum of $r(s_t,a_t;\theta)+\mathcal H(\pi(\cdot\mid s_t))$ along the trajectory of $\pi$ from $s$. The soft-optimal Q-function $Q_\theta$ is the fixed point of the soft-Bellman operator $\Lambda_\theta Q(s,a)=r(s,a;\theta)+\gamma\sum_{s'}P(s'\mid s,a)\log\sum_b e^{Q(s',b)}$; the soft-optimal policy is $\pi_\theta(a\mid s)\propto e^{Q_\theta(s,a)}$ and $V_\theta(s)=\log\sum_a e^{Q_\theta(s,a)}$.

Given a finite dataset $\mathcal D$ of expert trajectories, the surrogate likelihood is

$$\widehat L(\theta;\mathcal D)=\mathbb E_{\tau\sim\mathcal D}\Big[\sum_{t\ge0}\gamma^tr(s_t,a_t;\theta)\Big]-\mathbb E_{s_0\sim\rho}[V_\theta(s_0)].$$

Algorithm 1 (ML-IRL). Starting from $(\theta_0,\pi_0)$ and for $k=0,\dots,K-1$: estimate the soft Q-function $Q_k$ of $(\theta_k,\pi_k)$ by $\widehat Q_k$ with $\|\widehat Q_k-Q_k\|_\infty\le\varepsilon$; set $\pi_{k+1}(a\mid s)\propto e^{\widehat Q_k(s,a)}$; sample an expert trajectory $\tau^E_k$ from $\mathcal D$ and an agent trajectory $\tau^A_k$ from $\pi_{k+1}$; set $\theta_{k+1}=\theta_k+\alpha\big(h(\theta_k;\tau^E_k)-h(\theta_k;\tau^A_k)\big)$ with $h(\theta;\tau)=\sum_t\gamma^t\nabla_\theta r(s_t,a_t;\theta)$.

The assumptions are: (1) $0\le r\le C_r$; (2) under every policy the state chain mixes geometrically in total variation; (3) $\|\nabla_\theta r\|\le L_r$ and $\nabla_\theta r$ is $L_g$-Lipschitz in $\theta$.

Formalization targets

Goal: Theorem 1, explicit form

Write $L_q=L_r/(1-\gamma)$, $L_c=2L_qL_rC_d\sqrt{|\mathcal S||\mathcal A|}/(1-\gamma)+2L_g/(1-\gamma)$, $C_1=4C_dL_q^2\sqrt{|\mathcal S||\mathcal A|}$, $C_0=\|Q_0-Q_{\theta_0}\|_\infty$ and

$$B=\frac{C_0}{K(1-\gamma)}+\frac{2\gamma\varepsilon}{(1-\gamma)^2}+\frac{4L_q^2}{1-\gamma}\alpha .$$

There is $C_d>0$ depending only on $(P,\rho,\gamma)$ such that every run with $K\ge1$ and $\alpha=\alpha_0/K^\sigma$, $\alpha_0>0$, $\sigma\in(0,1)$, satisfies, for every realization,

$$\frac1K\sum_{k=0}^{K-1}\|\log\pi_{k+1}-\log\pi_{\theta_k}\|_\infty\le2\varepsilon+2B,$$

and in expectation

$$\frac1K\sum_{k=0}^{K-1}\mathbb E\|\nabla_\theta\widehat L(\theta_k;\mathcal D)\|^2\le2L_cL_q^2\alpha+C_1(B+\varepsilon)+\frac{\mathbb E[\widehat L(\theta_K;\mathcal D)-\widehat L(\theta_0;\mathcal D)]}{K\alpha}.$$

The printed Theorem 1 states only the rates $O(K^{-1})+O(K^{-\sigma})+O(\varepsilon)$ and $O(K^{-\sigma})+O(K^{-1+\sigma})+O(K^{-1})+O(\varepsilon)$; the goal is the explicit pair of inequalities its proof derives, from which those rates follow because $\widehat L$ is bounded.

Milestones

Lemma 2 (the gradient of $\widehat L$), Lemma 5 (Lipschitz visitation measures), Lemma 3 (Lipschitz $Q_\theta$ and smooth $\widehat L$), Lemma 6 and Lemma 7 (approximate soft policy iteration), and the proof's displays (35), (40), (41), the averaged tracking bound after (44) and the averaged gradient bound on p. 24. The bias bound (48) is a further item of the mission without being a milestone.

Significance

The result. Theorem 1 is a finite-time guarantee for a single-loop structural estimator: with $\sigma=1/2$ both the policy-tracking error and the squared gradient of the surrogate likelihood decay as $O(K^{-1/2})+O(\varepsilon)$. It shows that the inner dynamic program need not be solved to optimality at each likelihood evaluation, and it quantifies the price of approximate policy evaluation through $\varepsilon$. The paper reports it as the first finite-time result for an algorithm for either the dynamic discrete choice problem or ML-IRL.

Formalizing it. The result is proved on paper; no part of it is machine-checked. A complete development would put on the platform an entropy-regularized MDP layer (soft values, the soft-Bellman fixed point, the soft-optimal policy), its Lipschitz dependence on a reward parameter, the gradient of a soft-optimal value through its fixed point, and a two-timescale analysis with a biased stochastic gradient. Each of these is reusable by later soft-RL, IRL and structural-estimation formalizations.

Difficulty

Neither iterate converges on its own. The policy $\pi_{k+1}$ chases a target $\pi_{\theta_k}$ that moves whenever $\theta$ moves, so the standard linear convergence of soft policy iteration for a fixed reward does not apply directly. The stochastic gradient $g_k$ samples from $\pi_{k+1}$ rather than from $\pi_{\theta_k}$, so it is biased, and the standard analysis of unbiased stochastic gradient ascent does not apply either. The analysis must show that the tracking error contracts faster than the reward drifts, and bound the bias by the tracking error through the dependence of the state-action visitation measure on the policy. The gradient formula itself requires differentiating a soft-optimal value through a fixed point.

Formalization scope

The Lean development works with finite $\mathcal S$ and $\mathcal A$ (both nonempty), policies as functions $\mathcal S\to\mathcal A\to\mathbb R$, $\theta\in$ EuclideanSpace ℝ (Fin p), and discounted expectations as tsums over the occupation distribution of the published FoundationsML.ReinforcementLearning layer. $\|\cdot\|_\infty$ is the maximum over $(s,a)$; Lemma 5's $\|w-w'\|$ is the Frobenius norm; total variation is half the $\ell_1$ distance. $Q_\theta$ is chosen by Classical.epsilon among fixed points of $\Lambda_\theta$, which exist and are unique because $\Lambda_\theta$ is a $\gamma$-contraction.

Disclosed deviations from the page: Assumption 3 is a hypothesis of the goal (Theorem 1 prints "Assumptions 1 - 2" but its proof uses Assumption 3); $\mathcal S$ is finite, as the proof's $\sqrt{|\mathcal S||\mathcal A|}$ requires, although the title speaks of high-dimensional state spaces; Assumption 3 includes differentiability of $r$, which the page uses implicitly; $\varepsilon\ge0$ (the page writes $\epsilon_{\rm app}>0$); Assumption 2 is stated as the mixing bound the paper derives from irreducibility and aperiodicity; and Algorithm 1's sampling is represented by the conditional means of the sampled gradients given the past, measurable with respect to a filtration, which is the only way the proof uses it.

The statement admits no trivializing reading: the run structure is inhabited (a sorry-free check exhibits a run), $C_d$ is fixed before the reward, the data and the run, every expectation is of a bounded measurable function, the gradient is that of a differentiable function (Lemma 2), and the Frobenius norm is used where the page uses it rather than Lean's sup norm on function types.

Welcome contributions: the existence and uniqueness of the soft-Bellman fixed point, the performance-difference and Gibbs-variational facts behind Lemma 7, the visitation-measure Lipschitz bound of Lemma 5, and the fixed-point differentiation behind Lemma 2.

Selected references

• S. Zeng, M. Hong, A. Garcia, Structural Estimation of Markov Decision Processes in High-Dimensional State Space with Finite-Time Guarantees, Operations Research, 2025; arXiv:2210.01282v3, 2024. https://arxiv.org/abs/2210.01282
• J. Rust, Optimal Replacement of GMC Bus Engines: An Empirical Model of Harold Zurcher, Econometrica 55(5), 1987. https://doi.org/10.2307/1911259
• B. D. Ziebart, A. Maas, J. A. Bagnell, A. K. Dey, Maximum Entropy Inverse Reinforcement Learning, AAAI 2008. https://cdn.aaai.org/AAAI/2008/AAAI08-227.pdf
• T. Haarnoja, H. Tang, P. Abbeel, S. Levine, Reinforcement Learning with Deep Energy-Based Policies, ICML 2017. https://arxiv.org/abs/1702.08165