Probability

Motivation

Many problems in statistical learning, signal processing and distributed optimization minimize a sum of a large number $m$ of convex components over a convex set: a data-fit term per sample plus a regularizer or constraint per sample. When $m$ is large, a method that processes one component per iteration is often far cheaper per step than one that evaluates the whole sum. Incremental methods do exactly this. The incremental subgradient method of Nedić and Bertsekas (SIAM J. Optim., 2001) takes a subgradient step on one component at a time; the incremental proximal method replaces some of these steps by proximal steps, which are more stable and are cheap when a component has a closed-form proximal map (an $\ell_1$ term, an indicator of a simple set).

Bertsekas, Incremental Proximal Methods for Large Scale Convex Optimization (Report LIDS-P-2847, MIT, 2010, revised 2011; Math. Program. 129 (2011), doi:10.1007/s10107-011-0472-0), combines the two: each component is split as $F_i=f_i+h_i$, with a proximal step on $f_i$ and a subgradient step on $h_i$, followed by a projection. The paper analyzes two ways of choosing the component at each iteration, a fixed cyclic order and a randomized order. This mission covers the randomized order (§4 of the paper); its companion mission covers the cyclic order.

Setting

Let $X\subseteq\mathbb R^n$ be a nonempty closed convex set and let $f_i,h_i:\mathbb R^n\to\mathbb R$, $i=1,\dots,m$, be convex. The problem is

$$\text{minimize } F(x)=\sum_{i=1}^m\bigl(f_i(x)+h_i(x)\bigr)\quad\text{subject to } x\in X,$$

with optimal value $F^*=\inf_{x\in X}F(x)$, possibly $-\infty$, and optimal set $X^*=\{x^*\in X\mid F(x^*)=F^*\}$, possibly empty. $P_X$ is the Euclidean projection on $X$ and $\tilde\nabla f(x)$ a subgradient of $f$ at $x$.

At iteration $k$ a component index $\omega_k\in\{1,\dots,m\}$ is drawn and, with stepsize $\alpha_k>0$, one of three updates is applied:

$$z_k=P_X\bigl(x_k-\alpha_k\tilde\nabla f_{\omega_k}(z_k)\bigr),\qquad x_{k+1}=P_X\bigl(z_k-\alpha_k\tilde\nabla h_{\omega_k}(z_k)\bigr),\qquad(42)$$ $$z_k=x_k-\alpha_k\tilde\nabla f_{\omega_k}(z_k),\qquad x_{k+1}=P_X\bigl(z_k-\alpha_k\tilde\nabla h_{\omega_k}(z_k)\bigr),\qquad(43)$$ $$z_k=x_k-\alpha_k\tilde\nabla h_{\omega_k}(x_k),\qquad x_{k+1}=P_X\bigl(z_k-\alpha_k\tilde\nabla f_{\omega_k}(x_{k+1})\bigr).\qquad(44)$$

The implicit equations are proximal steps: in (42), $z_k$ minimizes $f_{\omega_k}(x)+\frac1{2\alpha_k}\|x-x_k\|^2$ over $X$. The randomized order means that $\omega_k$ is uniformly distributed over $\{1,\dots,m\}$ and independent of the past history $\mathcal F_k=\{x_k,z_{k-1},x_{k-1},\dots,z_0,x_0\}$ (Assumptions 3(a), 4(a)). The growth conditions (Assumptions 3(b), 4(b)) ask for a constant $c$ bounding, with probability 1 and for every component $i$, the norms of the subgradients used by the step that would be taken if $\omega_k$ were $i$, and the decrease of $f_i$, $h_i$ along that step by $c$ times its length.

Formalization targets

Goal: Proposition 9

If $\alpha_k\to0$ and $\sum_k\alpha_k=\infty$, then

$$\liminf_{k\to\infty}F(x_k)=F^*\quad\text{with probability 1},$$

and if in addition $X^*\neq\emptyset$ and $\sum_k\alpha_k^2<\infty$, then with probability 1 the iterates $x_k$ converge to some $x^*\in X^*$ (which may depend on the sample path).

Milestones

1. Eq. (58). For every $x^*\in X^*$ and every $k\ge0$,

$$E\{\|x_{k+1}-x^*\|^2\mid\mathcal F_k\}\le\|x_k-x^*\|^2-\frac{2\alpha_k}{m}\bigl(F(x_k)-F^*\bigr)+5\alpha_k^2c^2.$$

2. Proposition 2, the supermartingale convergence theorem: if $E\{Y_{k+1}\mid\mathcal F_k\}\le Y_k-Z_k+W_k$ for nonnegative adapted $Y_k,Z_k,W_k$ and $\sum_kW_k<\infty$ almost surely, then almost surely $\sum_kZ_k<\infty$ and $Y_k$ converges.
3. Eq. (59). If $\sum_k\alpha_k^2<\infty$, then for each $x^*\in X^*$, almost surely, $\sum_k\frac{2\alpha_k}{m}(F(x_k)-F^*)<\infty$ and $\|x_k-x^*\|$ converges.
4. Proposition 7 (constant stepsize $\alpha$): almost surely $\inf_{k\ge0}F(x_k)=F^*$ if $F^*=-\infty$, and $\inf_{k\ge0}F(x_k)\le F^*+\frac{5\alpha mc^2}{2}$ otherwise.
5. Proposition 8 (constant stepsize, $X^*\neq\emptyset$, $\epsilon>0$): the first index $N$ with $F(x_N)<F^*+\frac{5\alpha mc^2+\epsilon}{2}$ is almost surely finite and $E\{N\}\le m\,\mathrm{dist}(x_0;X^*)^2/(\alpha\epsilon)$.

Significance

Proposition 9 says that a randomized incremental method with a diminishing stepsize solves the problem exactly, almost surely, under conditions that do not require differentiability, bounded level sets, or strong convexity. Propositions 7 and 8 quantify the constant-stepsize regime: the error bound is $O(\alpha mc^2)$, smaller by a factor of $m$ than the worst case of the cyclic order (Proposition 4 of the paper). This is the paper's argument for randomization, and the same comparison recurs in the later literature on stochastic and incremental methods.

The results are proved in the paper. As far as known, none of them is machine-checked: Mathlib has conditional expectation, filtrations and Doob's martingale convergence theorem, but not the Robbins–Siegmund almost-supermartingale theorem in the form used here, and no incremental or stochastic proximal method has a formal convergence proof on the platform. The mission produces a formal model of a randomized algorithm with implicit (proximal) steps, a formal Robbins–Siegmund special case, and a complete a.s. convergence proof that other stochastic-approximation formalizations can reuse.

Difficulty

