Probability

Motivation

A decision maker who must choose $x$ to minimize an expected cost $\mathbb E_F[c(x;\xi)]$ rarely knows the distribution $F$ of the uncertain parameter $\xi$; what is available is a sample $\xi^1,\dots,\xi^N$. Sample average approximation (SAA) replaces $F$ by the empirical distribution. Data-driven distributionally robust optimization (DRO) instead minimizes the worst case of the expected cost over a set $\mathcal F_N$ of distributions built from the data, which protects against the error of the empirical distribution at small $N$. Many such sets have been proposed: moment sets (Delage and Ye, 2010), $\phi$-divergence balls (Ben-Tal et al., 2013), Wasserstein balls (Mohajerin Esfahani and Kuhn, 2018).

Bertsimas, Gupta and Kallus (arXiv:1408.4445v3; Mathematical Programming, 2018, doi:10.1007/s10107-017-1174-z) observe that each such set can be read as the confidence region of a statistical goodness-of-fit (GoF) test, and call the resulting method Robust SAA. A basic question for any such method is whether, as $N\to\infty$, its objective, optimal value and optimal solutions converge to those of the full-information problem. The paper answers it for all data-driven DROs at once, with a single property of the test.

Setting

The support $\Xi\subseteq\mathbb R^d$ of $\xi$ is closed, and $\mathcal P(\Xi)$ is the set of Borel probability distributions on $\Xi$ with the topology of weak convergence. The data $\xi^1,\xi^2,\dots$ are i.i.d. from an unknown $F\in\mathcal P(\Xi)$. A data-driven uncertainty set (DUS) map assigns to each sample $(\xi^1,\dots,\xi^N)$ a set $\mathcal F_N\subseteq\mathcal P(\Xi)$; it is the confidence region of the test that rejects a hypothesis $F_0$ exactly when $F_0\notin\mathcal F_N$. Decisions lie in a closed set $X\subseteq\mathbb R^{d_x}$, the cost is $c(x;\xi)$, and the robust objective is the worst-case expectation

$$\mathcal C(x;\mathcal F_N)=\sup_{F_0\in\mathcal F_N}\mathbb E_{F_0}[c(x;\xi)] .$$

A test is uniformly consistent (Definition 3) if, for every data-generating $F$, almost surely every sequence $F_N$ that does not converge weakly to $F$ lies outside $\mathcal F_N$ for infinitely many $N$. The admissible instances are those satisfying three assumptions: (1) $c(\cdot;\xi)$ is equicontinuous in $x$ uniformly over $\xi$; (2) $X$ is bounded, or $c$ is coercive in $x$ uniformly over a set $D$ of positive $F$-probability and bounded below off $D$; (3) $\Xi$ is bounded, or there is a growth function $\phi\ge0$ with $c(x;\xi)=O(\phi(\xi))$ whose expectation the DUS tracks: $\sup_{F_0\in\mathcal F_N}|\mathbb E_{F_0}\phi-\frac1N\sum_i\phi(\xi^i)|\to0$ almost surely. The convergence conditions are (18) $\mathcal C(x;\mathcal F_N)\to\mathbb E_F[c(x;\xi)]$ uniformly on compact subsets of $X$; (19) convergence of optimal values; and (20) every sequence of robust minimizers has a limit point, and all its limit points are true minimizers.

Formalization targets

Goal: Theorem 2

For a DUS map with nonempty sets,

$$\mathcal F_N\ \text{is uniformly consistent}\iff\Big[\forall F,X,c\ \text{satisfying Assumptions 1–3}:\ (18),(19),(20)\ \text{hold a.s.}\Big].$$

The statement carries no rates and no constants; it is a characterization, so it does not depend on any particular test.

Milestones

1. Proposition 8: under uniform consistency and Assumptions 1 and 3, almost surely $\mathbb E_{F_N}[c(x;\xi)]\to\mathbb E_F[c(x;\xi)]$ for every $x\in X$ and every sequence $F_N\in\mathcal F_N$.
2. Proposition 9: deterministically, convergence of $\mathcal C(x_N;\mathcal F_N)$ along every convergent $x_N\to x$ implies (18).
3. Theorem 2, "only if" side: uniform consistency implies (18)–(20) a.s. for every admissible instance.
4. Theorem 2, "if" side: if the test is not uniformly consistent, some admissible instance fails (18)–(20) with positive probability.
5. Theorem 3: if $\mathcal F_N$ always contains the empirical distribution and the test is $c$-consistent (Definition 5, consistency with respect to the expected costs only), then (18)–(20) hold a.s.
6. Proposition 4 (first sentence): a uniformly consistent test is consistent in the classical sense, $\mathbb P(F_0\notin\mathcal F_N)\to1$ for each $F_0\neq F$.

Significance

The result. Theorem 2 reduces the asymptotic analysis of a data-driven DRO to a property of a statistical test, which can be checked once per test rather than once per optimization model. The paper uses it to classify DUSs: the $\chi^2$ and G-tests on a finite support and the Kolmogorov–Smirnov, Kuiper, Cramér–von Mises, Watson and Anderson–Darling tests on the line are uniformly consistent (Theorems 4–5, separate missions of this series), while the test of marginals is not even consistent and so cannot give convergence for every cost. The necessity direction makes the property sharp: a weaker test always admits a well-behaved cost on which the DRO fails to converge. Theorem 3 explains the remaining cases where a DRO converges for one given cost.

Formalizing it. The result is proved in the paper (§10.5), but its proof leans on several standard facts used without detail: the portmanteau theorem, uniform integrability arguments from Billingsley's Convergence of Probability Measures, the Lévy continuity theorem with the Cramér–Wold device, and coercivity arguments carried over from the paper's Theorem 1. A machine-checked version would fix exactly which regularity of the cost these steps need; three such conditions are stated explicitly here (see the scope section). No part of the result is formalized elsewhere to our knowledge; the platform has no notion of a data-driven uncertainty set or of uniform consistency.

Difficulty

Uniform consistency is a statement about weak convergence, while (18)–(20) are statements about expectations of an unbounded, $x$-dependent cost under the members of $\mathcal F_N$. Weak convergence controls expectations only of bounded continuous functions, so the "only if" side must recover convergence of $\mathbb E_{F_N}[c(x;\xi)]$ from Assumption 3, which requires uniform integrability, and then upgrade pointwise convergence to uniform convergence on compacts and to convergence of minimizers when $X$ is unbounded. The tempting route through a single limiting minimization problem fails: the sets $\mathcal F_N$ change with the sample, the worst case is a supremum over infinitely many distributions, and the minimizers of $\mathcal C(\cdot;\mathcal F_N)$ could escape to infinity unless coercivity on $D$ transfers to every member of $\mathcal F_N$. The "if" side needs, from the mere failure of uniform consistency, a single admissible cost whose worst-case objective detects every failure of weak convergence.

Formalization scope

Points are EuclideanSpace ℝ (Fin d), distributions are ProbabilityMeasure ↥Ξ (whose topology is weak convergence), and the data live on the canonical product space $\Xi^{\mathbb N}$ with the product law, 0-indexed. "Almost surely" is ∀ᵐ, and in Definition 3 one null set serves every sequence $F_N$. An expectation over a member of $\mathcal F_N$ is $+\infty$ when the integrand is not integrable, never Lean's default $0$. Minima in (19)–(20) are infima in the extended reals, so the empty and unattained cases need no special treatment; (20) applies to sequences that are minimizers for all large $N$.

