Convex Optimization

Motivation

Distributed energy resources (DERs) — rooftop solar, home batteries, electric vehicles — turn electricity consumers into prosumers who can both buy and sell power. Their individual capacities are far too small to bid in a wholesale electricity market directly, so regulators have opened these markets to DER aggregators, intermediaries that pool many small resources and trade on their behalf (FERC Order 2222, 2020). An aggregator is a monopolist toward the prosumers it serves, and a profit-seeking monopolist between a market and its suppliers ordinarily distorts quantities: with a single unit price, the aggregator buys less than the efficient amount, and social welfare falls (Alshehri, Ndrio, Bose, Başar 2019, 2020).

Gao, Alshehri and Birge ask whether this loss can be avoided without regulating the aggregator. Their answer is that it can, provided the aggregator uses two-part pricing: a participation fee plus a per-unit price. This mission formalizes that efficiency result.

Setting

A power network has a finite set $K$ of nodes and a finite set $L$ of transmission lines. The ISO chooses nodal net injections $h\in\mathbb R^K$; the DC approximation of the AC network gives a matrix $B$ and line capacities $f$, and the network constraints are (5b): $\mathbf 1^\top h=0$ and $Bh\le f$.

A finite set $I$ of prosumers sits at the nodes. Prosumer $i$ owns a DER capacity $C_i\ge0$ and has a utility of consumption $u_i$ on $[0,Z]$, $Z>C_i$. Assumption 1: $u_i$ is increasing, strictly concave and continuous on $[0,Z]$, differentiable on $(0,Z)$, with $u_i'(z)\to\infty$ as $z\to0^+$ and $u_i'(z)\to0$ as $z\to Z^-$. A finite set $J$ of conventional generators sits at the nodes; generator $j$ produces $y_j\in[\underline y_j,\overline y_j]$ at cost $c_j(y_j)$. Assumption 2: $c_j$ is increasing, strictly convex and continuous on its interval, differentiable inside, with $c_j'\to0$ at the lower end and $c_j'\to\infty$ at the upper end.

Benchmark (direct participation). Prosumer $i$ sells $x_i$ and buys $d_i$ directly in the market at the locational price; only the net sale $z_i=x_i-d_i$ matters. Writing $X^k$, $D^k$, $Y^k$ for the nodal totals of sales, purchases and generation, the ISO solves the economic dispatch problem (9):

$$\max\ \mathcal W_B=\sum_i u_i(C_i-z_i)-\sum_j c_j(y_j)\quad\text{s.t. (5a) } h=D-Y-X,\ \text{(5b)},\ \text{(6) } C-Z\le z\le C,\ \underline y\le y\le\overline y .$$

The wholesale prices $\lambda\in\mathbb R^K$ are the optimal Lagrange multipliers of the nodal balance constraints (5a).

Unregulated aggregation. Each prosumer sells only to the aggregator $\mathcal A$, which offers her a fee $P_i$ and a unit price $p_i$. At wholesale price $\lambda$ she maximizes the payoff (10), $p_ix_i-P_i+u_i(d_i+C_i-x_i)-\lambda d_i$ if she sells $x_i>0$ and $u_i(d_i+C_i)-\lambda d_i$ otherwise, over $x_i\in[0,C_i]$, $d_i\in[0,Z-C_i+x_i]$ (11). The aggregator earns (13) $P_i\mathbf 1\{x_i>0\}+(\lambda-p_i)x_i$ and chooses nonnegative offers anticipating the responses: a Stackelberg game $\mathcal G(\lambda)$ (Definition 1). The ISO now dispatches $x$ and $d$ separately, solving (21): maximize $\mathcal W_A=\sum_i u_i(d_i+C_i-x_i)-\sum_j c_j(y_j)$ subject to (5a), (5b) and (18) $0\le x\le C$, $0\le d\le Z-C+x$, $\underline y\le y\le\overline y$; its wholesale prices are again the multipliers of (5a).

Formalization targets

Goal: Theorem 1 (p. 14)

Under Assumptions 1–3 (Assumption 3: (9) is feasible), with $(h^*,z^*,y^*)$ the optimal solution of (9),

$$\mathcal W_A^*=\mathcal W_B^*,$$

every optimal solution of (21) has $x-d=z^*$, $y=y^*$, $h=h^*$, the split $([z^*]^+,[-z^*]^+)$ is optimal for (21), and a price vector is a multiplier of (5a) for (21) if and only if it is one for (9).

Milestones

1. Lemmas 1 and 2 (pp. 5–6): a price-taking prosumer's problem (1) and generator's problem (3) have unique optima, characterized by $u'(C-z^*)=\lambda$ (2) and $c'(y^*)=\lambda$ (4).
2. Proposition 1 (p. 8): (9) has a unique optimum, and at every multiplier vector of (5a) it is a competitive equilibrium.
3. Lemma 3 (p. 10): the prosumer's optimal response to a two-part offer, in terms of $u'(z_1)=\lambda$, $u'(z_2)=p$.
4. Lemma 4 (p. 11): the aggregator's optimal offer is

$$p^*=\lambda,\qquad P^*=\lambda(C-z_1)+u(z_1)-u(C).$$

5. Proposition 2 (p. 12): these offers form a Stackelberg equilibrium of $\mathcal G(\lambda)$.
6. Proposition 3 (p. 14): (21) has an optimum consistent with Lemmas 3, 4 and (4) at its multipliers.

Significance

The result. Theorem 1 shows that the efficiency loss attributed to profit-seeking aggregators is a consequence of one-part pricing, not of aggregation itself. With two-part pricing the aggregator passes the locational marginal price through as its unit price and extracts its profit only through participation fees, so welfare, dispatch and locational prices are exactly those of direct participation. The paper builds on this to analyse a regulated aggregator (§4) and the interaction of prosumer participation with generators' market power (§5, the companion mission of this series).

Formalizing it. The result is proved on paper, in a short argument relying on unstated conventions; no machine-checked version exists. A formal proof must make precise what "optimal Lagrange multiplier" means for a nonsmooth-at-the-boundary concave program on a network, handle the indicator in the prosumer's payoff (10) and the ties it creates, and settle the edge cases (nonpositive locational prices, capacity below the efficient consumption level) that the printed statements pass over.

Difficulty

The welfare identity is the easy part: the objective (20) and the balance (5a) of (21) depend on $(x,d)$ only through $x-d$, and the box (18) projects onto the box (6). The work lies elsewhere. Price equality requires an argument about saddle points of the Lagrangian on two different domains, not just optimal values. The prosumer's two-part problem (11) is discontinuous at $x=0$ because of the fee, so its optimal responses must be found by comparing branches, and the aggregator's optimality in Lemma 4 must hold against every nonnegative offer — including unit prices above the wholesale price — and every optimal response to it, not a selected one. The first-order conditions (2) and (4) require interior optima, which follow from the derivative limits in Assumptions 1–2 but only at positive prices.

Formalization scope

Everything lives in the namespace DERAggregation.Unregulated, in one definition file Setting. Nodes, prosumers, generators and lines are finite types; the node of prosumer $i$ is loc i. All quantities are real. Optimality is "feasible and at least as good as every feasible point", never a supremum. A multiplier vector of (5a) is a saddle point of the partial Lagrangian: (5a) and (5b) are dualized (with $\nu\ge0$ and complementary slackness for $Bh\le f$), the participant box is kept as the domain, and $h$ is free. Prices are never free variables and never defined by a closed form.

Assumptions 1–2 read "differentiable" as differentiable on the open interval and continuous on the closed one, since the derivative limits rule out differentiability at the endpoints; $0\le C_i$ and $\underline y_j<\overline y_j$ are added. Theorem 1 names no assumptions; it is stated under Assumptions 1–3. Problem (21) determines only $x-d$, so "the same $x^*,d^*$" is stated as equality of $x-d$ plus optimality of the canonical split. The first-order conditions are stated at nodes with positive price, Lemma 3 adds $P\ge0$ and $0<p\le\lambda$, and Lemma 4's second part adds the standing restriction $p\le\lambda$; each addition is disclosed in its item. Problem (21) is written in the separate variables $x$ and $d$ with the constraint $d\le Z-C+x$ exactly as printed: a formalization through $z=x-d$ would make Theorem 1 true by unfolding and is ruled out.

The source is the authors' SSRN working paper (abstract 3931052, PDF of September 26, 2021); the published version in Manufacturing & Service Operations Management (2024) may number or state results differently. Useful contributions include the one-dimensional lemmas (unique maximizers of strictly concave functions with derivative limits at the endpoints), which are reusable well beyond this mission, and a general saddle-point lemma for separable concave programs with linear coupling constraints.

Selected references

• Z. Gao, K. Alshehri, J. R. Birge, Aggregating Distributed Energy Resources: Efficiency and Market Power, working paper, SSRN abstract 3931052, 2021. https://ssrn.com/abstract=3931052 ; published in Manufacturing & Service Operations Management, 2024, https://doi.org/10.1287/msom.2021.0539
• K. Alshehri, M. Ndrio, S. Bose, T. Başar, The impact of aggregating distributed energy resources on electricity market efficiency, 53rd Annual Conference on Information Sciences and Systems (CISS), IEEE, 2019, pp. 1–6.
• K. Alshehri, M. Ndrio, S. Bose, T. Başar, Quantifying market efficiency impacts of aggregated distributed energy resources, IEEE Transactions on Power Systems 35(5), 2020, pp. 4067–4077.
• Federal Energy Regulatory Commission, Participation of Distributed Energy Resource Aggregations in Markets Operated by Regional Transmission Organizations and Independent System Operators, Order No. 2222, 2020.

