Operations Research

Motivation

Many demand, traffic and click-through series are seasonal: their mean repeats after a fixed number of periods (a week of days, a year of months), while the length of that cycle is not known in advance. A retailer choosing among $K$ promotions, or a platform choosing among $K$ recommendations, then faces a multi-armed bandit whose arms have time-varying but periodic mean rewards. Standard stochastic bandit algorithms assume stationary means and fail here, and fully adversarial or arbitrarily drifting models give up the structure that periodicity offers.

N. Chen, C. Wang and L. Wang (arXiv:2005.08088, Operations Research, 2025) propose a two-stage policy for this problem: a spectral first stage that estimates every arm's period from a short exploration phase, and a confidence-bound second stage that learns and exploits the resulting "effective arms". Their main upper bound, Theorem 1, shows that the policy's regret grows like $\sqrt{T\sum_k T_k}$ up to logarithmic factors. This mission formalizes that theorem and the chain of lemmas behind it. The matching lower bound (Theorem 3 of the paper) is the subject of a separate mission of this series.

Setting

At each epoch $t=1,\dots,T$ a decision maker pulls one of $K$ arms. Pulling arm $k$ at epoch $t$ yields the reward $Y_{k,t}=\mu_{k,t}+\epsilon_t$. The mean $\mu_{k,t}$ has a minimum period $T_k\ge1$: $\mu_{k,t+T_k}=\mu_{k,t}$ for all $t\ge1$, and no smaller positive shift has this property. The standing assumptions are:

• Assumption 1: $\mu_{k,t}\in[0,1]$.
• Assumption 2: the noises $\epsilon_t$ are independent and sub-Gaussian with parameter $\sigma$, i.e. $\mathbb E[e^{\lambda\epsilon_t}]\le e^{\sigma^2\lambda^2/2}$ for all real $\lambda$ and $\mathbb P(|\epsilon_t|>x)\le2e^{-x^2/(2\sigma^2)}$.

The pseudo-regret of an arm sequence $\pi$ is $R^\pi_T=\sum_{t=1}^T(\max_k\mu_{k,t}-\mu_{\pi_t,t})$, and the number of effective arms is $d=\sum_{k=1}^KT_k$: arm $k$ at phase $t \bmod T_k$ is one effective arm.

Stage one (Algorithm 1). Each arm is pulled $n$ times in a row. From its $n$ rewards the policy computes the periodogram $|\tilde y_k(v)|$, the modulus of the discrete Fourier transform $\tilde y_k(v)=\frac1n\sum_sY_{k,s}e^{-2\pi ivs}$, on $v\in[0,1/2]$. A data-driven threshold $\tau_k$ is computed from the constants $U_1,U_2$ (sums of sinc-type maxima), $\bar\epsilon_v=\frac{2\sigma H}{1-\pi/24}\sqrt{\log(n)/n}$ and $\sup_v|\tilde y_k(v)|$. The algorithm repeatedly takes the highest peak above $\tau_k$ in $[g/n,1/2]$, snaps it to the nearest fraction $j_1/j_2$ with $j_2<n/(2g)$, and removes a $2g/n$-neighbourhood. The period estimate $\hat T_k$ is the least common multiple of the selected reciprocals.

Stage two (Algorithm 2). At every later epoch an $S$-round screening tournament, $S=\lfloor\log_2T\rfloor$, compares the arms at their current phases modulo $\hat T_k$. It uses estimated means $m^{(s)}_{k,t}$ and widths $w^{(s)}_{k,t}$ pooled from the stage-one samples and from round-specific index sets $\Psi^{(s)}(t)$. The weak oracle runs the same policy with the true periods in place of $\hat T_k$.

The parameters are fixed by (7): $n=\lfloor\sqrt{T/K}\rfloor$, $g=\lceil\sqrt n\rceil$, $H=\sqrt{1+\log n}$. Assumption 3 asks $T>4K$, $g\ge\max\{2,\sqrt n\}$ and $T_k<n/(2g)$. Assumption 4 asks the smallest present Fourier coefficient $b_k$ of each arm to dominate a combination of $\bar\epsilon_v$ and the largest coefficient $B_k$.

Formalization targets

Goal: Theorem 1

Under Assumptions 1–4 and (7), the two-stage policy satisfies

$$\mathbb E\big[R^\pi_T\big]\le C\sqrt{T\,d\,\log^2(T)\,\log(T/d)} ,$$

with $C$ depending only on $\sigma$ and $K$, and with Algorithm 2 run at $\delta=8/T$.

Stage one: correct period identification

• Lemma 1: uniform noise bound for the periodogram, $48n\exp(-(n\delta^2/4\sigma^2)(1-\pi/24)^2)$.
• Lemmas 2–3: leakage bounds $\pi B_kU_1$, $\pi B_kU_2$, and $B_k\le(\sup|\tilde\epsilon_k|+\sup|\tilde y_k|)/(1-\pi U_2)$.
• Lemmas 4–5: the threshold separates the neighbourhoods of the present frequencies from the rest, with probability $1-48/n^{H^2-1}$.
• Lemmas 6–7: the sharper noise bound near possible present frequencies, and the location of the peaks within $1/n$ of them.
• Theorem 2: $\mathbb P(\Lambda)\ge1-48K/n^{H^2-1}-200K/n^{0.867H^2-1}-200K/n^{0.6934H^2-1}$.

Stage two: the oracle's regret

• Lemma 15: an anytime sub-Gaussian deviation bound.
• Lemma 9: the confidence event $\mathcal E$ has probability at least $1-\delta S$.
• Lemma 10: on $\mathcal E$ the optimal arm survives screening, and each epoch's gap is at most $1$, $8\sigma/2^s$ or $2\sigma/\sqrt T$.
• Lemma 16: the summed widths of a round are at most $4\sigma\sqrt{|\Psi^{(s)}(T)|\,d\log(8T/\delta)\log(T/d)}$.
• Lemma 11: the oracle's expected regret is at most $C\sqrt{Td\log^2(T)\log(T/d)}$ with $C$ depending only on $\sigma$.

Significance

The theorem shows that unknown seasonality costs only the factor $\sqrt{d}=\sqrt{\sum_kT_k}$ that would be paid if every phase of every arm were a separate stationary arm. Up to logarithmic factors this matches the $\sqrt{TK}$ rate of the classical stationary bandit with $d$ arms in place of $K$. Together with the paper's lower bound $\Omega(\sqrt{T\max_kT_k})$ it locates the minimax regret of periodic bandits within a factor $\sqrt K$. Stage one is a non-asymptotic, finite-sample period-identification guarantee for a thresholded periodogram, which is of independent use in spectral estimation.

The paper proves these results; none of them is machine-checked. A complete development yields a verified finite-sample periodogram theory (noise bounds for random trigonometric polynomials, Dirichlet-kernel leakage estimates), a verified anytime sub-Gaussian inequality, and a verified analysis of a nested elimination algorithm with data reuse. The formalization also pins down several points the printed text leaves open: the constant $0.233$ of Lemma 6 and the exponent $0.694$ of Lemma 7 and Theorem 2 are slightly stronger than what the proofs give, and the printed claim that Theorem 1's constant is independent of $K$ is not established by the printed argument.

Difficulty

Two steps resist the obvious approach. In stage one, the periodogram has to be controlled at uncountably many frequencies at once. A union bound over $v$ is unavailable, and the leakage of each present frequency spreads over the whole spectrum, so both the noise and the signal must be bounded uniformly in $v$ with explicit constants. In stage two, the samples used to estimate an effective arm are selected with the estimated periods, which were computed from the same stage-one data, so the usual independence behind confidence bounds fails. Lemmas 9–11 are therefore stated for the weak oracle, whose sample selection does not depend on the data; on the event $\Lambda$ the definitions make the oracle's run and the policy's run the same function of the noise path.