Four hypotheses are added to the page, each used by the paper's own proof: every $\mathcal F_N$ is nonempty (otherwise the worst case is $-\infty$ and uniform consistency is vacuous); $c(x;\cdot)$ is continuous on $\Xi$; the set $D$ of Assumption 2b is open; the growth function $\phi$ of Assumption 3b is continuous, with $\mathbb E_F\phi<\infty$ as fixed on p. 10 of the paper. Theorem 3 additionally assumes Assumption 2, which its proof uses. Proposition 4 assumes the rejection events are measurable. A formalization in which the worst case uses the raw Bochner integral, the supremum ranges over a possibly empty set, or (20) requires minimizers at $N=0$ would make the statements false or vacuous, and is ruled out.

A full development needs weak convergence and the portmanteau theorem (in Mathlib), uniform integrability and its relation to convergence of means under weak convergence, the strong law of large numbers for the growth function and the empirical measure, the Lévy continuity theorem in several dimensions (in Mathlib, via characteristic functions), and a countable convergence-determining class of bounded continuous functions. The uniform-integrability step and the path characterization of local uniform convergence (Proposition 9) are reusable beyond this mission. Contributions to any milestone are welcome; Proposition 9 is self-contained and deterministic.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Robust Sample Average Approximation, arXiv:1408.4445v3, 2016; Mathematical Programming 171 (2018). https://arxiv.org/abs/1408.4445v3, https://doi.org/10.1007/s10107-017-1174-z
• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999. https://doi.org/10.1002/9780470316962
• E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3), 2010. https://doi.org/10.1287/opre.1090.0741
• A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg, G. Rennen, Robust Solutions of Optimization Problems Affected by Uncertain Probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641
• P. Mohajerin Esfahani, D. Kuhn, Data-Driven Distributionally Robust Optimization Using the Wasserstein Metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1

Why sampling from $e^{-U}$ needs non-asymptotic guarantees

Bayesian inference, statistical physics and machine learning all ask for samples from a probability distribution $\pi$ on $\mathbb R^d$ whose density is known only up to a constant, $\pi(dx)\propto e^{-U(x)}dx$. The unadjusted Langevin algorithm (ULA) is the Euler–Maruyama discretisation of the Langevin diffusion, whose invariant law is $\pi$. It needs only gradients of $U$, has no accept/reject step, and is therefore cheap in high dimension. Without the Metropolis correction, however, the chain does not leave $\pi$ invariant, so its usefulness rests on quantitative bounds: how far, in total variation, the law of the $p$-th iterate is from $\pi$, as an explicit function of the dimension $d$, the step sizes and the regularity of $U$.

Durmus and Moulines (arXiv:1507.05021, Ann. Appl. Probab. 27(3), 2017) gave such bounds for constant and decreasing step sizes. Earlier work of Dalalyan (arXiv:1412.7392, 2017) treated strongly log-concave targets with constant steps. Durmus and Moulines cover nonincreasing step sequences and, among other regimes, potentials that are only strongly convex outside a ball; this mission formalizes that case.

Setting

Write $\|\cdot\|$ and $\langle\cdot,\cdot\rangle$ for the Euclidean norm and inner product of $\mathbb R^d$. The total variation norm of a difference of probability measures is

$$\|\mu-\nu\|_{\mathrm{TV}}=\sup\Big\{\Big|\int f\,d\mu-\int f\,d\nu\Big|: f\text{ Borel},\ |f|\le1\Big\},$$

which ranges in $[0,2]$.

The potential $U:\mathbb R^d\to\mathbb R$ satisfies two assumptions:

• L1: $U$ is differentiable and $\nabla U$ is $L$-Lipschitz;
• H3($M_s$): $U$ is convex and $\langle\nabla U(x)-\nabla U(y),x-y\rangle\ge m\|x-y\|^2$ whenever $\|x-y\|\ge M_s$, for some $M_s\ge0$, $m>0$.

The point $x^\star$ is a minimiser of $U$, and $\pi(dx)=e^{-U(x)}dx/\int e^{-U}$.

The Langevin diffusion is $dY_t=-\nabla U(Y_t)dt+\sqrt2\,dB^d_t$, with $B^d$ a standard $d$-dimensional Brownian motion. Its transition semigroup is $P_t(x,A)=\mathbb P(Y_t(x)\in A)$.

ULA with step sizes $(\gamma_k)_{k\ge1}$ is the chain

$$X_{k+1}=X_k-\gamma_{k+1}\nabla U(X_k)+\sqrt{2\gamma_{k+1}}Z_{k+1},$$

with $(Z_k)$ i.i.d. standard Gaussian. Its one-step kernel is $R_\gamma(x,\cdot)=\mathcal N(x-\gamma\nabla U(x),2\gamma I_d)$, and $\delta_xQ^n_\gamma=\delta_xR_{\gamma_1}\cdots R_{\gamma_n}$ is the law of $X_n$ started at $x$. Write $\Gamma_{n,p}=\sum_{k=n}^p\gamma_k$, and let $A(\gamma,x)=\sup_{k\ge0}\int\|\nabla U\|^2\,d(\delta_xQ^k_\gamma)$.

The explicit constants use

• $F(\lambda,a,c,\gamma,w)=\lambda^aw+c(-\lambda^\gamma\log\lambda)^{-1}$ and $G(\lambda,c,\gamma,w)=w+c(-\lambda^\gamma\log\lambda)^{-1}$;
• $\omega(\varepsilon,R)=R^2/\{2\Phi^{-1}(1-\varepsilon/2)\}^2$, with $\Phi$ the standard Gaussian distribution function;
• $\lambda=e^{-2m+\bar\gamma L^2}$ and $c=2(d+mM_s^2)$.

Formalization targets

Goal: Theorem 21 (p. 16)

Let $d\ge1$, and let $(\gamma_k)$ be positive and nonincreasing with $\gamma_1\le\bar\gamma<2mL^{-2}$. Then for all $0\le n<p$ and $x$,

$$\|\delta_xQ^p_\gamma-\pi\|_{\mathrm{TV}}\le2^{-1/2}L\Big(\sum_{k=n}^{p-1}\Big\{\tfrac{\gamma^3_{k+1}}3A(\gamma,x)+d\gamma^2_{k+1}\Big\}\Big)^{1/2}+C(\delta_xQ^n_\gamma)\kappa^{\Gamma_{n+1,p}}.$$

The three constants are explicit:

• the rate, $\log\kappa=-\frac m2\log2\,[\log\{(1+e^{m\omega(1/2,\max(1,M_s))/4})(1+\max(1,M_s))\}+\log2]^{-1}$;
• the constant of the first term, $A(\gamma,x)\le L^2G(\lambda,c,\gamma_1,\|x-x^\star\|^2)$;
• the constant of the second term, $C(\delta_xQ^n_\gamma)\le6+2(d/m+M_s^2)^{1/2}+2F^{1/2}(\lambda,\Gamma_{1,n},c,\gamma_1,\|x-x^\star\|^2)$.

Milestones, in the order of the proof (§5.1, p. 34)

