Optimization

Motivation

Data-protection laws such as the European Union's General Data Protection Regulation (GDPR) shift control over personal data from firms to consumers: data may be collected and used only with the consumer's consent and only for the purposes she allows. The usual expectation is that such a rule helps consumers and costs firms. Xu, Wang and Zhang (Management Science, forthcoming) examine this expectation in an online retail market where consumer data has two uses. Upside utilization (saved carts, location sharing, recommendations) lowers the consumer's shopping inconvenience. Downside exploitation (monetizing the data) earns the retailer money at the consumer's expense.

For a single retailer the paper finds that the GDPR raises the firm's profit and social welfare (Theorem 1). This mission formalizes the second main result, Theorem 2: once the retailer buys from an upstream supplier, the GDPR can make consumers, the retailer and the supplier all strictly worse off at once. Supply chains are the common structure of online retail, so this matters for anyone assessing a privacy rule by its effect on a single firm.

Setting

A unit mass of consumers values one product at $v>0$. Shopping without the website's data-driven functions costs a consumer an inconvenience $\theta$, uniform on $[0,1]$. The data quality is $\delta\in(0,1)$. A consumer who buys at retail price $p$ and hides her data gets $v-p-\theta$; one who buys and discloses gets

$$v-p-(1-\delta)\theta-r\delta,$$

where $r\ge 0$ is the retailer's monetization intensity. Monetizing at intensity $r$ costs the retailer $cr^2$ ($c>0$) and earns $r\delta$ per disclosed record, so her data profit is $r\delta s-cr^2$ when $s$ consumers disclose. A consumer buys iff her best buying utility is non-negative. The demand is the measure of buyers, and the consumer surplus is $\int_0^1\max\{0,U(\theta)\}\,d\theta$, where $U(\theta)$ is the consumer's best buying utility.

The game has four stages. The retailer decides whether to collect data ($\ell\in\{0,1\}$). The supplier, whose production cost is zero, sets a wholesale price $w$. The retailer sets $p$. Then consumers buy and disclose or hide. The retailer earns $(p-w)\cdot\text{demand}+r\delta s-cr^2$ and the supplier $w\cdot\text{demand}$. Two data policies are compared:

• ℝ mode (retailer-controlled, before the GDPR): after collecting, the retailer chooses $r$ to maximize $r\delta s-cr^2$ given the realized disclosing quantity $s$. Consumers anticipate $s$ correctly: the consumer stage is a rational expectations equilibrium (REE).
• ℂ mode (consumer-controlled, the GDPR): consumers allow upside utilization and block exploitation, so $r=0$ and every buyer discloses.

Without collection both modes give the hiding utility $v-p-\theta$. The paper's constants are

$$\mathcal Z=2c+\delta,\qquad \mathcal M=4c^2(1-\delta)+c\delta(4-3\delta)+\delta^2,\qquad \mathcal F=4c^2(1-\delta)+4c\delta(1-\delta)+\delta^2.$$

Outcomes are those of a subgame-perfect equilibrium (SPE): an REE at every $(\ell,p)$, a retailer price that is a best response at every $(\ell,w)$, a supplier price that is a best response after each $\ell$, and a profit-maximizing $\ell$.

Formalization targets

Goal: Theorem 2 (p. 23)

With $t_1=\frac{4\sqrt{(1-\delta)\mathcal M}}{\mathcal Z}$, $t_2=\frac{4\mathcal M\sqrt{1-\delta}}{\mathcal Z\sqrt{\mathcal F}}$, $t_3=4\sqrt{1-\delta}$, $t_4=\frac{4\sqrt{\mathcal F}}{\mathcal Z}$ and $t_5=\frac{4\sqrt{\mathcal M}}{\mathcal Z}$, SPE exist under both policies, and for every pair of SPE the GDPR's effect on (consumer surplus, retailer profit, supplier profit) is:

$$\begin{array}{ll} v<t_1: & (+,+,+)\ \text{triple win}\\ t_1<v<t_2: & (+,-,+)\\ t_2<v<t_3: & (-,-,+)\\ t_3<v<t_4: & (-,-,-)\ \text{triple lose}\\ t_4<v<t_5: & (+,-,-)\end{array}$$

Every sign is strict.

Milestones