Motivation

A Fisher market allocates a common supply of items among buyers with separate budgets. When the items form a continuum, such as positions in a measurable interval, a buyer's valuation and the market price are functions rather than finite lists. This is a useful model for divisible resources and for settings in which an allocation can be described as a measurable subset of a continuous item space. Gao and Kroer develop equilibrium and convex-programming results for this setting in Infinite-Dimensional Fisher Markets and Tractable Fair Division. Their Section 6 extends the analysis from linear utility to quasilinear utility, where the buyer subtracts the cost of the allocated bundle from its value.

Quasilinear utility changes the role of money. A buyer can retain an unspent part of the budget and value it outside the market. Consequently, normalizing each buyer's valuation independently, which is harmless for linear demand, changes quasilinear demand. The extension therefore needs its own equilibrium definition and its own pair of optimization programs. This mission concerns the existence and exact equilibrium characterization stated in Theorem 10 of the cited preprint, rather than the numerical algorithms discussed elsewhere in that paper.

Setting

There are $n$ buyers and an item space $\Theta$, a compact subset of $\mathbb R^d$, with restricted Lebesgue measure $\mu$. Buyer $i$ has an integrable, nonnegative valuation density $v_i$ with $\int_\Theta v_i\,d\mu>0$, and a strictly positive budget $B_i$. A bundle is an essentially bounded, nonnegative measurable function $x_i$ on $\Theta$. An allocation $x=(x_i)$ is feasible when $\sum_i x_i\le1$ almost everywhere. A pure allocation assigns almost disjoint measurable sets $\Theta_i$ to buyers, so $x_i=\mathbf1_{\Theta_i}$ almost everywhere; some items may remain unallocated.

A price density $p$ is nonnegative and integrable. The pairing $\langle f,g\rangle=\int_\Theta f(\theta)g(\theta)\,d\mu(\theta)$ gives the value of a bundle and its cost. At price $p$, buyer $i$ chooses an affordable bundle maximizing $\langle v_i-p,x_i\rangle$, with affordability $\langle p,x_i\rangle\le B_i$. A quasilinear market equilibrium (QLME) is a feasible allocation and price at which every buyer makes such a choice and unsold items have zero total price: $\langle p,1-\sum_i x_i\rangle=0$.

The quasilinear Eisenberg–Gale primal program uses a nonnegative variable $\delta_i$ for each buyer and maximizes $\sum_i(B_i\log u_i-\delta_i)$, where $u_i\le\langle v_i,x_i\rangle+\delta_i$. Its dual program minimizes $\langle p,1\rangle-\sum_i B_i\log\beta_i$ subject to $p\ge\beta_i v_i$ and $0\le\beta_i\le1$. The primal is represented by $(x,\delta)$ with $u_i=\langle v_i,x_i\rangle+\delta_i$ at an optimum. This saturated form has the same optimum as the displayed program and makes the optimality conditions unambiguous.

Formalization targets

Theorem 10: attainment and equilibrium

The goal is the full four-part statement. The primal attains its maximum at a pure allocation. The dual attains its minimum with a unique vector $\beta^*$ and price density $p^*=\max_i\beta_i^*v_i$ almost everywhere. For feasible primal and dual points, simultaneous optimality is equivalent to market clearance and

$$\beta_i(\langle v_i,x_i\rangle+\delta_i)=B_i,\qquad \delta_i(1-\beta_i)=0,\qquad \langle p-\beta_i v_i,x_i\rangle=0 \quad\text{for every }i.$$

Finally, $(x,p)$ is a QLME exactly when there are $\delta$ and $\beta$ for which $(x,\delta)$ and $(p,\beta)$ are optimal in the two programs. The same given $p$ must appear on both sides of this equivalence.

Milestone results

The milestones follow the statements in the proof of Theorem 10: attainment of the utility-space program (A.14), uniqueness of the minimizer in the reduced dual program, weak duality (A.15) with its additive constant $\sum_iB_i(\log B_i-1)$, the KKT characterization, and each direction of the QLME equivalence. The earlier paper's Lemma 1 identifies the feasible utility set with utilities of pure allocations and supplies the compactness used here. It belongs to the first mission of this series and is not duplicated as a target in this one.

Significance

The theorem establishes that the two infinite-dimensional programs describe the quasilinear market exactly. Attainment guarantees actual optimal allocation and price objects rather than only approximating sequences. Pure attainment gives a measurable partition-type allocation. The unique $\beta^*$ pins down each buyer's utility price, while $p^*=\max_i\beta_i^*v_i$ identifies the price density almost everywhere. The KKT equations give precise tests for a candidate optimal pair, and the final equivalence translates between optimization solutions and buyer-level equilibrium behavior. These are the claims made by Theorem 10 and its appendix proof.

The result is proved in the paper; the work here is to formalize its statement and, in later solver contributions, its proof in Lean. A complete development will also provide reusable infrastructure for integrating valuation densities against essentially bounded bundles, representing continuum-item allocations, and relating a finite buyer-indexed vector to pointwise price maxima. No machine-checked proof of this mission's goal is supplied with this draft.

Difficulty

The optimization variables include functions in $L^\infty$ and $L^1$, and the positive cone of $L^1$ has no useful interior for a direct appeal to standard infinite-dimensional convex-duality theorems. The finite-dimensional utility vector is easier to optimize over, but recovering a pure allocation from it requires the measurable-allocation result established earlier in the paper. The dual price is a pointwise maximum of integrable densities, and equality of prices is meaningful almost everywhere. Equilibrium demand compares a buyer's assigned bundle with every affordable essentially bounded bundle, so an optimality statement about program variables must account for that full comparison.

Formalization scope

Lean represents densities and bundles as functions on the ambient Euclidean space, with the measure restricted to $\Theta$; values outside $\Theta$ do not matter. The standing hypotheses are compactness of $\Theta$, integrability and almost-everywhere nonnegativity of every $v_i$, strictly positive total valuation, and strictly positive budgets. There is no assumption that total budgets or total item measure equal one. The buyer type Fin n is zero-based; the paper numbers buyers from one. The empty-buyer case is allowed and has the expected trivial finite-vector interpretation.

The equilibrium predicate includes supply feasibility. The printed QLME definition on page 29 omits it, although the linear-market definition includes it and Theorem 10(d) requires it. Without it, a buyer can receive more than unit supply on part of the item space while buyer optimality and market clearance still hold. The primal uses the saturated value $u_i=\langle v_i,x_i\rangle+\delta_i$; leaving $u$ free below that value makes the printed KKT converse false. These two choices are disclosed in the item descriptions and moderation notes, with concrete counterexamples there.

The paper treats $\log0$ as a limiting infinite cost. Lean's real logarithm is total, so optimality compares only points whose logarithm arguments are positive. The utility KKT equation is multiplied by $\beta_i$ to avoid division by zero. Valuation and price densities are integrable, and bundles are essentially bounded, so pairings are genuine finite integrals. The pointwise maximum over buyers is an indexed supremum; feasibility and uniqueness use almost-everywhere equality for price functions and exact equality for the finite vector $\beta$. These conventions prevent degenerate total-function values from deciding the theorem.

Contributions can address the measurable utility-set and pure-allocation infrastructure, finite-dimensional attainment, weak duality, the equality conditions, or the demand comparison. The intermediate milestones are stated at the strength used in the paper; the goal contains the entire four-part result.

Selected references

• Yuan Gao and Christian Kroer, Infinite-Dimensional Fisher Markets and Tractable Fair Division, preprint arXiv:2010.03025v5, 2021; published in Operations Research, 2023. arXiv preprint.

Why continuum Fisher markets matter

A Fisher market divides a supply of goods among buyers with fixed budgets. In a finite market, each good is a separate coordinate. Fair division can instead involve a continuum of items, such as locations along an interval or points in a region, where a buyer's valuation varies measurably from point to point. Finite dimensional existence and duality arguments do not automatically apply: the allocation is now a function, and the feasible set need not be compact in its natural function space. Gao and Kroer formulate a market and two Eisenberg–Gale programs for this setting, then prove that their optima exist and characterize equilibrium Gao and Kroer, §3.

The result also connects market equilibrium to fair division. A pure allocation assigns measurable regions of the item space to buyers, allowing overlap only on null sets. Existence of a pure optimizer means that a market outcome can be represented by such a division, rather than by fractional shares at each item. The same paper derives Pareto optimality, budget weighted envy freeness, and proportionality for equilibrium allocations Gao and Kroer, Theorems 1 and 3.

Market, allocations, and programs