1. (56), p. 30: for $dX_t=b(X_t)dt+dB^d_t$ with $b$ Lipschitz and monotone (G1), $\sup_{\|x-y\|\le R}\|P_t(x,\cdot)-P_t(y,\cdot)\|_{\mathrm{TV}}\le2(1-\varepsilon)$ for $t\ge\omega(\varepsilon,R)$.
2. Theorem 36, p. 33: under G1 and the contraction G3, $\|P_t(x,\cdot)-P_t(y,\cdot)\|_{\mathrm{TV}}\le2\{(1-\varepsilon)^{-1}+1+\|x-y\|\}\kappa^t$ with an explicit $\kappa$.
3. §5.1, p. 34: $\|P_t(x,\cdot)-\pi\|_{\mathrm{TV}}\le2\{3+\|x-x^\star\|+\int\|y-x^\star\|d\pi(y)\}\kappa^t$ for the Langevin semigroup.
4. §5.1, p. 34: $\int\|y-x^\star\|^2d\pi(y)\le d/m+M_s^2$.
5. Proposition 20, p. 16: $V(x)=\|x-x^\star\|^2$ satisfies $R_\gamma V\le\lambda^\gamma V+\gamma c$ for $\gamma\in(0,\bar\gamma]$.
6. Lemma 1, p. 5: such a drift gives $Q^n_\gamma V(x)\le F(\lambda,\Gamma_n,c,\gamma_1,V(x))$.
7. Proposition 2, p. 5: the decomposition bound (10), given the geometric ergodicity (3) of the diffusion.

The paper's proofs follow each statement in the body of the paper (§4.1, §4.12, §5, §5.1).

Significance

The theorem bounds the sampling error of ULA in total variation non-asymptotically, with a dimension-free contraction rate $\kappa$ and constants polynomial in $d$. With steps decreasing to zero and cumulative step size diverging, its bound gives convergence of $\delta_xQ^p_\gamma$ to $\pi$; for constant steps, the paper reports iteration counts of order $d\log d$ at a prescribed precision in Table 2. H3 covers log-concave targets whose potential can lack strong convexity inside a ball.

The result is proved in the paper but, as far as the platform's catalogue shows, not formalized anywhere. A formalization adds machine-checked versions of several reusable pieces:

• a Foster–Lyapunov moment bound for time-inhomogeneous Markov chains (Lemma 1);
• a Girsanov–Pinsker discretisation estimate for Euler schemes (Proposition 2);
• a reflection-coupling contraction for diffusions with monotone drift (56), Theorem 36.

Difficulty

The ULA chain is not reversible with respect to $\pi$, so the spectral and Dirichlet-form tools of reversible MCMC do not apply to it directly. The bound must instead compare the chain with the continuous diffusion.

That comparison needs Girsanov's theorem on path space and a uniform control of $\int\|\nabla U\|^2$ along a time-inhomogeneous chain.

The rate of the diffusion itself is the second obstacle. Without global strong convexity, synchronous coupling gives no contraction inside the ball $\|x-y\|<M_s$. An explicit rate requires a reflection coupling together with return-time estimates, and it has to be transferred through the time change between $dY=-\nabla U\,dt+\sqrt2dB$ and $dX=-\frac12\nabla U\,dt+dB$.

Formalization scope

The state space is the published EthierKurtz.SDEState d, i.e. EuclideanSpace ℝ (Fin d), and Brownian motion and strong solutions are the published EthierKurtz.IsStandardBrownian and EthierKurtz.SolvesBrownianSDE. The conventions are:

• Semigroup. A semigroup is pinned down by the laws of solutions. $P$ is the semigroup of $dX=b(X)dt+s\,dB$ when every strong solution from $x$, on every probability space, has time-$t$ law $P_t(x,\cdot)$. The Langevin case is $b=-\nabla U$, $s=\sqrt2$.
• Total variation. It is the $\sup_{|f|\le1}$ norm. Using $\sup_A|\mu(A)-\nu(A)|$ instead would halve every bound.
• ULA. The laws $\delta_xQ^n_\gamma$ are iterated Measure.bind with the Gaussian kernel $\mathcal N(x-\gamma\nabla U(x),2\gamma I_d)$. Steps are indexed from $1$, and $\Gamma_{n,p}=0$ for $p<n$.
• Moments. Upper-bounded moments ($Q^n_\gamma V$, $\int\|\nabla U\|^2$, $\int\|y-x^\star\|^2d\pi$) are lower Lebesgue integrals, so a non-integrable function cannot make a bound free. $A(\gamma,x)\le a$ is a bound for every $k$, not a real supremum.
• Normalisation of $\pi$. No hypothesis $\int e^{-U}<\infty$ is added; it follows from L1 and H3.
• Quantile. $\Phi^{-1}(u)=\inf\{z:\Phi(z)\ge u\}$.
• Logarithms and powers. $\lambda$, $\kappa$ lie in $(0,1)$, so the logarithms and real powers are genuine.

Several hypotheses are added or read in a particular way, and each is disclosed in the item's statement:

• $x^\star$. It is a bound variable with the hypothesis that it minimises $U$; the paper uses $x^\star$ in §3.3 without defining it.
• Proposition 20. The dimension is positive so its printed $c=2(d+mM_s^2)$ satisfies (6)'s requirement $c>0$; this is stated in Lean.
• Lemma 1. It carries the §2 standing assumption L1, which makes the Euler transition family measurable in its starting point. It is stated for Borel $V\ge0$ rather than $V\ge1$, because Theorem 21 applies it to $\|x-x^\star\|^2$.
• Proposition 2. It assumes (3) only at $\mu_0=\delta_xQ^n_\gamma$, with finite $C$ and a finite bound on $A(\gamma,x)$.
• (11). The printed $Q^k_\gamma(y,dz)$ is read as $Q^k_\gamma(x,dz)$.

The citations [20] (existence of solutions), [27] (Lindvall), [32] (Meyn–Tweedie) and Girsanov's theorem are used inside the proofs and are not restated.

The library work needed is substantial: Itô calculus for the reflection coupling, Girsanov's theorem, Pinsker's inequality in this norm, and generator–drift arguments for the moments of $\pi$. Contributions of any of these as standalone platform theorems are welcome.

Selected references

• A. Durmus, É. Moulines, Nonasymptotic convergence analysis for the unadjusted Langevin algorithm, Ann. Appl. Probab. 27(3), 2017; cited as arXiv:1507.05021v3. https://arxiv.org/abs/1507.05021
• A. S. Dalalyan, Theoretical guarantees for approximate sampling from smooth and log-concave densities, J. R. Stat. Soc. B 79(3), 2017. https://arxiv.org/abs/1412.7392
• T. Lindvall, L. C. G. Rogers, Coupling of multidimensional diffusions by reflection, Ann. Probab. 14(3), 1986. https://doi.org/10.1214/aop/1176992436
• S. P. Meyn, R. L. Tweedie, Stability of Markovian processes III: Foster–Lyapunov criteria for continuous-time processes, Adv. Appl. Probab. 25(3), 1993. https://doi.org/10.2307/1427522
• G. O. Roberts, R. L. Tweedie, Exponential convergence of Langevin distributions and their discrete approximations, Bernoulli 2(4), 1996. https://doi.org/10.2307/3318418

Motivation

The newsvendor problem is the basic single-period inventory decision: a retailer orders $q\ge0$ units at unit cost $c$ before a random demand $\tilde d$ is observed, sells at unit price $p>c$, and loses unsold units. When the demand law is known, the optimal order is a quantile of that law. In practice the law is rarely known, and a distributionally robust newsvendor instead hedges against the worst law in an ambiguity set of laws consistent with partial information.

