Optimization

Why optimize a quantile of a black box

Risk-sensitive decisions are often judged by a quantile of an outcome rather than by its mean: the 95th percentile of waiting time in a service system, the value-at-risk of a portfolio, the tail of a project's completion time. When the outcome is produced by a stochastic simulation or another black box, its distribution is unknown and only samples are available, so neither the quantile nor its gradient can be evaluated. Hu, Song and Fu (arXiv:2308.07607, Operations Research, 2025) propose a local search method for this problem that uses three samples per iteration in any dimension, and they prove that its iterates converge almost surely and at an explicit rate.

Earlier approaches estimate the quantile gradient by finite differences of order statistics, which requires sample sizes growing to infinity (Kibzun and Matveev 2012), or run a multi-timescale stochastic approximation driven by direct gradient estimators such as perturbation analysis or likelihood ratios (Hu, Peng, Zhang and Zhang 2022), which a black box does not provide. The present paper estimates the gradient from indicator differences along a simultaneous perturbation in the spirit of Spall's SPSA (1992), using a coordinate-wise variant (SDQO) as a baseline whose cost grows with the dimension $d$, and, by its own account (p. 5), gives the first convergence rate for a three-timescale stochastic approximation scheme.

Setting

For every input $\theta\in\mathbb R^d$ a black box returns a random output $Y(\theta)$ with c.d.f. $F(y;\theta)$ and density $f(y;\theta)=\partial F(y;\theta)/\partial y$. For a fixed level $\varphi\in(0,1)$ the quantile function $q(\theta)$ solves $F(q(\theta);\theta)=\varphi$, and the problem is

$$\min_{\theta\in\Theta} q(\theta),$$

where the parameter set $\Theta=\{\theta: h_j(\theta)\le0,\ j=1,\dots,m\}$ is compact and convex, with each $h_j$ continuously differentiable and $\nabla h_j\ne0$ on $\{h_j=0\}$. Under smoothness, $\nabla q(\theta)=-\nabla_\theta F(y;\theta)|_{y=q(\theta)}/f(q(\theta);\theta)$.

Algorithm SPQO keeps a quantile estimate $q_k$, a gradient estimate $D_k$ and the decision $\theta_k$. With step sizes $\alpha_k,\beta_k,\gamma_k$, perturbation sizes $c_k$, the adaptive perturbation $\bar c_k=c_k/\max\{1,\|D_k\|/\sqrt d\}$ and a random direction $\Delta_k\in\{\pm1\}^d$ with independent uniform signs,

$$\begin{aligned} q_{k+1}&=q_k+\gamma_k\big(\varphi-I\{Y(\theta_k)\le q_k\}\big),\\ D_{k+1}&=D_k+\beta_k\,\frac{-I\{Y(\theta_k+\bar c_k\Delta_k)\le q_k+\bar c_kD_k^T\Delta_k\}+I\{Y(\theta_k-\bar c_k\Delta_k)\le q_k-\bar c_kD_k^T\Delta_k\}}{2\bar c_k\Delta_k},\\ \theta_{k+1}&=\Pi_\Theta(\theta_k-\alpha_kD_k), \end{aligned}$$

with division by $\Delta_k$ taken componentwise and $\Pi_\Theta$ the Euclidean projection onto $\Theta$. The timescales are separated by $\alpha_k=o(\gamma_k)$ and $\gamma_k=o(\beta_k)$.

The analysis rests on assumptions A1–A3 (local smoothness of $F$ and a lower bound on $f$ near the iterates; Rademacher directions; step-size conditions) and, for rates, B1–B3 (two-sided bounds on $f$ between $q_k$ and $q(\theta_k)$; Lipschitz continuity of $f$ and $\nabla_\theta F$ in $y$; a lower bound $\varrho>0$ on the smallest eigenvalue of the Hessian $H(\theta)=\nabla^2q(\theta)$ along the segments $[\theta_k,\theta^*]$). Section 4 uses step sizes $\alpha_k=a/k^\alpha$, $\beta_k=b/k^\beta$, $\gamma_k=r/k^\gamma$, $c_k=c/k^\tau$ with exponents in $(0,1)$.

Formalization targets

Goal: Theorem 3 (p. 19)

Under A1–A3 and B1–B3, with the Section 4 step sizes, $q$ twice continuously differentiable and $\theta^*$ the unique equilibrium of the projected gradient ODE (25), lying in the interior of $\Theta$,

$$E\big[\|\theta_k-\theta^*\|\big]=O\Big(\frac{\alpha_k}{\gamma_k}\Big)+O\big(c_k^2\big)+O\Big(\frac{\beta_k^{1/2}}{c_k}\Big).$$

The constants are left unspecified: the goal asserts the shape of the rate, which is what the paper proves.

Milestones

1. Display (4): the quantile gradient formula.
2. Lemma 1: $\sup_kE\|D_k\|^2<\infty$ and $\sup_k\|D_k\|<\infty$ almost surely.
3. Lemma 2: the conditional bias of the simultaneous-perturbation estimator is $O(c_k^2)$ almost surely and in mean.
4. Theorem 1 (strictly convex case): $\theta_k\to\theta^*$ almost surely.
5. Lemma 3: $\sum_{i=1}^k\big[\prod_{j=i+1}^k(1-a/j^p)\big](a/i^p)w(i)=O(k^{-s})$ when $w(i)=O(i^{-s})$.
6. Lemma 4: $\sqrt{E[(q_k-q(\theta_k))^2]}=O(\alpha_k/\gamma_k)+O(\gamma_k^{1/2})$.
7. Lemma 5: $\sqrt{E\|D_k-\nabla q(\theta_k)\|^2}=O(\alpha_k/\gamma_k)+O(c_k^2)+O(\beta_k^{1/2}/c_k)$.

Significance

The rate (27) makes the trade-off among the three timescales explicit: $\alpha_k/\gamma_k$ is the cost of tracking a moving quantile, $c_k^2$ the bias of the perturbation, and $\beta_k^{1/2}/c_k$ its noise. Balancing them selects the step-size exponents, and the special cases recover the $O(1/\sqrt k)$ rate of recursive quantile estimation and Spall's SPSA rate. The intermediate results (moment bounds for a gradient tracker with adaptive perturbation, an $O(c_k^2)$ bias bound for an indicator-based SPSA estimator, and the weighted-sum estimate of Lemma 3) apply to other multi-timescale stochastic approximation schemes.