The deterministic estimate behind (58) is the one of the cyclic analysis with the sampled component in place of the cyclic one. The new difficulty is the conditioning step: $E\{F_{\omega_k}(z_k)\mid\mathcal F_k\}=\frac1m\sum_iF_i(z_k^i)$ needs the step that would be taken for each component $i$ to be a function of the past, and $\omega_k$ to be independent of it, and both must be stated so that the conditional expectation is that of an integrable function. The obvious route from (59) to part 2 of the goal fails: (59) gives, for each $x^*$, an event of probability 1, and $X^*$ is in general uncountable, so the events cannot be intersected directly. Part 1 must also handle $F^*=-\infty$, where no point of $X^*$ is available.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n); components are indexed by Fin m ($0,\dots,m-1$), with $m\ge1$.
• $X$ is nonempty, closed and convex and $f_i,h_i$ are real-valued convex (the paper's standing assumptions of p. 4), stated as explicit hypotheses; stepsizes are positive.
• $P_X$ is a predicate (nearest point of $X$); subgradients are given by the subgradient inequality. The iterations (42)–(44) are their subgradient forms, with the subgradient of $f_i$ the one that makes the implicit equation hold, which is the paper's proximal step.
• $F^*$ is an infimum in EReal, so $F^*=-\infty$ is represented and the $\liminf$ and $\inf$ statements are in EReal.
• The run carries, for each $k$ and each component $i$, the would-be step from $x_k$; the realized step is the one for $i=\omega_k$. The bounds (45)–(48) are required for all $i$, as in the paper.
• "Independent of the past history" is formalized as independence of $\sigma(\omega_k)$ from $\mathcal F_k=\sigma(x_0,\dots,x_k,z_0,\dots,z_{k-1})$. Added hypotheses that make it meaningful: the iterates are measurable, the would-be step at $k$ is $\mathcal F_k$-measurable, and $x_0$ is a fixed vector.
• Proposition 2 adds integrability of $Y_k$ (Lean's conditional expectation of a non-integrable function is $0$).
• Proposition 8 uses the paper's own $N$ (the first entry time into the level set of its proof), not an arbitrary random variable, and adds the hypothesis $x_0\in X$, which its proof uses.

A formalization in which the would-be steps may depend on $\omega_k$, or in which $\omega_k$ is only assumed uniform, would let a step pick its component adversarially; the measurability and independence hypotheses rule this out, and none of the hypotheses is unsatisfiable (a sorry-free instance with $m=2$ is checked locally).

Needed infrastructure: the Robbins–Siegmund special case (Proposition 2), conditional expectation of a function of an independent uniform index and a past-measurable quantity, and existence of a countable dense subset of a closed set in $\mathbb R^n$. The supermartingale theorem and the conditioning lemma are reusable beyond this mission. Proofs of the milestones, of the goal, and of reusable lemmas about projections and proximal steps are welcome.

Selected references

• D. P. Bertsekas, Incremental Proximal Methods for Large Scale Convex Optimization, Report LIDS-P-2847, MIT, 2010 (revised March 2011); Mathematical Programming 129 (2011) 163–195. https://doi.org/10.1007/s10107-011-0472-0
• A. Nedić and D. P. Bertsekas, Incremental Subgradient Methods for Nondifferentiable Optimization, SIAM Journal on Optimization 12 (2001) 109–138. https://doi.org/10.1137/S1052623499362111
• H. Robbins and D. Siegmund, A Convergence Theorem for Non Negative Almost Supermartingales and Some Applications, in Optimizing Methods in Statistics, Academic Press, 1971, 233–257. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• J. Neveu, Discrete Parameter Martingales, North-Holland, 1975 (the paper's reference [43] for Proposition 2).
• D. P. Bertsekas and J. N. Tsitsiklis, Neuro-Dynamic Programming, Athena Scientific, 1996 (the paper's reference [7] for Proposition 2).

Motivation

Reflected backward stochastic differential equations describe processes that must remain above a prescribed obstacle. El Karoui, Kapoudjian, Pardoux, Peng and Quenez connect that probabilistic construction to a parabolic partial differential equation with an obstacle in their 1997 paper. A representation by a stochastic process is useful only if the associated differential equation identifies a definite function. The comparison result in Theorem 8.6 supplies that identification: within a specified growth class, two viscosity solutions cannot disagree. This mission isolates that deterministic uniqueness statement. The companion existence and stochastic representation result is Theorem 8.5 of the same paper.

Setting

Fix a terminal time $T>0$ and a spatial dimension $d\ge1$. At time $t\in[0,T]$ and point $x\in\mathbb R^d$, the drift $b(t,x)$ is a vector and the diffusion coefficient $\sigma(t,x)$ is a $d\times d$ matrix. Both are continuous and Lipschitz in $x$ uniformly over $t$. A continuous terminal payoff $g(x)$ has at most polynomial growth. The continuous generator $f(t,x,r,z)$ depends on a scalar value $r$ and a vector $z$; it has polynomial growth at $(r,z)=(0,0)$ and is Lipschitz in $(r,z)$. The continuous obstacle $h(t,x)$ has a polynomial upper bound and satisfies $h(T,x)\le g(x)$.

Write $a(t,x)=\sigma(t,x)\sigma(t,x)^\top$. The associated second order spatial operator is $L_t\phi=\tfrac12\operatorname{Tr}(aD^2\phi)+b\cdot D\phi$. The obstacle problem asks for a function whose terminal value is $g$ and whose interior value obeys

$$\min\{u-h,\,-\partial_tu-L_tu-f(t,x,u,Du\,\sigma)\}=0.$$

A parabolic superjet or subjet at an interior point is a triple $(p,q,X)$ of a time slope, spatial slope and symmetric second order matrix that bounds the function locally above or below by the associated quadratic expansion, up to $o(|s-t|+|y-x|^2)$. These jets let a continuous function satisfy the differential inequality without having ordinary derivatives. A viscosity subsolution uses superjets and a terminal upper bound; a viscosity supersolution uses subjets and a terminal lower bound. A viscosity solution satisfies both definitions.

Formalization targets

Uniqueness in the polynomial growth class

The goal is the paper's Theorem 8.6. Under the coefficient assumptions above and condition (27), every pair of continuous viscosity solutions with polynomial growth agrees on the entire closed time strip:

$$\bigl(u,v\text{ solve (24) and have polynomial growth}\bigr) \Longrightarrow u(t,x)=v(t,x)\quad\text{for every }(t,x)\in[0,T]\times\mathbb R^d.$$

Condition (27) gives a continuous modulus $m_R$ for the change in $f$ between bounded spatial points, with argument $|x-y|(1+|z|)$ and $m_R(0)=0$. The quantifiers include every radius $R>0$, every bounded scalar argument, and every gradient vector $z$. The milestone is Lemma 8.7, which controls the location and separation of the maximizers of the paper's doubled-variable function $\Phi_\alpha(t,x,y)=u(t,x)-v(t,y)-\alpha|x-y|^2/2$.

Significance

The theorem shows that the obstacle PDE has at most one solution in the natural class allowed by polynomially growing coefficients and payoffs. Together with Theorem 8.5, which identifies the reflected backward SDE value as a viscosity solution, and the growth estimate at the end of Section 8, it yields the paper's probabilistic representation of the unique solution. Theorem 8.6 alone asserts uniqueness, so it makes no existence claim.

The formal development provides reusable interfaces for parabolic jets, viscosity inequalities, the obstacle operator and uniform polynomial growth on a finite time strip. Those interfaces can serve other comparison theorems and other parabolic obstacle problems. The mathematical result is proved in the 1997 article; this mission asks for a Lean proof of its deterministic uniqueness statement. The proposal declares the theorem with a proof placeholder and includes the comparison lemma as an intermediate target.

Difficulty

The first obstruction is that the candidate solutions need only be continuous. Subtracting their PDE expressions directly would assume derivatives they may not possess. The paper instead uses viscosity jets, and its comparison argument invokes the theorem of sums from Crandall, Ishii and Lions' viscosity-solutions guide. The generator's spatial modulus must control a gradient argument that grows as the two spatial points approach each other. Lemma 8.7 provides the necessary separation limit for the maximizers. The argument also treats a polynomial growth class on all of $\mathbb R^d$, so a comparison confined to one fixed bounded ball would not establish the stated result.

Formalization scope

Lean uses nonnegative real time and functions on $\mathbb R^d$ represented by Fin d → ℝ. The terminal time and dimension are positive. Bounds with existential constants use the finite-dimensional sup norm, which is equivalent to the Euclidean norm in the paper. The displayed quadratic form, $\operatorname{Tr}(aX)$ and $q\sigma$ are written by coordinate sums, so their signs, factor $\tfrac12$, and matrix order are exact. The obstacle is bounded only above in the data assumptions, exactly as condition (22) states. Condition (27) is imposed only on uniqueness, not folded into the definition of viscosity solution.

Jets are taken at $0<t<T$ through a one-sided little-$o$ bound in the relative neighborhood of the interior strip. The terminal equality comes from the two terminal inequalities; the viscosity tests impose no separate condition at $t=0$. The printed text calls $S(d)$ “symmetric nonnegative matrices,” but the proof of Theorem 8.6 uses arbitrary symmetric matrices produced by the theorem of sums. The formal definition therefore uses all symmetric matrices and records this correction for review.

The mission permits every continuous solution of polynomial growth. It does not restrict candidates to smooth, bounded or stochastic-representation functions. The companion reflected SDE construction, penalization limit and existence theorem are outside this mission's goal; the general stochastic interface Peng1990.SMP.Stochastic is listed as series context but is not imported by the deterministic statements. Useful contributions include the comparison proof, the lemma on doubled-variable maximizers, and reusable lemmas about jet transformations and the matrix trace inequality.

Selected references

• N. El Karoui, C. Kapoudjian, É. Pardoux, S. Peng and M.-C. Quenez, Reflected solutions of backward SDE's, and related obstacle problems for PDE's, The Annals of Probability 25(2), 1997, pp. 702–737. DOI.
• M. G. Crandall, H. Ishii and P.-L. Lions, User's guide to viscosity solutions of second order partial differential equations, Bulletin of the American Mathematical Society 27(1), 1992, pp. 1–67. DOI.

Motivation

A retailer choosing which variants of a product to stock (colours, sizes, models) faces a trade-off that operations management has studied since van Ryzin and Mahajan (1999): a deeper assortment attracts more purchases, but each added variant takes demand away from the variants already on the shelf. This loss is called cannibalization. In the standard model of consumer choice, the multinomial logit (MNL), cannibalization holds exactly: every variant's purchase probability falls when a variant is added.

The MNL assumes that a consumer who walks into a store buys either from that store or nothing. Real consumers can also leave to search elsewhere, and a deeper assortment makes them less likely to leave. Cachon, Terwiesch and Xu (working paper, 2002; published in Manufacturing & Service Operations Management, 2005, doi:10.1287/msom.1050.0088) add search to the MNL and ask whether cannibalization survives. Two forces now act on a variant's demand when the assortment expands: the share of buyers who choose it falls, and the share of consumers who stay in the store rises. This mission formalizes their answer for the first of their two search models, the independent assortment model, in which the outside option does not depend on what the retailer stocks.

Setting

There are $n$ possible variants $N=\{1,\dots,n\}$; the retailer stocks an assortment $S\subseteq N$. A faux variant $0$ represents not buying.

Gumbel shocks. Fix a scale $\mu>0$ and let $\gamma$ be Euler's constant. The zero-mean Gumbel law with scale $\mu$ has distribution function and density

$$F(x)=\exp\Big[-\exp\Big(-\Big(\frac{x}{\mu}+\gamma\Big)\Big)\Big],\qquad f(x)=F'(x).$$

Utilities. Variant $j$ has expected net utility $u_j-p_j$ (utility minus price), and the no-purchase option has $u_0$ (its price is $p_0=0$). A consumer's realised utilities are $U_j=(u_j-p_j)+\zeta_j$ and $U_0=u_0+\zeta_0$, with $\zeta_0,\zeta_1,\dots,\zeta_n$ independent and Gumbel. The preference of variant $j$ is $v_j=\exp((u_j-p_j)/\mu)$, and $v_0=\exp(u_0/\mu)$.

No search. The consumer buys the variant of $S$ with the highest utility, or nothing if $U_0$ is higher. The probability that she buys $i\in S$ is $q_i^m(S)$.

Search. A consumer may instead search at a cost $b$ and receive $U_r=u_r+\zeta_r$, where $\zeta_r$ is another independent Gumbel shock that she has not yet observed. Having seen $y=U_{\max}$, the best utility in the store, she searches when the expected gain minus the expected loss is at least $b$:

$$\int_{y-u_r}^{\infty}(u_r+x-y)f(x)\,dx-\int_{-\infty}^{y-u_r}(y-u_r-x)f(x)\,dx\ \ge\ b .$$

The independent-assortment demand $q_i^{si}(S)$ is the probability that variant $i$ has the highest utility in $S$, beats the no-purchase option, and the consumer does not search. Write $\bar U=u_r-b$ (the search threshold), $\lambda=\exp[-(\bar U/\mu+\gamma)]$ and $H(\bar U,S)=\exp\big(-\lambda(v_0+\sum_{j\in S}v_j)\big)$.

Formalization targets

Goal: Theorem 2 (p. 9)

For all $S$ and $S^+$ with $i\in S\subsetneq S^+$,

$$q_i^{si}(S)\ >\ q_i^{si}(S^+).$$

The goal leaves the utilities $u_j-p_j$, $u_0$, $u_r$, the search cost $b$, the scale $\mu$ and the number of variants $n$ arbitrary.

Milestones

1. The MNL formula (2): $q_i^m(S)=v_i/(\sum_{j\in S}v_j+v_0)$ for $i=0$ and $i\in S$.
2. The Gumbel law with the constant $\gamma$ has mean zero, $E[\zeta_r]=0$.
3. The search rule: search is worthwhile at $y$ if and only if $u_r-b\ge y$.
4. The integral representation of $q_i^{si}(S)$ over the realisation $\phi$ of $\zeta_i$.
5. The change of variables $\delta=\exp[-(\phi/\mu+\gamma)]$ that turns it into $\int_0^\alpha\exp[-\delta(v_0+\sum_{j\in S}v_j)/v_i]\,d\delta$.
6. Theorem 1 (p. 8): $q_i^{si}(S)=q_i^m(S)\,\big(1-H(\bar U,S)\big)$ for $i\in S$.
7. $T(\omega)=\omega(1-e^{-\lambda/\omega})$ is strictly increasing on $(0,\infty)$, with the derivative the paper displays.
8. $q_i^{si}(S)=v_i\,T\big((\sum_{k\in S}v_k+v_0)^{-1}\big)$.

Significance

Theorem 1 says that under independent-assortment search the demand for every stocked variant is its MNL demand scaled by one common factor, the probability $1-H(\bar U,S)$ that the best option in the store clears the threshold $\bar U$. The threshold itself does not depend on the assortment. Theorem 2 then shows that the MNL's cannibalization effect dominates the retention effect of a deeper assortment, so each variant's demand still falls strictly when variants are added. The paper's later results on the shape of the profit function and on the structure of optimal assortments under search build on this closed form.

The paper's proofs are short but rely on steps it states without proof: the MNL formula is cited from Anderson, de Palma and Thisse (1992), the search rule is obtained "after rearranging terms", and the closed form follows from a change of variables. No machine-checked version of these steps is known. The mission produces a checked derivation of a logit-type closed form from an explicit random-utility model with an outside option and an endogenous stopping decision, at the paper's scale $\mu$ and with its centring constant $\gamma$.

Difficulty

Theorem 2 is not monotonicity of a single fraction. Adding a variant enlarges the denominator of $q_i^m(S)$ and simultaneously raises the factor $1-H(\bar U,S)$, so the sign of the change is a competition between the two, and a bound on either factor alone does not settle it. The comparison becomes one-dimensional only after Theorem 1 is available, and Theorem 1 itself requires computing a probability of an event defined by finitely many strict inequalities among independent Gumbel variables together with the consumer's search decision. That calculation is an iterated integral over the product law, with the decision rule, the mean of the Gumbel law and the change of variables each needing their own justification.

Formalization scope

• Indices. Variants are Fin n, 0-based (the paper's variant $i$ is index $i-1$). The no-purchase option is the extra index none of Option (Fin n). Assortments are Finset (Fin n), and $S\subsetneq S^+$ is S ⊂ Splus.
• The law. IsZeroMeanGumbel μ G says the probability measure G on ℝ has distribution function $F$ above; $\mu>0$ and $\gamma$ is Real.eulerMascheroniConstant. Such a law exists for every $\mu>0$ (checked sorry-free locally).
• The sample space is Option (Fin n) → ℝ with the product measure Measure.pi (fun _ => G). The search shock does not appear in it: the consumer decides before observing $\zeta_r$, so only its law enters, as integration against G in the search rule.
• Demand. $q_i^m(S)$ (noSearchProb) and $q_i^{si}(S)$ (searchProb) are the real values of the probabilities of the choice events, with strict inequalities. The search event uses the paper's decision rule (the displayed integral), not the threshold $\bar U$; the equivalence is a milestone. The closed form $v_i/(\sum_{j\in S}v_j+v_0)$ is the published RetailVariety.Structure.share.
• Corrected typo. The paper prints $\alpha=\exp[-((\bar U-u_i)/\mu+\gamma)]$; the change of variables gives $u_i-p_i$ in place of $u_i$, and the milestone states the corrected value.
• $T$ is used on $(0,\infty)$; the paper's interval $[0,\infty)$ includes a point where $T$ is undefined.

Ruled out. Demand defined by the closed form (3), which would make Theorem 1 true by definition and Theorem 2 a calculus fact; Theorem 2 with $\subseteq$ and $\ge$; a standard Gumbel law (scale $1$, mean $\gamma$) in place of the paper's zero-mean scale-$\mu$ law; and a model without the no-purchase option.

Infrastructure. A complete development needs the distribution theory of the Gumbel law (density, mean), choice probabilities of products of i.i.d. continuous variables as iterated integrals, and calculus for $T$. The Gumbel and MNL lemmas are reusable for any logit-based choice model, including the other missions of this series. Contributions of proofs of any milestone, or of general MNL infrastructure that the milestones can import, are welcome.

Selected references

• G. P. Cachon, C. Terwiesch, Y. Xu, Retail Assortment Planning in the Presence of Consumer Search, working paper, The Wharton School, Dec. 20, 2002; published in Manufacturing & Service Operations Management 7(4), 330–346, 2005. https://doi.org/10.1287/msom.1050.0088
• S. P. Anderson, A. de Palma, J.-F. Thisse, Discrete Choice Theory of Product Differentiation, MIT Press, 1992.
• G. van Ryzin, S. Mahajan, On the Relationship Between Inventory Costs and Variety Benefits in Retail Assortments, Management Science 45(11), 1496–1509, 1999. https://doi.org/10.1287/mnsc.45.11.1496
• D. McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, 1974, 105–142.

Interacting diffusions on large weighted graphs

Classical mean field theory describes $n$ exchangeable diffusions, each interacting with the empirical average of all the others. As $n\to\infty$ the particles become independent copies of a McKean–Vlasov process (propagation of chaos). Many systems of interest are not exchangeable. Particles sit at the vertices of a network and interact only with their neighbours, as in models of opinion dynamics, epidemics on contact networks, synchronisation of oscillators and systemic risk in financial networks. When the network is dense and its adjacency structure converges, the natural limit object is a graphon, a symmetric measurable function $G:[0,1]^2\to[0,1]$ that encodes the limiting edge density between "positions" $u,v\in[0,1]$ (Lovász, Large Networks and Graph Limits, 2012).

Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) develop a law of large numbers for such systems. This mission formalizes their second main result, Theorem 3.1. Under cut-metric convergence of the interaction kernels, the empirical measure of the $n$-particle system converges in probability to the averaged law of a continuum graphon particle system. Related work includes Bhamidi, Budhiraja and Wu (Stochastic Process. Appl., 2019) on weakly interacting particles on inhomogeneous random graphs, Coppini, Dietert and Giacomin (Stoch. Dyn., 2020) on Erdős–Rényi graphs, and Bet, Coppini and Nardi (arXiv:2006.07670) on oscillators on dense random graphs.

Setting

Write $I=[0,1]$ with Lebesgue measure and fix a horizon $T>0$. Let $\mathcal C_d=C([0,T]:\mathbb R^d)$ with the uniform norm $\|x\|_{*,T}=\sup_{s\le T}|x_s|$. On one probability space take independent initial states $X_u(0)$ with laws $\mu_u(0)$ and independent $d$-dimensional Brownian motions $B_u$, for all $u\in I$. The graphon particle system (2.1) for a graphon $G$ and Lipschitz coefficients $b,\sigma$ is the continuum of nonlinear diffusions

$$X_u(t)=X_u(0)+\int_0^t\!\!\int_I\!\int_{\mathbb R^d}b(X_u(s),x)G(u,v)\,\mu_{v,s}(dx)\,dv\,ds+\int_0^t\!\!\int_I\!\int_{\mathbb R^d}\sigma(X_u(s),x)G(u,v)\,\mu_{v,s}(dx)\,dv\,dB_u(s),$$

where $\mu_{v,s}$ is the law of $X_v(s)$. Write $\mu_u\in\mathcal P(\mathcal C_d)$ for the path law of $X_u$ and $\bar\mu=\int_I\mu_u\,du$ for the averaged law.

The $n$-particle system (3.1) places particle $i$ at label $i/n$, starts it at $X_{i/n}(0)$, drives it by $B_{i/n}$, and weights its interaction with particle $j$ by $\xi^n_{ij}$:

$$X^n_i(t)=X_{i/n}(0)+\int_0^t\frac1n\sum_{j=1}^n\xi^n_{ij}\,b(X^n_i(s),X^n_j(s))\,ds+\int_0^t\frac1n\sum_{j=1}^n\xi^n_{ij}\,\sigma(X^n_i(s),X^n_j(s))\,dB_{i/n}(s).$$

The weights come from a step graphon $G_n$, constant on the squares of the $n$-grid. Either $\xi^n_{ij}=G_n(i/n,j/n)$, or $\xi^n_{ij}=\xi^n_{ji}$ are independent Bernoulli$(G_n(i/n,j/n))$ variables for $i\le j$, independent of the noise (Condition 3.1). The kernels converge in the cut norm $\|W\|_\square=\sup_{S,T}\big|\int_{S\times T}W\big|$. Two further norms appear: the operator norm $\|W\|=\sup_{\|g\|_\infty\le1}\int_I|\int_I W(u,v)g(v)\,dv|\,du$, and the Wasserstein-2 distance $W_{2,T}$ on $\mathcal P(\mathcal C_d)$.

Formalization targets

Goal: Theorem 3.1

Assume the initial laws are measurable in $u$ with a uniform $(2+\varepsilon)$-moment and $b,\sigma$ are Lipschitz (Condition 2.1). Assume $u\mapsto\mu_u(0)$ is $W_2$-continuous on each interval of a finite cover of $I$ (Condition 2.2(a)), and that Condition 3.1 holds with $G_n\to G$ in the cut metric. Then

$$\mu^n:=\frac1n\sum_{i=1}^n\delta_{X^n_i}\longrightarrow\bar\mu\quad\text{in }\mathcal P(\mathcal C_d)\text{ in probability}.$$

If, in addition, $G$ is continuous at $(u,v)$ for a.e. $v$ at each interior point $u$ of the cover (Condition 2.2(b)), then

$$\frac1n\sum_{i=1}^n\mathbb E\|X^n_i-X_{i/n}\|^2_{*,T}\longrightarrow0 .$$

Milestones

In order: Remark 2.1, where cut-norm convergence implies operator-norm convergence; Theorem 2.1(a), continuity of $u\mapsto\mu_u$ in $W_{2,T}$; the weak-LLN bound (6.4); the discretization bound (6.11); Lemma 6.1,

$$\limsup_{n}\frac1n\sum_i\mathbb E\|X^n_i-X_{i/n}\|^2_{*,T}\le\kappa(M)\limsup_n\|G_n-G\|+\kappa M^{-\varepsilon};$$

Lemma 6.2, a law of large numbers for the continuum particles $X_{1/n},\dots,X_{n/n}$; the approximation of $G$ by continuous graphons; the continuity (6.12) of $\bar\mu$ in the graphon, in a corrected qualitative form; the empirical coupling bound for $W_{2,T}$; and (6.14).

Significance

Theorem 3.1 shows that the averaged graphon law $\bar\mu$ is the correct macroscopic description of a dense heterogeneous particle system. This holds for deterministic weights and for Erdős–Rényi-type random weights, and the graphon may be discontinuous. It is the foundation for graphon mean field games and for control of large networked systems, where $\bar\mu$ replaces the intractable $n$-particle law. Under the regularity Condition 2.2(b) the convergence holds in $L^2$, particle by particle, along the natural coupling.

The result is proved in the paper (§6.1–§6.2). Nothing in it is formalized. A formal proof would produce reusable infrastructure: graphons, the cut and operator norms, Lusin approximation of graphons, Wasserstein distances between empirical measures, and laws of large numbers for random probability measures on path space. It also needs pathwise stability estimates for SDE systems built on Itô integrals, which goes well beyond what Mathlib has today.

Difficulty

The particles are neither exchangeable nor identically distributed. The classical propagation-of-chaos argument compares each particle with an i.i.d. copy of one McKean–Vlasov process, and it does not apply here. Each $X^n_i$ must be compared with its own limit $X_{i/n}$, and the error has two sources: the random or discretized weights $\xi^n_{ij}$, and the replacement of $G$ by $G_n$. Cut-metric convergence controls $G_n-G$ only through integrals against bounded test functions. The interaction term, however, integrates the unbounded function $b(X_{i/n}(s),\cdot)$ against varying laws $\mu_{j/n,s}$. When $G$ is merely measurable, the map $u\mapsto\mu_u$ need not be continuous, and the error of replacing $\int_I\cdot\,dv$ by the average over the labels $j/n$ need not vanish. The direct estimate therefore fails for (3.3) without Condition 2.2(b), and this is the case the goal must cover.

Formalization scope

The setting file GraphonMF.DenseLLN.Setting fixes these conventions:

• $\mathbb R^d$ is Fin d → ℝ with the sup norm. All statements are invariant under this choice: constants are existential and the other conclusions are limits.
• Processes are path-valued maps $\Omega\to\mathcal C_d$, and $\mathcal C_d$ carries its Borel σ-algebra.
• Each SDE is encoded through the published Itô-process predicate Peng1990.SMP.IsItoProcess. The filtrations are the uncompleted natural filtrations $\sigma(X_u(0),B_u(r):r\le t)$ and $\sigma(\xi^n,X_{j/n}(0),B_{j/n}(r):j\le n,r\le t)$.
• A solution of (2.1) carries the membership of its law family in the class $\mathcal M$ (measurable in $u$, uniformly bounded second moments), which makes every Bochner integral of the drift meaningful.
• $W_2$ and $W_{2,T}$ are the published WassersteinDRO.Duality.wassersteinDistance with values in $[0,\infty]$.
• Expectations of nonnegative quantities are lower Lebesgue integrals.
• Convergence in probability is topological: $\mathbb P(\mu^n\notin U)\to0$ for every weak-topology neighbourhood $U$ of $\bar\mu$.
• The $n$-particle system shares the noise of the graphon system: particle $i$ (Lean index $i$, label $(i+1)/n$) uses $X_{(i+1)/n}(0)$ and $B_{(i+1)/n}$.
• Each $\xi^n$ is assumed measurable.

Two encodings would trivialize the targets, and both are ruled out. A pointwise or almost-sure reading of (3.3), or convergence of $\int f\,d\mu^n$ for a single test function, is not the claim. Choosing the constants of Lemma 6.1 and (6.11) after the sequence $(G_n)$ would make them nearly empty, so they are chosen before it. A sorry-free check confirms that the solution predicates are satisfiable: with $b=\sigma=0$ the constant paths solve both systems.

Solvers will need several pieces of library work: the inequality $\|W\|_{\infty\to1}\le4\|W\|_\square$, BDG-type moment bounds for the Itô integrals of Peng's library, Gronwall estimates, Lusin's theorem on $[0,1]^2$, and the metrization of weak convergence on $\mathcal P(\mathcal C_d)$ (Lévy–Prokhorov). Contributions to any of these are welcome independently of the goal. The paper's proofs are in its §5 (Theorem 2.1) and §6.1–§6.2 (Lemmas 6.1, 6.2 and Theorem 3.1).

Selected references

• E. Bayraktar, S. Chakraborty, R. Wu, Graphon mean field systems, Ann. Appl. Probab. 33(5):3587–3619, 2023. https://doi.org/10.1214/22-AAP1901
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60, 2012. https://doi.org/10.1090/coll/060
• S. Bhamidi, A. Budhiraja, R. Wu, Weakly interacting particle systems on inhomogeneous random graphs, Stochastic Process. Appl. 129:2174–2206, 2019. https://doi.org/10.1016/j.spa.2018.06.014
• F. Coppini, H. Dietert, G. Giacomin, A law of large numbers and large deviations for interacting diffusions on Erdős–Rényi graphs, Stoch. Dyn. 20:2050010, 2020. https://doi.org/10.1142/S0219493720500100
• G. Bet, F. Coppini, F. R. Nardi, Weakly interacting oscillators on dense random graphs, arXiv preprint, 2020. https://arxiv.org/abs/2006.07670
• A.-S. Sznitman, Topics in propagation of chaos, École d'Été de Probabilités de Saint-Flour XIX, LNM 1464, 1991. https://doi.org/10.1007/BFb0085169

Interacting diffusions on large heterogeneous networks

Classical mean-field theory describes $n$ diffusions that interact symmetrically, each feeling the empirical average of all the others, and shows that as $n\to\infty$ every particle behaves like an independent copy of a single McKean–Vlasov process. Many systems of interest are not symmetric: neurons, agents in a financial network, or oscillators interact through a graph, and particles in different parts of the graph feel different neighbourhoods. A graphon $G:[0,1]^2\to[0,1]$ is the limit object of dense graph sequences (Lovász, Large Networks and Graph Limits, AMS 2012), and it is the natural way to describe the interaction structure of such systems in the limit.

Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) study a continuum of diffusions indexed by labels $u\in[0,1]$ whose interaction is weighted by a graphon, and prove laws of large numbers and rates of convergence for $n$-particle systems on graphs sampled from the graphon. This mission targets their uniform rate of convergence for weights sampled from a Lipschitz graphon (Theorem 3.2).

Setting

Write $I=[0,1]$ with Lebesgue measure. Fix a horizon $T\in(0,\infty)$ and let $\mathcal C_d=C([0,T]:\mathbb R^d)$ with $\|x\|_{*,t}=\sup_{0\le s\le t}|x_s|$.

On one probability space, $\{B_u:u\in I\}$ are i.i.d. $d$-dimensional Brownian motions and $\{X_u(0):u\in I\}$ are independent initial states with laws $\mu_u(0)$, independent of the Brownian motions. Given a graphon $G$ and coefficients $b,\sigma$, the graphon particle system (2.1) is

$$X_u(t)=X_u(0)+\int_0^t\!\!\int_I\!\int_{\mathbb R^d}b(X_u(s),x)G(u,v)\,\mu_{v,s}(dx)\,dv\,ds+\int_0^t\!\!\int_I\!\int_{\mathbb R^d}\sigma(X_u(s),x)G(u,v)\,\mu_{v,s}(dx)\,dv\,dB_u(s),$$

with $\mu_{u,t}=\mathcal L(X_u(t))$. The particles are independent but not identically distributed, and their laws are coupled through the $dv$-integral.

The $n$-particle system (3.1) uses the same randomness at the labels $i/n$:

$$X^n_i(t)=X_{i/n}(0)+\int_0^t\frac1n\sum_{j=1}^n\xi^n_{ij}\,b(X^n_i(s),X^n_j(s))\,ds+\int_0^t\frac1n\sum_{j=1}^n\xi^n_{ij}\,\sigma(X^n_i(s),X^n_j(s))\,dB_{i/n}(s),$$

so particle $i$ and the continuum particle at $u=i/n$ share their initial state and Brownian motion.

The hypotheses are:

• Condition 2.1: $u\mapsto\mu_u(0)$ is measurable, $\sup_u\mathbb E|X_u(0)|^{2+\varepsilon}<\infty$ for some $\varepsilon>0$, and $b$, $\sigma$ are Lipschitz in both arguments.
• Condition 2.3: there are finitely many intervals $I_1,\dots,I_N$ covering $I$ and a $\kappa>0$ with $W_2(\mu_{u_1}(0),\mu_{u_2}(0))\le\kappa|u_1-u_2|$ on each $I_i$ and $|G(u_1,v_1)-G(u_2,v_2)|\le\kappa(|u_1-u_2|+|v_1-v_2|)$ on each block $I_i\times I_j$. The graphon may jump across block boundaries.
• Condition 3.2: the weights are sampled from $G$ itself, either deterministically, $\xi^n_{ij}=G(i/n,j/n)$, or as a random graph, $\xi^n_{ij}=\xi^n_{ji}\sim\mathrm{Bernoulli}(G(i/n,j/n))$ independently for $i\le j$ and independently of the noise.

Formalization targets

Goal: Theorem 3.2 (p. 3596)

Under Conditions 2.1, 2.3 and 3.2 there is $\kappa\in(0,\infty)$ such that

$$\max_{i=1,\dots,n}\mathbb E\|X^n_i-X_{i/n}\|^2_{*,T}\le\frac{\kappa}{n}\qquad\forall n\in\mathbb N.$$

Milestones (§6.3, in attack order)

• (6.15): $\mathbb E\|X^n_i-X_{i/n}\|^2_{*,t}$ is bounded by $\kappa$ times the time-integrated mean-square mismatch between the finite-$n$ drift and diffusion and their graphon counterparts.
• The drift mismatch is split by (6.16) into three terms $\tilde T^{n,1}_s,\tilde T^{n,2}_s,\tilde T^{n,3}_s$, bounded by

$$\tilde T^{n,1}_s\le2\kappa\max_i\mathbb E|X^n_i(s)-X_{i/n}(s)|^2\ \ (6.17),\qquad\tilde T^{n,2}_s\le\frac{\kappa}{n}\ \ (6.18),\qquad\tilde T^{n,3}_s\le\frac{\kappa}{n^2}\ \ (6.19).$$

• Theorem 2.1(b) (p. 3593): under Condition 2.3, $W_{2,T}(\mu_u,\mu_v)\le\kappa|u-v|$ whenever $u,v$ lie in the same interval $I_i$. It is used in (6.19).

Significance

The result. Theorem 3.2 gives a quantitative propagation of chaos for heterogeneous interactions: with weights sampled from a blockwise Lipschitz graphon, every particle of the finite system, not just an average particle, is within $O(n^{-1/2})$ in root-mean-square path distance of the continuum particle with the same label. The rate matches the classical mean-field rate (e.g. Sznitman 1991), so heterogeneity of the interaction costs nothing in the exponent. The same estimate covers the deterministic weighted graph and the random graph sampled from $G$ (in the annealed sense), and it is the dense counterpart of Theorem 4.2 for percolated graphs.

Formalizing it. The result is proved in the paper (§6.3); it has no machine-checked proof. A formal development would produce a reusable account of graphon particle systems and their finite-$n$ approximations: graphon-weighted McKean–Vlasov drifts, couplings through shared noise, and the decomposition of the interaction error into a Lipschitz feedback term, a law-of-large-numbers term and a Riemann-sum discretization term.

Difficulty

The obvious approach is to compare $X^n_i$ with $X_{i/n}$ directly and close a Gronwall inequality. The difficulty is that the comparison involves the empirical, graph-weighted average of the other particles, which is neither the graphon average nor an average of independent terms. Three different errors must be controlled simultaneously and uniformly in $i$: the feedback of all particles' errors into particle $i$, the fluctuation of a sum of independent but non-identically distributed terms whose weights may themselves be random, and the error of replacing an integral over labels by a sum over the grid $\{j/n\}$. The last needs regularity of the law $\mu_u$ in the label $u$, which is itself a theorem about the graphon system (Theorem 2.1(b)) and fails at block boundaries of $G$, where only the small number of boundary cells saves the $1/n^2$ rate. Averaging over $i$, as in the law of large numbers of Theorem 3.1, is not enough: the goal bounds the maximum.

Formalization scope

• $\mathbb R^d$ is Fin d → ℝ with the sup norm; matrices are measured entrywise. All statements are norm-invariant because every constant is existential. Particle $i\in\{1,\dots,n\}$ is Lean's i : Fin n with label $(i+1)/n$; time is ℝ≥0; $I$ is Mathlib's unitInterval.
• Brownian motions, Itô integrals and Itô processes are the published Peng1990.SMP.Stochastic definitions; an SDE with random initial value $X(0)$ is stated as an Itô process for $X-X(0)$. Each continuum particle uses the natural filtration of $(X_u(0),B_u)$; the $n$-particle system uses the natural filtration of the weights, initial states and Brownian motions at the labels.
• $W_2$ and $W_{2,T}$ are the published WassersteinDRO.Duality.wassersteinDistance 2, valued in $[0,\infty]$; expectations of nonnegative quantities are lower Lebesgue integrals.
• A solution of (2.1) is required to have continuous paths, measurable path maps, and a law family in the class $\mathcal M$ (measurable in $u$, uniformly bounded second moments), as Proposition 2.1 asserts; this makes every inner integral meaningful.
• The constant $\kappa$ is chosen after the data and before $n$ and $i$. A $\kappa$ chosen after $n$, a bound on the average over $i$, or a solution predicate that no process satisfies would trivialize the goal; the first two are excluded by the statement, and a sanity check exhibits the zero-coefficient system as a solution of both systems.
• Condition 2.2 is not assumed, and the weights come from $G$, not from a step graphon $G_n$; no cut-metric hypothesis appears.
• Needed infrastructure: Doob/Burkholder–Davis–Gundy for Itô integrals, Gronwall's inequality in integrated form, moment bounds for the graphon system, Kantorovich–Rubinstein-type duality for Lipschitz test functions, and independence of functionals of independent noises. Proofs of the milestones, of Theorem 2.1(b), and of the goal are all welcome; the paper's proofs are in its §5–§6.

Selected references

• E. Bayraktar, S. Chakraborty, R. Wu, Graphon mean field systems, Ann. Appl. Probab. 33(5):3587–3619, 2023. https://doi.org/10.1214/22-AAP1901
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60, 2012. https://doi.org/10.1090/coll/060
• A.-S. Sznitman, Topics in propagation of chaos, École d'Été de Probabilités de Saint-Flour XIX, LNM 1464, Springer, 1991. https://doi.org/10.1007/BFb0085169
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4):966–979, 1990. https://doi.org/10.1137/0328054

Motivation

Policy gradient methods optimize a parameterized policy for a Markov decision process by local search on its expected cost. The objective is nonconvex, so local search can in principle stall at a poor stationary point. Bhandari and Russo, Global Optimality Guarantees for Policy Gradient Methods show that for a broad family of control problems this does not happen, and, in quantitative form, that the objective is gradient dominated: its suboptimality is bounded by a multiple of the size of its gradient. The multiple involves a single problem-dependent quantity, the effective concentrability coefficient $\kappa_\rho$, which measures how well the initial state distribution $\rho$ covers the states that matter for optimal behaviour. Theorem 2 and the convergence rates of Theorem 5 of the paper are only informative when $\kappa_\rho$ is finite, so sufficient conditions for a finite $\kappa_\rho$ are what make those results usable. This mission formalizes the paper's three such conditions (Theorem 4).

Distribution-mismatch coefficients of this kind go back to Kakade and Langford (2002), and appear in the analyses of approximate dynamic programming by Scherrer and Geist (2014) and of policy gradient methods in finite MDPs by Agarwal et al. (2021).

Setting

A discounted Markov decision process consists of a measurable state space $\mathcal S$, nonempty feasible action sets $\mathcal A_s$, a bounded measurable per-period cost $g(s,a)$, a transition kernel $P(\cdot\mid s,a)$, a discount factor $\gamma\in(0,1)$ and an initial probability distribution $\rho$ on $\mathcal S$. A feasible measurable stationary policy $\pi$ ($\pi\in\Pi$) picks an action $\pi(s)\in\mathcal A_s$ in every state. Its cost-to-go $J_\pi(s)$ is the expected discounted cost from $s$, its discounted state-occupancy measure is

$$\eta_\pi(\cdot)=(1-\gamma)\sum_{t\ge0}\gamma^t\,\Pr{}^\pi_\rho(s_t\in\cdot),$$

and its average cost is $\ell(\pi)=(1-\gamma)\int J_\pi\,d\rho$. The Bellman operator acts on bounded measurable functions by

$$(TJ)(s)=\min_{a\in\mathcal A_s}\Big[g(s,a)+\gamma\int J(s')\,P(ds'\mid s,a)\Big].$$

An optimal policy $\pi^*$ minimizes $J_\pi$ at every state; $J^*=J_{\pi^*}$. A policy class $\Pi_\Theta=\{\pi_\theta:\theta\in\Theta\}$ is indexed by a convex set $\Theta\subseteq\mathbb R^d$, and $\mathcal J_\Theta=\{J_{\pi_\theta}:\theta\in\Theta\}$.

The effective concentrability coefficient $\kappa_\rho$ (Definition 3) is the smallest scalar $\kappa$ such that

$$\|J-J^*\|_{1,\rho}\le\frac{\kappa}{1-\gamma}\,\|J-TJ\|_{1,\rho}\qquad\forall J\in\mathcal J_\Theta,\tag{13}$$

with $\|J\|_{1,\rho}=\int|J|\,d\rho$, and $\kappa_\rho=\infty$ if no scalar works. It converts a $\rho$-weighted Bellman error into a $\rho$-weighted optimality gap.

Formalization targets

Goal: Theorem 4(b)

If $\eta_{\pi^*}(B)\le C\rho(B)$ for every measurable set $B$, then $C$ satisfies (13); equivalently

$$\kappa_\rho\le\Big\|\frac{d\eta_{\pi^*}}{d\rho}\Big\|_\infty .$$

Companions: Theorem 4(a) and 4(c)

(a) If $\mathcal S$ is finite and $\rho(s)>0$ for all $s$, then $\kappa_\rho\le 1/\min_{s}\rho(s)$. (c) If $T$ is a contraction with modulus $\gamma$ in a norm $\|\cdot\|$ with $c\|J\|\le\|J\|_{1,\rho}\le C\|J\|$, then $\kappa_\rho\le C/c$.

Milestones

The element-wise inequalities $TJ\preceq T_\pi J$, $TJ_\pi\preceq J_\pi$ (5); the performance difference identity $\ell(\pi)-\ell(\bar\pi)=\int[T_\pi J_{\bar\pi}-J_{\bar\pi}]\,d\eta_\pi$ (29); the sup-norm bound $\|J_\pi-J^*\|_\infty\le(1-\gamma)^{-1}\|J_\pi-TJ_\pi\|_\infty$ (26); the occupancy-weighted inequality $(1-\gamma)\int(J_\pi-J^*)\,d\rho\le\int(J_\pi-TJ_\pi)\,d\eta_{\pi^*}$ from the proof of part (b); and the contraction step $\|J-J^*\|\le(1-\gamma)^{-1}\|J-TJ\|$ from the proof of part (c).

Significance

Theorem 4 is what turns the paper's gradient-dominance theorem into a usable statement: with part (b), the constant in Theorem 2 is bounded by the worst-case likelihood ratio between the optimal policy's state distribution and the initial distribution, a quantity that can be checked without knowing the policy class. Part (a) shows that in finite problems any fully supported initial distribution suffices, and part (c) gives a route through weighted norms, used in the paper for optimal stopping (Lemma 13).

The results are proved in the paper. None of them is machine-checked. The mission produces a general-state-space formalization of the discounted cost MDP (kernels, occupancy measures, Bellman operators, measurable selection) together with the performance difference identity on measurable state spaces; existing formal developments of policy gradient theory on the platform are for finite MDPs only. The occupancy-measure and Bellman-operator layer is shared with the other missions of this series.

Difficulty

The argument for part (b) is short on paper, but each step is a measure-theoretic statement about infinite-horizon objects. The performance difference identity (29) exchanges an infinite discounted sum with integration against the chain's laws and needs the occupancy measure to be built from the $t$-step kernels of the controlled chain. The change of measure from $\eta_{\pi^*}$ to $\rho$ needs the Bellman error $J_\pi-TJ_\pi$ to be nonnegative and integrable; its measurability is not automatic, because $TJ$ is a pointwise minimum over uncountably many actions, and is supplied by the measurable selection assumption. Part (c) needs the fixed-point property $TJ^*=J^*$ of the optimal cost-to-go, which again rests on measurable selection.

Formalization scope

All statements use one Lean layer: MDP S A with measurable spaces S, A (a generalization of the paper's Borel subsets of Euclidean spaces), the cost and kernel given on all of $\mathcal S\times\mathcal A$, measurable stationary policies MPolicy S A, and costToGo, occupancy, loss, bellmanPi, bellmanOpt. The paper prints the Bellman operators (3)–(4) without the discount factor; every later use includes it, and so does the formalization. The optimal policy is a binder πstar with IsOptimal M πstar. Assumptions 1 and 2 of the paper are standing hypotheses of every main statement.

The coefficient $\kappa_\rho$ is never formed as a number: "$\kappa_\rho\le X$" is the predicate IsConcBound M Θ πθ πstar X, which says that $X$ satisfies (13); because the right-hand side of (13) is nondecreasing in the scalar, the two are equivalent. Part (b) quantifies over every $C$ with $\eta_{\pi^*}\le C\rho$ setwise, which is equivalent to $\|d\eta_{\pi^*}/d\rho\|_\infty\le C$; a real-valued essential supremum is avoided because it reads $0$ exactly when the paper's bound is infinite. Part (a) assumes $\rho(s)>0$ for every state, since otherwise $1/\min\rho$ is $+\infty$ on paper and $0$ in Lean. Part (c) requires the norm comparison (21) on all bounded measurable functions, as its proof uses it on $J-J^*$ and $J-TJ$, and encodes "a norm" by subadditivity, the one property used.

A formalization in which (13) or the occupancy-weighted inequality is assumed, or in which $\kappa_\rho$ is a junk value of an empty infimum, would make the goal trivial; neither is used.

Contributions are welcome on every milestone, in particular on the performance difference identity and the measurability of the cost-to-go and of $TJ$, which are reusable for any discounted MDP on a measurable state space.

Selected references

• J. Bhandari, D. Russo, Global Optimality Guarantees for Policy Gradient Methods, Operations Research, 2024; cited version arXiv:1906.01786v3, 2022. https://arxiv.org/abs/1906.01786v3 (DOI 10.1287/opre.2021.0014)
• S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• B. Scherrer, M. Geist, Local Policy Search in a Convex Space and Conservative Policy Iteration as Boosted Policy Search, ECML PKDD 2014. https://arxiv.org/abs/1306.1520
• A. Agarwal, S. Kakade, J. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, JMLR 22, 2021. https://arxiv.org/abs/1908.00261
• D. Bertsekas, Dynamic Programming and Optimal Control, Athena Scientific, 1995.