Formalization scope

Epochs are natural numbers $t\ge1$; arms are Fin K (the paper's arm $k$ is index $k-1$), and $K\ge1$. The noise is a sequence $\epsilon:\mathbb N\to\Omega\to\mathbb R$ on a probability space, independent, with Mathlib's HasSubgaussianMGF at variance proxy $\sigma^2$, plus the printed tail clause. Both algorithms are defined in full, as deterministic functions of the noise path, with canonical tie-breaking: smallest maximizer, smallest closest candidate, smallest arm index. Algorithm 1's loop runs at most $n$ passes, and $\mathrm{LCM}(\hat v_i^{-1})$ is the least common multiple of the reduced denominators of the selected frequencies. Algorithm 2 takes its period vector as an argument; the two-stage policy and the oracle are its two instances. Expected regret is an outer expectation: an integrable majorant of the regret whose integral obeys the bound. Probability bounds bound the outer measure of the bad event. Every DFT uses the absolute stage-one epochs, as in Step 8 of Algorithm 1.

Disclosed deviations: Theorem 1's constant depends on $\sigma$ and $K$ (the printed proof does not give uniformity in $K$), and $\delta=8/T$ is fixed as in the proof of Lemma 11. Lemma 6 uses $0.2328$ for the printed $0.233$; Lemma 7 and Theorem 2 use $0.6934$ for the printed $0.694$. Lemma 7 covers the nonzero present frequencies. Lemma 11 states the standing Assumption 3 and the parameters (7) as hypotheses, as its proof uses them.

The algorithm is the object of the theorem. Replacing Algorithm 1 by "any estimator that is correct with high probability", or Algorithm 2 by "any policy with the oracle's regret", would make the goal a different and much weaker statement. So would placing the constant after the horizon or the instance, since the regret is at most $T$, or using a bare Lebesgue integral of a possibly non-measurable regret.

A complete development needs discrete Fourier analysis of finite sequences, Bernstein's inequality for complex polynomials on the unit disc (Lemma 14 of the paper, from Nagy and Totik), sinc-function estimates, anytime concentration for sub-Gaussian sums, and a bookkeeping layer for the nested index sets of Algorithm 2. The concentration and polynomial-inequality parts are reusable beyond this mission. Proofs of individual lemmas, helper lemmas such as the closed form (6) of the frequency components, and alternative arguments are welcome.

Selected references

• N. Chen, C. Wang, L. Wang, Learning and Optimization with Seasonal Patterns, arXiv:2005.08088v4, 2021; Operations Research, 2025. https://arxiv.org/abs/2005.08088
• P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 397–422, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• L. Li, Y. Lu, D. Zhou, Provably Optimal Algorithms for Generalized Linear Contextual Bandits, ICML 2017. https://arxiv.org/abs/1703.00048
• B. Nagy, V. Totik, Bernstein's Inequality for Algebraic Polynomials on Circular Arcs, Constructive Approximation 37, 223–232, 2013.

Motivation

Ride-hailing platforms match riders with drivers who choose for themselves whether to work. Autonomous vehicles (AVs) would replace part of this self-scheduling labor with capital whose fleet size the platform chooses. Lian and van Ryzin study when, and under which market configuration, the cost savings of AVs reach riders. Their comparison needs a benchmark: the market served by human drivers (HVs) alone. This mission formalizes that benchmark, Proposition 1 of the paper, together with the lemmas on minimal supply and utilization that the rest of the paper uses.

Two economic forces drive the benchmark. The first is the density effect: in a denser market an idle car is closer to the next rider, so pickups are shorter and each driver spends more of the hour on paid trips. The second is the supply effect of labor: a larger fleet requires higher hourly earnings to attract the marginal driver. Proposition 1 describes how the equilibrium demand, fleet size, utilization and price respond to market size when both forces are present.

The source is the authors' 2023 SSRN working paper (abstract 3716491, version of 23 August 2023); all theorem, lemma and equation numbers refer to that version, not to the 2025 Management Science article.

Setting

A market has an ETA function $t_1(s) = a s^{-r}$ with $a > 0$ and $0 \le r < 1$, the expected pickup time when $s$ cars are open (idle); $r$ is the ETA elasticity, and $r > 0$ means a density effect. A trip lasts $t_2 > 0$ hours. Rider values for a ride hour are uniform on $[0, V]$, $V > 0$. HVs have the supply curve $w(n) = w_0 + \alpha n$, $w_0 > 0$, $\alpha \ge 0$: a fleet of $n$ drivers participates when hourly earnings are $w(n)$.

There are $I$ demand scenarios with potential demand masses $0 < m_1 < \dots < m_I$. In scenario $i$, the inverse demand at demand rate $d \in [0, m_i]$ is $p_i(d) = V(1 - d/m_i)$, and the market revenue per hour is $r_i(d) = d\,p_i(d)\,t_2$.

To serve demand $d$ with $s$ open cars, Little's law requires $s + d(t_1(s) + t_2)$ cars. The minimal supply level is

$$\underline{n}(d) = \tilde a\, d^{\frac{1}{r+1}} + t_2 d, \qquad \tilde a = r^{\frac{1}{r+1}} a^{\frac{1}{r+1}} + r^{-\frac{r}{r+1}} a^{\frac{1}{r+1}},$$

and the maximal utilization is $\bar u(d) = d t_2/\underline{n}(d)$. A demand rate $d \in [0, m_i]$ is an equilibrium when revenue covers exactly the minimal driver cost,

$$r_i(d) = w(\underline{n}(d))\,\underline{n}(d). \qquad (13)$$

It is stable (Definition 1) if there is no $\epsilon > 0$ with $r_i(d-\epsilon) < w(\underline{n}(d-\epsilon))\underline{n}(d-\epsilon)$ and $r_i(d+\epsilon) > w(\underline{n}(d+\epsilon))\underline{n}(d+\epsilon)$. The maximal stable equilibrium $d^*_{HV,i}$ is the greatest stable equilibrium; then $n^*_{HV,i} = \underline{n}(d^*_{HV,i})$, $u^*_{HV,i} = \bar u(d^*_{HV,i})$ and $p^*_{HV,i} = p_i(d^*_{HV,i})$. The loose labor market condition of scenario $i$ is

$$r_i(m_i/2) > w(\underline{n}(m_i/2))\,\underline{n}(m_i/2), \qquad (33)$$

the paper's restatement of its Assumption 2: the revenue curve meets the cost curve on its decreasing branch.

In Lean the parameters form the structure MarketParams, and the objects above are aTilde, nMin, uBar, priceFn, revenue, wage, hvCost, IsEquilibrium, IsStable, IsMaxStableEq and LooseMarket, in the namespace AVRideHail.PureHV.

Formalization targets

Goal: Proposition 1 (p. 14)

Under the standing parameter assumptions and (33) in every scenario, each scenario has a unique maximal stable equilibrium, and for the family $d^*_{HV,i}$:

$$d^*_{HV,i} > 0,\quad r_i(d^*_{HV,i}) = w(n^*_{HV,i})\, n^*_{HV,i}, \quad p^*_{HV,i} = \frac{w(n^*_{HV,i})}{u^*_{HV,i}},$$ $$d^*_{HV,i}\ \text{and}\ n^*_{HV,i}\ \text{strictly increasing in } i, \qquad u^*_{HV,i}\ \begin{cases}\text{strictly increasing in } i, & r > 0,\\ \text{constant in } i, & r = 0.\end{cases}$$

Milestones

1. Lemma 1 Item 1 (p. 38, with (26)): $\underline{n}(d)$ is the minimum of $s + d(as^{-r} + t_2)$ over $s > 0$, attained only at $s = (ra)^{1/(r+1)} d^{1/(r+1)}$.
2. Lemma 1 Item 2 (p. 38): $\underline{n}$ is a strictly increasing bijection of $[0,\infty)$, so its inverse $\bar d(n)$ exists.
3. Lemma 2 (p. 39): $\bar u$ is strictly increasing and strictly concave, $\bar u(0) = 0$ and $\bar u(d) \to 1$.
4. App. B.1.1 (p. 42): under (33), (13) has exactly one root in $[m_i/2, m_i]$, and it is the maximal stable equilibrium.
5. App. B.1.3 (p. 43): $d^*_{HV,i}$ is strictly increasing in $m_i$.
6. App. B.1.6 (pp. 45–46): $p^*_{HV,i}$ is strictly increasing in $m_i$ when $r = 0$, $\alpha > 0$, and strictly decreasing when $r > 0$, $\alpha = 0$.

Significance

Proposition 1 is the reference point for every comparison in the paper: the AV markets of Sections 5–6 (common platform, independent platforms, monopoly AV supplier) are judged by how far their prices and served demand move from $p^*_{HV,i}$ and $d^*_{HV,i}$. Its Item 3 isolates the density effect as the source of rising utilization, and the special cases of Item 5 show that the HV price can rise or fall with market size, so neither direction can be assumed in the AV analysis. Lemmas 1 and 2 are used throughout the appendices.

The paper proves these results by hand; to our knowledge none of them has a machine-checked proof. The mission produces a checked version of the benchmark and of the two technical lemmas, with every boundary case ($r = 0$, $\alpha = 0$, $d = 0$) stated explicitly.

Difficulty

The equation (13) always has the root $d = 0$, and it can have a second, unstable positive root below the stable one; the naive reading "the equilibrium is the root of (13)" therefore picks the wrong point. The work is to show that the greatest stable root exists, lies on the decreasing branch of the revenue curve, and moves monotonically with $m_i$. This requires strict monotonicity of the cost curve $w(\underline{n}(d))\underline{n}(d)$, which combines a real power $d^{1/(r+1)}$ with the linear supply curve, and continuity on $[m_i/2, m_i]$. Lemma 2 needs strict concavity of a quotient of real powers on a closed half-line including $0$, where the function is defined by its limit.

Formalization scope

All quantities are real numbers; fleet sizes and demands are continuous, as in the paper. Powers are Real.rpow. Scenarios are indexed by Fin I, 0-based. The maximal stable equilibrium is never chosen by Classical.choose: statements take a family dstar with IsMaxStableEq in each scenario.

Committed conventions and pinned hypotheses:

• $a, t_2, V, w_0 > 0$ and $0 \le r < 1$, $\alpha \ge 0$ are explicit binders. Lemma 1 Item 1 and Lemma 2 add $r > 0$, which the page leaves implicit and without which they fail.
• The loose-market condition (33) is a hypothesis of the goal in every scenario. Proposition 1's printed statement omits it, but its proof uses it, and without it a thin scenario has $d^*_{HV,i} = 0$.
• In Definition 1, $\epsilon$ ranges over $0 < \epsilon \le d$ with $d + \epsilon \le m_i$, keeping $d \pm \epsilon$ in the domain $[0, m_i]$ of $p_i$.
• At $r = 0$, Real.rpow gives $\tilde a = a$ and $\underline{n}(d) = (a + t_2)d$; $\bar u(0) = 0/0 = 0$ agrees with Lemma 2.
• "Increasing" means strictly increasing.
• The uniqueness in "unique maximal stable equilibrium" is automatic for a greatest element; the content of the first conjunct is existence.

Encoding the equilibrium as "the root of (13) in $[m_i/2, m_i]$" would make the goal follow from its own hypotheses; the goal instead quantifies over greatest stable equilibria, and that root is the conclusion of a milestone.

A complete development needs the intermediate value theorem on $[m_i/2, m_i]$, strict monotonicity and concavity facts for real powers, and limits at infinity. The minimal-supply and utilization lemmas are reusable in any model with a pickup-time function $a s^{-r}$. Proofs of any milestone are welcome, as are proofs of the remark of Item 5 in other parameter regimes.

Selected references

• Z. Lian and G. van Ryzin, Capturing the Benefits of Autonomous Vehicles in Ride-Hailing: The Role of Market Configuration, SSRN working paper 3716491, version of 23 August 2023. https://ssrn.com/abstract=3716491
• Z. Lian and G. van Ryzin, Capturing the Benefits of Autonomous Vehicles in Ride-Hailing: The Role of Market Configuration, Management Science, 2025. https://doi.org/10.1287/mnsc.2020.03112

Motivation

Probabilistic (chance) constraints require that a decision keeps a random constraint satisfied with probability at least $p$. They are the standard way to model reliability requirements in engineering design, energy networks and the control of systems driven by uncertain data, and they are increasingly imposed on infinite-dimensional decisions such as the control of a partial differential equation. Geiersbach and Henrion (arXiv:2306.03965v2) derive first-order optimality conditions for such problems. This mission formalizes the general part of their paper (§2.1): a necessary and sufficient multiplier rule for a convex objective under a Gaussian probabilistic constraint on a Banach space.

The difficulty with chance constraints is that the probability function $\varphi(u)=\mathbb P(g(u,\xi)\le0)$ is given only implicitly and is in general neither smooth nor convex. Prékopa's theory of log-concave measures (Prékopa 1995) shows that $\log\varphi$ is concave under joint convexity, and Farshbaf-Shaker, Henrion and Hömberg (2018) carried this to infinite dimensions. For Gaussian data, van Ackooij and Henrion (2014) gave gradient formulae via the spherical-radial decomposition, and Hantoute, Henrion and Pérez-Aros (2019) proved local Lipschitz continuity of $\varphi$ and an estimate of its Clarke subdifferential under a moderate growth condition. The paper combines the two lines into an optimality system.

Setting

Let $U$ be a reflexive separable Banach space with dual $U^*$, let $F:U\to\mathbb R$ be convex and Fréchet differentiable with derivative $DF(u)\in U^*$, and let $\xi$ be an $m$-dimensional centered Gaussian random vector with nondegenerate covariance matrix $\Sigma$. A constraint function $g:U\times\mathbb R^m\to\mathbb R$ is locally Lipschitzian with $g(u,\cdot)$ convex for every $u$ (Assumption 2.1). For $p\in(0,1]$ the problem is

$$\min_{u\in U}F(u)\quad\text{s.t.}\quad\varphi(u):=\mathbb P(\omega\mid g(u,\xi(\omega))\le0)\ge p. \tag{9}$$

The Clarke directional derivative of a locally Lipschitzian $f:U\to\mathbb R$ is $f^\circ(u;h)=\limsup_{u'\to u,\,t\downarrow0}(f(u'+th)-f(u'))/t$, and its Clarke subdifferential is $\partial^Cf(u)=\{x^*\in U^*\mid\langle x^*,h\rangle\le f^\circ(u;h)\ \forall h\}$. At a point $u^*$ the paper assumes $g(u^*,0)<0$ (10) and either the moderate growth condition (12) or boundedness of $M=\{z\mid g(u^*,z)\le0\}$ (11).

The radial probability function is $e(u,v)=\mu_\eta\{r\ge0\mid g(u,r\Sigma^{1/2}v)\le0\}$ for $v$ on the unit sphere $\mathbb S^{m-1}$, where $\mu_\eta$ is the chi distribution with $m$ degrees of freedom; with $\mu_\zeta$ the uniform distribution on $\mathbb S^{m-1}$, $\varphi(u)=\int_{\mathbb S^{m-1}}e(u,v)\,d\mu_\zeta(v)$ (14). Integrals of set-valued maps are taken in the sense of Aumann.

Formalization targets

Goal: Proposition 2.6, statement (21)

If $g$ is jointly convex, there is a generalized Slater point $\hat u$ with $\varphi(\hat u)>p$, and $u^*$ is feasible with (10) and either (12) or $M$ bounded, then $u^*$ is a global minimizer of (9) if and only if, for some $\lambda\ge0$,

$$DF(u^*)\in\lambda\,\partial^C\varphi(u^*),\qquad\varphi(u^*)\ge p,\qquad\lambda(\varphi(u^*)-p)=0. \tag{21}$$

Milestones

1. Theorem 2.2, Lipschitz part: $e(\cdot,v)$ is uniformly locally Lipschitzian and $\varphi$ is locally Lipschitzian around $\bar u$.
2. Prékopa's statement (p. 7): joint quasi-convexity of $g$ and a log-concave density give a log-concave $\varphi$.
3. Lemma 2.5: $\tilde\varphi=-\log\varphi+\log p$ is convex and lower semicontinuous, and (9) is equivalent to $\min\{F\mid\tilde\varphi\le0\}$ (20).
4. The convex multiplier rule for (20): $-DF(u^*)\in\lambda\partial\tilde\varphi(u^*)$, $\lambda\tilde\varphi(u^*)=0$.
5. Convex and Clarke subdifferentials agree for locally Lipschitz convex functions.
6. The chain rule $\partial^C\tilde\varphi(u^*)=-\varphi(u^*)^{-1}\partial^C\varphi(u^*)$.

Companion targets

The spherical-radial representation (14); the inclusion (15) $\partial^C\varphi(\bar u)\subseteq\int_{\mathbb S^{m-1}}\partial^C_ue(\bar u,v)\,d\mu_\zeta(v)$ with equality under (16); the radius representation (17)–(19); Lemma 2.3 (Clarke regularity of $-e(\cdot,v)$); Theorem 2.4 (equality in (15) when $M$ is bounded); and Proposition 2.6's second statement (22), where $\partial^C\varphi(u^*)$ is replaced by the spherical integral.

Significance

Statement (21) is a complete first-order characterization of optimality for a nonconvex, nonsmooth constraint in infinite dimensions: the constraint function is neither differentiable nor convex in general, yet the multiplier rule is both necessary and sufficient. The companion formula (22), with the exact subdifferential of Theorem 2.4, makes the system computable from the explicit radial function $e$; the paper's later sections evaluate it for an elliptic PDE with a random source and derive explicit optimality conditions for a probabilistic state constraint.

The results of §2.1 are proved on paper, partly by citation. None of them has a machine-checked proof in Mathlib or on Prove2Me. Formalizing them requires a Clarke calculus on Banach spaces, Prékopa-type log-concavity for Gaussian measures, the spherical-radial decomposition of a Gaussian vector, and a convex multiplier rule with an extended-valued constraint. Each of these is reusable well beyond chance constraints.

Difficulty

The direct route fails because $\varphi$ is not convex: probability functions bounded between 0 and 1 are essentially never concave, and the Clarke subdifferential of a nonconvex function supports only necessary conditions. The paper's argument needs the convex reformulation through $-\log\varphi$, which is extended-valued where $\varphi=0$. It then needs three facts that do not come for free in a Banach space: local Lipschitz continuity of $\varphi$ (which fails for merely locally Lipschitz $g$ without (12) or a bounded $M$), the identification of the convex and Clarke subdifferentials, and a chain rule through the logarithm. The companion formula (22) needs Clarke's theorem on subdifferentials of integral functionals, whose equality case requires a regularity that the radial function only has after a sign change (Lemma 2.3).

Formalization scope

$\mathbb R^m$ is EuclideanSpace ℝ (Fin m) with $m\ge1$. The law of $\xi$ is Mathlib's multivariateGaussian 0 Sigma with Sigma.PosDef, and $\Sigma^{1/2}$ is the positive semidefinite square root used there. $\varphi(u)$ is the real number $\mathbb P(\{g(u,\xi)\le0\})$. Reflexivity is surjectivity of the canonical map into the bidual. The Clarke directional derivative is the limsup over $u'\to u$, $t\downarrow0$ with denominator $t$ (the page prints $h$, a misprint). Clarke regularity includes local Lipschitz continuity. $\tilde\varphi$ is valued in EReal with $-\log0=+\infty$, and its convexity is convexity of its epigraph. A solution is a global minimizer over the feasible set. "$DF(u^*)\in\lambda S$" is encoded as "$DF(u^*)=\lambda x^*$ for some $x^*\in S$", which is unambiguous at $\lambda=0$. The ball in (12) is open. The Aumann integral uses selections whose scalar components $v\mapsto\langle\hat x^*_v,h\rangle$ are integrable.

The convex multiplier rule (milestone 4) carries one disclosed addition: the extended-valued constraint is finite and continuous near $u^*$. The paper cites [39, Theorem 3.66] without spelling out a qualification condition, and in the application this property follows from milestone 1. Prékopa's statement is formalized with $\log0=-\infty$ (the page prints $+\infty$), as the multiplicative inequality $\varphi(u)^t\varphi(w)^{1-t}\le\varphi(tu+(1-t)w)$.

A formalization that makes any of these statements trivial is ruled out: the Clarke limsup is only used with a local Lipschitz hypothesis, so the junk value of an unbounded limsup never enters; the Aumann integral demands integrable selections; the multiplier carries its sign and complementarity condition; and optimality is global, not stationarity.

Contributions are welcome at every level: a Clarke calculus on normed spaces (subdifferential nonemptiness, sum and chain rules), log-concavity of Gaussian measures and Prékopa's theorem, polar coordinates for Gaussian vectors, and a Slater-type multiplier rule for extended-valued convex constraints.

Selected references

• C. Geiersbach and R. Henrion, Optimality conditions in control problems with random state constraints in probabilistic or almost-sure form, arXiv:2306.03965v2, 2024 (Math. Oper. Res., 2025). https://arxiv.org/abs/2306.03965
• A. Hantoute, R. Henrion and P. Pérez-Aros, Subdifferential characterization of probability functions under Gaussian distribution, Math. Program. 174, 167–194, 2019. https://doi.org/10.1007/s10107-018-1237-9
• W. van Ackooij and R. Henrion, Gradient formulae for nonlinear probabilistic constraints with Gaussian and Gaussian-like distributions, SIAM J. Optim. 24(4), 1864–1889, 2014. https://doi.org/10.1137/130922689
• M. H. Farshbaf-Shaker, R. Henrion and D. Hömberg, Properties of chance constraints in infinite dimensions with an application to PDE constrained optimization, Set-Valued Var. Anal. 26, 821–841, 2018. https://doi.org/10.1007/s11228-017-0452-5
• A. Prékopa, Stochastic Programming, Kluwer, 1995. https://doi.org/10.1007/978-94-017-3087-7
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983. https://doi.org/10.1137/1.9781611971309
• J. Peypouquet, Convex Optimization in Normed Spaces: Theory, Methods and Examples, SpringerBriefs in Optimization, Springer, 2015.

Motivation

Optimal control of partial differential equations under uncertainty arises whenever a physical system is steered by a control while its sources, coefficients or loads are only known in distribution. A typical requirement is a state constraint: the state (a temperature, a concentration, a displacement) must stay below a threshold everywhere in the domain. When the source term is random, demanding this for every realization is often impossible or too conservative, and the natural relaxation is a probabilistic (chance) constraint: the state must stay below the threshold uniformly on the domain with probability at least $p$.

Probabilistic constraints are classical in operations research (Prékopa, Stochastic Programming, 1995), but in a PDE setting the constraint is an infinite family of random inequalities, one per point of the domain, and the probability function is not differentiable in general. C. Geiersbach and R. Henrion (arXiv:2306.03965v2, Math. Oper. Res. 2025) derive optimality conditions for such problems in terms of the Clarke subdifferential, building on the spherical-radial decomposition of Gaussian vectors developed by Hantoute, Henrion and Pérez-Aros (Math. Program. 2019) and van Ackooij and Henrion. This mission formalizes the PDE half of §2 of that paper: explicit formulas for the subdifferential of the probability function and the resulting optimality conditions.

Setting

Let $D\subseteq\mathbb R^d$, $d\in\{1,2,3\}$, be a nonempty, open, bounded set of class S: there are $\gamma\in(0,1)$ and $r_0>0$ with $\operatorname{meas}(B_r(x)\setminus D)\ge\gamma\operatorname{meas}(B_r(x))$ for all $x\in\partial D$ and $0<r<r_0$. For $F\in L^2(D)$ the Dirichlet problem $-\Delta y=F$ in $D$, $y=0$ on $\partial D$ has a unique weak solution in $H^1_0(D)\cap C(\bar D)$; the solution operator $A^{-1}:L^2(D)\to C(\bar D)$ is linear and continuous.

Fix $f_0,\varphi_1,\dots,\varphi_m\in L^2(D)$ and a threshold $\alpha\in\mathbb R$. The control-to-state operator is

$$S(u,z)=A^{-1}\Big(u+f_0+\sum_{i=1}^m z_i\varphi_i\Big)=P(u,z)+y_0,\qquad P(u,z)=A^{-1}u+\sum_i z_iA^{-1}\varphi_i,\ y_0=A^{-1}f_0.$$

The random vector $\xi$ on a probability space $(\Omega,\mathcal F,\mathbb P)$ is Gaussian $\mathcal N(0,\Sigma)$ with $\Sigma$ positive definite, and $y(\cdot,\omega)=S(u,\xi(\omega))$ is the random state. With $g(u,z)=\max_{x\in\bar D}[S(u,z)](x)-\alpha$ and the probability function $\varphi(u)=\mathbb P(\omega\mid g(u,\xi(\omega))\le0)$, the problem is

$$\min_{u\in L^2(D)}F(u)\quad\text{s.t.}\quad \varphi(u)=\mathbb P\big(y(x,\omega)\le\alpha\ \ \forall x\in D\big)\ge p,\tag{24}$$

with $F$ convex and Fréchet differentiable and $p\in(0,1]$.

The analysis uses the spherical-radial decomposition. Let $\mu_\zeta$ be the uniform distribution on the unit sphere $\mathbb S^{m-1}$, $\mu_\eta$ the chi distribution with $m$ degrees of freedom and density $\chi(t)=Kt^{m-1}e^{-t^2/2}$, $\Sigma^{1/2}$ the square root of $\Sigma$. The radial probability function is $e(u,v)=\mu_\eta\{r\ge0\mid g(u,r\Sigma^{1/2}v)\le0\}$ and the radius function $\rho(u,v)\in[0,\infty]$ is the supremum of that set. For $x\in\bar D$, $u_x\in L^2(D)$ is defined by $(u_x,h)_{L^2(D)}=(A^{-1}h)(x)$, and

$$M^*(\bar u,v)=\{x\in\bar D\mid[P(0,\Sigma^{1/2}v)](x)>0,\ \bar y(x)+\rho(\bar u,v)[P(0,\Sigma^{1/2}v)](x)=\alpha\},\qquad \bar y=S(\bar u,0).$$

$\partial^C$ is the Clarke subdifferential, with $L^2(D)^*$ identified with $L^2(D)$, and integrals of set-valued maps are Aumann integrals.

Formalization targets

Goal: Theorem 2.16

Assume a control $\hat u$ with $\varphi(\hat u)>p$ (41), and let $u^*$ be feasible with expected state $\tilde y=S(u^*,0)$ satisfying $\tilde y(x)<\alpha$ on $\bar D$ (42). If $u^*$ solves (24), there is $\lambda\ge0$ with

$$DF(u^*)\in-\lambda\int_{\{v\mid\rho(u^*,v)<\infty\}}\chi(\rho(u^*,v))\cdot\operatorname{clco}\Big\{\frac{u_x}{[P(0,\Sigma^{1/2}v)](x)}\ \Big|\ x\in M^*(u^*,v)\Big\}\,d\mu_\zeta(v),$$ $$\lambda\big(\mathbb P(y^*(x,\omega)\le\alpha\ \forall x\in D)-p\big)=0,$$

and these conditions are sufficient when $M^*(u^*,v)$ is a singleton for $\mu_\zeta$-a.e. $v$ with $\rho(u^*,v)<\infty$, or the set $\{z\mid g(u^*,z)\le0\}$ is bounded. The goal has no hard-coded constants; it asserts the form of the optimality system.

Milestones

In attack order: well-posedness of the state equation with the bound $\|\hat y\|_{C(\bar D)}\le C(\|z\|_2+\|u+f_0\|_{L^2(D)})$ (Lemma 1.2); measurability of the random state (Lemma 1.4); convexity and global Lipschitz continuity of $g$ (Lemma 2.9); moderate growth (Lemma 2.10); the Lipschitz and subdifferential conclusions of the general theory under (26) (Corollary 2.11); the optimality conditions (21), (22) for (24) (Corollary 2.12); $\partial^C_ue(\bar u,v)=\{0\}$ when $\rho(\bar u,v)=\infty$ (Lemma 2.13); the explicit formula $\partial^C_ue(\bar u,v)=-\chi(\rho(\bar u,v))\cdot\operatorname{clco}\{u_x/[P(0,\Sigma^{1/2}v)](x)\mid x\in M^*(\bar u,v)\}$ when $\rho(\bar u,v)<\infty$ (Lemma 2.14); and the upper estimate (40) of $\partial^C\varphi(\bar u)$ with its equality cases (Theorem 2.15).

Significance

The result turns an abstract statement — $DF(u^*)$ lies in a multiple of the Clarke subdifferential of a probability function that has no closed form — into a condition written in the problem data: Green-type functions $u_x$, the expected state, and the radius function along each direction of the sphere. This is what makes the conditions usable for checking candidate controls and for designing algorithms, and Example 2.18 of the paper computes a solution this way. The sufficiency half identifies when the nonconvex chance-constrained problem behaves like a convex one.

The paper's proofs are on paper only; to our knowledge none of these results, nor the spherical-radial decomposition, Clarke calculus in Hilbert spaces, or Aumann integrals in $L^2$, has a machine-checked proof. Formalizing Theorem 2.16 requires connecting elliptic regularity, Gaussian measure theory and nonsmooth analysis, and the milestones are reusable on their own: Lemma 1.2 is a regularity statement for the Poisson equation, and Lemmas 2.13 and 2.14 are max-function subdifferential formulas in an infinite-dimensional space.

Difficulty

The obvious route — differentiate $\varphi$ and use a Lagrange multiplier — fails because $\varphi$ is generally not differentiable even for smooth data (Example 2.17 of the paper), and because $g$ is only Lipschitz, being a maximum over $\bar D$. The general subdifferential estimate (Theorem 2.2, from Hantoute–Henrion–Pérez-Aros) needs a growth condition and only gives an inclusion, since the radial probability function is not Clarke regular; the radius function $\rho(\cdot,v)$ is an infimum over the open set where $P(0,\Sigma^{1/2}v)>0$, which is neither compact nor independent of $u$, so standard max-function formulas do not apply directly. Directions with $\rho=\infty$ require a separate limiting argument through the Mordukhovich subdifferential (Lemma 2.13). The regularity input, continuity of solutions on $\bar D$ for class-S domains (Kinderlehrer–Stampacchia 1980), is not in Mathlib.

Formalization scope

All declarations are in the namespace ChanceStateCtrl.PDE. $\mathbb R^d$ and $\mathbb R^m$ are EuclideanSpace ℝ (Fin d) and EuclideanSpace ℝ (Fin m), indices are Fin m, $L^2(D)$ is Lp ℝ 2 (volume.restrict D). Weak derivatives are the published HunterPDE.Shared.HasWeakDeriv; a weak solution is a function continuous on $\bar D$, zero on $\partial D$, in $L^2(D)$ with weak first derivatives in $L^2(D)$, satisfying the weak form against $C_c^\infty(D)$.

Standing hypotheses on every theorem: $D$ open, bounded and nonempty, $d\in\{1,2,3\}$, class S, and CompactSpace (closure D) (a consequence of boundedness). Nonemptiness of $D$ is the one added hypothesis: Lean's supremum over an empty domain is $0$, not $-\infty$, and Lemma 2.9's identification of events fails for $D=\emptyset$. $A^{-1}$ is a continuous linear map to $C(\bar D)$ together with the hypothesis that it returns the weak solution; it is never an arbitrary operator. $m\ge1$, as the uniform distribution on $\mathbb S^{m-1}$ requires. $\Sigma^{1/2}$ is the positive semidefinite root; $\|\Sigma^{1/2}\|$ is its operator norm. The Clarke directional derivative is $\limsup_{u'\to u,t\downarrow0}(f(u'+th)-f(u'))/t$ (the page's denominator $h$ is a misprint). $\rho$ takes values in $[0,\infty]$. clco is the norm closure of the convex hull. The integral in (40)/(43) is over the restriction of $\mu_\zeta$ to $\{\rho<\infty\}$, not a renormalization. A solution is a global minimizer over $\{u\mid\varphi(u)\ge p\}$; the page's "solution to (9)" refers to this instance of the abstract problem (9).

Trivializing formalizations are ruled out: every Clarke subdifferential is taken at a point where the function is locally Lipschitz (proved in Corollary 2.11 and Theorem 2.15), the state operator is tied to the PDE, the multiplier carries its sign and complementarity, Aumann selections must be scalarly integrable, and optimality is global.

Needed infrastructure: elliptic regularity in $C(\bar D)$ for class-S domains; the spherical-radial decomposition of $\mathcal N(0,\Sigma)$; Clarke calculus (chain rule, max functions) on Hilbert spaces; Clarke's theorem on subdifferentials of integral functionals. Contributions of any of these as stand-alone theorems are welcome.

Selected references

• C. Geiersbach, R. Henrion, Optimality conditions in control problems with random state constraints in probabilistic or almost-sure form, arXiv:2306.03965v2, 2024; Math. Oper. Res., 2025. https://arxiv.org/abs/2306.03965
• A. Hantoute, R. Henrion, P. Pérez-Aros, Subdifferential characterization of probability functions under Gaussian distribution, Math. Program. 174 (2019), 167–194. https://doi.org/10.1007/s10107-018-1237-9
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983; SIAM reprint 1990. https://doi.org/10.1137/1.9781611971309
• D. Kinderlehrer, G. Stampacchia, An Introduction to Variational Inequalities and Their Applications, Academic Press, 1980; SIAM reprint 2000. https://doi.org/10.1137/1.9780898719451
• A. Prékopa, Stochastic Programming, Kluwer, 1995. https://doi.org/10.1007/978-94-017-3087-7

Motivation

A correlated equilibrium (Aumann, 1974) is an equilibrium of a game with a mediator: the mediator draws a profile of recommendations from a known distribution and tells each player privately what to play. The distribution is an equilibrium if no player gains by deviating from the recommendation they receive. Correlated equilibria can give higher payoffs than Nash equilibria, they are cheaper to compute, and many adaptive learning procedures converge to them.

Mean field games describe symmetric games with many players, each of whom interacts with the others only through the empirical distribution of their states. The standard justification of a mean field model is an approximation theorem: a solution of the limit game induces approximate equilibria of the games with $N$ players, with an error that vanishes as $N\to\infty$.

Correlated solutions of discrete-time mean field games were introduced by Campi and Fischer (arXiv:2004.07936) for restricted strategies, in which both the recommendations and the deviations are Markov in the player's own state. Bonesini, Campi and Fischer (arXiv:2212.01656) keep restricted recommendations but allow the deviating player to use progressive strategies, which see the whole history of the system, together with a private randomization device. This mission formalizes their main approximation result, Theorem 6.2.

Setting

Time runs over $[\![0,T]\!]$. States lie in a finite set $\mathcal X$ and actions in a finite set $\Gamma$. Noise variables are uniform on $\mathcal Z=[0,1]$; their law is $\nu$. The set $\mathcal P(\mathcal X)$ of probability measures on $\mathcal X$ carries the metric $\mathrm{dist}(\mu,\tilde\mu)=\frac12\sum_x|\mu(x)-\tilde\mu(x)|$. A player's state moves by

$$X_{t+1}=\Psi(t,X_t,\mu_t,u_t,\xi_{t+1}),$$

where $\mu_t$ is the distribution of the other players' states, $u_t\in\Gamma$ is the player's action and $\xi_{t+1}\sim\nu$ is idiosyncratic noise. The player pays a running cost $f(t,X_t,\mu_t,u_t)$ and a terminal cost $F(X_T,\mu_T)$.

A restricted strategy $\varphi\in\mathcal R$ is a map $(t,x)\mapsto\varphi(t,x)\in\Gamma$. A progressive strategy $\varphi\in\widehat{\mathcal R}$ chooses the action at time $t$ as a Borel function of the player's state history $x^{(t)}$ and the history $m^{(t)}$ of the measure flow.

$N$-player game. The mediator draws $(\Phi_1,\dots,\Phi_N)$ from a correlated suggestion $\gamma^N$. Every player $j$ applies $\Phi_j$ to their own state path and to the empirical measure $\mu^{j,N}$ of the other $N-1$ players. A strategy modification of player $i$ replaces $\Phi_i$ by a progressive strategy $\tilde\Phi_i$. At time $t$ the component $\tilde\Phi_i(t,\cdot)$ may depend on $\Phi_i$ and on an independent uniform variable $\vartheta_t$; the set of joint laws of $(\Phi_i,\tilde\Phi_i)$ obtained this way is $\mathcal N^N_{\gamma^N_i}$. Player $i$'s expected cost is $J^N_i(\mathfrak m^N,\gamma^N,\tilde\gamma)$. The suggestion $\gamma^N$ is an $\varepsilon$-correlated equilibrium if no player gains more than $\varepsilon$ by any modification.

Mean field game. The mediator draws a pair $(\Phi,\mu)$ from $\rho\in\mathcal P(\mathcal R\times\mathcal P(\mathcal X)^{T+1})$: a restricted recommendation and a random flow of measures. The representative player may deviate through any map $w:\mathcal R\to\widehat{\mathcal R}$. The pair $\rho$ is a correlated solution if following the recommendation is optimal (Opt), and if, in that case, $\mu_t$ is the conditional law of $X_t$ given the whole flow $\mu$ (Con).

Formalization targets

Goal: Theorem 6.2

Assume (A1)–(A3), and let $\rho$ be a correlated solution with initial law $\mathfrak m_0$ satisfying (R1)–(R2). Write $\rho(d\varphi,dm)=\rho_1(d\varphi|m)\rho_2(dm)$. Then there are $\varepsilon_N\ge0$ with $\varepsilon_N\to0$ such that, for every $N\ge2$,

$$\gamma^N(C_1\times\cdots\times C_N)=\int\prod_{j=1}^N\rho_1(C_j|m)\,\rho_2(dm)$$

is an $\varepsilon_N$-correlated equilibrium with initial law $\mathfrak m_0^{\otimes N}$.

Milestones

The milestones follow the proof:

• the identification of $\gamma^N$ (Remark 6.3) and the two disintegrations (6.4), (6.5);
• convergence of the cost when nobody deviates, (6.2);
• the conditional dynamic programming principle for the value function $V_\varphi$ of a player who received the suggestion $\varphi$ (Proposition 5.5), and the equivalence of closed-loop and open-loop solutions (Proposition 5.6);
• three limits in the coupling of the deviation argument, (6.20), Claim 6.4 and (6.34);
• the lower bound for a deviating player, (6.3).

An additional milestone, (4.3), states that the cost does not depend on the realization.

Significance

The theorem justifies correlated mean field solutions as models of large games with a mediator. It applies when the mediator's recommendations and the population flow are genuinely random, and when deviators may use the full history of the system. The paper's Section 7 gives an explicit example satisfying all its hypotheses. In that example the flow of measures is non-deterministic, so the correlated solution is not a mixture of Nash solutions.

No part of this result has a machine-checked proof. Formalizing it requires:

• a complete account of correlated equilibria for dynamic games in Lean: suggestions, randomized strategy modifications, realizations;
• a conditional law of large numbers for empirical measures;
• the open-loop/closed-loop equivalence of Section 5.

These components are reusable beyond this paper.

Difficulty

When the flow $\mu$ is deterministic, the usual propagation-of-chaos argument for Nash approximation applies. Here it does not, for three reasons.

• The flow is random, and every player's recommendation is correlated with it. Convergence must therefore be proved conditionally on the flow, and the disintegrations (6.4)–(6.5) are needed for this.
• The deviating player sees the empirical measures of the others and may use extra randomness. The limit of their behaviour is not a closed-loop strategy of the mean field game. Optimality against it requires the open-loop formulation, Proposition 5.6, whose proof uses a conditional dynamic programming principle under (R1).
• The empirical measure seen by the deviator is perturbed by the deviation itself. Claim 6.4 and (6.34) control this perturbation through the continuity assumption (A2).

Formalization scope

Lean conventions:

• Spaces. $\mathcal X$ and $\Gamma$ are Fintypes with the discrete σ-algebra. $\mathcal P(\mathcal X)$ is stdSimplex ℝ X with its subspace topology and Borel σ-algebra. $\nu$ is volume on unitInterval.
• Indexing. States and flows are indexed by Fin (T+1), and actions and noises by Fin T; the noise $\xi_{t+1}$ has index $t$. Players are Fin N, and the paper's player 1 is index 0.
• Strategies. Progressive strategies are non-anticipative, measurable functions of full paths. $N$-player strategies read empirical measures of $N-1$ points, so $\widehat{\mathcal R}_N$ is finite and carries the discrete σ-algebra.
• The private coin. Condition v) of Definition 3.1 says that $\tilde\Phi_i(t,\cdot)$ is $\sigma(\Phi_i,\vartheta_t)$-measurable. It is stated literally. $\mathcal N^N_\gamma$ is defined from kernels as in (3.1).
• Realizations. A realization is a structure on a probability space Ω : Type. Conditions i)–iv) form a single product-law identity, and the dynamics hold almost surely. Completeness of the spaces and filtrations is dropped. Costs are the expected costs of realizations, and every inequality or limit between costs is required for every realization (or sequence of realizations) of each side.
• Equilibrium. In the $\varepsilon_N$-equilibrium, one $\varepsilon_N$ serves every player and every modification. All $N$-player statements assume $N\ge2$, and sequences run along $N=n+2$.
• (Con) conditions on $\sigma(\mu)$ of the whole flow, via Lean's condExp.
• (R2) is read in distribution (Remark 6.1). $\rho_1$ is any kernel that disintegrates $\rho$ along its second marginal.
• Implicit hypotheses made explicit. Joint measurability of $\Psi$ is added. (A3) is stated as Lipschitz continuity in the measure argument with one constant.
• $V_\varphi$ (Proposition 5.5) is defined through the explicit representation (5.10) of the conditional cost, a sum over flows weighted by $\mathbb P_\varphi(\mu=m'\mid\mu^{(t)}=m^{(t)})$, rather than by conditioning on events. The proposition is stated with $V_\varphi(t+1,\dots)$ on the right, as in its proof; the printed statement has $t$.
• (6.3) is stated for every sequence of modifications, which is equivalent to the paper's near-minimizing sequence. A $\liminf$ bound is written as "for every $\delta>0$, eventually".

Ruled out: none of the following is a faithful formalization of this mission:

• a deterministic flow (a Dirac $\rho_2$);
• deviations without the private coin, or restricted to $\mathcal R$;
• (Con) conditioned on $\mu^{(t)}$ only;
• an arbitrary kernel in place of the disintegration $\rho_1$.

Sorry-free checks in the workspace show that realizations of both games and the coupling exist, so the realization predicates are not vacuous.

Needed infrastructure, and welcome contributions:

• conditional laws of large numbers for empirical measures of finite-state particles;
• propagation of chaos in the sense of Kac–Sznitman;
• disintegration lemmas for finite product kernels.

Selected references

• O. Bonesini, L. Campi, M. Fischer, Correlated Equilibria for Mean Field Games with Progressive Strategies, arXiv preprint, 2022. https://arxiv.org/abs/2212.01656
• L. Campi, M. Fischer, Correlated equilibria and mean field games: a simple model, Mathematics of Operations Research 47(3):2240–2259, 2022. https://arxiv.org/abs/2004.07936
• R. J. Aumann, Subjectivity and correlation in randomized strategies, Journal of Mathematical Economics 1(1), 1974. https://doi.org/10.1016/0304-4068(74)90037-8
• A. D. Gottlieb, Markov Transitions and the Propagation of Chaos, PhD thesis, University of California, Berkeley, 1998 (the chaos theorem cited as Theorem A.1). https://arxiv.org/abs/math/0001076

Motivation

Online marketplaces (ride hailing, delivery, freelancing, retail supply chains) test changes to their product with randomized controlled trials: a fraction $\rho$ of the arriving customers is treated, the rest is kept as control, and the difference in outcomes is scaled up to estimate what would happen if everybody were treated. In a market with limited supply this estimate is biased. Treated and control customers compete for the same drivers or the same inventory, so the outcome of one group depends on the size of the other. This effect is called marketplace interference, and it makes the standard estimator overstate the effect of a treatment.

Bright, Delarue and Lobel (arXiv:2205.02274v4) model the platform's matching decision as a linear program and propose to estimate the treatment effect from the shadow prices of that program, which measure the marginal value of one more unit of demand of each type. This mission formalizes their fluid-limit comparison between the standard RCT estimator and the shadow-price estimator: in a symmetric experiment, the shadow-price estimator is never more biased.

Setting

A matching network is a finite directed graph with one demand node $u^d_i$ for each demand type $i\in[n_d]$ (only incoming arcs), one supply node $u^s_j$ for each supply type $j\in[n_s]$ (only outgoing arcs), and intermediate nodes. Each arc $(u,w)$ has a value $v_{u,w}\in\mathbb R$ per unit of flow and a capacity $k_{u,w}\ge0$. Given a demand vector $d$ and a supply vector $s$, the platform solves the LP (2)

$$\Phi(d,s)=\max\sum_{(u,w)}v_{u,w}x_{u,w}$$

over arc flows $x$ with $0\le x\le k$, flow into each $u^d_i$ at most $d_i$, flow out of each $u^s_j$ at most $s_j$, and flow balance at each intermediate node. Its dual (5) has a nonnegative price $a_i$ for each demand constraint, a price $b_j$ for each supply constraint, a price $\xi_{u,w}$ for each capacity and a free potential at each intermediate node. The price $a_i$ is the shadow price of demand type $i$.

Demand arrives at rate $\lambda\ge0$ under global control and at rate $\lambda+\beta\ge0$ under global treatment; supply arrives at rate $\pi\ge0$. An experiment treats a fraction $\rho\in(0,1)$ of demand, so the platform observes the market at the intermediate rate $\lambda+\rho\beta$. The partial-treatment value function is $\Psi(\eta)=\Phi(\lambda+\eta\beta,\pi)$ for $\eta\in[0,1]$, and the global treatment effect in the fluid limit is

$$\Delta=\Psi(1)-\Psi(0)=\Phi(\lambda+\beta,\pi)-\Phi(\lambda,\pi).$$

Two estimators are computed from the experiment state alone. The RCT estimator is $\hat\Delta_{\mathrm{RCT}}=\bar v^*\cdot\beta$, where $\bar v^*_i$ is the average value per unit of type-$i$ demand in the optimal flow of $\Phi(\lambda+\rho\beta,\pi)$, computed along the supply-to-demand paths that carry it ((9)–(10)). The shadow-price estimator is $\hat\Delta_{\mathrm{SP}}=a^\rho\cdot\beta$, where $a^\rho$ is the demand part of the optimal dual solution of $\Phi(\lambda+\rho\beta,\pi)$ ((11)). Two assumptions stand throughout: the optimal primal and dual solutions of $\Phi(\lambda+\rho\beta,\pi)$ are unique (Assumption 2), and $\beta$ is sign-consistent, $\beta\ge0$ or $\beta\le0$ componentwise (Assumption 3).

Formalization targets

Goal: Theorem 4 (p. 21)

In a symmetric experiment, $\rho=\tfrac12$,

$$\bigl|\hat\Delta_{\mathrm{SP}}-\Delta\bigr|\ \le\ \bigl|\hat\Delta_{\mathrm{RCT}}-\Delta\bigr|.$$

The statement fixes no constant other than the symmetric design. It holds for every network, every admissible rate vector and every path decomposition of the optimal flow.

Milestones

• Proposition 1 (p. 13): $\Psi$ is concave and piecewise linear with finitely many pieces on $[0,1]$.
• Theorem 2 (p. 14): if $\beta\ge0$, then $\bar v^*\cdot(\lambda+\beta)\ge\Psi(1)$ and $\bar v^*\cdot\lambda\le\Psi(0)$, with the reverse inequalities if $\beta\le0$. Consequently $|\hat\Delta_{\mathrm{RCT}}|\ge|\Delta|$.
• Proposition 6 (p. 21): $\Psi'(\eta)=a^\eta\cdot\beta$ off finitely many points, and $\Delta=\int_0^1a^\eta\cdot\beta\,d\eta$.

Companion results

• Theorem 9 (p. 27): for $\rho<\tfrac12$ and $\beta\le0$, the estimator $\hat\Delta_{\mathrm{SP+}}=(1-2\rho)\hat\Delta_{\mathrm{RCT}}+2\rho\hat\Delta_{\mathrm{SP}}$ is no more biased than $\hat\Delta_{\mathrm{RCT}}$.
• Theorem 10 (p. 27): for any $\rho$, if $(\bar v^*-a^0)\cdot\beta\ge(a^0-a^1)\cdot\beta$, then $\mathrm{Bias}_{\mathrm{SP}}\le\mathrm{Bias}_{\mathrm{RCT}}$; if $(a^0-a^1)\cdot\beta=0$, then $\mathrm{Bias}_{\mathrm{SP}}=0$.

Significance

Theorem 4 says that a platform running a 50/50 experiment never does worse by replacing the average value $\bar v^*$ with the marginal value $a^\rho$. The comparison does not depend on the network, on the capacities, or on how strongly treatment and control interfere. Theorem 2 shows that the standard estimator is biased in a known direction, and Theorem 4 shows that a different use of the same experiment data reduces that bias. The SP estimator needs only the dual solution of an LP the platform already solves.

All results of this mission are proved in the paper (Appendix C), and none has a machine-checked proof. The milestones are statements about parametric linear programs: concavity and piecewise linearity of the optimal value in the right-hand side, and the identification of its derivative with the optimal dual. These hold well beyond this paper and are absent from the platform.

Difficulty

Two steps resist the naive argument. The bound $\bar v^*\cdot\lambda\le\Psi(0)$ needs a feasible flow for the control market built from the experiment's optimal flow. Scaling the arc flow does not give one, because types share arcs. The flow has to be scaled path by path and type by type, which is why $\bar v^*$ is defined through paths. The identification $\Psi'(\eta)=a^\eta\cdot\beta$ needs LP sensitivity analysis in a parametric right-hand side: strong duality at every $\eta$, and the fact that dual optima are supergradients of $\Psi$. Because $\Psi$ has kinks, the identification holds only off finitely many points. Finally, a pointwise comparison of $a^\rho$ with $\bar v^*$ does not give Theorem 4. The proof compares integrals of $a^\eta\cdot\beta$ over $[0,\rho]$ and $[\rho,1]$, and the symmetric design is what balances the two sides.

Formalization scope

Everything is defined in MarketInterference.FluidBias. The network is a structure with arcs E and intermediate nodes I, both finite. An arc's tail is a supply node or an intermediate node, and its head is a demand node or an intermediate node, so the sink and source convention holds by construction. Demand types are Fin nd, and Lean index $i$ is the paper's type $i+1$. $\Phi$ is the supremum of the objective over the feasible set. For $d,s\ge0$ that set contains $0$ and lies in the box $[0,k]$, so the supremum is a maximum. The dual (5) is encoded arc by arc, and the four printed constraint families (5b)–(5e) are its four tail/head cases. Optimality of a primal or dual solution is stated explicitly. Strong duality is not assumed.

The estimators are the right-hand sides of (9)–(11). They are computed from an optimal primal flow, one of its path decompositions, and an optimal dual solution of the experiment LP. Neither is defined from $\Psi$ or from its derivative. A formalization that defined $\hat\Delta_{\mathrm{SP}}$ as $\Psi'(\rho)$, or $\hat\Delta_{\mathrm{RCT}}$ through $\Psi$, would trivialize the goal and is ruled out. With intermediate nodes, the decomposition of the optimal flow into paths, which (10) treats as given, is not unique. The theorems therefore hold for every decomposition. Paths are lists of distinct arcs. In (10), a type with $\lambda_i+\rho\beta_i=0$ has $\beta_i=0$, and Lean's $x/0=0$ makes its term vanish. Assumption 2 is stated as uniqueness of the whole optimal primal flow and of the whole dual solution $(a,b,m,\xi)$, as printed. Assumption 3 is a disjunction of the two sign conditions. Assumption 1 (random tie-breaking) concerns only the finite random market and is not added. The limits in Corollary 1 and Propositions 2 and 5 are not needed here: $\Delta$, $\hat\Delta_{\mathrm{RCT}}$ and $\hat\Delta_{\mathrm{SP}}$ are defined directly in the fluid model. Proposition 6's derivative is stated with HasDerivAt off a finite set, and its dual selection $\eta\mapsto a^\eta$ is arbitrary. The statements follow arXiv:2205.02274v4. Its printed slips are corrected as disclosed: the ill-defined $y^*$ of (10) is read as any path decomposition, and "$u^s_i$" on p. 9 is read as $u^d_i$.

A complete development needs LP strong duality and complementary slackness for this network LP, parametric-LP results (concavity and piecewise linearity of the optimal value along a ray, and dual optima as supergradients), path decompositions of flows, and the fundamental theorem of calculus for piecewise linear functions. The parametric-LP layer can be reused for any LP-based value function. Proofs of any milestone are welcome, as are general lemmas on network LPs.

Selected references

• I. Bright, A. Delarue, I. Lobel, Reducing Marketplace Interference Bias Via Shadow Prices, arXiv:2205.02274v4, 2024; Management Science, 2025. https://arxiv.org/abs/2205.02274
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 5 (sensitivity analysis; Theorem 5.1).
• R. Johari, H. Li, I. Liskovich, G. Y. Weintraub, Experimental Design in Two-Sided Platforms: An Analysis of Bias, Management Science, 2022 (cited by the paper as [Johari et al. 2022]). https://arxiv.org/abs/2002.11142