The item space $\Theta$ is a compact subset of $\mathbb R^d$ with restricted Lebesgue measure $\mu$. There are $n$ buyers. Buyer $i$ has a budget $B_i>0$ and a nonnegative integrable valuation density $v_i$ with $\int_\Theta v_i\,d\mu>0$. The utility of a bounded nonnegative bundle $x_i$ is $\langle v_i,x_i\rangle=\int_\Theta v_i x_i\,d\mu$. An allocation $x=(x_i)$ is feasible when $\sum_i x_i\le1$ almost everywhere. It is pure when each $x_i$ equals the indicator of a measurable set $\Theta_i\subseteq\Theta$, up to almost everywhere equality, and these sets are pairwise disjoint up to null sets. Leftover items are allowed.

A nonnegative integrable price density $p$ defines a buyer's affordable bundles by $\langle p,x_i\rangle\le B_i$. A market equilibrium $(x,p)$ is a feasible allocation and price at which every buyer maximizes utility among affordable bundles and $\langle p,1-\sum_i x_i\rangle=0$. Thus unallocated supply may remain only where it has zero price. The paper's primal Eisenberg–Gale program, $\mathcal P_{EG}$, maximizes weighted log utility over feasible allocations. Its dual program, $\mathcal D_{EG}$, minimizes total price minus weighted log multipliers subject to $p\ge\beta_i v_i$ almost everywhere Gao and Kroer, pp. 6–8.

Formalization targets

The goal is the three part Theorem 1. In the notation above, it asserts attainment of the primal objective at a pure allocation, attainment of the dual objective with a unique multiplier vector $\beta^*$ and price $p^*=\max_i\beta_i^*v_i$ almost everywhere, and the equivalence

$$(x,p)\text{ is a market equilibrium} \quad\Longleftrightarrow\quad x\text{ optimizes }\mathcal P_{EG}\ \text{and}\ (p,\beta^*)\text{ optimizes }\mathcal D_{EG}.$$

The milestone list follows the results the paper uses to reach that goal. Lemma A.1 gives a convex, compact range for utility matrices and, under atomlessness, identifies mixed and partition based ranges. Lemma 1 specializes this to the market's feasible utility set $U$, proving that $U$ is compact and convex and equals the pure utility set $U'$. Lemma 2 establishes attainment and uniqueness in the finite dimensional reduction of the dual problem. Lemma 3 gives weak duality with the paper's constant $C=\sum_i B_i-\sum_i B_i\log B_i$ and its three optimality conditions. Theorem 2 expands the equivalence between optimality and equilibrium, including budget exhaustion and the utility formula $\langle v_i,x_i\rangle=B_i/\beta_i$. These are the paper's numbered results on pp. 8–10 and a1 Gao and Kroer, §3 and Appendix A.1.

The proposal also states Theorem 3, Lemma 4, and Corollaries 1–3 as companion results. They record the resulting fairness properties, normalized equilibrium bounds, winning sets, a construction of dual prices from a pure optimum, and a test for a pure equilibrium Gao and Kroer, pp. 10–11.

What the result provides

Theorem 1 shows that the two programs give actual allocations and prices in the continuum market, not merely limiting objective values. The pure optimizer provides measurable regions for buyers. The dual multipliers give a unique utility price for each buyer, while the price density is determined almost everywhere. Theorem 2 makes these program outputs economically interpretable: each buyer exhausts its budget at equilibrium. Theorem 3 then supplies efficiency and fairness guarantees for those allocations Gao and Kroer, Theorems 1–3.

These results are proved in the cited paper. This mission asks for machine checked Lean proofs of those mathematical statements. Its definitions of allocations, demand, equilibrium, the two programs, and feasible utilities could also support formalization of the paper's later geometric and quasilinear results. The draft declarations compile as open statements; compilation does not establish the theorems.

Why the proof is difficult

The feasible allocations are bounded in an infinite dimensional function space, but that does not make the set compact in the topology used for the optimization problem. The paper instead needs compactness of the finite dimensional set of achievable utility vectors. The range result in Lemma A.1 is therefore central, and its atomless conclusion must be strong enough to replace fractional allocations by measurable partitions Gao and Kroer, Lemma 1 and Appendix A.1.

Standard constraint qualification arguments also do not supply the required duality theorem here: the positive cone in $L^1(\Theta)$ has empty interior. The proposal consequently asks for the paper's specific weak duality inequality, attainment, and optimality characterization rather than assuming a general finite dimensional duality theorem applies Gao and Kroer, Remark 1.

Formalization scope

Lean uses real valued measurable functions on the ambient Euclidean space with measure $\mu=\mathrm{volume}|_\Theta$. It identifies prices and allocations up to $\mu$ almost everywhere equality, as the paper identifies $L^1$ and $L^\infty$ equivalence classes. Bundles must belong to $L^\infty(\mu)$ and prices and valuations must be integrable; these conditions prevent a nonintegrable product from receiving Lean's default integral value of zero. The number of buyers may be zero, consistent with the finite index formulation, while the standing positivity hypotheses apply to every buyer present.

The real logarithm in Lean returns zero at zero. The optimization predicates instead require positive utility or positive dual multipliers and compare only with other positive points, matching the paper's $\log 0=-\infty$ objective convention. The maximization over buyers is the finite supremum $\sup_i\beta_i v_i$. Price and allocation uniqueness is stated almost everywhere; multiplier uniqueness is exact. Lemma A.1 uses the paper's divisible measure condition for atomlessness and fixes its unnamed almost everywhere partition convention by requiring $\sum_jx_j=1$ everywhere. Corollary 3 explicitly requires each denominator $v_i(\Theta_i)$ to be positive. Lemma 4 alone assumes the normalizations $v_i(\Theta)=1$ and $\sum_iB_i=1$, which the paper recalls before its statement.

The goal remains the full three part theorem. It does not assume the range theorem, duality equality, or optimality conditions it is meant to establish. Contributions to the measure range theorem, utility set compactness, the dual reduction, and the equilibrium characterization are all within scope.

Selected references

• Yuan Gao and Christian Kroer, Infinite-Dimensional Fisher Markets and Tractable Fair Division, Operations Research, 2023; formalization follows arXiv:2010.03025v5, 2021, §§2–3 and Appendix A.1.

Why spatial pricing needs a dynamic control

A ride-hailing firm chooses prices while drivers move through a city. A trip from one region uses a driver immediately and returns that driver at another region only after a travel delay. Prices affect which trips are requested, but the actual requests fluctuate. A plan that ignores these fluctuations can run out of available drivers at a busy origin even when its average flows fit the fleet. Chen, Lei, and Jasin study how closely a feasible pricing control can approach a deterministic revenue benchmark in this setting (accepted manuscript, published article).

Their Arc Balancing Control (ABC) responds to realized trips. It groups each directed arc's periods into batches and adjusts the next batch's demand rates according to the previous batch's cumulative surplus or deficit. The paper proves a loss rate for ABC that is smaller than the rate established there for its Static Price Control. The target here is the paper's Theorem 3, with the model and parameters of its authors' accepted manuscript. Its e-companion contains the paper's proofs.

The pricing network and benchmark

The network has $N\ge1$ regions and a horizon of $T\ge1$ periods. Every ordered pair $i\to j$, including $i=j$, is an arc. At most one customer can request an arc's trip in a period. A served trip takes one server from region $i$ for $\tau_{ij}\ge1$ periods, then returns it at $j$. Region $i$ starts with $C_i\ge N$ servers. A control must respect the available server count before it serves each period's realized requests.

The decision is a demand rate $\lambda_{t,ij}\in[0,1]$ rather than its inverse price. The expected revenue from that arc and period is $r_{t,ij}(\lambda_{t,ij})$. The revenue functions are nonnegative and strongly concave, vanish at zero, and have bounded first and second derivatives. The bound on those derivatives is $\Psi_3>0$. The paper's price-side assumptions imply these rate-side conditions; the Lean model states the conditions directly.

The deterministic convex program $\mathrm{DCP}(\zeta)$ chooses rates to maximize the sum of expected revenues. Its flow constraints replace realized trips with their rates, while its cushion requires $\zeta\le\lambda_{t,ij}\le1-\zeta$. Write $J(\zeta)$ for its value and $\lambda^{\zeta,D}$ for an optimal schedule. In the $n$th system, the fleet, horizon, and travel times are multiplied by $n$; each original period's revenue curve is used for $n$ consecutive scaled periods. Thus $T^n=nT$ and $\underline\tau^n=n\min_{i,j}\tau_{ij}$. For a control $\pi$, the per-period benchmark loss is

$$L^\pi(n)=\frac{J(n,0)-\mathbb E^\pi[R^\pi(n)]}{T^n}.$$

ABC uses $\lambda^{n,\zeta,D}$ as its baseline. Its batches have a target sum $b$ of the baseline variance weights $\lambda^{n,\zeta,D}_{t,ij}(1-\lambda^{n,\zeta,D}_{t,ij})$. Within a batch, the control subtracts a weighted share of the preceding batch's realized surplus $\bar\delta^k_{ij}=\sum_{t\in\mathcal T^k_{ij}}(D_{t,ij}-\lambda^{ABC}_{t,ij})$. A rate is projected to $[0,1]$, and an origin with too few available servers is turned off. The finite path law uses the rates posted along each path.

Formalization targets

The principal target is Theorem 3. With $b_n=(\underline\tau^n)^{2/3}$ and