The theorem is proved in the paper; no machine-checked version exists. A formalization would check a rate argument for three coupled recursions, a setting in which hypotheses are easily lost: the paper's own proofs use a bound on $\nabla_\theta F$ that A1 does not list, and one step of the proof of Theorem 3 (display (29)) treats a conditional mean as an unconditional one. The statement survives both, as recorded in the formalization notes.

Difficulty

The three recursions are coupled in both directions. The gradient tracker $D_k$ is driven by indicator differences whose perturbation is itself scaled by $D_k$, so the $O(c_k^2)$ bias holds only once $D_k$ is known to be bounded, and boundedness must be shown with the adaptive $\bar c_k$. The natural first idea, analyzing each recursion with the slower ones frozen, gives convergence but not rates: the targets $q(\theta_k)$ and $\nabla q(\theta_k)$ move, and the error of each tracker must be bounded in mean square while the tracker it depends on is still converging. The rate also needs the almost-sure convergence of Theorem 1, which is an ODE-method argument for a projected, coupled scheme.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with $d\ge1$. The black box is a family of laws $\mu_\theta$ on $\mathbb R$, defined for every $\theta\in\mathbb R^d$ because SPQO samples outside $\Theta$. A run lives on a probability space with a general filtration; initial values are deterministic with $\theta_0\in\Theta$; the sampling model fixes the conditional law of each output given the past (and $\Delta_k$), which covers independent sampling and common random numbers. Expectations are Lebesgue integrals in $[0,\infty]$, and the bias of Lemma 2 is an explicit average over the $2^d$ sign vectors. $O(\cdot)$ is the paper's one-sided notion: a constant, depending on the instance and the run but not on $k$, times the rate, for all large $k$.

The following departures from the page are disclosed in every affected statement:

• D1 the quantile step is projected onto a closed interval $I\supseteq q(\Theta)$, the truncation the paper recommends on p. 13; $I=\mathbb R$ is the printed recursion;
• D2 step sizes use $k+1$ in place of $k$;
• D3 A1 bounds the first derivatives of $F$, which the proofs use;
• D4 only conditional marginal laws of the outputs are imposed;
• D5 $\theta_0\in\Theta$;
• D6 the Section 4 standing assumption (a unique globally asymptotically stable equilibrium $\theta^*$ of the projected ODE (25) in the interior of $\Theta$) is stated in its equivalent first-order form: $\theta^*$ is interior and is the only $\theta\in\Theta$ with $-\nabla q(\theta)$ in the normal cone of $\Theta$ at $\theta$ (the equilibria of (25); $q$ is a Lyapunov function for (25), so uniqueness gives global asymptotic stability);
• D7 joint continuity of $f$ is required on $\mathbb R\times\Theta$.

B3 is stated as the quadratic-form bound $v^TH(\theta)v\ge\varrho\|v\|^2$, equivalent to the eigenvalue bound for the symmetric Hessian. Theorem 1 is formalized only in its strictly convex clause.

Several trivializing formalizations are ruled out. Without the truncation of D1 no run satisfies A1(b) or B1, so the untruncated statement would be vacuous. No statement takes a Bochner expectation or conditional expectation of a possibly non-integrable quantity. Gradients and Hessians of $q$ are read only where $q$ is $C^2$. No $O$-constant may depend on $k$.

A complete development needs stochastic approximation tools that Mathlib lacks: Robbins–Siegmund-type supermartingale convergence, the ODE method for projected recursions, and second-moment recursions for coupled trackers. These are reusable beyond this mission. Contributions are welcome for any milestone, and Lemma 3 is pure real analysis.

Selected references

• J. Hu, M. Song, M. C. Fu, Quantile Optimization via Multiple Timescale Local Search for Black-box Functions, Operations Research, 2025; arXiv:2308.07607v1, 2023. https://arxiv.org/abs/2308.07607
• J. C. Spall, Multivariate stochastic approximation using a simultaneous perturbation gradient approximation, IEEE Transactions on Automatic Control 37(3):332–341, 1992. https://doi.org/10.1109/9.119632
• M. C. Fu, L. J. Hong, J.-Q. Hu, Conditional Monte Carlo estimation of quantile sensitivities, Management Science 55(12):2019–2027, 2009. https://doi.org/10.1287/mnsc.1090.1090
• J. Hu, Y. Peng, G. Zhang, Q. Zhang, A stochastic approximation method for simulation-based quantile optimization, INFORMS Journal on Computing 34(6):2889–2907, 2022.
• A. I. Kibzun, E. Matveev, Optimization of the quantile criterion for the convex loss function by a stochastic quasi-gradient algorithm, Annals of Operations Research 200(1):183–198, 2012.

Motivation

During the COVID-19 pandemic most U.S. payers began reimbursing a telehealth consultation at the same rate as the corresponding office visit, a policy called pay parity. Many states have since made it permanent, on the stated ground that it improves patients' access to care. In acute care (primary and urgent care) a telehealth visit sometimes cannot resolve the problem and the patient must also come to the office: a duplicate visit. Duplicate visits are paid as well, and they consume office capacity.

Çakıcı and Mills (MSOM 2024; this mission follows the SSRN working-paper version of August 19, 2024) model a provider who splits capacity between an office and a telehealth channel, and patients who choose a channel strategically. Their main finding for the setting in which demand exceeds capacity is that pay parity can make the provider's revenue-maximizing choice and the access-maximizing choice disagree: for a moderate duplicate-visit probability the provider prefers telehealth while patients are better served by an office-only practice. This mission formalizes that result and the equilibrium analysis on which it rests.

Setting

A provider serves at total rate $\mu$ and devotes the fraction $\theta\in[0,1]$ of its capacity, the telehealth commitment, to telehealth. Episodes of care arrive at rate $\lambda$. Each patient balks (value $0$), visits the office, or uses telehealth; a telehealth visit needs a duplicate office visit with probability $q$. A resolved episode is worth $V$; waiting costs $h$ per unit of sojourn time; the co-payments are $c_O$ and $c_T$; an office visit costs an extra inconvenience $\tau$. With $\pi^O,\pi^T$ the proportions choosing the office and telehealth, the expected sojourn times are