Scarf (1958; reference [42] of arXiv:1806.05379) solved the case where only the mean and the variance of demand are known, and observed that for a range of small profit margins the robust newsvendor orders nothing. Demand data in retail and spare-parts settings are often heavy tailed: Pareto fits with exponent close to $1$ have been reported, so a finite mean is plausible while a finite variance is not. Das, Dhara and Natarajan (arXiv:1806.05379) therefore replace the variance by an $\alpha$-th moment for an arbitrary real $\alpha>1$. This mission formalizes their result that the zero-order phenomenon survives for every such $\alpha$.

Setting

Write the critical ratio as $\eta=1-c/p\in[0,1)$. A demand law is a probability measure $F$ on $[0,\infty)$. Fix a real $\alpha>1$ and two moments $m_1,m_\alpha$ with

$$m_\alpha>m_1^\alpha>0 .$$

The ambiguity set is

$$\mathcal F_{1,\alpha}=\Big\{F:\ \int_0^\infty w\,dF(w)=m_1,\ \int_0^\infty w^\alpha\,dF(w)=m_\alpha\Big\},$$

the laws on $[0,\infty)$ with mean $m_1$ and $\alpha$-th moment $m_\alpha$. The worst-case expected shortage is

$$\Pi_{1,\alpha}(q)=\sup_{F\in\mathcal F_{1,\alpha}}\mathbb E_F[\tilde d-q]^+ ,$$

and the robust newsvendor problem (3.2) is

$$\min_{q\ge0}\ \big((1-\eta)q+\Pi_{1,\alpha}(q)\big).$$

An optimal order quantity is a minimizer $q^*\ge0$ of this objective. Two thresholds appear:

$$\eta_0=1-\Big(\frac{m_1^\alpha}{m_\alpha}\Big)^{1/(\alpha-1)},\qquad q_0=\frac{\alpha-1}{\alpha}\Big(\frac{m_\alpha}{m_1}\Big)^{1/(\alpha-1)} .$$

In Lean these are ambiguitySet, worstCase, robustCost, eta0, q0 and IsOptimalOrder in the namespace HeavyTailNV.ZeroOrder.

Formalization targets

Goal: Proposition 3.2 (p. 13)

$\eta_0\in(0,1)$, and

• for every $\eta\in[0,\eta_0)$ the set of optimal order quantities is exactly $\{0\}$;
• for every $\eta\in(\eta_0,1)$ an optimal order quantity exists, and every optimal order quantity $q^*$ satisfies $q^*>0$ and

$$q^*\ge q_0 ;$$

• for $\eta=\eta_0$ every $q\in[0,q_0]$ is optimal.

Milestones

1. Proposition 3.1 (p. 12): for $0\le q\le q_0$,

$$\Pi_{1,\alpha}(q)=m_1-q\Big(\frac{m_1^\alpha}{m_\alpha}\Big)^{1/(\alpha-1)},$$

and the two-point law with mass $(m_1^\alpha/m_\alpha)^{1/(\alpha-1)}$ at $(m_\alpha/m_1)^{1/(\alpha-1)}$ and the rest at $0$ lies in $\mathcal F_{1,\alpha}$ and attains the supremum. 2. Properties of $\Pi$ (§2.1, p. 6): $\Pi_{1,\alpha}$ is non-increasing and convex, $\Pi_{1,\alpha}(q)+q=m_1$ for $q\le0$, and $\Pi_{1,\alpha}(q)\to0$ as $q\to\infty$. 3. Display (3.10) (p. 14): for $\eta\in[0,1)$ and $0\le q\le q_0$,

$$(1-\eta)q+\Pi_{1,\alpha}(q)=m_1-q(\eta-\eta_0).$$

Significance

Proposition 3.2 shows that for every finite moment order $\alpha>1$, however high, there is a nonempty interval $[0,\eta_0)$ of critical ratios in which the robust newsvendor orders nothing, and it gives the threshold $\eta_0$ and the minimum positive order $q_0$ in closed form. For $\alpha=2$ it recovers Scarf's zero-order region. The worst-case law associated with $\Pi_{1,\alpha}$ therefore carries a positive mass at zero demand, which is the low-service-level counterpart of the paper's heavy-tail result for high critical ratios (the companion mission of this series).

The results are proved in the paper: the proof of Proposition 3.1 follows the statement on pp. 12–13 and the proof of Proposition 3.2 is on p. 14. None of them has a machine-checked proof. Formalizing them requires a usable treatment of moment-constrained suprema over probability measures on $[0,\infty)$, of the stop-loss transform $q\mapsto\mathbb E[\tilde d-q]^+$, and of minimizers of convex functions on a half-line. These pieces recur across robust inventory and pricing models.

Difficulty

The closed form of Proposition 3.1 is the central step. The lower bound is a computation with a two-point law. The matching upper bound has to hold against every law in $\mathcal F_{1,\alpha}$, including laws with unbounded support and non-integer $\alpha$. The paper obtains it from a dual certificate for the moment problem (3.3)–(3.4), and weak duality for this semi-infinite problem is not available off the shelf. The closed form also holds only on $[0,q_0]$. To conclude anything about minimizers on all of $[0,\infty)$, where no closed form is known for general $\alpha$ (the dual leads to equations $aw^\alpha+bw+c=0$, p. 11), one needs convexity of $\Pi_{1,\alpha}$ on the whole line. Inspecting the objective on $[0,q_0]$ alone does not determine the global minimizers.

Formalization scope

• Demand laws are Measure ℝ with IsProbabilityMeasure F and F (Set.Iio 0) = 0. Moments are Bochner integrals, and the set requires Integrable (fun w => w) F and Integrable (fun w => w ^ α) F (real rpow), so that the moment equalities are genuine.
• $\Pi_{1,\alpha}$ is a real sSup. Under the standing hypotheses $\alpha>1$, $m_1>0$, $m_\alpha>m_1^\alpha$ the set is nonempty (it contains the two-point law of Proposition 3.1) and the expectations are bounded above by $m_1+|q|$, so the value is not Lean's default for an empty or unbounded set. Every statement carries these standing hypotheses of (3.1); no other hypothesis is added except the range $\eta\in[0,1)$ in (3.10), which is the paper's standing range of the critical ratio.
• Optimality is minimization over $q\in[0,\infty)$, as in (3.2), not over $\mathbb R$. Over $\mathbb R$ the objective equals $m_1-\eta q$ for $q\le0$, and part (a) would fail at $\eta=0$.
• Trivializing readings are ruled out. Part (a) asserts that $\{0\}$ is the whole set of minimizers, not only that $0$ is a minimizer. Part (b) asserts that a minimizer exists, so its lower bound is not vacuous. Dropping the support constraint, the normalization, or the integrability clauses would change the problem or let junk integrals satisfy the moment constraints.
• The unit cost and price never appear; everything is stated in $\eta$.
• The ambiguity set, worst-case value and objective come from the shared HeavyTailNV.Tail.Model. This mission defines the thresholds, optimality predicate and two-point law in HeavyTailNV.ZeroOrder.Model. Contributions to the general moment-problem duality used by Proposition 3.1 are welcome and reusable well beyond this mission.

Selected references