$$\epsilon_n=(\underline\tau^n)^{-1}\left(1+16\sqrt{2(b_n+1)\log T^n}\right),\qquad \zeta_n=2\epsilon_n,$$

there is a constant $\widetilde\Psi_2$, independent of $n$, for which every integer $n\ge1$ satisfies

$$L^{ABC}(n)\le\widetilde\Psi_2\frac{\log(1+n)^{3/2}}{n^{2/3}}.$$

The milestone list follows the source results used in the analysis: Lemma 2 bounds the deterministic cost of a small cushion and gives feasibility; Lemma EC.1 bounds a maximal cumulative Bernoulli deviation; and the two parts of Lemma 4 characterize ABC on a batchwise good event $\mathcal A$ and bound that event's probability. Theorem 3 fixes the complete control and these exact parameters; its constant may depend on the fixed network instance and $\Psi_3$.

What the result establishes

The theorem gives a finite-$n$ loss bound relative to $J(n,0)$, with the stated $n^{-2/3}$ rate and logarithmic factor. In the paper, Lemma 1 shows that $J(n,0)$ bounds the optimal admissible policy's revenue. Theorem 3 therefore bounds ABC's distance from a benchmark that is at least as high as the unknown stochastic optimum. The paper compares this rate with its $n^{-1/2}$ result for Static Price Control and explains the resulting value of adapting prices to realized demand (Theorems 2–3).

The published mathematical result and its manuscript proof are known; the statements in this mission are Lean targets with proofs still to be formalized. A complete development would also make reusable definitions for finite controlled path laws, delayed network flow balance, and cushioned deterministic relaxations. The batch and feedback definitions isolate the paper-specific control from that general infrastructure.

Main difficulty

The deterministic program controls expected flows, while ABC must keep every realized path feasible. An unadjusted baseline can accumulate demand fluctuations over the whole horizon; bounding those fluctuations alone does not describe the effect of ABC's feedback. The control's posted rate in a period depends on earlier realized requests, which changes the distribution of later requests. The manuscript's proof of Lemma 4 bounds a variance proxy from its deterministic baseline when treating the adaptive posted rates; that step needs separate justification in a formal proof. Lemma EC.1, as posed here, covers deterministic Bernoulli rates and does not by itself close that gap. The finite-horizon claim, including small scaling factors for which the cushioned DCP may be infeasible, must still be established.

Formalization scope

Lean represents regions by Fin N, periods by natural numbers $1,\ldots,T$, travel times and server counts by naturals, demand by Boolean paths, and revenue and rates by real numbers. The $\mathrm{DCP}(n,\zeta)$ program uses a real supremum; statements involving positive $\zeta$ assert feasibility, and $J(n,0)$ has the zero schedule as a feasible point. ABC's path law is the product of sequential Bernoulli factors at its own posted rates. Its rate history is built by structural recursion, and the event $\mathcal A$ checks every nonempty batch and all its partial sums.

The accepted manuscript leaves the final incomplete batch unspecified, so the last short batch is merged with its predecessor. The printed ABC box turns an origin off at $C_{t,i}\le N$, while Lemma 4 and its base case require service when $C_{t,i}=N$; the formal control uses $C_{t,i}\ge N$. If the cushioned DCP has no optimum, the baseline is zero. The sample-path part of Lemma 4 adds the hypothesis $\underline\tau\le T$, which the manuscript does not print. Without it the part is false: when the horizon is shorter than every travel time, no server returns, and a single realized trip can leave a region below $N$ servers on the good event. These conventions are recorded with the source discrepancies in the moderation notes. The rate model drops assumptions A1 and A3(i), which concern only the price parametrization, and writes A2, A3(ii), $r\ge0$, and $r(0)=0$ directly. It assumes a twice continuously differentiable extension of revenue to $\mathbb R$. No statement substitutes expected demand for the realized batch surplus or lets the theorem's parameters depend on $n$ by existential choice. Contributions toward the source milestones, the adaptive concentration step, and the reusable model definitions are all within scope.

Selected references

• Q. Chen, Y. Lei, and S. Jasin, Real-Time Spatial-Intertemporal Pricing and Relocation in a Ride-Hailing Network: Near Optimal Heuristics and The Value of Dynamic Pricing, authors' accepted manuscript, LBS Research Online eprint 2845, pp. 7–25 and ec2–ec6; published as Real-Time Spatial–Intertemporal Pricing and Relocation in a Ride-Hailing Network: Near-Optimal Policies and the Value of Dynamic Pricing, Operations Research 72(5):2097–2118, 2024. Manuscript, DOI.

Motivation

Bayesian persuasion studies a sender who observes a state of the world and commits in advance to a randomized disclosure rule, in order to influence the action of a receiver who updates her belief by Bayes' rule. Since Kamenica and Gentzkow (2011) the model has been applied to platform design, recommendation systems, queue information and rating systems. Almost all of this theory assumes the receiver is an expected-utility maximizer, so that her payoff from each action is linear in her belief.

Many receivers are not. A customer who joins a queue only if the mean of her waiting time plus a multiple of its standard deviation is below a threshold has a utility that is nonlinear in her belief. Anunrojwong, Iyer and Lingenbrink (2023) call such receivers risk-conscious and show that, for them, the standard revelation-principle reduction to action recommendations fails. Their first main result replaces it with a convex program over the joint distribution of state and action. This mission formalizes that result and the lemmas leading to it.

Setting

Let $\Omega$ be a finite set of states and $\Delta(\Omega) \subseteq \mathbb{R}^{\Omega}$ the simplex of beliefs, with the Euclidean topology. Sender and receiver share a prior $\mu^* \in \Delta(\Omega)$. The receiver chooses an action from a finite nonempty set $A$. Her utility is an arbitrary function $\rho : \Delta(\Omega) \times A \to \mathbb{R}$; the sender's utility is $v : \Omega \times A \to \mathbb{R}$.

For each action $a$, the beliefs at which $a$ is optimal for the receiver form the set

$$P_a = \{\mu \in \Delta(\Omega) : a \in \arg\max_{a' \in A} \rho(\mu, a')\}.$$

The paper assumes throughout (Assumption 1) that every $P_a$ is closed.

A signaling scheme consists of a measurable signal space $S$ and a probability measure $\pi$ on $\Omega \times S$ whose $\Omega$-marginal is $\mu^*$. After signal $s$ the receiver holds the posterior $\mu_s \in \Delta(\Omega)$ given by Bayes' rule, and plays an optimal strategy $a(\cdot)$, with $a(s) \in \arg\max_a \rho(\mu_s, a)$, that is $\mu_s \in P_{a(s)}$. The sender's persuasion problem (3) is to maximize $\mathbb{E}_\pi[v(\bar\omega, a(\bar s))]$ over signal spaces, schemes and optimal receiver strategies; when the receiver is indifferent, the sender picks the strategy she prefers.

A probability measure $\eta$ on $\Delta(\Omega)$ is Bayes-plausible if its mean is the prior: $\mathbb{E}_\eta[\bar s] = \mu^*$.

Formalization targets

Goal: Theorem 1

The sender's problem (3) can be optimized by solving the convex program

$$\max_{\{t_a : a \in A\}} \sum_{\omega \in \Omega} \sum_{a \in A} t_a(\omega)\, v(\omega,a) \quad \text{s.t.} \quad \sum_{a \in A} t_a(\omega) = \mu^*(\omega)\ (\omega \in \Omega), \qquad t_a \in \operatorname{Conv}(P_a \cup \{0\})\ (a \in A). \qquad (7)$$

It is formalized as an equality of sets: the values achievable in (3) are exactly the objective values of feasible points of (7). This says that every scheme yields a feasible point of (7) with the same value, and every feasible point is realized by a scheme. In particular the supremum of (3) equals the maximum of (7), and an optimal solution of (7) gives an optimal scheme.

Milestones

1. Lemma 1 (Aumann–Maschler, Kamenica–Gentzkow): schemes whose signals are beliefs and satisfy $\mu_s = s$ correspond to Bayes-plausible measures.
2. Lemma 5: the belief-recommendation problem (4) is equivalent to problem (14) over Bayes-plausible measures.
3. Lemma 2: a Bayes-plausible measure and an optimal strategy give action probabilities $b_a \in [0,1]$ and mean-posteriors $m_a \in \operatorname{Conv}(P_a)$ with $\sum_a b_a m_a = \mu^*$ and the same sender value; the converse also holds.

Further result: Theorem 2

Let $\Upsilon_a$ be the states at which $a$ is sender-optimal, assume these sets partition $\Omega$, and set $t^*_a = \mu^* \mathbb{1}_{\Upsilon_a}$. Then the sender can fully persuade the receiver (almost surely, the receiver takes a sender-optimal action) if and only if $t^*$ is feasible for (7), i.e. $t^*_a \in \operatorname{Conv}(P_a \cup \{0\})$ for all $a$.

Significance