$$W^O=\frac{1}{(1-\theta)\mu-(\pi^O+q\pi^T)\lambda},\qquad W^T=\frac{1}{\theta\mu-\pi^T\lambda},$$

and the expected utilities are $V-c_O-\tau-hW^O$ (office) and $V-c_T-hW^T-q(c_O+\tau+hW^O)$ (telehealth). A patient equilibrium is a split $(\pi^B,\pi^O,\pi^T)$ in which every action used is a best response.

The paper assumes $V>h/\mu+c_O+\tau$, $c_T<c_O+\tau$, and, with $\kappa(q)=\frac{h/\mu}{V-c_T-q(c_O+\tau)}$, that $0<\kappa(q)\le 1/(1+\sqrt q)^2$. In the large-market setting some patients balk at every $\theta$. There the equilibrium is of one of four types, by region of $\theta$: balk/office on $[0,\theta^T]$, balk/office/telehealth on $(\theta^T,\theta^O)$, balk/telehealth on $[\theta^O,\bar\theta)$, all-balk on $[\bar\theta,1]$, with explicit thresholds $\theta^T,\theta^O,\bar\theta$ and explicit proportions $\pi^O(\theta),\pi^T(\theta)$. The patient access rate and the provider's revenue rate under telehealth reimbursement $r$ (office revenue $R$) are

$$A(\theta)=\bigl(\pi^O(\theta)+\pi^T(\theta)\bigr)\lambda,\qquad F(r,\theta)=\bigl(R\pi^O(\theta)+(r+Rq)\pi^T(\theta)\bigr)\lambda .$$

The commitment that maximizes telehealth usage in the balk/telehealth region is $\theta^*=\bigl(1-\kappa(q)(1-q)\sqrt q\bigr)/(1+q)$.

Formalization targets

Goal: Proposition 4 with the thresholds of Proposition 3

Fix all parameters except $\theta$ and $q$, with $R>0$. There are thresholds $0<q^\dagger<q^*<1$ such that, for every admissible $q$, pay-parity revenue $F(R,\cdot)$ is maximized over $[0,1]$ at $\theta^*$ when $q<q^*$ and at $0$ when $q>q^*$; access $A$ is maximized at $\theta^*$ when $q<q^\dagger$ and at $0$ when $q>q^\dagger$; and for $q^\dagger<q<q^*$

$$A(\theta^*)<A(0)\qquad\text{and}\qquad F(R,0)<F(R,\theta^*).$$

The thresholds are existential; no closed form is fixed, so the statement survives any later computation of them.

Milestones

In attack order: Lemma 2 (order of $\theta^T,\theta^O$); Theorems 1–3 (where each equilibrium type occurs) and Lemma 3 ($\bar\theta<1$); Theorem 4 (shape of $F$ in $\theta$); Corollaries 1–2 (the maximizers of $F$ and $A$ are $0$ or $\theta^*$); Proposition 3 (the two thresholds). Two further items are not milestones: the uniqueness of the large-market equilibrium proportions, and Proposition 5 (the reimbursement $\tilde r=R(1-q)$ aligns the two objectives).

Significance

The result is the paper's argument against pay parity in acute care: when duplicate visits are neither rare nor frequent, paying telehealth at parity induces the provider to adopt it although fewer patients are then seen. Proposition 5 shows the misalignment disappears under the less-than-parity reimbursement $R(1-q)$, which pays the same per patient seen through either channel. The thresholds $q^*$ and $q^\dagger$ are what turn this into a policy statement about measurable duplicate-visit rates.

The paper proves these results by hand. None of them has a machine-checked proof, and nothing about strategic channel choice with duplicate service exists on Prove2Me. Formalizing them checks a case analysis with four regions, two square-root closed forms and an intermediate-value argument in $q$. The formalization has already exposed two places where the printed statements need a hypothesis (see Formalization scope).

Difficulty

Each step is elementary; the difficulty is bookkeeping. The equilibrium characterization requires solving the indifference conditions in each region and choosing the root of a quadratic that gives stable queues. The shape results require continuity of $A$ and $F$ across region boundaries and concavity of a function of the form $c\theta-\sqrt{\kappa^2+(a-b\theta)^2}$. The obvious comparison of the closed-form values at $0$ and at $\theta^*$ does not suffice on its own: the closed-form value at $\theta^*$ is the revenue only when $\theta^*$ lies in the balk/telehealth region, which fails for some admissible parameters. Whether that failure matters for the maximization is the central question.

Formalization scope

All objects are real-valued closed forms in the namespace TelehealthParity.Access. The definition Setting holds the parameters (the arrival rate is lam, since λ is a Lean keyword), $\kappa,\theta^T,\theta^O,\bar\theta,\theta^*$, the region-wise proportions, $A$, $F$, the large-market condition and the predicate Admissible p q. The definition Equilibrium holds the sojourn times, utilities and the equilibrium predicate. Conventions:

• Lemma 1 (the sojourn times) is adopted as the model, as in the paper; no queueing theory is formalized.
• A channel whose queue is unstable is unavailable: it cannot be used and constrains nothing. This is how the paper discards the unstable root in the balk/telehealth region.
• "Large market" (stated verbally on p. 12) is encoded as $A(\theta)<\lambda$ for all $\theta\in[0,1]$.
• Admissible p q collects $0<q<1$, assumption (6), Lemma 2's ordering condition, the large market, and $(1-q)V-c_T>0$. The last is not printed; the proof of Lemma 2 presumes it, and Lemma 2 fails without it.
• $R>0$ is added where strictness needs it: Theorem 4, the goal, and Proposition 5. The paper allows $R\ge0$.
• Corollary 1 carries the added hypothesis "$r\le R$ or $\theta^O\le\theta^*$". As printed, for every $r>0$, it is false for some $r>R$, where the maximizer is $\theta^O$.
• "Maximized at" is IsMaxOn over $[0,1]$; "linear" is affine.

Excluded trivializations. $A$, $F$ and $\theta^*$ are closed forms, not suprema or argmaxes. The goal states the strict misalignment and the full threshold characterization, not a comparison with one point. A sorry-free sanity check shows that the hypotheses hold on an admissible instance in the misaligned range ($V=4$, $c_T=c_O=\tau=1$, $h=1/2$, $\mu=1$, $\lambda=2$, $q=1/25$).