Lemma 1 (the hide / disclose / no-buy partition of the market), display (5) (the retailer's pricing reaction $p(w)$), Propositions 3 and 4 (the equilibria of the two modes), Corollary EC.1 (who collects data under which policy), and Propositions EC.11, EC.12, EC.13 (one column of the theorem each: consumer surplus, retailer profit, supplier profit).

Significance

The result. Theorem 2 is a counterexample to the view that consumer data protection is a transfer from firms to consumers. In the triple-lose interval the GDPR makes the retailer stop collecting data. That removes the inconvenience reduction consumers valued and shrinks the market, so the supplier loses too. Corollary EC.1 shows that the GDPR shrinks the range of valuations in which data is collected at all. The comparison with the single-firm case (Theorem 1) isolates the supplier's wholesale pricing as the source of the harm.

Formalizing it. The paper's arguments are algebraic and piecewise: an REE fixed point with a kink at full market coverage, global maximization of piecewise-quadratic profits, a nested maximization for the supplier, and comparisons of thresholds involving square roots. Several printed statements hold only on part of their stated range. Display (5) fails when the market saturates. The "otherwise" clauses of Propositions EC.11 and EC.13 fail at the points where the retailer is indifferent about collecting. Several proof displays carry typos. A machine-checked development pins the exact ranges and gives a reusable, fully specified model of consumer-data policies in a vertical chain. No machine-checked proof of these results is known.

Difficulty

The obvious argument plugs the printed closed forms into each other and compares them. That argument does not reach the theorem as stated. The theorem is about every subgame-perfect equilibrium of the game, defined from the utilities, not about the closed forms. So the work is to show that the equilibrium is pinned down at every node, including off the path. The REE must be shown unique at every price. The retailer's best response must be derived globally over $p\in\mathbb R$, including the saturated branch, where demand equals 1 and the printed formula (5) is wrong. The supplier's profit $w\cdot\min\{1,(v-w)\mathcal Z^2/(2\mathcal M)\}$ must be maximized across the kink. After that, the five sign patterns rest on a chain of strict inequalities among $t_1,\dots,t_5$ and among the equilibrium profits, which must hold for all $c>0$ and $\delta\in(0,1)$.

Formalization scope

All statements live in the namespace RetailPrivacy.SupplyChain and use one definition file, RetailPrivacy.SupplyChain.Model. That file holds the policy (Policy.R, Policy.C), the constants $\mathcal Z,\mathcal M,\mathcal F$, the hide and disclose utilities, demand and disclosing quantity as Lebesgue measures of sets of $\theta\in[0,1]$, consumer surplus as an interval integral, the REE predicate, strategy profiles with actions at every node, and the SPE predicate. Collection is a Bool. Prices range over all of $\mathbb R$ and the intensity over $[0,\infty)$. The standing assumptions are $c>0$, $\delta\in(0,1)$ and the added $v>0$: the paper leaves $v>0$ implicit, and at $v\le 0$ nothing is sold and every strict claim fails. The consumer-stage definitions are textually identical, up to the namespace, to those of the single-firm mission of this series.

Departures from the print, each disclosed in the item: display (5) is stated on its valid range; Propositions 3(iii) and 4(iii) are stated as comparisons of the retailer's subgame profits; Corollary EC.1 is stated with strict inequalities; and the "otherwise" clauses of EC.11 and EC.13 are stated without the indifference points.

Four formalizations would trivialize the goal, and none is acceptable: comparing the printed closed forms instead of equilibrium outcomes; an "every equilibrium" claim that might be vacuous (the goal asserts existence); profiles that omit off-path actions, which would make the supplier's or the retailer's optimality checks vacuous; and price domains restricted to $[0,v]$ or to unsaturated markets.

The paper's proofs are in its e-companion, Appendix C (pp. ec21–ec38). Useful contributions include the consumer-stage lemmas (REE uniqueness and its closed form), the global best-response computations, and the threshold inequalities, each a self-contained lemma.

Selected references

• F. Xu, X. Wang, F. Zhang, Consumer Privacy in Online Retail Supply Chains, Management Science (forthcoming); author manuscript, version of November 2024. https://doi.org/10.1287/mnsc.2022.01819
• X. Su, F. Zhang, Strategic Customer Behavior, Commitment, and Supply Chain Performance, Management Science 54(10), 2008. https://doi.org/10.1287/mnsc.1080.0886
• Regulation (EU) 2016/679 (General Data Protection Regulation), Official Journal of the European Union L 119, 2016. https://eur-lex.europa.eu/eli/reg/2016/679/oj

Motivation

Social-media influencers earn money by endorsing products to their followers. An endorsement of a product that does not fit the audience brings in money today but costs followers, and followers are also what spreads awareness of the influencer to new people. Nistor, Selove and Villas-Boas (Influencer Authenticity: To Grow or to Monetize, Management Science, 2024) model this trade-off as a deterministic, infinite-horizon, discounted optimal-control problem with a single binary control. In their base model (§3) the optimal policy is to grow first and monetize later: authentic while awareness is small, permanently inauthentic once awareness passes a threshold.

Section 4.2 of the paper asks how this changes when the audience is not permanent: users join and leave the platform, or the influencer covers a topic that interests people only for a while. With follower turnover the influencer never reaches full awareness, and Proposition 3 says that if turnover is fast enough she never monetizes at all. The model gives a testable prediction: influencers on platforms with rapid user turnover, or in product categories with short-lived interest, should stay authentic.

Setting

Time is $t \in [0, \infty)$. There is a unit mass of potential followers, and $A_t \in [0,1]$ is the share of them who are aware of the influencer, starting from $A_0$. At each time she is either authentic or inauthentic. Following Table 1 of the paper:

• authentic: $F_t = A_t$ followers and instantaneous profit $\pi_t = A_t$;
• inauthentic: $F_t = \gamma A_t$ followers and profit $\pi_t = \gamma\varphi A_t$,

with $0 < \gamma < 1$ and $\varphi > 1$. These are the reduced-form parameters of §3.1: a fraction $\gamma$ of aware people follow an inauthentic influencer, who earns $\varphi$ per follower, and authentic profit per follower is normalized to $1$. The paper assumes $\gamma\varphi > 1$ "for the remainder of the paper", so that being inauthentic pays more today.

Potential followers leave and are replaced at a turnover rate $x \in (0, \beta)$, and awareness follows equation (6):

$$\frac{dA_t}{dt} = \beta F_t (1 - A_t) - x A_t ,$$

where $\beta > 0$ is the word-of-mouth rate. Under the always-authentic policy this is the logistic equation $\frac{dA_t}{dt} = A_t(\beta - x - \beta A_t)$, with steady state $\frac{\beta - x}{\beta}$. The influencer maximizes the discounted profit (2), $\int_0^\infty e^{-rt}\pi_t\,dt$, with discount rate $r > 0$.

In the Lean development (namespace InfluencerAuth.Turnover) a policy is a measurable set $S \subseteq \mathbb R$ of the times at which she is inauthentic, so $S = \emptyset$ is "always authentic". IsPath β γ x A₀ S A says $A$ is an admissible awareness path, discountedProfit γ φ r S A is (2) at time $0$, and IsOptimalFrom β γ φ r x A₀ S A says that $(S, A)$ earns at least as much as every measurable policy with any admissible path from the same $A_0$. authValue β x r is the closed form $\overline V$ of Lemma 5, and Condition2 γ φ β r x is

$$\frac{(1-\gamma)x}{r + \beta - x} > \gamma\varphi - 1 .$$

Formalization targets

Goal: Proposition 3 (p. 9)

Under the standing assumptions $0<\gamma<1$, $\varphi>1$, $\gamma\varphi>1$, $\beta>0$, $r>0$, with $0 < x < \beta$ and Condition 2,

$$\forall A_0 \in \Bigl(0, \tfrac{\beta - x}{\beta}\Bigr),\quad \exists A,\ \ (\emptyset, A) \text{ is optimal from } A_0 .$$

The range of $A_0$ is the paper's set of "all feasible levels of awareness". The statement fixes no constant beyond those of Condition 2.

Milestone: Lemma 5 (p. 9)

For $0 < A_0 < 1$ and every admissible always-authentic path $A$ from $A_0$,

$$\int_0^\infty e^{-rt} A_t\,dt = \overline V(A_0) = \int_0^\infty \frac{e^{-rs}}{\frac{\beta}{\beta - x} + \frac{1 - A_0\beta/(\beta - x)}{A_0} e^{-(\beta - x)s}}\,ds .$$

Milestone: display (7) (p. 9)

$$\left.\frac{d\overline V(A)}{dA}\right|_{A = \frac{\beta - x}{\beta}} = \int_0^\infty e^{-(r + \beta - x)s}\,ds = \frac{1}{r + \beta - x}.$$

Significance

Proposition 3 is the paper's result on when the grow-then-monetize pattern of the base model breaks down. Without turnover the influencer always monetizes once she is large enough (Proposition 1, §3). With turnover there is a whole parameter region, given by Condition 2, where monetizing is never optimal. The condition compares the extra current profit from being inauthentic, $\gamma\varphi - 1$, with the awareness lost by being inauthentic, $(1-\gamma)x$, valued at the marginal value of awareness at the steady state, $1/(r+\beta-x)$ from (7).

The proofs are in an online appendix that is not part of the published article, and this result has no machine-checked proof. The mission provides a precise statement of the control problem: optimality over every measurable switching pattern, with the dynamics in integral form. It also gives the closed-form always-authentic value and its derivative as separate targets. A complete development would be one of the first formal optimality proofs for an infinite-horizon, discounted, continuous-time deterministic control problem.

Difficulty

Optimality is claimed against every measurable policy, not only against constant or threshold policies. The natural argument is a verification theorem: show that $\overline V$ satisfies the Hamilton–Jacobi–Bellman inequality on the feasible range, then integrate along an arbitrary competitor path. Condition 2 is stated only at the steady state $(\beta-x)/\beta$, where (7) gives the marginal value of awareness. At a lower awareness level the inequality comparing the two actions involves $\overline V'(A)$ at that level, so it does not follow from Condition 2 alone; it needs control of $\overline V'$ on the whole interval. A competitor path may also switch infinitely often, so its awareness is only absolutely continuous, and the comparison must work almost everywhere. Above the steady state the always-authentic policy is in general not optimal, so any argument must use the restriction $A_0 < (\beta - x)/\beta$.

Formalization scope

• Policies and dynamics. A policy is a measurable Set ℝ. An admissible path is continuous on $[0,\infty)$, starts at $A_0$, stays in $[0,1]$, and satisfies $A_t = A_0 + \int_0^t (\beta f_S(s) A_s(1-A_s) - xA_s)\,ds$ for $t \ge 0$, with $f_S = \gamma$ on $S$ and $1$ off $S$. This is the Carathéodory form of (6). A derivative everywhere is not required, because that would exclude every switching policy. The clause $A_t\in[0,1]$ follows from the equation and is stated to make integrability explicit.
• Objective. discountedProfit is $\int_{(0,\infty)} e^{-rt} p_S(t) A_t\,dt$ with $p_S = \gamma\varphi$ on $S$ and $1$ off $S$; the paper's value from time $t$ is the same object after the shift $s = u - t$. No optimal value is defined as a real supremum; optimality is a comparison with every competitor.
• Hypotheses. The goal carries every standing assumption of the paper: $0<\gamma<1$, $\varphi>1$, $\gamma\varphi>1$, $\beta>0$, $0<x<\beta$. It also assumes $r>0$, which is how "discount rate $r$" is read and which makes (2) finite. The milestones drop $\gamma$, $\varphi$ and their assumptions, which the always-authentic value does not involve.
• No trivialization. The goal produces the optimal path existentially, so it cannot hold for lack of an admissible path. The competitor class is nonempty (the logistic solution is admissible), and every competitor's profit is the integral of a bounded measurable function, so no competitor collapses to the junk value $0$. Widening $A_0$ to $(0,1)$ would make the statement false, not stronger.
• Infrastructure. The development needs the explicit logistic solution with turnover, differentiation under the integral sign for $\overline V$, and a comparison or verification argument for scalar ODEs with measurable coefficients. The verification lemma for discounted bang-bang control of a one-dimensional state is reusable for chunk 1 of this series and for similar marketing-diffusion models. Proofs of either milestone, a sanity proof that the logistic path is admissible, and the verification argument are all welcome contributions.

Selected references

• C. Nistor, M. Selove, J. M. Villas-Boas, Influencer Authenticity: To Grow or to Monetize, Management Science, Articles in Advance, 2024. https://doi.org/10.1287/mnsc.2023.03479
• F. M. Bass, A New Product Growth for Model Consumer Durables, Management Science 15(5), 1969, 215–227. https://doi.org/10.1287/mnsc.15.5.215
• W. H. Fleming, R. W. Rishel, Deterministic and Stochastic Optimal Control, Springer, 1975. https://doi.org/10.1007/978-1-4612-6380-7

Why platform fee design matters

Large online retailers such as Amazon, Walmart and JD.com run a retailer-led marketplace: they sell products on their own account and, on the same storefront, host independent third-party sellers whose sales they tax. How the platform charges those sellers is a live question for competition authorities and for the platforms themselves. Real marketplaces mostly use ad valorem fees (a percentage of the seller's revenue, the "referral fee"), sometimes together with per-item charges. Hervas-Drane and Shelegia (Management Science, 2025) build a model of such a marketplace in which the platform chooses its fee, steers part of the demand, and decides which products to sell itself under a capacity constraint. In their Appendix B.3 they ask whether a per-unit fee would serve the platform better than the ad valorem fee, and answer that it would not: provided the per-unit fee is not a subsidy, the platform sets it to zero (Lemma B.1). The comparison echoes the classical public-finance question of ad valorem versus specific taxation under imperfect competition (Suits and Musgrave, 1953).

Setting

There is a unit mass of products, indexed by their value $v$ to consumers, distributed by a probability measure $\mu$ (the CDF $G$ of the paper) on $[c,\infty)$, where $c>0$ is the common marginal cost of supplying a unit. Each product is its own market, with a unit mass of unit-demand consumers and one potential third-party seller $T$. The monopolist $M$:

• charges an ad valorem fee $f\in[0,1]$ on $T$'s revenue and a per-unit fee $t\ge0$ on each unit $T$ sells;
• steers a share $\lambda\in[1/2,1]$ of the consumers of each product to the seller of his choice (Assumption 1 of the paper); the other $1-\lambda$ buy from the cheapest seller;
• can sell himself at most a fraction $k\in[0,1]$ of all products (assortment capacity).

The game has three stages: $M$ announces $(f,t)$; each $T$ decides whether to enter, then $M$ chooses which products to sell; then prices are set. In a product sold by $T$ alone (SBT) she charges $v$ and $M$ earns $fv+t$. In a product sold by both (SBMT), $M$ serves the steered consumers at $v$ and $T$ charges

$$\bar p_T=\frac{\lambda v+(1-\lambda)(c+t)}{1-f(1-\lambda)}\qquad\text{(B.1)},$$

so $M$ earns $\pi_M^{SBMT}=\lambda(v-c)+(1-\lambda)(f\bar p_T+t)$. A product sold by $M$ alone (SBM) earns him $v-c$. Sellers enter the products of the marketplace set $\mathrm{mp}(c,f,t)=\{v: v(1-f)\ge c+t\}$, that is $v\ge v_T=(c+t)/(1-f)$ when $f<1$.

An allocation is a measurable set $A$ of products with $\mu(A)\le k$. $M$'s profit $\mathrm{profit}_M(A)$ adds $v-c$ over $A\setminus\mathrm{mp}$, $\pi_M^{SBMT}$ over $A\cap\mathrm{mp}$ and $fv+t$ over $\mathrm{mp}\setminus A$, and his profit at fees $(f,t)$ is

$$\Pi_M(k,f,t)=\sup\{\mathrm{profit}_M(A): A\ \text{measurable},\ \mu(A)\le k\}.$$

Formalization targets

Goal: Lemma B.1

For every maximiser $(f^*,t^*)$ of $\Pi_M(k,\cdot,\cdot)$ over $[0,1]\times[0,\infty)$ with $f^*<1$,

$$t^*=0.$$

The goal asserts nothing about existence of a maximiser or about the value of $f^*$; it constrains every maximiser.

Milestones

1. Entry threshold with a unit fee (App. B.3). For $f<1$: $(1-f)v-c-t>0\iff v>v_T$, $\ \bar p_T(1-f)-c-t>0\iff v>v_T$, and $v\in\mathrm{mp}\iff v\ge v_T$, with $v_T=(c+t)/(1-f)$.
2. The fee switch (proof of Lemma B.1). For $0<\varepsilon<t^*$ and $f^*<1$, the fees $t'=t^*-\varepsilon$, $f'=\dfrac{\varepsilon+f^*(c+t^*-\varepsilon)}{c+t^*}$ satisfy $t'>0$, $f^*<f'<1$ and $v_T(f',t')=v_T(f^*,t^*)$.
3. SBT step. $vf'+t'>vf^*+t^*\iff v>v_T(f^*,t^*)$.
4. SBMT step. $\bar p_T(f',t')f'+t'>\bar p_T(f^*,t^*)f^*+t^*\iff v>v_T(f^*,t^*)$.

Significance

The result. Lemma B.1 justifies restricting the platform's instrument to an ad valorem fee, which is how the paper's main analysis (entry modes, the positive optimal fee, fee regulation) proceeds. It also isolates a mechanism: a per-unit fee raises the seller's effective marginal cost and so the price she must charge, while an ad valorem fee with the same entry threshold extracts more from high-value products. The paper notes on p. 19 that once subsidies $t<0$ are allowed the conclusion reverses; that is a different optimisation and not part of this mission.

Formalizing it. The result is proved on paper in a short argument; it has no machine-checked proof. A formal proof must make precise what the paper leaves implicit: that $\Pi_M$ is a supremum over all allocations, re-optimised after a fee change, that the profit gain from the fee switch is strictly positive and survives the supremum, and which degenerate corners (a foreclosed marketplace, full capacity with full steering) must be excluded. The model file is shared in form with the series' two other missions, which formalize the paper's entry-mode theorem (Proposition 2) and the positivity of the optimal ad valorem fee (Lemma 2).

Difficulty

The milestone algebra is elementary. The difficulty is in passing from a pointwise gain to the value function. The fee switch raises $M$'s revenue on every marketplace product above $v_T$ for a fixed allocation; $\Pi_M$ is a supremum over allocations, so a pointwise strict gain does not by itself give a strict gain of the supremum. When $\lambda<1$ the gain is bounded below uniformly over allocations, through the positive mass of $[v_T,\infty)$. When $\lambda=1$ the SBMT gain vanishes, and an allocation that covers almost all marketplace products gains nothing; ruling out that the supremum is approached by such allocations requires comparing with a different fee pair, and uses that $\mu$ has a density and full support. The naive reading, "keep $M$'s allocation fixed and compare", only gives a lower bound on the new value and is not itself a proof of optimality failure.

Formalization scope

Lean conventions, all in the namespace RetailerMarketplace.UnitFee:

• $G$ is a measure μ : Measure ℝ with IsProbabilityMeasure μ, μ (Set.Iio c) = 0, μ ≪ volume (a density), Integrable (fun v => v) μ (finite mean, never stated in the paper but needed for profits to be finite), and full support on $[c,\infty)$, ∀ a b, c ≤ a → a < b → 0 < μ (Set.Ioo a b) (the reading of $G^{-1}$ in the paper's display (3)).
• 0 < c is a standing hypothesis (the paper's $v\in[c,\infty)$ and "$f=1$ such that $v_T\to\infty$" presuppose it); $\lambda\in[1/2,1]$ is Assumption 1; $k\in[0,1]$.
• The marketplace set is $\{v: c+t\le v(1-f)\}$ (entry at zero profit, as in the paper's Lemma 1), never $\{v: (c+t)/(1-f)\le v\}$, which Lean's division by zero would make wrong at $f=1$. vT and the switched fee $f'$ appear only under $f<1$ and $c+t>0$.
• (B.1) and the unit-fee payoffs are definitions: the paper states them without proof as the Stage-3 outcome, and this mission does not formalize a unit-fee pricing game.
• PiM is sSup of the profits of all measurable allocations of mass at most $k$; under integrability the set is nonempty and bounded above, so this is a genuine supremum.
• The goal adds two disclosed restrictions: $f^*<1$ (at $f=1$ no seller enters, $t$ is payoff-irrelevant, and $(1,t)$ with $t>0$ can be optimal) and $(k,\lambda)\ne(1,1)$ (every fee pair is then optimal).

A formalization that fixes $M$'s allocation in the definition of $\Pi_M$, restricts allocations to intervals, takes the supremum over a set that may be unbounded, or replaces "every maximiser has $t^*=0$" by "some pair beats $(f^*,t^*)$" would trivialize or change the statement, and is ruled out.

A complete development needs set integrals over the marketplace set, the bathtub-type comparison of allocations, and order properties of sSup on ℝ. The model file and the milestone lemmas are reusable for any fee-design question in the same model. Proofs of the milestones, of the goal, and of intermediate lemmas about PiM (monotonicity in the fees, strict improvement under the fee switch) are welcome.

Selected references

• A. Hervas-Drane and S. Shelegia, Retailer-Led Marketplaces, Management Science, Articles in Advance, 2025. https://doi.org/10.1287/mnsc.2023.00315 (App. B.3, p. 18).
• D. B. Suits and R. A. Musgrave, Ad Valorem and Unit Taxes Compared, The Quarterly Journal of Economics 67(4):598–604, 1953. https://doi.org/10.2307/1883604

Motivation

Large online retailers such as Amazon sell their own products and, on the same storefront, host third-party sellers who pay a commission on their sales. The owner of such a retailer-led marketplace sets the commission, competes with the sellers it hosts, and can direct inattentive consumers to the offer of its choice. How these levers interact is a central question in the economics of digital platforms and in the current policy debate on platform fees and self-preferencing.

Hervas-Drane and Shelegia (2025) build a model of a monopoly retailer with a marketplace and an assortment capacity constraint, and derive the platform's entry pattern, its fee and the effect of policy interventions. A basic question about the fee is whether a retailer that can sell products itself would ever choose to run its marketplace for free, collecting nothing from the sellers it hosts. This mission formalizes the paper's answer, Lemma 2: it never does.

Setting

There is a unit mass of products, indexed by their consumer valuation $v$. Valuations are distributed according to a probability measure $\mu$ (the CDF $G$ of the paper) on $[c,\infty)$, where $c>0$ is the marginal cost every firm incurs per unit. Each product is an independent market with a unit mass of consumers who each buy one unit at any price $p\le v$.

The monopolist $M$ owns the storefront. For each product there is one third-party seller $T$ who can sell only through the marketplace. The game has three stages.

1. $M$ announces an ad valorem fee $f\in[0,1]$, the share of $T$'s revenue he collects.
2. Each $T$ decides whether to enter; then $M$ chooses which products to sell himself, subject to his capacity $k\in[0,1]$: the set $A$ of products he enters must have $\mu(A)\le k$.
3. Prices are set. $M$ can steer a share $\lambda$ of consumers to the seller of his choice; the remaining $1-\lambda$ buy from the cheapest seller.

The pricing stage (Proposition 1 of the paper) gives per-market payoffs. If $M$ sells alone (SBM) he earns $v-c$. If $T$ sells alone (SBT) she charges $v$ and $M$ collects $fv$. If both sell (SBMT), $T$ charges

$$\bar p_T=\frac{\lambda v+c(1-\lambda)}{1-f(1-\lambda)},$$

and $M$ earns $\pi_M^{SBMT}=\lambda(v-c)+(1-\lambda)f\bar p_T$. Seller $T$ enters exactly the marketplace products $\mathrm{mp}(c,f)=\{v: v(1-f)\ge c\}$ (Lemma 1). Given an allocation $A$, $M$'s profit is

$$\mathrm{profit}_M(A)=\int_{A\setminus\mathrm{mp}}(v-c)\,d\mu+\int_{A\cap\mathrm{mp}}\pi_M^{SBMT}\,d\mu+\int_{\mathrm{mp}\setminus A}fv\,d\mu,$$

and his profit as a function of the fee is the value of his allocation problem,

$$\Pi_M(k,f)=\sup\{\mathrm{profit}_M(A): A\ \text{measurable},\ \mu(A)\le k\}.$$

The paper maintains Assumption 1, $\lambda\ge\tfrac12$: the monopolist steers over half of the consumers.

Formalization targets

Goal: Lemma 2 (p. 7)

For every $f^*\in[0,1]$ with $\Pi_M(k,f)\le\Pi_M(k,f^*)$ for all $f\in[0,1]$,

$$f^*>0 .$$

The statement is about every maximising fee. It does not assert that a maximiser exists, which the paper does not claim in Lemma 2.

Milestone: the derivative in the proof of Lemma 2 (p. 8)

The map $f\mapsto\Pi_M(k,f)$ has a right derivative at $f=0$, and it is strictly positive:

$$\exists\, d>0:\quad \frac{\partial\Pi_M}{\partial f}(k,0^+)=d .$$

Significance

Lemma 2 is the first result of the paper's fee analysis. It says that the fee is an active instrument in every configuration of capacity and steering: even a monopolist who can sell every product himself extracts revenue from the sellers he hosts, because at a zero fee the first-order effect of raising it is positive. The paper's subsequent characterisation of the optimal fee (Proposition 3) and its policy results on fee caps and on banning the retailer from its own marketplace (Propositions 4–6) all take place in the region $f^*>0$ that this lemma secures.

The paper proves Lemma 2 in two sentences, by "inspection of $\Pi_M$". None of the results is formalized elsewhere. The formal development has to make the inspection precise: $\Pi_M$ is the value of an infinite-dimensional allocation problem whose optimal allocation changes with $f$, so its one-sided differentiability at $0$ is an envelope-type statement rather than a calculus exercise. The model layer (the marketplace set, the Proposition 1 payoffs, the allocation problem and its value) is shared, in identical form, with the two companion missions of this series.

Difficulty

$\Pi_M$ is a supremum over measurable sets, not a closed-form function of $f$, so its derivative cannot be read off a formula. Two effects change as $f$ grows from zero: fee revenue rises on every marketplace product, while the products with $c\le v<c/(1-f)$ leave the marketplace and their sellers stop paying fees. At $f=0$ these products pay no fee, so their loss is of second order. Making this precise requires control of the optimal allocation uniformly near $f=0$ and of the mass of the exiting products, using only that $G$ has a density.

The naive argument "keep the allocation optimal at $f=0$ and raise the fee slightly" shows that some positive fee beats $f=0$, but it does not compute the derivative. The claim also fails in one corner: with $k=1$ and $\lambda=1$ the SBMT payoff equals the SBM payoff, the monopolist supplies every product at every fee, and $\Pi_M$ does not depend on $f$.

Formalization scope

The Lean development lives in the namespace RetailerMarketplace.PositiveFee. Valuations are a measure μ : Measure ℝ with IsProbabilityMeasure μ, μ (Set.Iio c) = 0 (support in $[c,\infty)$) and μ ≪ volume (the density $g$). Allocations are arbitrary measurable sets of mass at most $k$, never intervals. $\Pi_M$ is defined as the supremum of profitM over them (PiM); by the paper's Proposition 2 it coincides with the closed form (4), which this mission cannot use because its thresholds $v_L,v_H$ are the conclusion of Proposition 2. The marketplace set is {v | c ≤ v * (1 - f)}, correct also at $f=1$, where it is empty.

Standing and added hypotheses, all disclosed in the item statements:

• $c>0$, implicit in the paper's "$v\in[c,\infty)$" and "$f=1$ such that $v_T\to\infty$";
• $\lambda\in[\tfrac12,1]$ (Assumption 1), $k\in[0,1]$, fees in $[0,1]$;
• $\int|v|\,d\mu<\infty$, needed for the profits to be finite and not stated in the paper;
• $\neg(k=1\wedge\lambda=1)$, the corner where the printed claim is false.

No full-support hypothesis and no existence of an optimal fee are assumed.

Trivializing formalizations are ruled out: the supremum is over a nonempty family that is bounded above under integrability, so PiM is not a junk sSup; and the goal quantifies over every maximiser rather than asserting that some positive fee beats $f=0$.

A complete development needs set integrals over $\mu$, a bathtub-type comparison of allocations, and one-sided derivatives of a value function. The value-function and allocation lemmas are reusable for the companion missions on entry modes and on per-unit fees. Contributions of intermediate lemmas, such as attainment of $\Pi_M(k,0)$ by a top-$k$ allocation, are welcome.

Selected references

• A. Hervas-Drane and S. Shelegia, Retailer-Led Marketplaces, Management Science, Articles in Advance, 2025. https://doi.org/10.1287/mnsc.2023.00315
• A. Hervas-Drane and S. Shelegia, Price competition with a stake in your rival, International Journal of Industrial Organization 84, 102862, 2022 (the paper's source for the simultaneous pricing game). https://doi.org/10.1016/j.ijindorg.2022.102862
• F. Zhu and Q. Liu, Competing with complementors: An empirical look at Amazon.com, Strategic Management Journal 39, 2618–2642, 2018. https://doi.org/10.1002/smj.2932

Why the topology of payment-channel networks matters

The Lightning Network (LN) is a second-layer payment system for Bitcoin. Instead of recording every payment on the blockchain, two parties lock funds in a payment channel and settle many payments off-chain; payments between parties without a common channel are routed along paths of channels. Locking funds is costly, and the amount a channel needs grows with the net flow it carries. Which channel topology supports a given pattern of payments at least total cost is therefore an economic design question for the network's participants.

Guasoni, Huberman and Shikhelman (SSRN 4439190, 2023; published in Management Science, 2024) study this question for a general cost function, assuming only a few qualitative properties derived in their earlier work on channel economics ([GHS22], Lightning Network Economics: Channels). This mission covers §3.1 of the paper, local channel reconfiguration: a relaying node can be bypassed at lower cost, odd cycles are never optimal, and a cost-minimizing network is bipartite with every net flow going from one side to the other. Three companion missions (II–IV of this series) cover hermetization by a routing hub (§3.2) and bounds on the global minimal cost (§3.3).

Setting

Let $V$ be a finite set of nodes. A payment flow is a vector $F=(f_i)_{i\in V}$ of net flows with $\sum_i f_i=0$. A Lightning Network on $V$ is an anti-symmetric real matrix $\Lambda=(\lambda_{u,v})_{u,v\in V}$, $\lambda_{u,v}=-\lambda_{v,u}$, where $\lambda_{u,v}$ is the net flow from $u$ to $v$ in the channel between them and $\lambda_{u,v}=0$ means there is no channel. The network supports $F$ if

$$\sum_{j\in V}\lambda_{i,j}=f_i\qquad\text{for every } i\in V .$$

A channel cost function is $c:\mathbb R\to\mathbb R_{\ge0}$ with

• (MO) $c(x)>c(y)$ for $x>y\ge 0$;
• (SY) $c(-x)=c(x)$;
• (CI) $c(0)=0$;
• (SA) $c(x+y)<c(x)+c(y)$ for $x,y>0$.

The cost of a network is $c(\Lambda)=\tfrac12\sum_{i,j}c(\lambda_{i,j})$, the sum of $c$ over its channels. A network is cost-minimizing for $F$ if it supports $F$ and no Lightning Network on the same node set $V$ that supports $F$ has smaller cost.

The paper's channel notation: $\overrightarrow{uv}^{\lambda}$ is a channel with net flow $\lambda$ from $u$ to $v$, and ${}^{a}\overleftrightarrow{xy}^{b}$ is a channel in which $y$ sends $a$ and $x$ sends $b$, so the net flow from $x$ to $y$ is $b-a$.

Formalization targets

Goal: Corollary 3.3

If $\Lambda$ is cost-minimizing for $F$, there is a set $A\subseteq V$ with $B=V\setminus A$ such that the channel graph ($i\sim j$ iff $\lambda_{i,j}\ne0$) is bipartite with parts $A,B$, and

$$\lambda_{i,j}>0\ \Longrightarrow\ i\in A,\ j\in B .$$

The statement is conditional and does not assert that a minimizer exists.

Milestones

1. Theorem 3.1. For distinct $u,v,w$ and $\lambda_1,\lambda_2>0$, the structure $\overrightarrow{uv}^{\lambda_1},\overrightarrow{vw}^{\lambda_2}$ is not cost-minimizing; if $\lambda_1\le\lambda_2$ the structure $\overrightarrow{uw}^{\lambda_1},{}^{\lambda_1}\overleftrightarrow{vw}^{\lambda_2}$ supports the same flow at strictly lower cost, and if $\lambda_1\ge\lambda_2$ so does ${}^{\lambda_2}\overleftrightarrow{uv}^{\lambda_1},\overrightarrow{uw}^{\lambda_2}$.
2. The in-and-out claim (proof of Corollary 3.2). In an arbitrary network supporting $F$, if $\lambda_{u,v}>0$ and $\lambda_{v,w}>0$ for some $u,v,w$, the network is not cost-minimizing.
3. Corollary 3.2. A network containing a cycle of odd length is not cost-minimizing.
4. Corollary 3.11 (a sibling corollary of Theorem 3.1, not on the path to the goal). If $f_{i_1},f_{i_2}>0>f_{j_1},f_{j_2}$ for distinct $i_1\ne i_2$, $j_1\ne j_2$, no star network is cost-minimizing.

Significance

Corollary 3.3 says that in an optimal Lightning Network every node is a pure sender or a pure receiver, and that no node relays payments. This sits in tension with the observed LN, which is organized around large routing hubs; the paper reconciles the two in §3.2 by allowing new nodes. Corollary 3.11 shows that the star, the intuitive candidate for a cheapest topology, is optimal only with a single net payer or a single net payee.

The results are proved in the paper, with short arguments in its Appendix A, and they have no machine-checked proof. This mission adds a precise version of the model, in which the meaning of "cost-minimizing", the sign conventions and the corrected cost axioms are fixed, and a formal proof of the chain Theorem 3.1 → odd cycles → bipartite structure for an arbitrary cost function satisfying the axioms.

Difficulty

Theorem 3.1 on its own is a two-line computation. The difficulty is in applying it inside an arbitrary network. When $u$ and $w$ already share a channel, adding $\lambda_1$ or $\lambda_2$ to it requires $c(a+b)\le c(a)+c(b)$ for reals of either sign. That inequality is not among the axioms and has to be derived from them. The odd-cycle step needs a pigeonhole argument on channel orientations around a cycle. The bipartite step needs either König's characterization of bipartite graphs or a direct construction of the parts from the flow directions. The naive formalization that re-states Theorem 3.1 only for a network with exactly two channels does not reach the corollaries.

Formalization scope

• The node set is an arbitrary finite type V, not $\{1,\dots,n\}$. The matrix is Λ : V → V → ℝ, because λ is a Lean keyword.
• Sign convention. Support is the row-sum display $\sum_j\lambda_{i,j}=f_i$ of §2.1, under which a net payer has $f_i>0$. The paper's examples (§2, Figure 1, proof of Theorem 3.1) use the opposite sign. Every statement here is invariant under $F\mapsto-F$, and Theorem 3.1 is stated with "the same flow" given by Supports, which is independent of the sign.
• Cost is the form $\tfrac12\sum_{i,j}c(\lambda_{i,j})$, which needs no order on $V$.
• Cost-minimizing compares with networks on the same node set $V$; a network with an added hub (§3.2) is not an alternative.
• Axiom correction (SA). The paper prints (SA) as "$c(x+y)<c(x)+c(y)$ for $x>y\ge0$", which fails at $y=0$, so every theorem would hold vacuously. The formalization uses $x,y>0$, the form verified in Appendix D. The stronger axiom (SA+) is not used in this mission.
• Cycles are injective maps Fin k → V, $k\ge3$ odd, with cyclic successor finRotate k. A channel is a nonzero entry in either direction.
• Bipartite is Mathlib's SimpleGraph.IsBipartiteWith A Aᶜ on the channel graph, with the flow-direction clause stated separately as the stronger content.
• The star is the network whose only channels join each $i\ne h$ to the hub $h$ with net flow $f_i$; Corollary 3.11 assumes $\sum_i f_i=0$.

Trivializing formalizations are ruled out: the cost function is arbitrary subject to the axioms (no $\sqrt{|x|}$ or linear cost); cost-minimization ranges over all networks on $V$, not over a fixed edge set; $V$ is not fixed to three nodes; the in-and-out claim is stated for arbitrary networks; and $A$ and $B$ are complementary, so they cannot overlap.

König's theorem is in Mathlib (SimpleGraph.two_colorable_iff_forall_loop_even) and proved on the platform (FamousTheorems.two_colorable_iff_no_odd_cycle_6b), so it is not posed here. The derived two-sided subadditivity of $c$, and a lemma rerouting a relayed flow inside an arbitrary network, are reusable in the other missions of the series. Contributions of such auxiliary lemmas are welcome.

Selected references

• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Topology, SSRN working paper 4439190, version of February 3, 2023. https://ssrn.com/abstract=4439190 (published in Management Science, 2024, https://doi.org/10.1287/mnsc.2023.03872).
• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels, working paper, 2022 ([GHS22] in the paper; the source of the cost axioms).
• D. Kőnig, Theorie der endlichen und unendlichen Graphen, Akademische Verlagsgesellschaft, Leipzig, 1936.
• J. Poon, T. Dryja, The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments, 2015 (as cited in the paper). https://lightning.network/lightning-network-paper.pdf

Motivation

Inverse optimization asks for the objective of an optimization problem when only its optimal decisions are observed. It was formalized for linear programs by Ahuja and Orlin (Operations Research 2001) and has since been used to infer costs, preferences and utilities from observed choices, for instance in routing, pricing and the imitation of expert planners (see the survey discussion in Chan, Lee and Terekhov, Management Science 2019, and the noisy-data setting of Aswani, Shen and Siddiq, Operations Research 2018).

Besbes, Fonseca and Lobel (arXiv:2106.14015; Operations Research, 2025) study a contextual version: the problems a decision-maker faces change from instance to instance, and the observed expert decisions constrain a fixed but unknown cost vector. Their question is not how to estimate the cost, but which decisions to take so that the loss against the expert is as small as possible in the worst case. This mission formalizes the answer in the offline setting, where a finite data set is given in advance. The text used is the arXiv preprint v3 (1 July 2023); all theorem numbers refer to it.

Setting

Actions live in $\mathbb R^n$ and costs in $\mathbb R^d$, both with the Euclidean norm, and $d\ge2$. The unknown cost $c^\star$ lies on the unit sphere $S^d=\{c:\|c\|=1\}$.

An instance is a pair $(\mathcal X,f)$: a feasible set $\mathcal X\in\mathcal B$, i.e. a nonempty compact subset of $\mathbb R^n$ with diameter at most $1$, and a context function $f\in\mathcal F$, i.e. a $1$-Lipschitz map $\mathbb R^n\to\mathbb R^d$. Given a cost $c$, the forward problem is

$$\psi(c,\mathcal X,f)=\operatorname*{arg\,min}_{x\in\mathcal X} f(x)'c,$$

a set of minimizers.

The offline data are $\mathcal D=\{(\mathcal X_i,f_i,x^\star_i)\}_{i=1}^N$ with $x^\star_i\in\psi(c^\star,\mathcal X_i,f_i)$. The costs compatible with them form the knowledge set

$$C(\mathcal D)=\{c\in S^d:\ c'f_i(x^\star_i)\le c'f_i(x)\ \ \forall x\in\mathcal X_i,\ i=1,\dots,N\}.$$

A policy maps the data and a new instance $(\mathcal X,f)$ to an action $x^\pi\in\mathcal X$, and its regret on the instance is $(f(x^\pi)-f(x^\star))'c^\star$ with $x^\star\in\psi(c^\star,\mathcal X,f)$. The worst-case regret $\mathcal{WCR}^\pi(\mathcal D)$ is the supremum of the regret over $c^\star\in C(\mathcal D)$, $\mathcal X\in\mathcal B$ and $f\in\mathcal F$.

The angle between two vectors is $\theta(c,\hat c)=\arccos\big(c'\hat c/(\|c\|\|\hat c\|)\big)$, with $\theta(c,0)=\theta(0,\hat c)=0$. The uncertainty angle of a set $C$ is

$$\alpha(C)=\inf_{\hat c\in S^d}\ \sup_{c\in C}\ \theta(c,\hat c),$$

and a circumcenter $\hat c(C)$ is a point of $S^d$ attaining the infimum. Geometrically, $\alpha(C)$ is the aperture of the narrowest revolution cone containing $C$ and $\hat c(C)$ is its axis. The circumcenter policy answers an instance with any $x^\pi\in\psi(\hat c(C(\mathcal D)),\mathcal X,f)$. Write $g(a)=\mathbf 1\{a<\pi/2\}\sin a+\mathbf 1\{a\ge\pi/2\}$.

Formalization targets

Goal: Theorem 1 (offline minimax regret), p. 12

For every realizable data set,

$$\mathcal{WCR}^{\pi}(\mathcal D)\ \le\ g\big(\alpha(C(\mathcal D))\big)$$

for the circumcenter policy $\pi$, whatever circumcenter and whatever minimizer it picks. Conversely, for every $\bar\alpha\in[0,\pi]$ there is an information set $C\subseteq S^d$ with $\alpha(C)=\bar\alpha$ on which every policy suffers regret at least $g(\bar\alpha)$ on some instance. The upper bound and the lower bound are one statement.

Milestones

1. Lemma 1 (p. 11). For a proxy cost $c^\pi\in S^d$ and a true cost $c^\star\in S^d$, the worst-case regret over instances and over minimizers $x^\pi\in\psi(c^\pi,\mathcal X,f)$ is attained and equals $g(\theta(c^\star,c^\pi))$:

$$\mathcal L(c^\pi,c^\star)=\begin{cases}\sin\theta(c^\star,c^\pi)&\theta(c^\star,c^\pi)<\pi/2,\\1&\text{otherwise.}\end{cases}$$

2. Lemma 2 (p. 12). Every nonempty $C\subseteq\mathbb R^d$ has a circumcenter; it is unique when $C\setminus\{0\}\neq\emptyset$ and $\alpha(C)<\pi/2$.

Significance

Theorem 1 identifies the minimax offline regret of contextual inverse optimization with a single geometric number of the knowledge set, $\sin\alpha(C(\mathcal D))$ (or $1$), and shows that one explicit policy, acting as if the cost were the circumcenter, attains it uniformly over all instances. It reduces the design of offline policies to computing a circumcenter, and it is the benchmark that the paper's online analysis (§4–§5) compares against: the online policies are judged by how fast they shrink the uncertainty angle.

The results are proved in the paper (App-3–App-9). To our knowledge none of them has a machine-checked proof. Formalizing them yields a verified statement of the minimax value, a reusable notion of uncertainty angle and circumcenter for arbitrary subsets of $\mathbb R^d$, and the exact tightness of the bound, including the regime $\alpha\ge\pi/2$ where nature can force the maximal regret.

Difficulty

The upper bound is not a direct consequence of the definitions: the regret involves an arbitrary compact action set and an arbitrary $1$-Lipschitz context, and the only link between the circumcenter's choice and $c^\star$ is that $x^\pi$ is optimal for the wrong cost. Lemma 1 is where this link is turned into an angle, and its value must be matched exactly, not up to constants. Lemma 2 requires care because the objective $\hat c\mapsto\sup_{c\in C}\theta(c,\hat c)$ is a supremum over an arbitrary, possibly non-closed, set and the angle convention at $0$ breaks continuity. The lower bound must hold for every policy, including ones that exploit tie-breaking, so the hard instance must be chosen after the policy.

Formalization scope

Vectors are EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin d). The angle vecAngle is defined directly with value $0$ when either argument is $0$; Mathlib's InnerProductGeometry.angle (which is $\pi/2$ there) is not used. $\alpha$ is a real infimum over the sphere of a real supremum over $C$; the angles lie in $[0,\pi]$, so both are genuine when $C$ is nonempty. Action sets are nonempty compact sets of diameter at most $1$ (nonemptiness is added: an empty feasible set has no action), contexts are $1$-Lipschitz, and data are indexed by Fin N.

Committed conventions and pins:

• $d\ge2$ is the paper's standing assumption (p. 7). $n\ge1$ is added on Lemma 1 and on Theorem 1: in $\mathbb R^0$ every regret is $0$ and the lower bounds would be false.
• Theorem 1's upper bound assumes realizable data (some $c_0\in S^d$ explains every observation), as the paper's data model does; this makes $C(\mathcal D)$ nonempty.
• Worst-case regrets are never written as real suprema. The upper bound quantifies over every $c^\star\in C(\mathcal D)$, instance, circumcenter, policy minimizer and expert minimizer. Lemma 1 is stated with IsGreatest, and the lower bound of Theorem 1 in attained form, which implies the paper's statement about the supremum.
• In the lower bound the quantifiers are ordered as in the paper: the set $C$, then the policy (any map from instances to feasible actions), then nature's instance.

A formalization that bounds the regret only for one selected minimizer of the forward problem, or that chooses the hard instance before the policy, proves a different and weaker theorem and is excluded.

The development needs: compactness and lower semicontinuity on the sphere (existence of a circumcenter), elementary spherical geometry for the uniqueness and for $\sin\theta$ as the value of a two-point instance, and monotonicity of $g$ on $[0,\pi]$. The angle, uncertainty angle and circumcenter definitions are reusable for the online missions of this series. Proofs of the two lemmas are the natural first contributions.

Selected references

• O. Besbes, Y. Fonseca, I. Lobel, Contextual Inverse Optimization: Offline and Online Learning, arXiv preprint v3, 2023; Operations Research, 2025. https://arxiv.org/abs/2106.14015v3
• R. K. Ahuja, J. B. Orlin, Inverse optimization, Operations Research 49(5):771–783, 2001. https://doi.org/10.1287/opre.49.5.771.10607
• T. C. Y. Chan, T. Lee, D. Terekhov, Inverse optimization: closed-form solutions, geometry, and goodness of fit, Management Science 65(3):1115–1135, 2019. https://doi.org/10.1287/mnsc.2017.2992
• A. Aswani, Z.-J. Shen, A. Siddiq, Inverse optimization with noisy data, Operations Research 66(3):870–892, 2018. https://doi.org/10.1287/opre.2017.1705
• R. Henrion, A. Seeger, Inradius and circumradius of various convex cones arising in applications, Set-Valued and Variational Analysis 18(3–4):483–511, 2010. https://doi.org/10.1007/s11228-010-0150-z

Motivation

Optimal control problems governed by partial differential equations (PDEs) often carry uncertainty in their data, for example a random source term. When the state must stay below a threshold, there are several ways to impose the constraint: with high probability (chance constraints), almost surely, or for every value in a fixed uncertainty set (robust constraints). C. Geiersbach and R. Henrion (arXiv:2306.03965v2, Math. Oper. Res. 2025) derive first-order optimality conditions for all three models for the same elliptic model problem. This mission covers the robust model of §3.2 (pp. 23–25). Its Karush–Kuhn–Tucker (KKT) system has a Radon measure as multiplier, and it is related to the semi-infinite programming view of the same problem.

Robust state constraints are also the limiting case of the almost-sure model: by Lemma 3.4 of the paper (p. 19), an almost-sure constraint and the constraint for every parameter in the support of the distribution coincide when the constraint function is lower semicontinuous in the parameter. The robust multipliers live in $C(\bar D\times\Xi)^*$, which is a space of measures, whereas the almost-sure multipliers of §3.1 contain singular functionals with no such representation.

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$ such that $\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$. Let $\Xi\subset\mathbb R^m$ be compact, let $f_0,\varphi_1,\dots,\varphi_m\in L^2(D)$, and set $f(x,z)=f_0(x)+\sum_{i=1}^m z_i\varphi_i(x)$ (Assumption 1.1, eq. (3)). The solution operator $A^{-1}:L^2(D)\to C(\bar D)$ maps $F$ to the unique weak solution $y\in H^1_0(D)\cap C(\bar D)$ of $-\Delta y=F$ in $D$, $y=0$ on $\partial D$.

For a control $u\in L^2(D)$, a cost $F:L^2(D)\to\mathbb R$ and a threshold $\alpha\in\mathbb R$, the robust problem (63) is

$$\min_{u\in L^2(D)}F(u)\quad\text{s.t.}\quad -\Delta\hat y(\cdot,z)=u+f(\cdot,z)\ \text{in }D,\quad \hat y(\cdot,z)=0\ \text{on }\partial D,\quad \hat y(x,z)\le\alpha\ \ \forall (x,z)\in D\times\Xi.$$

The state is $\hat{\mathcal S}(u)\in C(\bar D\times\Xi)$, $[\hat{\mathcal S}(u)](x,z)=[A^{-1}(u+f(\cdot,z))](x)$, and $\hat{\mathcal G}(u)=\hat{\mathcal S}(u)-\alpha$. The cone is $\hat{\mathcal K}=\{y\in C(\bar D\times\Xi):y\le0\}$ and its polar cone is $\hat{\mathcal K}^-=\{y^*\in C(\bar D\times\Xi)^*:\langle y^*,y\rangle\le0\ \forall y\in\hat{\mathcal K}\}$. The linear part of the state is $[\hat{\mathcal A}^{-1}\hat{\mathcal B}h](x,z)=[A^{-1}h](x)$. The active set is $M(u)=\{(x,z)\in\bar D\times\Xi:[\hat{\mathcal S}(u)](x,z)=\max_{\bar D\times\Xi}\hat{\mathcal S}(u)\}$.

Formalization targets

Goal: Lemma 3.14 refined to (66), pp. 23–24

Let $F$ be convex and continuously Fréchet differentiable, and assume the constraint qualification $0\in\operatorname{int}\{\hat{\mathcal G}(L^2(D))-\hat{\mathcal K}\}$. Then $u^*$ is a solution of (63) if and only if there is a nonnegative finite Borel measure $\mu^*$ on $\bar D\times\Xi$ with, for $y^*=\hat{\mathcal S}(u^*)$,

$$\langle DF(u^*),h\rangle+\int_{\bar D\times\Xi}[A^{-1}h](x)\,d\mu^*(x,z)=0\quad\forall h\in L^2(D),$$ $$y^*\le\alpha\ \text{on }\bar D\times\Xi,\qquad\int_{\bar D\times\Xi}(y^*-\alpha)\,d\mu^*=0.$$

The page derives (66) from the abstract system (65) of Lemma 3.14 (necessity). Sufficiency is the converse direction of Lemma 3.14, since a nonnegative measure defines a multiplier in $\hat{\mathcal K}^-$ by integration. Both directions are part of the goal.

Milestones

1. Lemma 3.13: unique solvability of (63b)–(63c) in $C(\bar D\times\Xi)$ with the bound (64).
2. Lemma 3.14: the abstract KKT system (65) with $\lambda^*\in C(\bar D\times\Xi)^*$.
3. The identification $C(\bar D\times\Xi)^*\cong\mathcal M(\bar D\times\Xi)$ (p. 23): every $\lambda^*$ is integration against a signed measure.
4. Nonnegativity (p. 24): $\lambda^*\in\hat{\mathcal K}^-$ gives a nonnegative $\mu^*$.
5. Lemma 3.15: (66) is equivalent to the scalar-multiplier form (67): $\lambda^*\ge0$ and a probability measure $\tilde\mu$ on $M(u^*)$ with $\langle DF(u^*),h\rangle+\lambda^*\int[A^{-1}h](x)\,d\tilde\mu=0$, $\max y^*\le\alpha$, $\lambda^*(\max y^*-\alpha)=0$.
6. Lemma 3.16: the convex-hull condition (68) is equivalent to the existence of such a $\tilde\mu$.
7. Lemma 3.4: for lower semicontinuous $h$, $h(\xi)\le0$ almost surely if and only if $h\le0$ on the support of the law of $\xi$.

Significance

The goal gives the robust problem a KKT system whose multiplier is a nonnegative measure on $\bar D\times\Xi$ that is carried by the points where the constraint is active. Lemmas 3.15 and 3.16 turn this into a scalar multiplier times a probability measure on the active set, and into a convex-hull condition. These are the forms used by semi-infinite programming algorithms and by discretizations that approximate the measure by finitely many atoms. Together with Lemma 3.4, they say when the KKT system of the almost-sure model (§3.1, with its singular multipliers) can be replaced by the measure-valued system of the robust model.

All statements of the mission are proved in the paper, some by reference: Lemma 3.14's proof refers to the argument of Lemma 3.7, and Lemma 3.16 relies on Phelps's barycenter theorem. None of them is formalized. A formal development would also check two points that the page leaves implicit. Lemma 3.15's proof divides by the total mass of $\mu^*$ and does not treat $\mu^*=0$. Condition (68) is printed per direction $h$, while (67a) needs one measure for all $h$.

Difficulty

The necessity direction of the goal needs a Lagrange multiplier theorem in a Banach space whose constraint cone $\hat{\mathcal K}$ has nonempty interior. The multiplier is a priori only an element of $C(\bar D\times\Xi)^*$, and the Riesz–Markov–Kakutani theorem on the compact space $\bar D\times\Xi$ turns it into a measure. The state $\hat{\mathcal S}(u)$ must also be shown to lie in $C(\bar D\times\Xi)$. Continuity of each slice in $x$ is the regularity of Lemma 1.2 (continuity of $H^1_0$ solutions up to the boundary for class-S domains, from Kinderlehrer–Stampacchia), and joint continuity needs the bound (64), uniform in $z$. Working pointwise in $z$ does not give these: a family of continuous slices need not be jointly continuous without an estimate that is uniform in the parameter.

Formalization scope

$\bar D$ and $\Xi$ are subtypes of Euclidean spaces with CompactSpace instances, so $C(\bar D\times\Xi)$ carries its sup norm. Measures on $\bar D\times\Xi$ are Borel measures; on this compact metric space every finite Borel measure is regular, so "regular Borel (Radon) measure" is IsFiniteMeasure, and nonnegativity (66c) is built into Lean's Measure type. The solution operator is a hypothesis: a bounded linear map $L^2(D)\to C(\bar D)$ such that $A^{-1}F$ is, for every $F$, the weak solution in $H^1_0(D)\cap C(\bar D)$, encoded with the published weak-derivative definitions HunterPDE.Shared.WeakDeriv. The page's "$\le0$ in $D\times\Xi$" is encoded on $\bar D\times\Xi$, the same condition for continuous functions. "Solution" means global minimizer over the feasible set. $L^2(D)^*$ is identified with $L^2(D)$ through the Riesz map. In Lemma 3.16 the clco of (68) is the norm closure of the convex hull, which equals the weak closure.

Added hypotheses: $D$ and $\Xi$ nonempty in Lemmas 3.15 and 3.16 (no probability measure exists on an empty set). Pinned reading: (68) is posed as one inclusion $0\in DF(u^*)+\lambda^*\,\overline{\operatorname{co}}\{u_x:(x,z)\in M(u^*)\}$ in $L^2(D)$, where $u_x$ represents $h\mapsto[A^{-1}h](x)$. The page derives (68) from exactly this inclusion. The closed hull is kept because the page's remark that "co" suffices is not proved in infinite dimension.

Several trivializing formalizations are ruled out. The state operator is tied to the PDE and is never an arbitrary map into $C(\bar D\times\Xi)$. The multiplier carries its sign (a nonnegative measure, or $\lambda^*\in\hat{\mathcal K}^-$) together with complementarity. Optimality is global minimality, not a stationarity condition. All integrands are continuous functions on a compact space against finite measures, so no integral takes a junk value.

A complete development needs elliptic regularity in $C(\bar D)$ for class-S domains, a Banach-space Lagrange multiplier theorem under a Robinson-type constraint qualification, the Riesz–Markov–Kakutani theorem for $C(K)^*$ with signed measures (the platform's FamousTheorems.riesz_markov_kakutani covers positive functionals on $C_c$), and barycenters of probability measures on compact convex sets. The last three are reusable beyond this mission. Contributions of proofs for any of them 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
• F. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983. https://doi.org/10.1137/1.9781611971309
• D. Kinderlehrer, G. Stampacchia, An Introduction to Variational Inequalities and Their Applications, Academic Press, 1980 (SIAM reprint 2000). https://doi.org/10.1137/1.9780898719451
• R. R. Phelps, Lectures on Choquet's Theorem, 2nd ed., Lecture Notes in Mathematics 1757, Springer, 2001. https://doi.org/10.1007/b76887
• H. W. Alt, Lineare Funktionalanalysis, Springer, 2012. https://doi.org/10.1007/978-3-662-08386-4