The result. Problem (3) optimizes over arbitrary signal spaces and joint distributions, so it is not finite-dimensional. Program (7) has $|A|$ vector variables in $\mathbb{R}^{\Omega}$, each in a convex set that depends only on the receiver's utility. Its variable $t_a(\omega)$ is the joint probability of state $\omega$ and action $a$. The program gives the paper's bound on the number of signals needed (Proposition 1), its characterization of when persuasion helps (Proposition 2), the full-persuasion criterion (Theorem 2) and, after replacing $\operatorname{Conv}(P_a \cup \{0\})$ by a polytope, the linear program for binary persuasion (Theorem 3, the companion mission). For expected-utility receivers each $P_a$ is convex, and (7) reduces to the familiar obedience-constrained linear program.

Formalizing it. The results are proved in the paper; none is formalized. A formal development fixes what "can be optimized by solving" means as a set equality and handles general measurable signal spaces with posteriors defined only almost everywhere. It also exposes two places where the printed lemmas need correction (see the scope section).

Difficulty

The usual revelation-principle shortcut would merge all signals that lead to the same action. For a risk-conscious receiver this can change the response: averaging posteriors in $P_a$ can produce a belief outside $P_a$, since $P_a$ need not be convex. The central geometric difficulty is relating a distribution of posteriors supported on a closed, potentially nonconvex $P_a$ to a finite-dimensional variable in $\operatorname{Conv}(P_a \cup \{0\})$. The converse must preserve both Bayes plausibility and receiver optimality. With general signal spaces, the posterior is determined only almost everywhere, while the stated strategy condition applies at every signal.

Formalization scope

• Representation. $\Omega$ and $A$ are Fintypes, $A$ nonempty, and $\Omega$ carries a measurable space in which singletons are measurable. Beliefs are functions $\Omega \to \mathbb{R}$ in stdSimplex ℝ Ω, Belief Ω is the simplex as a subtype, $\operatorname{Conv}$ is convexHull ℝ, and $0$ is the zero function. $\rho$ is a function on $\mathbb{R}^{\Omega}$, used only on the simplex.
• Signal spaces in (3) range over all measurable types. A scheme is a probability measure on $\Omega \times S$ with $\pi(\{\omega\} \times S) = \mu^*(\omega)$.
• Posteriors are any version of Bayes' rule: simplex-valued for every signal, measurable, and satisfying $\pi(\{\omega\} \times B) = \int_B \mu_s(\omega)\,\pi_S(ds)$. Quotients $\pi(\omega,s)/\sum_{\omega'} \pi(\omega',s)$ with Lean's $x/0 = 0$ are not used. "$\mu_s = s$" (Lemmas 1 and 5) means the identity is such a version, an almost-sure statement; the paper's "for all $s$" in Lemma 1's converse is proved only almost surely.
• Strategies are measurable (each event $\{a(\bar s) = b\}$ is measurable) and optimal at every signal. The sender's value is not computed with a fixed tie-breaking rule, so sender-preferred selection is kept.
• Assumption 1 is a hypothesis of every statement that involves $\rho$.
• Corrections to Lemma 2. If some $P_a$ is empty, $\operatorname{Conv}(P_a)$ is empty and the printed forward direction fails, so $m_a$ is left free there; then $b_a = 0$ necessarily. The printed converse fails for pure strategies when two actions must share a posterior, so it is stated for optimal mixed strategies, which the paper allows on p. 11.
• Ruled out: quantifying (3) only over belief signals with $\mu_s = s$ would turn Theorem 1 into Lemmas 5 and 2 and drop the coalescence step. The goal therefore quantifies over arbitrary signal spaces. Stating only "the optimal values are equal" through a real supremum would also be weaker, and is not done.
• Infrastructure needed: means of probability measures on compact sets in $\mathbb{R}^n$ lying in the convex hull (Convex.integral_mem, compactness of convex hulls of compact sets), Carathéodory's theorem (convexHull_eq_union), finite discrete measures on $\Omega \times S$, and conditional densities with respect to the signal marginal. The Bayes-plausibility and splitting lemmas are reusable in any persuasion development. Proofs of the milestones, of the goal, and of Theorem 2 are all welcome.

Selected references

• J. Anunrojwong, K. Iyer, D. Lingenbrink, Persuading Risk-Conscious Agents: A Geometric Approach, arXiv:2208.03758v3, 2023; Operations Research, 2024. https://arxiv.org/abs/2208.03758v3
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
• D. Bergemann, S. Morris, Bayes Correlated Equilibrium and the Comparison of Information Structures in Games, Theoretical Economics 11(2), 2016. https://doi.org/10.3982/TE1808

Motivation

In Bayesian persuasion a sender who observes the state of the world commits to a signaling scheme, a receiver updates her belief by Bayes' rule and acts, and the sender chooses the scheme that maximizes her own expected payoff (Kamenica and Gentzkow 2011). The classical theory assumes the receiver maximizes expected utility, so her payoff is linear in her belief. Many applications violate this: a customer who joins a queue only if the mean of her waiting time plus a multiple of its standard deviation is below a threshold, a commuter who values route reliability, a buyer who dislikes uncertainty about a product. Anunrojwong, Iyer and Lingenbrink (arXiv:2208.03758v3) call such receivers risk-conscious: the receiver's utility $\rho(\mu,a)$ of action $a$ at belief $\mu$ is an arbitrary function of $\mu$.

The paper's first result reduces the sender's problem, an optimization over distributions of posteriors, to a finite-dimensional convex program (program (7)). This mission concerns its second main result: in the practically important binary persuasion setting (two actions, the sender always weakly prefers action $1$), when the region of beliefs at which the receiver rejects action $1$ is convex, program (7) collapses further to a linear program whose feasible region is the convex hull of finitely many explicit beliefs.

Setting

Let $\Omega$ be a finite set of states and $\Delta(\Omega)\subseteq\mathbb R^{\Omega}$ the simplex of beliefs, with the Euclidean topology. For $\omega\in\Omega$, $e_\omega$ is the point-mass belief at $\omega$; states are identified with their point masses. The prior is $\mu^*\in\Delta(\Omega)$. The receiver has actions $A=\{0,1\}$ and utility $\rho(\mu,a)$. The optimality regions are

$$P_a=\{\mu\in\Delta(\Omega):\ a\in\arg\max_{a'\in A}\rho(\mu,a')\},$$

and the differential utility is $\hat\rho(\mu)=\rho(\mu,1)-\rho(\mu,0)$, so $P_1=\{\hat\rho\ge 0\}$ and $P_0=\{\hat\rho\le 0\}$ inside $\Delta(\Omega)$. The sender's utility is $v(\omega,a)$ with $v(\omega,1)\ge v(\omega,0)$ for every $\omega$.

Two assumptions are used.

• Assumption 1 (standing throughout the paper): $P_0$ and $P_1$ are closed.
• Assumption 2: the non-adoption region $P_1^c=\{\mu\in\Delta(\Omega):\hat\rho(\mu)<0\}$ is convex.

From these data the paper builds finitely many beliefs. $K_1=\{\omega: e_\omega\in P_1\}$ and $K_0=\{\omega:e_\omega\in P_0\}$ are the states where action $1$, respectively $0$, is optimal under full information, and $L_0=K_0\setminus K_1$ the states where action $0$ is uniquely optimal. For $\omega_0\in L_0$ and $\omega_1\in K_1$,

$$\gamma(\omega_0,\omega_1)=\sup\{g\in[0,1]:\ g e_{\omega_0}+(1-g)e_{\omega_1}\in P_1\},\qquad \chi(\omega_0,\omega_1)=\gamma(\omega_0,\omega_1)e_{\omega_0}+(1-\gamma(\omega_0,\omega_1))e_{\omega_1},$$

the mixture of $\omega_0$ and $\omega_1$ with the most weight on $\omega_0$ at which action $1$ is still optimal, and $K_{01}=\{\chi(\omega_0,\omega_1):\omega_0\in L_0,\ \omega_1\in K_1\}$.

A candidate solution is a pair $t=(t_0,t_1)$ of vectors in $\mathbb R^{\Omega}$, with $t_a(\omega)$ the joint probability of state $\omega$ and action $a$. The sender's objective is $\sum_\omega v(\omega,1)t_1(\omega)+v(\omega,0)t_0(\omega)$. Program (7) maximizes it subject to $t_0+t_1=\mu^*$ and $t_a\in\operatorname{Conv}(P_a\cup\{0\})$; program (10) subject to $t_0+t_1=\mu^*$, $t_1\in\operatorname{Conv}(K_1\cup K_{01}\cup\{0\})$ and $t_0\in\operatorname{Conv}(L_0\cup\{0\})$.

Formalization targets

Goal: Theorem 3

Under Assumptions 1 and 2, with $v(\omega,1)\ge v(\omega,0)$ for all $\omega$:

$$\text{(i)}\ \ t \text{ feasible for (10)} \Rightarrow t \text{ feasible for (7)};\qquad \text{(ii)}\ \ t \text{ feasible for (7)} \Rightarrow \exists\, t' \text{ feasible for (10)},\ \ \text{obj}(t)\le\text{obj}(t').$$

Together these say that (7) and (10) have the same optimal value and every optimal solution of (10) is optimal for (7): (7) "can be optimized by solving" (10).

Milestones