Welcome contributions are proofs of any milestone. The real-analysis lemmas (concavity of $c\theta-\sqrt{\kappa^2+(a-b\theta)^2}$, maximization of piecewise functions that are continuous across region boundaries) are reusable beyond this mission.

Selected references

• Ö. E. Çakıcı and A. F. Mills, Telehealth in Acute Care: Pay Parity and Patient Access, Manufacturing & Service Operations Management, 2024. https://doi.org/10.1287/msom.2022.0345 (SSRN working paper, version of August 19, 2024, followed here).

Rebalancing shared vehicles at scale

Shared bike and scooter systems (micromobility) must decide, every period, how to move vehicles between stations, which depleted vehicles to recharge, and how many vehicles to source from or return to a central warehouse. Customer trips redistribute the fleet in the meantime, and some vehicles come back with a depleted battery. For a realistic network, the exact Markov decision process has a state space that grows exponentially in the number of stations, so its optimal policy cannot be computed.

Akturk, Candogan and Gupta (Management Science, 2022; preprint SSRN 4155841) group stations into finitely many types and replace the stochastic network by a deterministic mean-field model that tracks, for each type, the fraction of stations holding each number of charged vehicles and the scaled stock of depleted vehicles. They show that the mean-field model is asymptotically exact as the number of stations grows (their Theorem 3.4), and they propose a control algorithm for it whose optimality gap they bound explicitly (their Theorem 4.2). This mission formalizes the second result.

The compact mean-field model

There are $\hat e$ station types, with $n_e$ stations of type $e$ and $n = \sum_e n_e$ in total. A customer leaving a type-$e'$ station returns the vehicle at a type-$e$ station with probability $p_{e',e} = n_e w_{e',e}/\sum_{e_2} w_{e',e_2} n_{e_2}$. Demand at a type-$e$ station has a law $D^e$ on $\mathbb N_0$ with finite mean and variance; a returned vehicle is still charged with probability $q$, and costs are discounted by $\gamma \in [0, 1)$.

The extended types are $0$ (the warehouse), $1, \dots, \hat e$ (charged vehicles of each type) and $\hat e + 1, \dots, 2\hat e$ (the depleted stock of each type). Moving one vehicle from extended type $e_1$ to $e_2$ costs $c_{e_1,e_2}$, with $c_{e_1,e_2} \ge c_{e_1,e_1}/2 + c_{e_2,e_2}/2$.

An action $\hat a \in \hat A$ is a post-rebalancing distribution: fractions $\hat a_{e,d} \ge 0$ of stations of type $e$ holding $d$ vehicles, supported on $\{L^e, \dots, U^e\}$ and summing to $n_e/n$, and a scaled depleted stock $\hat a_{e,r} \in [L^{r,e}, U^{r,e}]$. A state $\breve x \in \breve X$ records the fractions $\breve x_{e,d}$ for $d \le U^e$, the depleted stock $\breve x_{e,r}$, and two aggregates $\breve x_{e,s}, \breve x_{e,u}$ of the vehicles above $U^e$, within the bounds of the paper's Appendix F.

The next state $\breve x'(\hat a)$ depends on the action only, through the transitions (F.1)–(F.5): demand removes $\min(b, D^e)$ vehicles from a station holding $b$, and an independent Poisson number $\hat R^e$ of charged vehicles arrives, with a rate (3.2) that is linear in the action's expected trips. Each period costs $\hat c_2(\breve x, \hat a) + \hat N(\hat a)$, where

• $\hat c_2$ (F.6) is a truncated Wasserstein term plus $n$ times the optimal value of a min-cost-flow problem between the extended types;
• $\hat N$ (3.4) is the expected holding and shortage cost.

The value function $\hat V(\breve x)$ is the infimum over action sequences in $\hat A$ of $\sum_{k \ge 0}\gamma^k(\hat c_2(\breve x^k, a_k) + \hat N(a_k))$, where $\breve x^0 = \breve x$ and $\breve x^{k+1} = \breve x'(a_k)$.

The algorithm. Given $\breve x$ and a transient horizon $T \ge 0$, solve the finite program (4.1): choose $\tilde a^0, \dots, \tilde a^T \in \hat A$ to minimize

$$\sum_{k=0}^{T-1}\gamma^k\big(\hat c_2(\breve x^k, \tilde a^k) + \hat N(\tilde a^k)\big) + \gamma^T\hat c_2(\breve x^T, \tilde a^T) + \frac{\gamma^T}{1-\gamma}\big(\gamma\hat c_2(\breve x^{T+1}, \tilde a^T) + \hat N(\tilde a^T)\big),$$

then play $\tilde a^0, \dots, \tilde a^{T-1}$ and repeat $\tilde a^T$ forever ((4.2)–(4.3)). Call this policy $\tilde\pi$ and its discounted cost $\hat V_{\tilde\pi}(\breve x)$.

Formalization targets

Goal: Theorem 4.2

For every $T \ge 0$, every $\breve x \in \breve X$ and every minimizer of (4.1),

$$\hat V_{\tilde\pi}(\breve x) - \hat V(\breve x) \le \frac{\gamma}{1-\gamma}\,C\,\gamma^T, \qquad\text{and, if } q = 0,\qquad \hat V_{\tilde\pi}(\breve x) - \hat V(\breve x) \le C\,\gamma^T,$$

where

$$C = 2\sum_{e=1}^{\hat e}\Big(n_e\max(c_{0,e}, c_{e,0})(U^e - L^e) + n\max(c_{0,\hat e+e}, c_{\hat e+e,0})(U^{r,e} - L^{r,e})\Big).$$

Milestones