• B. Das, A. Dhara and K. Natarajan, On the heavy-tail behavior of the distributionally robust newsvendor, Operations Research 69(4), 2021; preprint arXiv:1806.05379v2, 2019. https://arxiv.org/abs/1806.05379
• H. Scarf, A min–max solution of an inventory problem, in K. Arrow, S. Karlin and H. Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, pp. 201–209, Stanford University Press, 1958 (no DOI; reference [42] of https://arxiv.org/abs/1806.05379).

Motivation

Robust Sample Average Approximation (Robust SAA) is a data-driven approach to stochastic optimization proposed by Bertsimas, Gupta and Kallus (arXiv:1408.4445; Mathematical Programming (2018), doi:10.1007/s10107-017-1174-z). Instead of minimizing the empirical average of a cost, a decision maker minimizes the worst-case expected cost over a distributional uncertainty set: the set of distributions that a statistical goodness-of-fit (GoF) test does not reject at a chosen significance level, given the observed data. Each classical GoF test therefore produces its own robust optimization model.

Whether such a model behaves well as data accumulate depends on a property of the test. Theorem 2 of the paper shows that Robust SAA converges, in objective, optimal value and optimal solutions, for every admissible cost if and only if the underlying test is uniformly consistent. This mission concerns the univariate case: it asks for a proof that the five standard tests on the real line, those of Kolmogorov–Smirnov, Kuiper, Cramér–von Mises, Watson and Anderson–Darling, are uniformly consistent (Theorem 5, p. 14). The companion missions of the series treat the characterization (Theorem 2) and the discrete χ² and G-tests (Theorem 4).

Setting

Let $F$ be a probability distribution on $\mathbb R$, and let $\xi^1,\xi^2,\dots$ be independent draws from $F$. As in §3.2 of the paper, $\xi$ is a continuous random variable: $F$ has no atoms. For a candidate distribution $F_0$ write $F_0(t)=F_0((-\infty,t])$ for its cdf, and write $\xi^{(1)}\le\dots\le\xi^{(N)}$ for the sorted sample of size $N$. With $u_i=F_0(\xi^{(i)})$, the five statistics (8) are

$$\begin{aligned} D_N&=\max_{1\le i\le N}\max\Big\{\tfrac iN-u_i,\ u_i-\tfrac{i-1}N\Big\},& V_N&=\max_i\Big(u_i-\tfrac{i-1}N\Big)+\max_i\Big(\tfrac iN-u_i\Big),\\ W_N&=\Big(\tfrac1{12N^2}+\tfrac1N\sum_{i=1}^N\Big(\tfrac{2i-1}{2N}-u_i\Big)^2\Big)^{1/2},& U_N&=\Big(W_N^2-\Big(\tfrac1N\sum_{i=1}^Nu_i-\tfrac12\Big)^2\Big)^{1/2}, \end{aligned}$$ $$A_N=\Big(-1-\sum_{i=1}^N\tfrac{2i-1}{N^2}\big(\log u_i+\log(1-u_{N+1-i})\big)\Big)^{1/2}.$$

For a statistic $S_N$ and a threshold $Q_{S_N}(\alpha)$, the confidence region (7) is $\mathcal F^\alpha_{S_N}=\{F_0: S_N(F_0;\xi^1,\dots,\xi^N)\le Q_{S_N}(\alpha)\}$: the distributions the test does not reject. A test is uniformly consistent (Definition 3, p. 13) if, for every data-generating $F$, almost surely every sequence $F_N$ that does not converge weakly to $F$ is rejected infinitely often, i.e. $F_N\notin\mathcal F_N$ for infinitely many $N$. The Lévy metric between cdfs is $d_{\text{Lévy}}(G,G')=\inf\{\epsilon>0: G(\xi-\epsilon)-\epsilon\le G'(\xi)\le G(\xi+\epsilon)+\epsilon\ \forall\xi\}$, and $\hat F_N$ denotes the empirical cdf.

Formalization targets

Goal: Theorem 5

For thresholds $\tau_N$ with $\tau_N\le q/\sqrt N$ for some constant $q$ and all $N\ge1$,

$$\text{the regions }\{F_0: S_N(F_0)\le\tau_N\},\quad S_N\in\{D_N,V_N,W_N,U_N,A_N\},\ \text{are uniformly consistent.}$$

The statement fixes only the rate $O(N^{-1/2})$ of the thresholds, which is all the paper's argument uses; it holds for any sequence with that rate, in particular for the tabulated quantiles $Q_{S_N}(\alpha)$.

Milestones (§10.7, pp. 38–39)

1. $d_{\text{Lévy}}$ metrizes weak convergence on $\mathbb R$; almost surely $d_{\text{Lévy}}(\hat F_N,F)\to0$.
2. $d_{\text{Lévy}}(\hat F_N,F_0)\le D_N(F_0)$, and $D_N\le V_N$.
3. $D_N^2(F_0)\le\max\{1/\sqrt N+3/(2N),\ \sqrt N\,W_N^2(F_0)+2/\sqrt N\}$, and the same with $W_N^2$ replaced by $A_N^2$.
4. $W_N^2-U_N^2=(\tfrac1N\sum_iF_0(\xi^{(i)})-\tfrac12)^2\le\max\{\dots\}$, a bound in terms of $D'_N(F_0)=\max_i|F_0(\xi^{(i)})-\tfrac{2i-1}{2N}|$.

Significance

The result. Together with Theorem 2 of the paper, Theorem 5 guarantees that Robust SAA built on any of these five univariate tests converges for every cost that is equicontinuous in the decision and satisfies the paper's growth conditions. It also feeds Proposition 5, which extends the guarantee to multivariate problems with separable costs by testing marginals. Without it, the univariate tests would carry only the finite-sample guarantee of Proposition 1 and no asymptotic one.

The formalization. The theorem is proved in the paper, but the published argument for the Watson test has a gap. Its last step asserts that $(\tfrac1N\sum_i\min\{1,\tfrac{2i-1}{2N}+D'_N\}-\tfrac12)^2=O(1/N)$ whenever $D'_N\ge1/\sqrt N+1/N$, which fails when $D'_N$ stays bounded away from $0$ (at $D'_N=1/2$ the expression tends to $9/64$). The Watson clause is believed true, but a complete proof needs a different argument. The Anderson–Darling step relies on a cited integral representation rather than an argument on the page. A machine-checked proof would close both points. No part of the theorem is formalized elsewhere, as far as a search of the platform shows.

Difficulty

The Kolmogorov–Smirnov case reduces to deterministic inequalities once the Lévy-metric picture is in place, but each of the other statistics controls $D_N$ only indirectly. The Cramér–von Mises statistic is an $L^2$ quantity, and an $L^2$ bound does not by itself control a supremum. What closes the gap is monotonicity of $F_0$ together with the rate of the threshold, so a threshold that merely tends to $0$ is not enough. The Watson statistic is invariant under cyclic rotation of the transformed sample $u_1,\dots,u_N$ on the circle $[0,1)$, so a small $U_N$ leaves the centring term $\tfrac1N\sum_iF_0(\xi^{(i)})-\tfrac12$ uncontrolled until the boundary constraints $0\le F_0\le1$ are used. The obvious attempt, bounding the centring term by $D'_N$ alone, is the step that fails on p. 39.

Formalization scope

Distributions are MeasureTheory.ProbabilityMeasure ℝ, with weak convergence as their topology. The cdf is Mathlib's ProbabilityTheory.cdf. The data are the coordinates of the canonical product space ℕ → ℝ under Measure.infinitePi, so the sample of size $N$ is $(\omega_0,\dots,\omega_{N-1})$. Order statistics are the sorted sample s ∘ Tuple.sort s, and every formula of (8) is written with the paper's 1-based index ($i$ in Lean is the paper's $i+1$; $\xi^{(N+1-i)}$ is Fin.rev i).

Committed conventions:

• distributions range over all of $\mathbb R$; a support $[\underline\xi,\overline\xi]$ with infinite endpoints is this case;
• the data law has no atoms (§3.2's standing assumption, expressed by the predicate IsContinuousLaw), although the paper's proof does not use it;
• $A_N$ takes values in $[0,\infty]$ and is $+\infty$ when some $F_0(\xi^{(i)})\in\{0,1\}$, so Lean's $\log0=0$ never makes a distribution look close;
• the threshold hypothesis is an explicit constant, $\tau_N\le q/\sqrt N$ for $N\ge1$;
• maxima over an empty index set are $0$, and every fixed-$N$ milestone assumes $N\ge1$.

Uniform consistency is quantified over all sequences $F_N$ inside the almost-sure event, as in Definition 3. A pointwise consistency statement for a fixed $F_0$ is a different and weaker theorem and does not count.

A full development needs the Lévy metric and its metrization of weak convergence on $\mathbb R$, the Glivenko–Cantelli theorem in Lévy form, and elementary order-statistic inequalities. The first two are reusable well beyond this mission. Contributions of independent value include a corrected proof of the Watson step, and a proof of the goal without the atomless hypothesis.

Selected references

• D. Bertsimas, V. Gupta, N. Kallus, Robust Sample Average Approximation, arXiv:1408.4445v3 (2016); Mathematical Programming (2018). https://arxiv.org/abs/1408.4445, https://doi.org/10.1007/s10107-017-1174-z
• R. M. Dudley, Real Analysis and Probability, Cambridge University Press, 2002, Theorem 11.4.1. https://doi.org/10.1017/CBO9780511755347
• R. B. D'Agostino, M. A. Stephens (eds.), Goodness-of-Fit Techniques, Marcel Dekker, New York, 1986 (reference [14] of the paper; the source of the formulas (8)).

Motivation

A decision made from sampled data can be sensitive to the distribution chosen to represent future uncertainty. Robust sample average approximation addresses this by optimizing against every distribution that passes a goodness of fit test, rather than against one fitted distribution. The resulting set of plausible laws is a data driven uncertainty set. Its finite sample coverage and its behavior as the sample grows serve different purposes: coverage protects against sampling error at a chosen sample size, while convergence asks whether the uncertainty set eventually stops admitting laws far from the true one. Bertsimas, Gupta, and Kallus distinguish these properties in their Robust Sample Average Approximation paper.

This mission concerns the two tests the paper assigns to a known finite support: Pearson's $\chi^2$ test and the G test. Both compare the empirical frequencies of the observed support points with the probabilities under a proposed law. Their confidence regions give concrete uncertainty sets for discrete data. The paper's Theorem 4 states that both tests have the stronger convergence property it calls uniform consistency. That property is used in its general characterization of when robust sample average approximation converges for every admissible cost function (Theorem 2 and Table 1, pp. 13–14).

Setting

Fix a known set of $n$ possible observations, labelled $j=1,\ldots,n$. A probability law $F$ on this support is specified by probabilities $p_F(j)$, each nonnegative and summing to one. A sample of size $N$ consists of independent observations $\xi^1,\ldots,\xi^N$ from an unknown true law $F$. Its empirical frequency at label $j$ is

$$\widehat p_N(j)=\frac1N\sum_{i=1}^N\mathbf 1\{\xi^i=j\}.$$

To assess a hypothetical law $F_0$ with probabilities $p_0(j)$, Pearson's statistic and the G statistic are, in the paper's normalization,

$$X_N(F_0)=\left(\sum_{j=1}^n\frac{(p_0(j)-\widehat p_N(j))^2}{p_0(j)}\right)^{1/2},\qquad G_N(F_0)=\left(2\sum_{j=1}^n\widehat p_N(j)\log\frac{\widehat p_N(j)}{p_0(j)}\right)^{1/2}.$$

The confidence region for each test is the set of hypothetical laws whose statistic is at most $\sqrt{Q/N}$, where $Q\ge0$ is fixed across sample sizes. An observed point to which $F_0$ assigns zero probability makes either statistic infinite. A term with zero empirical frequency contributes zero to the G sum, including when its hypothetical probability is zero. These conventions make the regions describe the same tests at the boundary of the probability simplex as they do in its interior (§3.1, p. 8; §10.6, p. 38).

A sequence of laws $F_N$ is weakly convergent to $F$ when expectations of every bounded continuous function converge. On this finite support, weak convergence can be measured by the total variation distance

$$d_{\mathrm{TV}}(q,q')=\frac12\sum_{j=1}^n|q(j)-q'(j)|.$$

The paper's Definition 3 calls a test uniformly consistent when, for every true law $F$, almost surely every sequence $F_N$ that fails to converge weakly to $F$ lies outside the confidence region infinitely often (Definition 3, p. 13). The almost sure event applies to all such sequences at once; this is stronger than a statement about one fixed false hypothesis.

Formalization targets

Goal: both tests are uniformly consistent

For the Pearson and G confidence regions $\mathcal F_N^{\chi^2}$ and $\mathcal F_N^G$ with fixed $Q\ge0$, the target is

$$\operatorname{UC}(\mathcal F_N^{\chi^2})\quad\text{and}\quad\operatorname{UC}(\mathcal F_N^G).$$

Here $\operatorname{UC}$ has the quantifier order of Definition 3: every generating $F$, almost every infinite sample, and every nonconvergent sequence $F_N$. This is Theorem 4, p. 14. Its four milestone claims are the finite support description of weak convergence, almost sure convergence of empirical frequencies, and the paper's total variation bounds for $X_N$ and $G_N$ (§10.6, p. 38).

Significance

The result says that distributions retained by either test cannot remain persistently separated from the data generating law as the sample grows. In the paper's framework, that is the statistical condition needed for its general theorem to turn test based confidence regions into convergent robust optimization values and decisions under its separate assumptions on the cost and feasible set (Theorem 2, p. 13). Theorem 4 itself concerns the tests; it does not assume a cost function or assert optimization convergence directly.

The paper proves Theorem 4, so the open work here is its Lean formalization. A complete development would also leave reusable statements for finite probability vectors, their empirical frequencies under an infinite product law, total variation, and the boundary aware Pearson and G divergences. These pieces can support other discrete goodness of fit and distributionally robust optimization results. The mission does not claim that Theorem 4 already has a machine checked proof.

Difficulty

Pointwise convergence of empirical frequencies does not by itself state uniform consistency. The latter quantifies over all moving hypothetical laws $F_N$ on one almost sure sample event, including laws chosen differently at every $N$. A direct argument about one fixed $F_0\ne F$ therefore does not address the target. The finite support makes weak convergence concrete, but the formal statement must still relate that topology to a finite total variation sum and keep the quantifiers in the order required by Definition 3.

The boundary of the probability simplex is another source of difficulty. Lean's real division and logarithm have default values at zero. Using those defaults in the test statistics would accept some laws that assign zero probability to an actually observed category. Both statistics must instead retain the paper's infinite penalty there. The G expression also contains individual logarithmic terms that may be negative before summation, so its extended value cannot be built by coercing each term directly to a nonnegative extended real.

Formalization scope

The known support is represented by Fin n. Its members are labels for the paper's distinct points $\hat\xi^1,\ldots,\hat\xi^n$; coordinates in Euclidean space are irrelevant to these tests. Laws use Mathlib's ProbabilityMeasure (Fin n) and its weak topology. The data are coordinates of the canonical infinite product law, with Lean index zero corresponding to the paper's first observation. The empty support has no probability law; all substantive instances have $n\ge1$. The empty sample $N=0$ is defined by total operations but has no bearing on an eventual or infinitely often assertion.

Pearson's statistic lives in $[0,+\infty]$. The squared G statistic uses extended real arithmetic so finite negative summands can be combined with an infinite boundary term. Its region compares $G_N^2$ with $Q/N$, equivalent to the paper's $G_N\le\sqrt{Q/N}$ at positive $N$. The free $Q\ge0$ stands for a fixed threshold constant, including the paper's chi square quantile; no particular quantile value is built into the theorem. This makes explicit the only property of that threshold used in §10.6: independence from $N$.

Contributions may prove the four milestone statements, connect Mathlib's finite probability and strong law interfaces to the empirical frequencies, or establish finite support versions of Cauchy–Schwarz and Pinsker with the correct infinite boundary cases. A proof of the goal must use the stated regions and preserve simultaneous quantification over every moving sequence of laws; replacing uniform consistency by convergence of $\widehat p_N$ would remove its main claim.

Selected references

• Dimitris Bertsimas, Vishal Gupta, Nathan Kallus, Robust Sample Average Approximation, arXiv:1408.4445v3, 2016; published in Mathematical Programming (2018). Preprint · Publication DOI.

Motivation

A McKean–Vlasov control problem asks a planner to steer a stochastic differential equation whose coefficients depend not only on the current path of the state but also on its (conditional) distribution. Such problems describe the cooperative optimum of a large population of interacting agents: when each agent reacts to the empirical distribution of all others and a social planner chooses everybody's control, the limit as the population grows is a McKean–Vlasov control problem (Lacker 2017). When all agents are also exposed to a common noise (a shared source of randomness, such as a market factor), the relevant distribution is the conditional law of the state given that noise.

Bellman's dynamic programming principle (DPP) is the standard route from a control problem to its Hamilton–Jacobi–Bellman equation and to verification arguments. For McKean–Vlasov dynamics it fails in the naive state variable, because the problem is time-inconsistent; it can be recovered by taking the (conditional) law of the state as the state.

Timeline. Laurière and Pironneau (2014) and Bensoussan, Frehse and Yam (2013–2017) proved a DPP for densities of the state law. Pham and Wei (2017, SICON) proved a DPP over closed-loop controls in a Markovian setting with a common-noise filtration, under regularity assumptions; Pham and Wei (2018, ESAIM:COCV) treated the case without common noise. Bayraktar, Cosso and Pham (2018, Trans. AMS) obtained a randomised DPP, again Markovian and without common noise. Djete, Possamaï and Tan (2022) proved the DPP for the general non-Markovian problem with common noise, under Borel measurability of the coefficients only. This mission formalizes their DPP for the weak formulation.

Setting

Fix a horizon $T>0$, dimensions $n,d,\ell\in\mathbb N$, a nonempty Polish space $(U,\rho)$ of control values, a point $u_0\in U$ and an exponent $p\ge0$. Let $\mathcal C^k:=C([0,T],\mathbb R^k)$ with the uniform norm, $\mathcal P(E)$ the Borel probability measures on $E$ with the weak topology, and $x_{t\wedge\cdot}$ the path $x$ stopped at time $t$. The coefficients $b,\sigma,\sigma_0,L$ are maps $[0,T]\times\mathcal C^n\times\mathcal P(\mathcal C^n\times U)\times U\to\mathbb R^n,\mathbb R^{n\times d},\mathbb R^{n\times\ell},\mathbb R$, and $g:\mathcal C^n\times\mathcal P(\mathcal C^n)\to\mathbb R$; all are Borel measurable, and $b,\sigma,\sigma_0,L$ depend on the path and the measure only through their restrictions to $[0,t]$ (non-anticipative).

A weak control $\gamma$ with initial condition $(t,\nu)\in[0,T]\times\mathcal P(\mathcal C^n)$ consists of a probability space carrying two filtrations $\mathbb F^\gamma\supseteq\mathbb G^\gamma$ (the second models the common noise), a state $X^\gamma$, Brownian motions $W^\gamma$ (idiosyncratic) and $B^\gamma$ (common) on $[t,T]$, a predictable $U$-valued control $\alpha^\gamma$, and measure-valued processes $\mu^\gamma_s=\mathcal L(X^\gamma_{s\wedge\cdot}\mid\mathcal G^\gamma_s)$ and $\bar\mu^\gamma_s=\mathcal L((X^\gamma_{s\wedge\cdot},\alpha^\gamma_s)\mid\mathcal G^\gamma_s)$, such that $X^\gamma_{t\wedge\cdot}\sim\nu(t)$, an integrability condition of order $p$ holds, a compatibility condition between the two filtrations holds, and

$$dX^\gamma_s=b(s,X^\gamma,\bar\mu^\gamma_s,\alpha^\gamma_s)\,ds+\sigma(s,X^\gamma,\bar\mu^\gamma_s,\alpha^\gamma_s)\,dW^\gamma_s+\sigma_0(s,X^\gamma,\bar\mu^\gamma_s,\alpha^\gamma_s)\,dB^\gamma_s,\qquad s\in[t,T].$$

The reward and the value function are

$$J(t,\gamma)=\mathbb E\Big[\int_t^TL(s,X^\gamma_{s\wedge\cdot},\bar\mu^\gamma_s,\alpha^\gamma_s)\,ds+g(X^\gamma_{T\wedge\cdot},\mu^\gamma_T)\Big],\qquad V_W(t,\nu)=\sup_{\gamma\in\Gamma_W(t,\nu)}J(t,\gamma),$$

with $\infty-\infty:=-\infty$ and $\sup\emptyset=-\infty$. Each weak control also carries $A^\gamma_s=\int_t^{s\vee t}\pi(\alpha^\gamma_r)\,dr$, where $\pi$ is a Borel isomorphism of $U$ onto a subset of $[0,1]$, and the continuous conditional-law process $\hat\mu^\gamma$ of $(X^\gamma,A^\gamma,W^\gamma,B^\gamma)$ given $\mathbb G^\gamma$.

Formalization targets

Goal: Theorem 3.1

$V_W:[0,T]\times\mathcal P(\mathcal C^n)\to[-\infty,\infty]$ is upper semi-analytic (every superlevel set $\{V_W>c\}$ is analytic), and for every stopping time $\tau^\star$ of the canonical filtration of $\Omega^\star:=\mathcal C^\ell\times C([0,T],\mathcal P(\mathcal C^n\times\mathcal C\times\mathcal C^d\times\mathcal C^\ell))$ with values in $[t,T]$, setting $\tau^\gamma:=\tau^\star(B^{\gamma,t},\hat\mu^\gamma)$,

$$V_W(t,\nu)=\sup_{\gamma\in\Gamma_W(t,\nu)}\mathbb E\Big[\int_t^{\tau^\gamma}L(s,X^\gamma_{s\wedge\cdot},\bar\mu^\gamma_s,\alpha^\gamma_s)\,ds+V_W(\tau^\gamma,\mu^\gamma_{\tau^\gamma})\Big].$$

Milestones

The canonical reformulation on $\bar\Omega:=\hat\Omega\times C([0,T],\mathcal P(\hat\Omega))$ with weak control rules $\bar{\mathcal P}_W(t,\nu)$ (Definition 4.1): Lemma 4.4(i) (weak controls and weak control rules correspond), Corollary 4.6 ($V_W(t,\nu)=\sup_{\bar{\mathbb P}\in\bar{\mathcal P}_W(t,\nu)}J(t,\bar{\mathbb P})$), Lemma 4.7 (analytic graphs, $V_W$ u.s.a.), Lemma 4.8 (stability under conditioning at a stopping time), Lemma 4.9 (dependence on the initial law only through $\hat\nu(t)$), (4.10) (moment truncation $V^M_W\nearrow V_W$, analytic and u.s.a.) and Lemma 4.10 (universally measurable $\varepsilon$-optimal families and concatenation).

Significance

The result. The theorem gives the DPP for McKean–Vlasov control with common noise in a non-Markovian setting, with no regularity on the coefficients beyond Borel measurability and no integrability on the rewards. It is the starting point for the dynamic programming (HJB) equation on the space of probability measures, for the Markovian corollaries of §3.2 of the paper, and, through the equivalence of formulations in the companion work, for the strong formulations treated in the second mission of this series.

Formalizing it. The result is proved on paper; nothing of it is machine-checked. A formal development needs a working theory of weak controls with conditional laws, a controlled martingale problem on a space of measure-valued paths, and analytic-set measurability in continuous time. None of these exists in Mathlib, and the analytic-selection layer on Prove2Me (Bertsekas–Shreve, Chapter 7) is stated but not yet proved.

Difficulty

The obvious argument conditions an optimal-ish control on its information at the stopping time and pastes in near-optimal controls from the conditioned states. Each step fails without additional structure: $V_W$ is not known to be measurable, so $\mathbb E[V_W(\tau^\gamma,\mu^\gamma_{\tau^\gamma})]$ is not obviously meaningful; conditioning a weak control on its information at $\tau^\gamma$ need not yield a weak control, because the conditional-law constraint involves the common-noise filtration and a compatibility condition between filtrations; and choosing a near-optimal control for each conditioned state is a selection problem over an uncountable family of probability spaces. The state of the problem is a law, which is itself defined only up to null sets, so random-time evaluations such as $\mu^\gamma_{\tau^\gamma}$ need a continuous version.

Formalization scope

The Lean development lives in the namespace MKVDPP.Weak. Conventions:

• Times are in $\mathbb R_{\ge0}$; paths are elements of $C([0,T],\mathbb R^k)$ with $\mathbb R^k$ Euclidean; a path is read at times beyond $T$ as its value at $T$.
• Expectations and time integrals are $\mathbb E[\xi^+]-\mathbb E[\xi^-]$ in $[-\infty,\infty]$ with $\infty-\infty=-\infty$, computed as lower integrals.
• The supremum defining $V_W$ ranges over weak controls on probability spaces in Type (universe 0).
• "The integrals are implicitly assumed to be well-defined" is pinned to local Itô integrals (EthierKurtz.HasBrownianItoIntegral) of integrands that are a.s. square integrable on $[t,T]$, taken against the shifted Brownian motions $W^{\gamma,t}$, $B^{\gamma,t}$; no $L^2(\mathbb P)$ condition, which would shrink $\Gamma_W$.
• The conditional-law requirement "for $d\mathbb P\otimes ds$-a.e. $(s,\omega)$" is read in Fubini form; $\mu^\gamma_T$ and $\mu^\gamma_{\tau^\gamma}$ are the $X$-marginals of the continuous process $\hat\mu^\gamma$.
• "Local martingale on $[t,T]$" in Definition 4.1 is pinned to: every localised process $S^{\varphi,m}$, $m\ge1$, is an $(\bar{\mathbb F},\bar{\mathbb P})$-martingale on $[t,T]$. The page integrates $|\bar S|$ and $\bar S^\varphi$ from $0$. Here they run from the initial time $t$, because before $t$ the canonical control may be $\partial$, where the coefficients are undefined, and a coefficient that is not integrable before $t$ would empty $\hat{\mathcal P}_W(t,\cdot)$.
• The cemetery value $\partial$ of the canonical control is read as $u_0$ inside the coefficients (a null set under Definition 4.1).
• In (3.2), $(+\infty)+(-\infty)$ inside the expectation is $-\infty$.
• Lemma 4.4(i)'s converse carries the hypothesis that the canonical $A$ is a.s. $\int_t^{\cdot\vee t}\pi(\bar\alpha_r)\,dr$; without it the converse is false, because Definition 4.1 leaves $A$ before $t$ unconstrained.

The goal does not mention the canonical space $\bar\Omega$, weak control rules or any selection; a formalization of $\Gamma_W$ that is empty, or a value function that is constant, would trivialize it. A sanity file exhibits a weak control in the degenerate case $n=d=\ell=0$ for every $t\le T$, so the structure is satisfiable.

Infrastructure a complete development needs: conditional laws and r.c.p.d. on Polish spaces, the predictable $\sigma$-algebra, stochastic integrals against a filtration, the Stroock–Varadhan martingale problem, Itô's formula, and analytic sets with the Jankov–von Neumann selection theorem. The analytic-selection results and the martingale-problem/SDE correspondence are reusable well beyond this mission. Contributions on any milestone, and on proving the referenced Bertsekas–Shreve selection theorems, are welcome. Out of scope: Theorem 3.4 (it rests on the companion paper), the Markovian results of §3.2, and the HJB discussion of §3.3.

Selected references

• M. F. Djete, D. Possamaï, X. Tan, McKean–Vlasov optimal control: the dynamic programming principle, Ann. Probab. 50(2), 2022; cited as arXiv:1907.08860v2. https://arxiv.org/abs/1907.08860v2
• H. Pham, X. Wei, Dynamic programming for optimal control of stochastic McKean–Vlasov dynamics, SIAM J. Control Optim. 55(2):1069–1101, 2017. https://arxiv.org/abs/1604.04057
• D. Lacker, Limit theory for controlled McKean–Vlasov dynamics, SIAM J. Control Optim. 55(3):1641–1672, 2017. https://arxiv.org/abs/1609.08064
• N. El Karoui, X. Tan, Capacities, measurable selection and dynamic programming part II: application in stochastic control problems, 2013. https://arxiv.org/abs/1310.3364
• E. Bayraktar, A. Cosso, H. Pham, Randomized dynamic programming principle and Feynman–Kac representation for optimal control of McKean–Vlasov dynamics, Trans. Amer. Math. Soc. 370(3):2115–2160, 2018. https://doi.org/10.1090/tran/7118
• M. Laurière, O. Pironneau, Dynamic programming for mean-field type control, C. R. Math. Acad. Sci. Paris 352(9):707–713, 2014. https://doi.org/10.1016/j.crma.2014.07.008
• A. Bensoussan, J. Frehse, S. Yam, Mean Field Games and Mean Field Type Control Theory, SpringerBriefs in Mathematics, Springer, 2013. https://doi.org/10.1007/978-1-4614-8508-7
• D. Bertsekas, S. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978. https://web.mit.edu/dimitrib/www/SOC_1978.pdf
• D. Stroock, S. Varadhan, Multidimensional Diffusion Processes, Springer, 1997. https://doi.org/10.1007/3-540-28999-2