1. $\chi(\omega_0,\omega_1)\in P_0\cap P_1$ for $\omega_0\in L_0$, $\omega_1\in K_1$ (Section 5.1, under Assumption 1).
2. Lemma 6: $\Delta(\Omega)=\operatorname{Conv}(L_0\cup K_{01})\cup\operatorname{Conv}(K_1\cup K_{01})$, with no assumption on $\rho$.
3. Lemma 7: under Assumption 2, $\operatorname{Conv}(P_1)=\operatorname{Conv}(K_1\cup K_{01})$.

Further results on the same objects

• Lemma 3: if $\hat\rho$ is quasiconvex on $\Delta(\Omega)$, Assumption 2 holds.
• Proposition 3: if $v(\omega,1)-v(\omega,0)=\bar v>0$ for all $\omega$ and a strict total order $\prec$ satisfies the monotonicity Assumption 3, every optimal solution of (10) has a threshold $\omega_0\in L_0$ with $t_1(\omega)=\mu^*(\omega)$ for $\omega\prec\omega_0$ and $t_1(\omega)=0$ for $\omega_0\prec\omega$.
• With strict preference $v(\omega,1)>v(\omega,0)$ for all $\omega$, every optimal solution of (7) is feasible for (10).

Significance

Theorem 3 replaces an optimization over a convex set described only implicitly through $\rho$ by a linear program over an explicit polytope. It identifies a canonical signal set: irrespective of the prior, an optimal scheme only needs to induce beliefs in $\Omega\cup K_{01}$, that is, either reveal the state or leave the receiver uncertain between one state of $L_0$ and one of $K_1$. Lemma 7 gives a simple full-persuasion test, $\mu^*\in\operatorname{Conv}(K_1\cup K_{01})$, and Proposition 3 a threshold structure of the induced actions that the paper uses in its queueing application. For expected-utility receivers the corresponding statements reduce to classical facts about concavification; the content here is that they survive non-linear utilities under a single convexity condition.

On the formal side, the results are proved in the paper and nothing about them is machine-checked. A complete development would give a verified reduction of a family of non-linear persuasion problems to linear programs, and a reusable library of convex-hull facts on the simplex (decompositions of the simplex into hulls of point masses and segment points). The formalization also corrects the paper at one point: the proof of Theorem 3 asserts that every optimal solution of (7) is feasible for (10), which fails when the sender is indifferent between actions in some state; the goal is stated in the form the proof establishes.

Difficulty

The inclusion of (10)'s feasible region in (7)'s is immediate once $K_{01}\subseteq P_1$. The content lies in the converse: $P_1$ is an arbitrary closed set whose complement in the simplex is convex, and one must show that every point of $P_1$ is a convex combination of point masses in $K_1$ and the boundary points $\chi(\omega_0,\omega_1)$ on the edges of the simplex. The natural first idea, to argue with extreme points of $\operatorname{Conv}(P_1)$, does not work directly: $P_1$ need not be convex, its convex hull need not be closed a priori, and the extreme points of $P_1$ are not in general on edges of the simplex. Assumption 2 constrains only the complement of $P_1$, so it has to be transported to a statement about $P_1$ itself. A second difficulty is that $t_0$ in a solution of (7) may put weight on states in $K_0\cap K_1$ or on interior beliefs, and it must be moved to $t_1$ without lowering the objective.

Formalization scope

• Beliefs are functions Ω → ℝ with [Fintype Ω] [DecidableEq Ω]; $\Delta(\Omega)$ is Mathlib's stdSimplex ℝ Ω; $e_\omega$ is Pi.single ω 1; actions are Fin 2; $\operatorname{Conv}$ is convexHull ℝ; $0$ is the zero vector.
• The receiver's utility is ρ : (Ω → ℝ) → Fin 2 → ℝ, and $P_a$ is defined from it by Eq. (1), intersected with the simplex; values of ρ off the simplex are irrelevant. Assumption 1 is IsClosed (P ρ a) for both actions.
• $K_0,K_1,L_0$ are sets of states; they enter convex hulls through their images under $e$. $\gamma$ is a real sSup, used only for $\omega_0\in L_0$, $\omega_1\in K_1$, where the set contains $0$ and is bounded by $1$.
• Programs (7) and (10) are feasibility predicates on t : Fin 2 → Ω → ℝ with a common objective. Theorem 3 is stated as (i) and (ii) above, never through a supremum of objective values. A formalization in which (10) only needs to have some feasible point, or in which the supremum of an empty or unbounded set of values is compared, would be trivial or meaningless and is not the target.
• Proposition 3 takes the order of Assumption 3 as a relation given with the data, and assumes $L_0\neq\emptyset$, which the paper uses implicitly.
• Needed infrastructure: convex hulls of finite sets of point masses in the simplex, Carathéodory-type finite decompositions (available in Mathlib), and the decomposition of a convex combination along a segment. Proofs of the milestones, alternative proofs of Lemma 7 (for example by a separation argument), and proofs of the further results are all welcome.

Selected references

• Anunrojwong, J., Iyer, K., Lingenbrink, D., Persuading Risk-Conscious Agents: A Geometric Approach, arXiv:2208.03758v3, 2023 (journal version: Operations Research, 2024). https://arxiv.org/abs/2208.03758v3
• Kamenica, E., Gentzkow, M., Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590

Motivation

Optimization under uncertainty usually fixes one probability distribution $\mathbb P$ for the uncertain data and optimizes an expected payoff, or fixes a set $\mathcal Q$ of distributions and protects against the worst one (robust optimization). The first is sensitive to a misspecified $\mathbb P$; the second can be very conservative, because it treats a barely plausible distribution exactly like the nominal one. Ben-Tal, Bertsimas and Brown (Oper. Res. 58(4), 2010) propose a graded alternative, the soft robust model: the decision maker accepts a loss of at most $\varepsilon$ in expected payoff under every distribution of a set $\mathcal Q(\varepsilon)$, simultaneously for all levels $\varepsilon$ up to a budget $\delta$. Larger sets of distributions are allowed a larger shortfall.

The paper's central result, Theorem 2.1, shows that this model is exactly a constraint on a convex risk measure in the sense of Föllmer and Schied (Finance Stoch. 6, 2002), and that every normalized convex risk measure arises from some soft robust model. This connects distributionally robust optimization with the theory of monetary risk measures, and gives a tractable convex reformulation of soft robust constraints. Related earlier work connected coherent risk measures with standard robust optimization (Bertsimas and Brown, Oper. Res. 57(6), 2009).

Setting

Let $(\Omega,\mathcal F)$ be a measurable space and $\mathcal P$ the set of all probability measures on it. A decision $x$ ranges over a nonempty, closed, convex set $X\subseteq\mathbb R^n$; a random variable $u:\Omega\to\mathbb R^m$ carries the uncertain parameters, and $f(x,u(\omega))$ is the payoff, concave in $x\in X$ for every $\omega$. For each $x\in X$ the random variable $f(x)=f(x,u(\cdot))$ is assumed bounded and measurable.

A family of measures is $\mathbf Q=\{\mathcal Q(\varepsilon)\subseteq\mathcal P:\varepsilon\ge0\}$. It is nondecreasing if $\mathcal Q(\varepsilon_1)\subseteq\mathcal Q(\varepsilon_2)$ for $\varepsilon_1\le\varepsilon_2$, and convex if $\mathbb Q_i\in\mathcal Q(\varepsilon_i)$ implies $\lambda\mathbb Q_1+(1-\lambda)\mathbb Q_2\in\mathcal Q(\lambda\varepsilon_1+(1-\lambda)\varepsilon_2)$ for $\lambda\in[0,1]$. The standing assumptions are that $\mathbf Q$ is nondecreasing and convex and that $\mathcal Q(0)\neq\emptyset$. The soft robust feasible set at level $\delta\ge0$ is

$$X^Q(\delta)=\Big\{x\in X:\ \inf_{\mathbb Q\in\mathcal Q(\varepsilon)}\mathbb E_{\mathbb Q}[f(x)]\ \ge\ -\varepsilon\quad\forall\,\varepsilon\in[0,\delta]\Big\}.\tag{5}$$

A risk measure, on the space $\mathcal Y$ of bounded payoffs, is a map $\rho:\mathcal Y\to\mathbb R$ with $Y_1\ge Y_2\Rightarrow\rho(Y_1)\le\rho(Y_2)$ and $\rho(Y+c)=\rho(Y)-c$ for $c\in\mathbb R$; it is convex if $\rho(\lambda Y_1+(1-\lambda)Y_2)\le\lambda\rho(Y_1)+(1-\lambda)\rho(Y_2)$. It is generated by a convex penalty $\alpha:\mathcal P\to[0,\infty]$ if $\rho(Y)=\sup_{\mathbb Q\in\mathcal P}\{-\mathbb E_{\mathbb Q}[Y]-\alpha(\mathbb Q)\}$, and normalized if in addition $\alpha(\mathbb Q)=0$ for some $\mathbb Q$. A family and a penalty determine each other:

$$\alpha^Q(\mathbb Q)=\inf\{\varepsilon\ge0:\mathbb Q\in\mathcal Q(\varepsilon)\},\qquad \mathcal Q^\alpha(\varepsilon)=\{\mathbb Q\in\mathcal P:\alpha(\mathbb Q)\le\varepsilon\},$$

and $\rho^Q$ denotes the risk measure generated by $\alpha^Q$.

Formalization targets

Goal: Theorem 2.1 for $\delta>0$