1. (3.6): $\hat V$ satisfies the Bellman equation $\hat V(\breve x) = \min_{\hat a \in \hat A}\hat c_2(\breve x, \hat a) + \hat N(\hat a) + \gamma\hat V(\breve x'(\hat a))$ on $\breve X$, with the minimum attained.
2. §4.1, p. 26: the cost of $\tilde\pi$ equals the optimal value of (4.1).
3. Lemma H.7: $\hat c_2(\breve x, \hat a) \le \hat c_2(\breve x, \hat z) + \hat c_2(\hat z, \hat a)$, an action read as a state.
4. Lemma H.9: $\hat c_2(\hat a^1, \hat a^2) \le C/2$ for all $\hat a^1, \hat a^2 \in \hat A$.
5. Lemma H.8: under the triangle inequality, there is an optimal policy with $\hat\pi^*(\hat\pi^*(\breve x)) = \hat\pi^*(\breve x)$.
6. Proposition H.3: for $q = 0$, the dynamic program has a fixed point $\breve x^f = \breve x'(\hat a^f)$ with $\hat a^f$ optimal at $\breve x^f$ (Definition H.1).

Significance

Theorem 4.2 makes the algorithm a certified approximation scheme. It turns an infinite-horizon problem into a finite program of $T + 1$ actions, and the loss from doing so decays geometrically in $T$, uniformly over the initial state, with a constant that depends only on the rebalancing costs and the action bounds. For $q = 0$ the transitions are affine, the program (4.1) becomes a linear program (the paper's Appendix G), and the sharper bound $C\gamma^T$ applies.

The result is proved in the paper (Appendix H), but not formalized anywhere. A formal proof combines a triangle inequality for an LP-valued cost, a dynamic-programming principle with attainment on a compact action set, and a fixed-point argument for a convex deterministic dynamic program. The paper has several small printed slips on this path (for example, Proposition H.10 states the $q = 0$ constant without the factor $2$ that its proof produces); the formal statements fix the corrected reading.

Difficulty

The bound is not a truncation estimate. Cutting the discounted sum at $T$ gives a gap proportional to the per-period cost, not to $C$. The comparison has to be made against an optimal action sequence, whose first $T + 1$ actions are feasible for (4.1). After period $T$, the optimal sequence and $\tilde\pi$ diverge, and the cost of that divergence must be controlled by the cost of moving between two actions, which requires:

• the triangle inequality for $\hat c_2$, whose flow component is the value of a linear program, not a closed form;
• the fact that, once rebalanced to an optimal action, staying there is optimal (Lemma H.8);
• the bound of Lemma H.9 on the cost between any two feasible actions.

The $q = 0$ bound needs, in addition, a steady state of the controlled system (Proposition H.3), which rests on a fixed-point theorem for convex deterministic dynamic programs (Flynn 1979). The Bellman equation itself is not free: with $\hat V$ defined as an infimum over sequences, attainment of the minimum needs continuity of $\hat c_2$, $\hat N$, the transition and $\hat V$ on the compact action set.

Formalization scope

Types are Fin ê (0-based) and the extended types are Fin (2ê+1) with chg e and dep e for the paper's $e$ and $\hat e + e$. Level vectors are functions $\mathbb N \to \mathbb R$ that vanish outside their support. $\mathbb P[b - \min(b, D^e) + \hat R^e = d]$ is the convolution of the demand law with the Poisson law, so $D^e$ and $\hat R^e$ are independent, as the paper presupposes. $\hat V$ is the infimum over the subtype of $\hat A$-valued sequences (p. 18 and Proposition F.3), and (3.6) is posed as a milestone rather than used as a definition. $\breve X$ is formalized as printed on p. A-22. The policy cost is the discounted cost of $\tilde a^0, \dots, \tilde a^{T-1}, \tilde a^T, \tilde a^T, \dots$, where $\tilde a$ is a hypothesis-given minimizer of (4.1). Everything is time-homogeneous and stated at $t = 0$.

Standing assumptions, as one predicate on the model: $0 \le \gamma < 1$, $0 \le q \le 1$, $n_e \ge 1$, $w \ge 0$ with positive normalizers, $L^e \le U^e$, $0 \le L^{r,e} \le U^{r,e}$, finite second moments of $D^e$, the cost assumption $c_{e_1,e_2} \ge c_{e_1,e_1}/2 + c_{e_2,e_2}/2$, $c_{0,0} = 0$, $c_{\hat e+e,\hat e+e} = 0$. Two additions are disclosed: $\gamma \ge 0$, and $c_{e_1,e_2} \ge 0$, without which Lemma H.9 and the goal fail (the right-hand side could be negative).

Trivializing formalizations are excluded: $\hat V$ ranges only over $\hat A$-valued sequences, the policy is tied to a minimizer of (4.1) and to no other objective, the flow value is an infimum over a nonempty set bounded below (warehouse routing is always feasible), and $C$ uses $c_{0,e}$, $c_{e,0}$, $c_{0,\hat e+e}$, $c_{\hat e+e,0}$ with the paper's indexing and the factor $2$.

Two general objects are separate definitions on which the model is built: a discounted deterministic dynamic program (trajectory, discounted cost, value as an infimum over admissible action sequences) and the uncapacitated transshipment LP on a complete digraph with free nodes. Both are reusable beyond this mission. A complete development further needs Poisson tail sums, subadditivity of the flow value, compactness of $\hat A$, a dynamic-programming principle and a fixed-point theorem for convex deterministic programs. Proofs of any milestone, and alternative arguments for the $q = 0$ fixed point, are welcome.

Selected references

• D. Akturk, O. Candogan, V. Gupta, Managing Resources for Shared Micromobility: Approximate Optimality in Large-Scale Systems, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.02023 (read as SSRN 4155841, version of 2024-05-22: https://ssrn.com/abstract=4155841)
• J. Flynn, Steady state policies for deterministic dynamic programs, SIAM Journal on Applied Mathematics 37(1):128–147, 1979 (as cited in the paper's appendix references).

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1, explicit form

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

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

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

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

and in expectation

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

Retail chains increasingly run their physical stores and online channels as one network. A customer who walks into a store and finds nothing she wants can be shown products stocked in other stores of the chain, to be shipped or picked up later. This raises a basic assortment question: when every store can point its customers to the rest of the network, should the stores still carry the assortment each would choose on its own, or should they coordinate?

Liu, Chen, Liu and Wan (MSOM 2025, DOI 10.1287/msom.2024.0761) compare two ways of showing the network's products. Under simultaneous recommendation (SMR), a customer sees her store's products and the other stores' products at the same time. Under sequential recommendation (SQR), she sees the other stores' products only after declining everything in her own store. This mission formalizes the paper's result for SMR, Theorem 1, together with the lemmas of its proof and two consequences (Theorem 5(a) and Proposition 2). The single-store model it builds on is the multinomial logit (MNL) assortment problem of Talluri and van Ryzin (2004).

Setting

A seller operates $m$ stores and sells $n$ products, indexed $1,\dots,n$, with revenues $r_1>r_2>\dots>r_n>0$. Product $k$ has attraction value $v_k=\exp(u_k)>0$, where $u_k$ is its utility; the no-purchase option has attraction value $1$. A fraction $\lambda_i\ge0$ of customers first visits store $i$, and $\sum_i\lambda_i=1$.

An assortment profile $\mathbf S=(S_1,\dots,S_m)$ lists the set $S_i\subseteq\mathcal N=\{1,\dots,n\}$ offered by each store. Write $\bar S=S_1\cup\dots\cup S_m$ for the products offered somewhere. A customer of store $i$ who buys product $k$ from store $j$ suffers a utility discount $c_{ij}^k\ge0$, with $c_{ii}^k=0$. She buys from the cheapest store that offers $k$, so the effective discount is $c_i^k(\mathbf S)=\min\{c_{ij}^k: k\in S_j\}$, and $c_i^k(\mathbf S)=\infty$ if no store offers $k$.

Under SMR, the customer of store $i$ chooses product $k$ with the MNL probability

$$p^M_{ik}(\mathbf S)=\begin{cases}\dfrac{v_k}{D_i(\mathbf S)},&k\in S_i,\\[2mm]\dfrac{v_ke^{-c_i^k(\mathbf S)}}{D_i(\mathbf S)},&k\in\bar S\setminus S_i,\\[2mm]0,&\text{otherwise},\end{cases}\qquad D_i(\mathbf S)=1+\sum_{l\in S_i}v_l+\sum_{l\in\bar S\setminus S_i}v_le^{-c_i^l(\mathbf S)}.$$

The seller's problem is

$$\max_{\mathbf S}\ R_M(\mathbf S)=\sum_{i=1}^m\lambda_i\sum_{k=1}^nr_k\,p^M_{ik}(\mathbf S).\tag{SMR}$$

The single-store problem is

$$R^*=\max_{S\subseteq\mathcal N}\frac{\sum_{k\in S}r_kv_k}{1+\sum_{k\in S}v_k}.\tag{3}$$

An assortment is revenue-ordered if it is $\{1,\dots,k\}$ for some $k\in[n]$. The paper writes $\tilde S$ for the smallest revenue-ordered optimal solution of (3).

Formalization targets

Goal: Theorem 1

$$R_M(\mathbf S)\ \le\ R_M(\tilde S,\tilde S,\dots,\tilde S)\qquad\text{for every profile }\mathbf S.$$

Offering the single-store optimal assortment in every store is optimal under SMR. The goal asserts optimality, not uniqueness: with ties, other profiles can be optimal too.

Milestones

1. Existence of $\tilde S$ (p. 11): some revenue-ordered assortment is optimal for (3).
2. Proposition A.1: in the two-store problem (A.1), store 1 offers products 1 through some threshold. A product belongs to the smallest revenue-ordered optimum if and only if its revenue exceeds the optimal value.
3. Proposition A.2: the optimal value of (A.1) does not decrease when the discounts increase.
4. The store-wise reduction: store $i$'s SMR revenue equals the objective of problem (A.2), the single-store problem with the other stores' products as discounted alternatives.
5. The store-wise bound: every store earns at most $R^*$ under any profile, and exactly $R^*$ under $(\tilde S,\dots,\tilde S)$.

Companions

• Theorem 5(a): $\max_{\mathbf S}R_Q(\mathbf S)\ge\max_{\mathbf S}R_M(\mathbf S)$, where $R_Q$ is the SQR revenue built from the sequential choice probabilities (2).
• Proposition 2: when store $m$ is an online channel with $S_m=\mathcal N$, and $c_{im}^k=c^k>0$ for every physical store $i$, some optimal profile among those with $S_m=\mathcal N$ offers one and the same revenue-ordered assortment $\hat S\supseteq\tilde S$ in every physical store.

Significance

Theorem 1 says that under simultaneous recommendation the network adds nothing for the seller: the revenue of independently run stores, $R^*$, is the best achievable. The paper calls this revenue the benchmark. Every later comparison is made against it. The sequential strategy beats it (Theorem 5(a)), and the paper's structural results on SQR and its ½-approximation are phrased relative to $\tilde S$ and $R^*$. Proposition 2 shows that adding an online channel enlarges the optimal assortments of the physical stores.

The results are proved in the paper, partly in an Additional Supplement. As far as is known, none of them has a machine-checked proof. The mission produces a reusable Lean model of multi-store MNL choice with cross-store discounts, the SQR choice probabilities, and checked proofs of the single-store threshold structure with discounted outside products (Propositions A.1 and A.2).

Difficulty

A store's SMR revenue depends on every other store's assortment, through both the denominator $D_i(\mathbf S)$ and the products of $\bar S\setminus S_i$. The objective does not separate across stores, so the obvious idea of optimizing each store on its own does not directly apply. Products of other stores enter at reduced weight $e^{-c_i^k}$, so the standard MNL result for (3) does not cover (A.1).

Proposition A.1's exchange argument has two cases, depending on whether the added product is already available elsewhere. In the second case the gain is weighted by $1-e^{-c^k}$, which vanishes when $c^k=0$. Proposition A.2 compares optimal values across two discount vectors whose optimal assortments differ.

Formalization scope

Products are Fin n (the paper's product $k$ is index $k-1$), stores are Fin m, and a profile is a function Fin m → Finset (Fin n). The attraction values $v_k>0$ are the primitive parameters. The discount factor $e^{-c_i^k(\mathbf S)}$ is the largest $e^{-c_{ij}^k}$ over the offering stores, and $0$ when none offers $k$. In (A.1) the discounts are encoded by the factors $\beta_k=e^{-c^k}\in[0,1]$, with $\beta_k=0$ for $c^k=\infty$. $\tilde S$ and $S^*_M(\mathbf c)$ are predicates: revenue-ordered (hence nonempty), optimal, and of least cardinality among revenue-ordered optima. "Optimal" means a global maximizer, and comparisons of optimal values are written as "for every $T$ there is an $S$ with $f(T)\le g(S)$", with no maximum operator. The SMR and SQR objectives are written from the choice probabilities (1) and (2), exactly as the paper writes them.

The standing assumptions are explicit hypotheses: $\lambda_i\ge0$, $\sum_i\lambda_i=1$, $r$ strictly decreasing, $v_k>0$, $c_{ij}^k\ge0$, $c_{ii}^k=0$. Two hypotheses are pinned. The first is $r_k>0$: revenues are prices, which the paper uses but never states as a sign condition. The second applies only to the second part of Proposition A.1: $c^k>0$, because its "if and only if" fails at $c^k=0$; the existence of a revenue-ordered optimum is stated for every $\mathbf c\ge0$. The goal and Proposition A.2 keep $c_{ij}^k\ge0$, so zero cross-store discounts are allowed. The Gumbel derivation of (2) (Proposition 1, cited from Gao et al. 2021) is not formalized; (1) and (2) are the model.

The hypothesis on $\tilde S$ is satisfiable: its existence is the first milestone. A statement that assumed some optimal profile, or that defined $R^*$ through a junk-valued supremum, would be trivial or vacuous, and the formalization avoids both. Contributions are welcome on any milestone. Propositions A.1 and A.2 are reusable for other multi-store and omnichannel MNL problems.

Selected references

• Y. Liu, X. A. Chen, Y. Liu, Z. Wan, Simultaneous vs. Sequential: Optimal Assortment Recommendation in Multistore Retailing, Manufacturing & Service Operations Management, 2025. https://doi.org/10.1287/msom.2024.0761 (cited from the authors' manuscript of 2024-09-17 with its Online and Additional Supplements)
• K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Gao, Y. Ma, N. Chen, G. Gallego, A. Li, P. Rusmevichientong, H. Topaloglu, Assortment Optimization and Pricing Under the Multinomial Logit Model with Impatient Customers: Sequential Recommendation and Selection, Operations Research 69(5):1509–1532, 2021.

Motivation

Optimal control of partial differential equations under uncertainty asks for a single deterministic control $u$ that performs well when the data of the PDE are random. When a constraint on the state must hold, the modeller has to decide how strictly: with high probability (a probabilistic constraint), for almost every realization (an almost-sure constraint), or for every realization in a support set (a robust constraint). C. Geiersbach and R. Henrion (arXiv:2306.03965v2, Math. Oper. Res. 2025) derive optimality conditions for all three forms on a common model problem. This mission covers §3.1 of that paper, the almost-sure case.

Almost-sure state constraints are the natural model when a bound (a temperature, a stress, a concentration) must never be violated, and they appear throughout risk-averse PDE-constrained optimization (Geiersbach and Wollner, SIAM J. Optim. 2021; Geiersbach and Hintermüller, ESAIM:COCV 2022). Their difficulty is functional-analytic: the constraint lives in $L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D))$, a space whose dual is not a function space, so Lagrange multipliers are a priori only finitely additive objects.

Setting

Let $D\subseteq\mathbb R^d$, $d\in\{1,2,3\}$, be open, bounded and 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 $y\in H^1_0(D)\cap\mathcal C(\bar D)$; the solution map is a continuous linear operator $A^{-1}:L^2(D)\to\mathcal C(\bar D)$.

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space and $\tilde f\in L^\infty_{\mathbb P}(\Omega,L^2(D))$ a random source. For a control $u\in L^2(D)$ the random state $y(\cdot,\omega)$ solves $-\Delta y(\cdot,\omega)=u+\tilde f(\cdot,\omega)$, $y(\cdot,\omega)=0$ on $\partial D$. With $\mathcal B$ the embedding of $L^2(D)$ into constant elements of $L^\infty_{\mathbb P}(\Omega,L^2(D))$ and $[\mathcal A^{-1}y](\omega)=A^{-1}y(\cdot,\omega)$, the control-to-state operator is $\mathcal S(u)=\mathcal A^{-1}(\mathcal Bu+\tilde f)$ and the constraint map is $\mathcal G(u)=\mathcal S(u)-\boldsymbol\alpha$, where $\boldsymbol\alpha$ is the constant function $\alpha\in\mathbb R$. The problem is

$$\min_{u\in L^2(D)}F(u)\quad\text{s.t.}\quad\mathcal G(u)\in\mathcal K,\qquad(51)$$

with the cone $\mathcal K=\{y\in L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D)):y(x,\omega)\le0\text{ on }\bar D,\ \mathbb P\text{-a.s.}\}$ and its polar $\mathcal K^-\subseteq(L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D)))^*$. The cost $F$ is convex and continuously Fréchet differentiable.