For every nondecreasing, convex family $\mathbf Q$ with $\mathcal Q(0)\ne\emptyset$, $\rho^Q$ is a convex risk measure generated by the normalized convex penalty $\alpha^Q$, the minimum below is attained for every $x\in X$, and

$$X^Q(\delta)=\Big\{x\in X:\ \min_{\lambda\ge0}\Big\{\lambda\delta+(\lambda+1)\,\rho^Q\Big(\frac{f(x)}{\lambda+1}\Big)\Big\}\le0\Big\}.\tag{6}$$

Conversely, for every convex risk measure $\rho$ generated by a normalized convex penalty $\alpha$, the family $\mathbf Q^\alpha$ is nondecreasing and convex with $\mathcal Q^\alpha(0)\ne\emptyset$, and (6) holds with $\rho$ on the right and $\mathbf Q^\alpha$ on the left.

Milestones: the steps of the proof (p. 1224)

1. The soft robust infimum $\inf\{\mathbb E_{\mathbb Q}[f(x)]+\varepsilon:\varepsilon\in[0,\delta],\ \mathbb Q\in\mathcal Q(\varepsilon)\}$ equals $\inf\{\mathbb E_{\mathbb Q}[f(x)]+\alpha^Q(\mathbb Q):\alpha^Q(\mathbb Q)\le\delta\}$.
2. Strong duality with an attained multiplier: that infimum equals $\max_{\lambda\ge0}\{-\lambda\delta+\inf_{\mathbb Q}\{\mathbb E_{\mathbb Q}[f(x)]+(\lambda+1)\alpha^Q(\mathbb Q)\}\}$.
3. The scaling identity $\inf_{\mathbb Q}\{\mathbb E_{\mathbb Q}[Y]+(\lambda+1)\alpha^Q(\mathbb Q)\}=-(\lambda+1)\rho^Q(Y/(\lambda+1))$.
4. $\rho^Q$ is a convex risk measure generated by the convex, normalized penalty $\alpha^Q$.
5. For a convex normalized $\alpha$, $\mathbf Q^\alpha$ is nondecreasing and convex with $\mathcal Q^\alpha(0)\ne\emptyset$.
6. $\alpha^{Q^\alpha}=\alpha$.

Significance

Theorem 2.1 makes the soft robust constraint usable: the right side of (6) is a single constraint in $(\lambda,x)$, and the function $(\lambda+1)\rho(f(x)/(\lambda+1))$ is jointly convex in $(\lambda,x)$ for $\lambda\ge0$, so soft robust problems are convex programs whenever the risk measure can be evaluated. Read in the other direction, it gives every normalized convex risk measure an interpretation as a graded robustness requirement over the level sets of its penalty, which is how the paper derives soft robust counterparts of optimized certainty equivalents, CVaR and entropic risk, and its later bounds on the probability of a loss.

The theorem is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it produces a Lean development of convex risk measures generated by penalties on an arbitrary measurable space, with extended-valued penalties and mixtures of probability measures, and a one-constraint Lagrange duality theorem over a convex set of probability measures. Mathlib does not currently provide Lagrange duality in this form.

Difficulty

The equalities of the proof read as routine, and two of them are not. The first equality is described as "the definition of $\alpha^Q$", but a measure with $\alpha^Q(\mathbb Q)=\delta$ need not belong to $\mathcal Q(\delta)$, because the infimum defining $\alpha^Q$ need not be attained; the equality relies on the convexity of the family, the nonemptiness of $\mathcal Q(0)$ and the boundedness of $f(x)$. The second equality is Lagrange duality with dual attainment for a convex program whose variable is a probability measure and whose objective and constraint are extended-valued; the classical theorem applies to convex subsets of vector spaces, and transferring it to mixtures of probability measures with $[0,\infty]$-valued penalties is the main formal work. Attainment of the minimum in (6), which the paper asserts by writing "min", is exactly dual attainment and does not follow from the inequality alone.

Formalization scope

The probability measures are ProbabilityMeasure Ω on a measurable space; a family is a map from levels $\varepsilon\in\mathbb R_{\ge0}$ to sets of probability measures, and mixtures are built from the measures $t\,\mathbb Q_1+(1-t)\,\mathbb Q_2$. Penalties, including $\alpha^Q$, take values in $[0,\infty]$, so that a measure in no $\mathcal Q(\varepsilon)$ has penalty $+\infty$; a real-valued $\alpha^Q$ would give such measures penalty $0$ through the junk value of an empty infimum, and is excluded. Risk measures are real functions whose axioms are imposed on bounded measurable payoffs, "generated by" includes the least-upper-bound property of the supremum, and "min" in (6) is attainment on $[0,\infty)$ together with a nonpositive minimum. The decision set and payoff carry the paper's assumptions; concavity of the payoff and closedness and convexity of $X$ are kept although Theorem 2.1 does not use them. Infima over measures in the milestones are taken in the extended reals.

The case $\delta=0$ is excluded. The paper states Theorem 2.1 for $\delta\ge0$, but at $\delta=0$ its proof interchanges a limit in $\lambda$ with a supremum over measures without justification, and (6) fails: on $\Omega=\{a,b\}$ with $\mathcal Q(0)$ the measures giving $a$ mass at most $1/4$ and $\mathcal Q(\varepsilon)$ those giving it mass at most $1/2$ for $\varepsilon>0$, the payoff $f(a)=-2$, $f(b)=1$ is soft robust at level $0$ while the right side of (6) is empty. The goal and the milestones therefore fix $\delta>0$, the case the paper's main argument treats.

A complete development needs: convex risk measures and their generation by penalties, mixtures of probability measures, Lagrange duality with Slater's condition over convex sets of measures, and the scaling identity for $\rho^Q$. The duality theorem and the risk-measure layer are reusable beyond this mission. Contributions of any milestone are welcome, as are general convex-duality lemmas that the strong-duality step can import.

Selected references

• A. Ben-Tal, D. Bertsimas, D. B. Brown, A Soft Robust Model for Optimization Under Ambiguity, Operations Research 58(4, Part 2):1220–1234, 2010. https://doi.org/10.1287/opre.1100.0821
• H. Föllmer, A. Schied, Convex measures of risk and trading constraints, Finance and Stochastics 6(4):429–447, 2002. https://doi.org/10.1007/s007800200072
• H. Föllmer, A. Schied, Stochastic Finance: An Introduction in Discrete Time, 2nd ed., de Gruyter, 2004. https://doi.org/10.1515/9783110212075
• D. G. Luenberger, Optimization by Vector Space Methods, Wiley, 1969, Chapter 8.
• D. Bertsimas, D. B. Brown, Constructing Uncertainty Sets for Robust Linear Optimization, Operations Research 57(6):1483–1495, 2009. https://doi.org/10.1287/opre.1080.0695

Motivation

Many engineering and operations problems must guarantee that a system operates safely with high probability, when the uncertain parameters $\tilde z$ are only partially known. A chance constraint asks that the safety condition $S\tilde z \le t$ hold with probability at least $1-\epsilon$ for a tolerance $\epsilon \in (0,1)$. When the distribution of $\tilde z$ is itself uncertain, the distributionally robust version asks this for every distribution in an ambiguity set $\mathcal P$ built from what is known: moments, supports, confidence regions. Two problems then arise: computing the worst-case probability $\inf_{\mathbb P \in \mathcal P}\mathbb P[S\tilde z \le t]$ (uncertainty quantification), and optimizing a design $x$ under the constraint $\inf_{\mathbb P \in \mathcal P}\mathbb P[S(x)\tilde z \le t(x)] \ge 1-\epsilon$ (chance constrained programming).

Hanasusanto, Roitch, Kuhn and Wiesemann (Math. Program. 151, 2015) chart which combinations of ambiguity sets and constraint structures admit exact finite reformulations and which are strongly NP-hard. This mission takes the positive core of that chart: for Markov ambiguity sets (first-order moment information plus a conic support), the worst-case probability is the value of a finite conic program, and an individual chance constraint is equivalent to a finite system of linear conic inequalities.

Timeline. Chebyshev-type bounds for worst-case probabilities under moment information go back to the generalized Chebyshev inequalities of Vandenberghe, Boyd and Comanor (2007), and to the duality theory of moment problems summarized by Shapiro (2001). Wiesemann, Kuhn and Sim (2014) introduced the nested conic ambiguity sets used here to evaluate worst-case expectations. Hanasusanto et al. (2015) applied them to worst-case probabilities of polytopes and to chance constraints, proving Theorem 3 (moment problem reformulation) and Theorem 7 (individual chance constraints over Markov sets), together with strong NP-hardness results, such as Theorem 8, showing that the restrictions cannot be dropped.

Setting

Let $\tilde z \in \mathbb R^P$ be the uncertain parameters and $\tilde u \in \mathbb R^Q$ an auxiliary random vector. Fix $A \in \mathbb R^{K\times P}$, $B \in \mathbb R^{K\times Q}$, $b \in \mathbb R^K$, and a confidence set

$$\mathcal C_1 = \{(z,u) : C_1 z + D_1 u \preccurlyeq_{\mathcal K_1} d_1\},$$