For a separable Banach space $X$, a functional $v\in(L^\infty_{\mathbb P}(\Omega,X))^*$ is absolutely continuous if $\langle v,x\rangle=\int_\Omega\langle x^*(\omega),x(\omega)\rangle\,d\mathbb P$ for a weakly measurable $x^*:\Omega\to X^*$ with $\int\|x^*\|\,d\mathbb P<\infty$ (the set $\Lambda_1(X^*)$ of such $x^*$), and singular if it vanishes on every $x$ that vanishes on some $F_n$, for a decreasing sequence of events with $\mathbb P(F_n)\to0$ (the set $\Lambda_\circ(X^*)$).

Formalization targets

Goal: Theorem 3.10

Under the constraint qualification $0\in\operatorname{int}\{\mathcal G(L^2(D))-\mathcal K\}$, $u^*$ solves (51) if and only if there are $\lambda\in\Lambda_1(\mathcal C(\bar D)^*)$, $\lambda^\circ\in\Lambda_\circ(\mathcal C(\bar D)^*)$ and a state $y^*$ with

$$DF(u^*)+\mathbb E[A^{-*}\lambda]+\mathcal B^*\mathcal A^{-*}\lambda^\circ=0,\qquad Ay^*(\cdot,\omega)=u^*+\tilde f(\cdot,\omega),$$ $$y^*(\cdot,\omega)\le\alpha,\quad\lambda(\cdot,\omega)\ge0,\quad\langle\lambda(\cdot,\omega),y^*(\cdot,\omega)-\boldsymbol\alpha\rangle=0\ \ \mathbb P\text{-a.s.},\qquad\lambda^\circ\in\mathcal K^-,\quad\langle\lambda^\circ,y^*-\boldsymbol\alpha\rangle=0.$$

Milestones

1. Lemma 3.6: the random state exists, is a.s. unique, lies in $L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D))$, and obeys the bound (52).
2. Lemma 3.7: the abstract KKT system (53) with a multiplier $\lambda^*\in(L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D)))^*$.
3. Theorem 3.9 (Ioffe–Levin): every $v^*\in(L^\infty_{\mathbb P}(\Omega,X))^*$ splits uniquely as $v^a+v^\circ$ with $\|v^*\|=\|v^a\|+\|v^\circ\|$.
4. The splitting $\langle\lambda^*,\mathcal A^{-1}\mathcal Bh\rangle=\mathbb E[\langle\lambda,A^{-1}h\rangle]+\langle\lambda^\circ,\mathcal A^{-1}\mathcal Bh\rangle$.
5. (57): $\lambda^*\in\mathcal K^-$ passes to both parts.
6. (59) and pointwise complementarity: $\lambda(\omega)\ge0$ and $\langle\lambda(\omega),y^*(\omega)-\boldsymbol\alpha\rangle=0$ almost surely.

Significance

The result. Lemma 3.7 gives a multiplier in the dual of $L^\infty$, which cannot be evaluated scenario by scenario. Theorem 3.10 shows that, for this problem, the multiplier consists of an honest random variable $\lambda(\omega)\in\mathcal C(\bar D)^*$ (a random signed measure on $\bar D$) satisfying sign and complementarity conditions for almost every realization, plus a singular remainder. This is the form needed to write adjoint equations and to design discretizations and algorithms (Proposition 3.12 of the paper). As Remark 3.11 notes, the derivation does not require reflexivity of the state space, unlike earlier work on $L^\infty_{\mathbb P}(\Omega,X)$-constraints.