where $C_1 \in \mathbb R^{L_1\times P}$, $D_1 \in \mathbb R^{L_1\times Q}$, $d_1 \in \mathbb R^{L_1}$ and $\mathcal K_1$ is a proper cone (closed, convex, pointed, with nonempty interior); $x \preccurlyeq_{\mathcal K} y$ means $y - x \in \mathcal K$, and $\mathcal K_1^\star = \{y : x^\top y \ge 0\ \forall x \in \mathcal K_1\}$ is the dual cone. The Markov ambiguity set is

$$\mathcal P = \{\mathbb P : \mathbb E_{\mathbb P}[A\tilde z + B\tilde u] = b,\ \mathbb P[(\tilde z,\tilde u) \in \mathcal C_1] = 1\},$$

the case $I = 1$, $\underline p_1 = \overline p_1 = 1$ of the paper's nested set (4).

Two regularity notions enter. $\mathcal C_1$ is essentially strictly feasible if it contains a point satisfying all non-polyhedral constraints of its description strictly. The Slater condition (S) for $I = 1$ requires $b$ to lie in the interior of $\{Az + Bu : (z,u) \in \mathcal C_1\}$.

For the safety system $S\tilde z \le t$ with rows $s_j^\top$, $j \in \mathcal J = \{1,\dots,J\}$, let $\mathcal L = \{j : \exists (z,u) \in \mathcal C_1,\ s_j^\top z > t_j\}$ be the rows that can be violated on $\mathcal C_1$. Problem (17) at $I = 1$ maximizes $b^\top\gamma + \underline p_1\lambda - \overline p_1\kappa$ over $\gamma \in \mathbb R^K$, $\lambda,\kappa \ge 0$, $\phi \in \mathcal K_1^\star$ and, for $j \in \mathcal L$, $\tau_j \ge 0$, $\psi_j \in \mathcal K_1^\star$, subject to $\lambda - \kappa + d_1^\top\phi \le 1$, $A^\top\gamma = C_1^\top\phi$, $B^\top\gamma = D_1^\top\phi$ and, for $j \in \mathcal L$, $\lambda - \kappa + d_1^\top\psi_j - \tau_j t_j \le 0$, $A^\top\gamma + \tau_j s_j = C_1^\top\psi_j$, $B^\top\gamma = D_1^\top\psi_j$.

For an individual constraint ($J = 1$) write $s^\top\tilde z \le t$. System (26) asks for $\beta \in \mathbb R$, $\gamma \in \mathbb R^K$, $\phi,\psi \in \mathcal K_1^\star$, $\tau \ge 0$ with

$$\beta + b^\top\gamma \ge (1-\epsilon)\tau,\ \ \beta + d_1^\top\phi \le \tau,\ \ \beta + d_1^\top\psi \le t,\ \ A^\top\gamma = C_1^\top\phi,\ \ B^\top\gamma = D_1^\top\phi,\ \ A^\top\gamma + s = C_1^\top\psi,\ \ B^\top\gamma = D_1^\top\psi.$$

Formalization targets

Goal: Theorem 7 (p. 18)

Under essential strict feasibility of $\mathcal C_1$, (S), and $\epsilon \in (0,1)$,

$$\inf_{\mathbb P \in \mathcal P}\mathbb P[s^\top\tilde z \le t] \ge 1-\epsilon \iff \text{(26) is solvable}.$$

Milestones

1. Theorem 3 (case $I = 1$), sufficiency. Every feasible point of (17) has objective value at most $\mathbb P[S\tilde z \le t]$ for every $\mathbb P \in \mathcal P$.
2. Theorem 3 (case $I = 1$). Under essential strict feasibility and (S),

$$\inf_{\mathbb P \in \mathcal P}\mathbb P[S\tilde z \le t] = \sup\,(17).$$

3. §5 feasibility claim (with (17), case $I = 1$). Under the same hypotheses and $\epsilon \in (0,1)$, the chance constraint holds iff (17) has a feasible point of value at least $1-\epsilon$.
4. Theorem 7, sufficiency. Any solution of (26) certifies $\mathbb P[s^\top\tilde z \le t] \ge 1-\epsilon$ for all $\mathbb P \in \mathcal P$.

Significance

Theorem 7 turns an individual distributionally robust chance constraint over a Markov ambiguity set into finitely many linear conic constraints whose size is polynomial in the data. Since $s(x)$ and $t(x)$ are affine in the design $x$, the chance constrained program becomes a single conic program, solvable with standard software. The paper notes (p. 18) that, apart from the Wasserstein set, all ambiguity sets of its Section 2.3 are Markov sets or intersections of Markov sets with structural ambiguity sets, and Theorem 8 shows that adding a second confidence set already makes the problem strongly NP-hard, so the theorem marks a precise tractability boundary. Theorem 3 underlies the paper's later results and its §5 heuristic for intractable cases.

All five statements are proved in the literature: the paper defers its proofs to an accompanying technical report. None is machine-checked. A formal proof would supply a verified duality theory for moment problems with conic supports, a reusable bridge between semi-infinite constraints and conic certificates, and a verified basis for the paper's hardness results to be stated against.

Difficulty

The sufficiency halves are weak-duality arguments. The converse directions are not: the worst-case probability is an infimum over an infinite-dimensional set of measures, and the conclusion of Theorem 7 requires the dual certificate to be attained, not just approached. Two separate duality steps must both close without a gap and with attainment: the moment problem against its semi-infinite dual, which is where (S) enters, and each semi-infinite constraint against its conic dual over $\mathcal C_1$, which is where essential strict feasibility enters. The event $\{s^\top z > t\}$ is open, so the semi-infinite constraint must also be passed to its closure. Mathlib has neither a duality theorem for moment problems nor conic strong duality with attainment.

Formalization scope

The mission covers Markov ambiguity sets only ($I = 1$, $\underline p_1 = \overline p_1 = 1$). The general nested case of Theorem 3 is not stated, because the paper does not make (S) explicit for $I > 1$. Symmetry and unimodality information, joint chance constraints and the hardness results are out of scope. The paper's proofs are in a technical report that the mission does not use.

Conventions committed to in Lean:

• Vectors are Fin n → ℝ, the single confidence set is index 0 : Fin 1 of the published DRConvexOpt.Reform.AmbData, and its field c 0 is $d_1$.
• Probabilities are μ.real. The local paperAmbiguitySet reuses the published data and confidence-set definitions and requires integrability only of $A\tilde z+B\tilde u$. This makes the expectation condition void when $K=0$, as the paper states.
• "$\inf_{\mathbb P}\mathbb P[E] \ge 1-\epsilon$" is stated as "$1-\epsilon \le \mathbb P[E]$ for every $\mathbb P \in \mathcal P$", so an empty $\mathcal P$ is not mishandled by sInf ∅ = 0.
• "Coincides with the optimal value" is one real number that is both the greatest lower bound of the probabilities and the least upper bound of the objective values of (17).
• Essential strict feasibility is read as: $\mathcal K_1 = \mathcal K_p \cap \mathcal K_n$ for some polyhedral cone $\mathcal K_p$ and closed convex cone $\mathcal K_n$, with a point of $\mathcal C_1$ whose slack lies in $\mathcal K_p \cap \operatorname{int}\mathcal K_n$.
• The decision $x$ is fixed: $s, t$ stand for $s(x), t(x)$, and the program (2) and the set $\mathcal X$ are not formalized.
• $\epsilon \in (0,1)$, proper $\mathcal K_1$, essential strict feasibility and (S) are explicit hypotheses. The sufficiency halves drop (S) and essential strict feasibility, which they do not need.

Replacing essential strict feasibility by full strict feasibility, adding $\tau > 0$ to (26), or imposing the $\psi_j$-constraints for $j \notin \mathcal L$ would each change the theorem and is ruled out. The hypotheses are jointly satisfiable: $\mathcal C_1 = [-1,1]$, $A = 1$, $b = 0$, $\mathcal K_1 = \mathbb R^2_+$ satisfies all of them, with a nonempty ambiguity set.

A complete development needs conic duality with attainment under partial Slater conditions, Lagrangian duality for moment problems, and the reduction of a measure-valued infimum to finitely supported measures. All three are reusable well beyond this mission, and contributions to any of them are welcome.

Selected references

• G. A. Hanasusanto, V. Roitch, D. Kuhn, W. Wiesemann, A distributionally robust perspective on uncertainty quantification and chance constrained programming, Mathematical Programming 151(1), 35–62, 2015. https://doi.org/10.1007/s10107-015-0896-z
• W. Wiesemann, D. Kuhn, M. Sim, Distributionally robust convex optimization, Operations Research 62(6), 1358–1376, 2014. https://doi.org/10.1287/opre.2014.1314
• A. Shapiro, On duality theory of conic linear problems, in: Semi-Infinite Programming, Kluwer, 135–165, 2001. https://doi.org/10.1007/978-1-4757-3403-4_7
• L. Vandenberghe, S. Boyd, K. Comanor, Generalized Chebyshev bounds via semidefinite programming, SIAM Review 49(1), 52–64, 2007. https://doi.org/10.1137/S0036144504440543
• A. Ben-Tal, A. Nemirovski, Lectures on Modern Convex Optimization, SIAM, 2001. https://doi.org/10.1137/1.9780898718829