Formalizing it. The paper's argument is complete, but it rests on two cited results: the regularity theory behind Lemma 1.2/3.6 (Stampacchia-type continuity of weak solutions on class-S domains, Kinderlehrer–Stampacchia) and the Ioffe–Levin decomposition of $(L^\infty_{\mathbb P}(\Omega,X))^*$ (Ioffe–Levin, Appendix 1, Theorem 3, and Levin 1974). Neither is in Mathlib. A formal development produces machine-checked versions of both, of a Robinson-type KKT theorem in Banach spaces, and of the multiplier refinement itself. None of these results has a machine-checked proof as far as the platform's catalog shows.

Difficulty

The obvious route is to apply the Riesz representation pointwise in $\omega$. It fails: $(L^\infty_{\mathbb P}(\Omega,\mathcal C(\bar D)))^*$ contains purely finitely additive functionals that are not given by any integrand, so $\lambda^*$ has no density in general. The decomposition theorem isolates them, and the proof of Theorem 3.10 must then show that the sign condition $\lambda^*\in\mathcal K^-$ and the complementarity condition pass to each part separately. The step from $\mathbb E[\langle\lambda,y\rangle]\le0$ for all $y\in\mathcal K$ to "$\lambda(\omega)\ge0$ for almost every $\omega$, simultaneously for all nonnegative test functions" requires the separability of $\mathcal C(\bar D)$; a version with a null set depending on the test function is weaker and is not the statement. Lemma 3.6 needs $\mathcal C(\bar D)$-regularity of weak solutions, which is where class S and $d\le3$ enter.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d). $L^2(D)$ is Lp ℝ 2 (volume.restrict D) and $L^\infty_{\mathbb P}(\Omega,X)$ is Lp X ⊤ P; their elements are a.e. classes, so every pointwise statement in $\omega$ is stated $\mathbb P$-a.s. $\mathcal C(\bar D)$ is C(closure D, ℝ) with [CompactSpace (closure D)] as an instance argument (implied by boundedness). Weak derivatives use the published HunterPDE.Shared.HasWeakDeriv; a weak solution in $H^1_0(D)\cap\mathcal C(\bar D)$ is encoded as continuity on $\bar D$, zero boundary values, $L^2$ weak gradient and the weak form. $A^{-1}$ is a hypothesis: a continuous linear map $L^2(D)\to\mathcal C(\bar D)$ whose values are weak solutions. "$\le0$ a.e. in $D$" for a function continuous on $\bar D$ is read as "$\le0$ on $\bar D$"; "$\lambda(\cdot,\omega)\ge0$" as positivity of the functional. "Solution of (51)" is a global minimizer. (56a) is stated applied to every direction $h$.

Trivializing formalizations are ruled out: the state operator is tied to the PDE, not an arbitrary bounded operator; the multipliers carry their sign and complementarity conditions; absolutely continuous functionals require a weakly measurable, integrable density; singular functionals are concentrated on a decreasing sequence of events of vanishing probability, not merely "not absolutely continuous"; optimality is global.

Needed infrastructure: Lax–Milgram on $H^1_0(D)$ and continuity of weak solutions (Lemma 3.6); a KKT theorem under Robinson's constraint qualification (Lemma 3.7); the Yosida–Hewitt decomposition for finitely additive measures and a weak*-measurable representation of $L^1(\Omega,X)^*$ (Theorem 3.9). The decomposition theorem is reusable far beyond this mission; contributions toward any of these 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. D. Ioffe, V. L. Levin, Subdifferentials of convex functions, Trudy Moskov. Mat. Obshch. 26, 3–73, 1972 (Appendix 1, Theorem 3).
• V. L. Levin, The Lebesgue decomposition for functionals on the vector-function space $L^\infty_X$, Funct. Anal. Appl. 8(4), 314–317, 1974. https://doi.org/10.1007/bf01075488
• K. Yosida, E. Hewitt, Finitely additive measures, Trans. Amer. Math. Soc. 72, 1952. https://doi.org/10.1090/S0002-9947-1952-0045194-X
• J. F. Bonnans, A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
• C. Geiersbach, W. Wollner, Optimality conditions for convex stochastic optimization problems in Banach spaces with almost sure state constraints, SIAM J. Optim. 31(4), 2455–2480, 2021.
• C. Geiersbach, M. Hintermüller, Optimality conditions and Moreau–Yosida regularization for almost sure state constraints, ESAIM: COCV 28, Paper No. 80, 2022. https://doi.org/10.1051/cocv/2022070
• D. Kinderlehrer, G. Stampacchia, An Introduction to Variational Inequalities and Their Applications, Academic Press, 1980 (Chapter II, Appendices B and C). https://doi.org/10.1137/1.9780898719451