Operations Research

Learning to bid in first-price auctions

Most online advertising inventory is sold one impression at a time in automated auctions, and since about 2019 the major ad exchanges have moved from second-price to first-price rules: the highest bidder wins and pays its own bid. A bidder in a first-price auction must trade off winning probability against the price paid, and that trade-off depends on the unknown distribution of competing bids. A bidder who takes part in many such auctions can learn that distribution as it goes. The natural yardstick is regret: the expected shortfall of the bidder's cumulative reward relative to an oracle that knows the distribution of competing bids from the start.

Han, Zhou and Weissman (arXiv:2003.09795, Operations Research, 2025) give bidding policies whose expected regret is $\widetilde O(\sqrt T)$ over $T$ auctions, both for iid and for adversarial private values, under the censored feedback that real exchanges provide (only the winning bid is announced). Their Theorem 9 shows that the $\sqrt T$ rate cannot be improved, even in a much easier setting. This mission is that lower bound.

Related results put it in context. With binary feedback (only "won" or "lost"), regret of order $T^{2/3}$ is unavoidable (Kleinberg and Leighton, 2003). With a fixed value, repeated first-price bidding is a pricing problem on a one-dimensional action set whose reward $(1-b)G(b)$ need not be continuous in $b$. Theorem 9 shows that the extra information of the full competing bid buys $\sqrt T$ and nothing better.

Setting

In each round $t=1,\dots,T$ a bidder has a private value $v_t\in[0,1]$, submits a bid $b_t\in[0,1]$, and faces the highest other bid (HOB) $m_t\in[0,1]$, the largest bid of all competitors. The bidder wins when $b_t\ge m_t$, and its payoff is

$$r(v_t,b_t;m_t)=(v_t-b_t)\,\mathbb 1(b_t\ge m_t).$$

The HOBs $m_1,\dots,m_T$ are iid with an unknown cumulative distribution function $G(x)=\mathbb P(m_t\le x)$ on $[0,1]$. No smoothness is assumed: $G$ may have atoms. The expected reward of bid $b$ at value $v$ is $R(v,b)=(v-b)G(b)$, and the regret of the bids $b_1,\dots,b_T$ is

$$R_T(\pi;v)=\sum_{t=1}^T\Bigl(\max_{b\in[0,1]}R(v_t,b)-R(v_t,b_t)\Bigr).$$

A policy $\pi$ chooses $b_t$ from what it has observed before round $t$, and it may use internal randomness. Theorem 9 makes the problem as easy as possible: the value is $v_t=1$ in every round, and the HOB $m_t$ is revealed at the end of every round (full information), rather than only when the bidder loses. A policy is then a rule $b_t=\beta_t(u,m_1,\dots,m_{t-1})$, where $u$ is the policy's internal randomness.

The lower bound uses two HOB laws on $\{1/3,2/3\}$. For $\Delta\in(0,1/4)$, $G_1$ puts mass $\tfrac12+\Delta$ on $1/3$ and $\tfrac12-\Delta$ on $2/3$, and $G_2$ the reverse. $P_i^{\otimes T}$ is the law of $T$ iid HOBs from $G_i$. The total variation distance is $\|P-Q\|_{\mathrm{TV}}=\tfrac12\int|dP-dQ|$, and $D_{\mathrm{KL}}(P\|Q)=\int dP\log\frac{dP}{dQ}$ is the Kullback–Leibler divergence.

Formalization targets

Goal: Theorem 9 (p. 36)

There is an absolute constant $c>0$ such that, for every horizon $T\ge1$,

$$\inf_\pi\sup_G\ \mathbb E_G\bigl[R_T(\pi;v)\bigr]\ \ge\ c\sqrt T,\qquad v_t\equiv 1,$$

where the supremum is over all HOB distributions on $[0,1]$ and the infimum is over all full-information policies, randomized ones included. The constant is left unspecified, as in the paper; the paper's proof gives $c=1/(24e^2)$.

Milestones (App. A–B, pp. 36–38)

1. Oracle rewards (p. 37): with $v_t=1$, $\max_b(1-b)G_1(b)=(1+2\Delta)/3$, $\max_b(1-b)G_2(b)=1/3$ and $\max_b(1-b)(G_1+G_2)(b)=2/3$.
2. Separation (20): for every bid $b_t\in[0,1]$, the instantaneous regrets under $G_1$ and $G_2$ sum to at least $2\Delta/3$.
3. Two-point reduction (21): for every policy, $\tfrac12\mathbb E_{G_1}[R_T]+\tfrac12\mathbb E_{G_2}[R_T]\ge\frac{\Delta T}{3}\bigl(1-\|P_1^{\otimes T}-P_2^{\otimes T}\|_{\mathrm{TV}}\bigr)$.
4. Lemma 12: $1-\|P-Q\|_{\mathrm{TV}}\ge\tfrac12\exp\bigl(-(D_{\mathrm{KL}}(P\|Q)+D_{\mathrm{KL}}(Q\|P))/2\bigr)$.
5. KL computation (p. 37): $D_{\mathrm{KL}}(P_1^{\otimes T}\|P_2^{\otimes T})=T\,D_{\mathrm{KL}}(G_1\|G_2)\le32T\Delta^2$.
6. (22): $1-\|P_1^{\otimes T}-P_2^{\otimes T}\|_{\mathrm{TV}}\ge\tfrac12\exp(-32T\Delta^2)$.

Significance

The theorem shows that the upper bounds of the paper, $C\sqrt T\log^{2.5}T$ for iid values and $C\sqrt T\log^3T$ for adversarial values, are optimal up to logarithmic factors. Because the lower bound holds with a constant value and with every HOB revealed, it is not caused by censoring or by the value process. The $\sqrt T$ comes from the statistical difficulty of locating the maximizer of $(1-b)G(b)$ when $G$ is learned from samples. The same lower bound therefore applies to every richer feedback model and every value model that contains the constant sequence.

The milestones are general tools. Lemma 12 (a symmetrised Bretagnolle–Huber inequality), the product rule for KL divergences of iid laws, and the reduction (21) are the standard steps of Le Cam's two-point method. They recur in essentially every minimax lower bound for bandits and online learning.

The theorem has a complete proof in the paper (App. B). As far as is known it has not been machine-checked, and the needed pieces are only partly in Mathlib: there is a Kullback–Leibler divergence with a chain rule, but at the pinned revision there is no total variation distance and no Bretagnolle–Huber or Le Cam inequality. The work is to formalize the known proof.

Difficulty

The arithmetic is elementary, and the difficulty lies in the probabilistic reduction. The first idea, bounding the regret round by round under a single law, fails: for any fixed $G$ a policy that happens to bid the right point has zero regret, so the lower bound must come from a policy's inability to know which of two laws it faces. Making that precise requires the law of the observed history $(m_1,\dots,m_{t-1})$ under each hypothesis, the identity $\int\min\{dP,dQ\}=1-\|P-Q\|_{\mathrm{TV}}$, and monotonicity of total variation under marginalization from $T$ to $t-1$ coordinates. A randomized policy adds one more integration, over its internal randomness, before the per-round bound applies. The KL step needs the tensorization of KL over product measures and an elementary but explicit logarithmic inequality.

Formalization scope

All declarations live in the namespace FirstPriceLearning.LowerBound.

• Time. Rounds are Fin T; Lean round t is paper time $t+1$.
• HOB law. A measure μG on ℝ. The goal asks for a probability measure giving no mass outside $[0,1]$. The CDF is (μG (Set.Iic x)).toReal, with atoms allowed.
• Reward and regret. $R(v,b)=(v-b)G(b)$, and the oracle term is the supremum over $b\in[0,1]$ (a bounded nonempty family, attained). The regret is the pseudo-regret (3), a sum of expected-reward gaps.
• Policies. A policy carries a probability space $(U,\mu_U)$, with U : Type, for its internal randomness and bid maps bid t : U → (Fin t → ℝ) → ℝ that are jointly measurable with values in $[0,1]$. The history type Fin t → ℝ makes the policy non-anticipating by construction: it cannot read $m_t$ or later HOBs, and it never sees $G$.
• Expectation. An integral over $u\sim\mu_U$ independent of $m\sim G^{\otimes T}$ (Measure.prod with Measure.pi).
• Quantifiers. The goal is stated as $\exists c>0\ \forall T\ge1\ \forall\pi\ \exists G$, which implies the inf–sup form. The constant precedes $T$ and the policy, and the law is chosen after the policy.
• Divergences. KL is Mathlib's InformationTheory.klDiv, valued in $[0,\infty]$. Total variation is defined locally as $\tfrac12\int|p-q|\,d(P+Q)$ with Radon–Nikodym densities. In Lemma 12 the right-hand side is $0$ when a divergence is infinite ($\exp(-\infty)=0$).
• Hard laws. $G_1,G_2$ are explicit two-point measures; the milestones (20)–(22) are stated for $\Delta\in(0,1/4)$ as printed.

Two trivializing formalizations are excluded. A policy that observes $m_t$ (or $G$) before bidding would make the bound false rather than trivial, and the types forbid it. A non-measurable bid map would make the expectation the junk value $0$, and measurability is required. Restricting the policy class to deterministic policies, or reading $(\infty).\mathrm{toReal}=0$ in Lemma 12, would change the theorem and is not done.

Reusable beyond this mission: the total variation distance, Lemma 12, and the tensorization bound for KL. Contributions are welcome at every milestone, especially Lemma 12 and the data-processing step behind (21).

Selected references

• Y. Han, Z. Zhou, T. Weissman, Optimal No-regret Learning in Repeated First-price Auctions, Operations Research, 2025; preprint arXiv:2003.09795v7, 2024. https://arxiv.org/abs/2003.09795
• A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009 (Lemma 2.6). https://doi.org/10.1007/b13794
• J. Bretagnolle, C. Huber, Estimation des densités: risque minimax, Z. Wahrscheinlichkeitstheorie verw. Gebiete 47, 1979. https://doi.org/10.1007/BF00535278
• R. Kleinberg, T. Leighton, The Value of Knowing a Demand Curve: Bounds on Regret for Online Posted-Price Auctions, FOCS, 2003. https://doi.org/10.1109/SFCS.2003.1238232

Reference prices and promotion-insensitive consumers

Consumers judge a price against a reference price, an internal standard formed from the prices they have seen before. A price above the reference is perceived as a loss and a price below it as a gain. When gains and losses weigh differently, the seller's current price shapes tomorrow's demand, and dynamic pricing becomes a sequential decision problem. A central question in this literature is whether the seller should hold a constant price in the long run or keep cycling through high and low prices.

For a single product, classic results show that loss aversion favours constant prices (Fibich, Gavious and Lowengart 2003; Popescu and Wu 2007; Nasiry and Popescu 2011). Hu and Nasiry (2018) showed that individual loss aversion need not carry over to aggregate demand, and under logit demand Jiang, Cao and Shen (2022, Proposition 5) found loss-averse single-product settings in which cyclic pricing is optimal. Guo, Jiang and Shen (2025) study the multi-product version under multinomial logit demand. For general parameters they show that an optimal steady state may fail to exist. This mission formalizes their positive result for one market: consumers who ignore gains, i.e. who do not respond to discounts. The paper motivates this case with luxury goods, where promotions can signal declining prestige.

Setting

A seller offers products $N=\{1,\dots,n\}$. Product $i$ has intrinsic utility $a_i\in\mathbb R$, price sensitivity $b_i>0$ and reference sensitivities $c_i^+\ge0$ (to gains) and $c_i^-\ge0$ (to losses). At price vector $\mathbf p$ and reference price vector $\mathbf r$, the utility of product $i$ is

$$u_i(\mathbf p,\mathbf r)=a_i-b_ip_i+c_i^+(r_i-p_i)_+-c_i^-(p_i-r_i)_+ ,$$

with $(x)_+=\max\{x,0\}$. The multinomial logit market share and the single-period revenue are

$$q_i(\mathbf p,\mathbf r)=\frac{e^{u_i(\mathbf p,\mathbf r)}}{1+\sum_{k\in N}e^{u_k(\mathbf p,\mathbf r)}},\qquad \Pi(\mathbf p,\mathbf r)=\sum_{i\in N}p_i\,q_i(\mathbf p,\mathbf r).$$

Prices and reference prices lie in the admissible box $\mathcal P^n=[0,p_H]^n$ with $p_H>0$. Reference prices follow exponential smoothing with memory $\alpha\in[0,1]$: $\mathbf r^{t+1}=\alpha\mathbf r^t+(1-\alpha)\mathbf p^t$. Revenue is discounted at rate $\beta\in[0,1)$, and the optimal value from reference price $\mathbf r^0$ is

$$V^\star(\mathbf r^0)=\sup_{(\mathbf p^t)_{t\ge0}\subset\mathcal P^n}\sum_{t\ge0}\beta^t\,\Pi(\mathbf p^t,\mathbf r^t).$$

The myopic policy $\mathbf p^m(\mathbf r)$ maximises $\Pi(\cdot,\mathbf r)$ over $\mathcal P^n$. An optimal steady state (Definition 4) is a price $\mathbf p^{\star\star}\in\mathcal P^n$ fixed by the optimal policy: holding the price at $\mathbf p^{\star\star}$ forever is optimal when the reference price is $\mathbf p^{\star\star}$.

Throughout §3–§4 the paper assumes the price ceiling is large enough: $p_H\ge\hat p_H$, where $\hat p_H$ is the root of

$$p=\chi+\sum_{i\in N}\frac{1}{b_i+c_i^+}\exp\big(a_i-b_ip+(b_i+c_i^+)\chi-1\big),\qquad \chi=\max_{i\in N}\frac{1}{b_i+\min\{c_i^+,c_i^-\}} .$$

Under this assumption the ceiling does not bind for the myopic problem.

Consumers are promotion-insensitive when $c_i^+=0$ for every $i$: a price below the reference brings no extra utility, while a price above it is penalised at rate $c_i^-\ge0$.

Formalization targets

Goal: Theorem 6 (p. 24)

If $c_i^-\ge c_i^+=0$ for all $i\in N$, then there exists $\mathbf p^{\star\star}\in\mathcal P^n$ with

$$V^\star(\mathbf p^{\star\star})\le\frac{\Pi(\mathbf p^{\star\star},\mathbf p^{\star\star})}{1-\beta}.$$

This holds for all parameters, memory and discount factors satisfying the hypotheses.

Milestone: the §4.2.1 observation (p. 24)

Under $c_i^+=0$ there is $\mathbf p^{\star\star}\in\mathcal P^n$ that is a fixed point of the myopic policy and whose diagonal pair attains the largest single-period revenue:

$$\Pi(\mathbf p,\mathbf r)\le\Pi(\mathbf p^{\star\star},\mathbf p^{\star\star})\qquad\text{for all }\mathbf p,\mathbf r\in\mathcal P^n .$$

Significance

Theorem 6 is the only general existence result for optimal steady states in the paper. Theorem 4 shows that a single gain-seeking product rules out any optimal steady state. Theorem 5 constrains where a steady state can lie when there is no gain-seeking product, but it does not say that one exists. Theorem 6 settles existence for promotion-insensitive markets, for every number of products and every parameter value: constant pricing is optimal in the long run regardless of parameters and initial reference prices. This holds even though the aggregate logit demand can be more sensitive to gains than to losses in some regions, which is exactly the situation in which earlier general guarantees for constant pricing do not apply.

The result is proved in the paper's online supplement (App. C.5), which is not part of the source file used here. It has no machine-checked proof. Formalizing it requires the first Lean treatment of reference-dependent MNL revenue, with a kinked utility, an outside option and an exponentially smoothed state. It also requires a sequence-form optimal value function for a deterministic infinite-horizon problem with a continuous state. The other missions of this series (myopic dynamics, optimality gap, gain-seeking cycles, steady-state structure, multi- versus single-price policies) use the same objects.

Difficulty

$\Pi(\mathbf p,\mathbf r)$ is neither concave nor monotone in a convenient way. Setting $c^+=0$ does not simply make the reference price irrelevant. Lowering a product's utility raises the logit revenue when that product's price is below the current revenue level, so a larger loss term can help. The joint maximisation over $(\mathbf p,\mathbf r)$ therefore does not reduce to "take $\mathbf r\ge\mathbf p$". The diagonal maximiser must also lie inside the box, and that is where the ceiling assumption $p_H\ge\hat p_H$, which involves the transcendental equation (9), enters. Finally, an optimal steady state is a statement about the infinite-horizon optimum $V^\star$, a supremum over all price sequences. It is not about the myopic policy, and a myopic fixed point is not in general an optimal steady state.

Formalization scope

Products are indexed by Fin n (the paper's product $i$ is index $i-1$), and vectors are Fin n → ℝ. The market shares (3) are defined directly. The Gumbel random-utility derivation is motivation only. Every statement carries the standing hypotheses of §2:

• $b_i>0$ and $c_i^\pm\ge0$ for all $i$;
• $\alpha\in[0,1]$ and $\beta\in[0,1)$ (Theorem 6 only);
• $p_H>0$;
• the ceiling assumption, stated as "some root $\hat p_H$ of (9) satisfies $\hat p_H\le p_H$", where $\chi$ is a supremum over Fin n (zero when $n=0$).

$V^\star$ is the supremum of the discounted revenue over all admissible price sequences rather than over stationary policies. For this deterministic problem with continuous revenue on a compact box the two values coincide. Optimal policies need not be unique, so an optimal steady state is stated as optimality of the constant price path: $\mathbf x\in\mathcal P^n$ and $V^\star(\mathbf x)\le\Pi(\mathbf x,\mathbf x)/(1-\beta)$. The milestone's "myopic fixed point" is stated as "$\mathbf p^{\star\star}$ maximises $\Pi(\cdot,\mathbf p^{\star\star})$ over the box", without fixing a myopic selection.

No trivializing reading is available. On the box $0\le\Pi\le p_H$, so the sequence family is bounded by $p_H/(1-\beta)$ and $V^\star$ is the genuine supremum, not Lean's default value $0$. The hypothesis is $c^+=0$ (no response to gains), not the opposite case $c^-=0$, and the conclusion is existence only, not uniqueness. A complete development needs bounds and continuity for the logit revenue, the joint single-period maximisation behind the milestone, and the comparison of the constant path with arbitrary sequences. The revenue model and the value function are reusable throughout the series. Proofs of either item, and of general facts about the shared model, are welcome.

Selected references

• M. A. Guo, H. Jiang, Z.-J. M. Shen, Multi-Product Dynamic Pricing with Reference Effects Under Logit Demand, Manufacturing & Service Operations Management, 2025; SSRN 4189049 (version of 2024-05-25). https://ssrn.com/abstract=4189049, https://doi.org/10.1287/msom.2024.0801
• G. Fibich, A. Gavious, O. Lowengart, Explicit Solutions of Optimization Models and Differential Games with Nonsmooth (Asymmetric) Reference-Price Effects, Operations Research 51(5):721–734, 2003.
• I. Popescu, Y. Wu, Dynamic Pricing Strategies with Reference Effects, Operations Research 55(3):413–429, 2007.
• J. Nasiry, I. Popescu, Dynamic Pricing with Loss-Averse Consumers and Peak-End Anchoring, Operations Research 59(6):1361–1368, 2011.
• Z. Hu, X. Chen, P. Hu, Dynamic Pricing with Gain-Seeking Reference Price Effects, Operations Research 64(1):150–157, 2016.
• Z. Hu, J. Nasiry, Are Markets with Loss-Averse Consumers More Sensitive to Losses?, Management Science 64(3):1384–1395, 2018.
• H. Jiang, J. Cao, Z.-J. M. Shen, Intertemporal Pricing via Nonparametric Estimation: Integrating Reference Effects and Consumer Heterogeneity, Manufacturing & Service Operations Management, 2022.

Motivation

Consumers judge a price against a reference price formed from the prices they have seen before. A price above the reference is perceived as a loss and depresses demand beyond the plain price effect; a price below it is perceived as a gain and lifts demand. Because today's price moves tomorrow's reference price, a seller who prices many products over time faces a dynamic problem: a discount today raises demand now but lowers the reference price and so weakens demand later.

Whether such a seller should eventually settle on constant prices or keep the prices cycling matters in practice. Stable prices mean stable demand, which simplifies production and inventory planning; cycling prices mean recurring promotions. For a single product with additive demand, Popescu and Wu (2007) showed that loss aversion favours constant prices and gain-seeking favours cycles. Guo, Jiang and Shen (2025) study the multi-product version with multinomial logit (MNL) demand, where products compete for the same customers and each product can have its own type of reference effect. This mission formalizes their characterization of the optimal constant prices.

Setting

There are $n$ products, $i \in N = \{1, \dots, n\}$. Product $i$ has an intrinsic utility $a_i$, a price sensitivity $b_i > 0$, a gain sensitivity $c_i^+ \ge 0$ and a loss sensitivity $c_i^- \ge 0$. Given a price vector $p$ and a reference price vector $r$, the utility of product $i$ is

$$u_i(p, r) = a_i - b_i p_i + c_i^+ (r_i - p_i)_+ - c_i^- (p_i - r_i)_+, \qquad (y)_+ = \max\{y, 0\}.$$

A customer buys product $i$ with the MNL probability $q_i(p, r) = e^{u_i}/(1 + \sum_k e^{u_k})$ and buys nothing otherwise. The single-period revenue is $\Pi(p, r) = \sum_i p_i\, q_i(p, r)$.

Product $i$ is loss-averse if $c_i^+ < c_i^-$, loss-neutral if $c_i^+ = c_i^-$ and gain-seeking if $c_i^+ > c_i^-$; $N_l$, $N_n$, $N_g$ denote the three classes.

Prices and reference prices lie in the box $P^n = [0, p_H]^n$. The reference price evolves by exponential smoothing with memory parameter $\alpha \in [0, 1]$:

$$r^{t+1} = \alpha r^t + (1 - \alpha) p^t .$$

With discount factor $\beta \in [0, 1)$, the optimal value from an initial reference price $r^0$ is

$$V^\star(r^0) = \sup_{(p^t)_{t \ge 0} \subset P^n} \sum_{t \ge 0} \beta^t\, \Pi(p^t, r^t).$$

An optimal steady state is a price vector $p^{\star\star} \in P^n$ that the optimal policy keeps fixed: starting from reference price $p^{\star\star}$, charging $p^{\star\star}$ forever is optimal. The constant path keeps $r^t = p^{\star\star}$ and earns $\Pi(p^{\star\star}, p^{\star\star})/(1 - \beta)$, so the condition reads $V^\star(p^{\star\star}) = \Pi(p^{\star\star}, p^{\star\star})/(1 - \beta)$.

Finally, set

$$\kappa := \frac{1 - \beta}{1 - \alpha\beta} \in (0, 1].$$

Formalization targets

Goal: Theorem 5 (p. 22)

If no product is gain-seeking ($N = N_l \cup N_n$), every optimal steady state satisfies

$$p_i^{\star\star} - \Pi(p^{\star\star}, p^{\star\star}) \in \Bigl[\frac{1}{b_i + c_i^-\kappa},\ \frac{1}{b_i + c_i^+\kappa}\Bigr], \qquad \forall i \in N. \qquad (20)$$

The theorem does not assert that an optimal steady state exists; it describes every one that does.

Corollary 3 (p. 22)

In the same scenario, the equations

$$\Pi = \sum_{i} \frac{e^{a_i - b_i\Pi - b_i/(b_i + c_i^+\kappa)}}{b_i + c_i^-\kappa} \quad (22a), \qquad \Pi = \sum_{i} \frac{e^{a_i - b_i\Pi - b_i/(b_i + c_i^-\kappa)}}{b_i + c_i^+\kappa} \quad (22b)$$

have unique solutions $\Pi^L$ and $\Pi^U$, and every optimal steady state satisfies $\Pi(p^{\star\star}, p^{\star\star}) \in [\Pi^L, \Pi^U]$ and $p_i^{\star\star} \in [\Pi^L + 1/(b_i + c_i^-\kappa),\ \Pi^U + 1/(b_i + c_i^+\kappa)]$.

Corollary 4 (p. 23)

If every product is loss-neutral, $c_i := c_i^+ = c_i^-$, an optimal steady state, if it exists, is unique, satisfies $p_i^{\star\star} = \Pi^{\star\star} + 1/(b_i + c_i\kappa)$, and $\Pi^{\star\star} = \Pi(p^{\star\star}, p^{\star\star})$ is the unique solution of $\Pi = \sum_i (b_i + c_i\kappa)^{-1} e^{a_i - b_i\Pi - b_i/(b_i + c_i\kappa)}$ (24).

Significance

Theorem 5 is the paper's only structural description of the optimal policy's long-run behaviour when it is stable. Computing the optimal policy requires solving a Bellman equation on an $n$-dimensional continuous state space, which is intractable for many products; the theorem replaces that with an explicit per-product markup interval around a single scalar, the steady-state revenue. Corollary 3 turns it into explicit price bounds computable from two one-dimensional equations, so candidate constant prices outside those bounds can be discarded without solving the dynamic program. Corollary 4 shows that pure loss-neutrality pins down the steady state completely, and the comparison with the myopic steady state (markup $1/(b_i + c_i)$) shows how forward-looking pricing shrinks the reference-effect term by the factor $\kappa$. The same paper shows (Theorem 4) that a single gain-seeking product rules out optimal steady states altogether, which is why the hypothesis $N = N_l \cup N_n$ is essential.

The results are proved in the paper's online supplement (Appendix C.4); that supplement is not part of the source file used for this mission, and none of these results has a machine-checked proof. This mission produces formal statements of Theorem 5 and Corollaries 3–4 over a formal definition of the optimal value; a complete development would also produce a Lean theory of the deterministic infinite-horizon pricing problem with reference effects.

Difficulty

An optimal steady state is defined through the value function $V^\star$, which has no closed form, and the revenue is not differentiable exactly where every steady state sits: the utility has a kink at $p_i = r_i$, with loss sensitivity $c_i^-$ on one side and gain sensitivity $c_i^+$ on the other. The obvious approach, writing first-order conditions of the Bellman equation at the fixed point, therefore does not apply directly. A change in today's price also moves every future reference price, so the comparison between a steady state and its alternatives involves the whole discounted future revenue stream rather than a single period, and the factor $\kappa$ in (20) reflects this intertemporal coupling. The myopic analysis of the same paper does not transfer, because the myopic problem is a single-period optimisation over $P^n$ while here optimality is a property of an infinite-horizon value.

Formalization scope

Products are indexed by Fin n (0-based). All vectors are Fin n → ℝ. The shares are defined directly by the MNL formula; the Gumbel random-utility derivation is motivation only. The theorems carry the paper's standing hypotheses explicitly: $b_i > 0$, $c_i^\pm \ge 0$, $\alpha \in [0, 1]$, $\beta \in [0, 1)$, $p_H > 0$, and the standing ceiling assumption of §2.4, $p_H \ge \hat p_H$, where $\hat p_H$ solves equation (9) (CeilingOK: some root of (9) is at most $p_H$).

Conventions committed to:

• $V^\star$ is the supremum of discounted revenue over all price sequences in $[0, p_H]^n$, not over stationary policies; for this deterministic problem the two coincide.
• Optimal policies need not be unique, so an optimal steady state is stated through values: IsOptSteadyState x means $x \in P^n$ and $V^\star(x) \le \Pi(x, x)/(1 - \beta)$. The reverse inequality always holds (the constant path is admissible), so this is the equality above.
• "If there exists an optimal steady state, $p^{\star\star}$ satisfies …" is stated for every optimal steady state.
• "The unique solution of (E)" is split into existence-and-uniqueness (∃!) or "solves (E), and every solution equals it"; no solution is chosen with Classical.choose.
• Corollary 3 is stated in Theorem 5's scenario ($c_i^+ \le c_i^-$), from which the paper derives it.

The hypothesis $N = N_l \cup N_n$ must not be dropped: with a gain-seeking product no optimal steady state exists (Theorem 4), so a statement without it would be vacuously true there. A formalization in which IsOptSteadyState is unsatisfiable by construction (for example a junk value of $V^\star$ above every constant path) would make every statement here empty; the supremum is over a nonempty family bounded by $p_H/(1 - \beta)$.

Needed infrastructure: summability and bounds for discounted revenue streams, one-sided perturbation estimates for the kinked MNL revenue, and comparison arguments for the value function. Contributions of reusable lemmas about the MNL revenue $\Pi$ and about reference-price dynamics are welcome.

Selected references

• M. A. Guo, H. Jiang, Z.-J. M. Shen, Multi-Product Dynamic Pricing with Reference Effects Under Logit Demand, Manufacturing & Service Operations Management, 2025. SSRN version of 2024-05-25: https://ssrn.com/abstract=4189049; DOI: https://doi.org/10.1287/msom.2024.0801
• I. Popescu, Y. Wu, Dynamic Pricing Strategies with Reference Effects, Operations Research 55(3), 2007. https://doi.org/10.1287/opre.1070.0393
• D. McFadden, Conditional Logit Analysis of Qualitative Choice Behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, 1974, pp. 105–142.

Motivation

A recurring proposal in the policy debate on dominant digital platforms is to make competing platforms interoperable, so that users of one service can interact with users of another; the EU Digital Markets Act (Regulation (EU) 2022/1925, Article 7) imposes such an obligation on gatekeepers' messaging services. The economic case is that users then enjoy network effects across platforms, not only within their own. The counter-argument is that a network shared with rivals is a weaker competitive weapon, so platforms may compete less hard and users may lose through higher fees.

Ekmekci, White and Wu, Platform Competition and Interoperability: The Net Fee Model (Management Science, 2025), resolve this trade-off in a tractable model of platform competition with strong network effects. Their device is the net fee: the membership fee net of the interaction charges a platform extracts once users have joined. Competition in net fees turns platform demand into an ordinary discrete-choice demand, so equilibria can be characterized by pricing formulas. This mission formalizes their Proposition 7(b): with symmetric platforms, more interoperability lowers the equilibrium net fee, except in a duopoly without an outside option, where it has no effect.

Setting

There are $J \ge 2$ ex ante identical platforms, indexed by $j$, and one side of users. Platform $j$ charges a net fee $t^j \in \mathbb R$. A user either joins one platform or takes an outside option whose weight is $w = e^{z} \ge 0$; $w = 0$ means there is no outside option. Under Logit demand (13), platform $j$'s user mass at the profile $t = (t^1,\dots,t^J)$ is

$$n^j(t) = \frac{e^{-t^j}}{w + \sum_{k} e^{-t^k}}.$$

Every platform has marginal cost $c$, and each user values each other user on the same platform at $\gamma$ (the network effect). The degree of interoperability $\lambda \in [0,1]$ lets a user value each user of every other platform at $\lambda\gamma$ (19). Platform $j$ extracts all interaction utility through its total price, so its profit is

$$\pi^j(t) = \Big(t^j + \gamma n^j + \lambda\gamma \sum_{k\ne j} n^k - c\Big)\, n^j .$$

A profile $t$ is a Nash equilibrium in net fees if no platform can raise its profit by changing its own net fee to any other real number. A symmetric equilibrium is an equilibrium in which every platform charges the same net fee. The diversion ratio $\varphi^j = \sum_{k\ne j} n^k/(1-n^j)$ (32) is the share of the users a platform gains by a small fee cut that come from rival platforms rather than from the outside option.

When all platforms charge $\tau$, each has share $n(\tau) = e^{-\tau}/(w + J e^{-\tau})$ and diversion ratio $\varphi(\tau) = (J-1)n(\tau)/(1-n(\tau))$. The proof of Proposition 7 introduces

$$\xi(\tau;\lambda) = -\tau + c + \frac{1}{1-n(\tau)} - 2\gamma n(\tau) - \gamma\lambda\big(J-1-\varphi(\tau)\big) n(\tau).$$

Formalization targets

Goal: Proposition 7(b), Logit case

Let $0 < \gamma \le 27/8$ and $0 \le \underline\lambda < \overline\lambda \le 1$, and suppose the constant profile $\underline t$ is a Nash equilibrium under $\underline\lambda$. Then

$$J \ge 3 \text{ or } w > 0 \;\Longrightarrow\; \exists\, \overline t < \underline t:\ (\overline t,\dots,\overline t) \text{ is a Nash equilibrium under } \overline\lambda,$$ $$J = 2 \text{ and } w = 0 \;\Longrightarrow\; (\underline t,\underline t) \text{ is a Nash equilibrium under } \overline\lambda.$$

Milestones

1. The Logit diversion ratio (32) is independent of the platform's own fee, and equals the ratio of rival-demand to own-demand derivatives.
2. Proposition 7(a): at a symmetric equilibrium, $\tau = c + \frac{1}{1-n} - \big(2 + \lambda(J-1-\varphi)\big)\gamma n$, the Logit form of (21).
3. For $\gamma \le 27/8$, the first-order condition (33) gives a global best response (Appendix E.1.3 with (36)).
4. Symmetric equilibria are the zeros of $\xi(\cdot;\lambda)$, the converse direction under $\gamma \le 27/8$.
5. $\xi(\tau;\overline\lambda) = \xi(\tau;\underline\lambda) - \gamma(\overline\lambda-\underline\lambda)(J-1-\varphi)n$, with $J - 1 - \varphi > 0$ unless $J = 2$ and $w = 0$.
6. $\xi(\tau;\lambda) > 0$ for every $\tau < c - 2\gamma - \gamma\lambda(J-1)$.

Significance

The result separates two forces that interoperability sets off. Platforms extract the new off-network utility of the users they add, which pushes them to compete harder for users; and part of the users they add are diverted from rivals, which erodes the off-network revenue they draw from existing users. Proposition 7(b) says the first force wins whenever there is an outside option or at least three platforms, so users gain twice from interoperability: wider network effects and lower net fees. In the knife-edge duopoly without an outside option the forces cancel exactly. The authors read the result, together with their Proposition 6 on dominance, as "reason for optimism about the effects of increasing interoperability" (p. 23) and as an encouraging view of interoperability regulation (p. 3).

The paper proves the result on pp. 52–53. No machine-checked version of it, or of any result of the paper, exists. The formalization adds three things: a fully specified equilibrium notion (global Nash, not a first-order condition); an explicit verification that first-order conditions are sufficient in the parameter range used; and a precise statement of the case split, which the paper phrases through $\varphi^j = 1$ and here is stated through the primitives $J$ and $w$.

Difficulty

The proof reduces the comparison of equilibria to the zeros of the one-variable function $\xi$, and then applies the intermediate value theorem. Two steps carry the substance. First, every symmetric equilibrium must satisfy $\xi = 0$: this needs the first-order condition for a maximum of a profit function that depends on the deviating platform's fee through every platform's share. Second, every zero of $\xi$ must be a Nash equilibrium: this is false for large network effects, since profit can then fail to be concave and a platform can profit from a large deviation. The paper establishes sufficiency through concavity of profit in the platform's own share, which needs $2\gamma(1-\lambda\varphi^j) \le 1/(n(1-n)^2)$ for all shares and the independence of $\varphi^j$ from the platform's own fee. Identifying equilibria with solutions of the pricing formula, without this argument, proves a statement about stationary points, not about equilibria.

Formalization scope

• Logit, one side, symmetric primitives. Proposition 7 is stated in the paper for general demand. This mission formalizes the Logit case (13), the specification of the paper's §5–6, with one side, common $c$ and common $\gamma$. The proof of 7(b) writes the Logit markup $1/(1-n^j)$, and its general-demand sufficiency argument is a sketch (Appendix E.1.3). General demand with Assumptions A1–A2, several sides, platform-specific parameters and the microfoundation of Appendix A are out of scope.
• Outside option. $w = e^{z} \ge 0$ is a real parameter; "no outside option" is $w = 0$, not a limit.
• Added hypotheses. $\gamma > 0$ (the paper's "as long as network effects are positive", p. 25; with $\gamma < 0$ the comparison reverses) and $\gamma \le 27/8$ (the bound (36), Proposition 2′'s 3.375, under which the paper's first-order sufficiency holds). The interoperability levels lie in $[0,1]$ as in part (a).
• Equilibrium. IsEquilibrium is the global Nash condition over every deviation $s \in \mathbb R$. A formalization in which equilibrium means "the pricing formula holds", or in which the interoperability term $\lambda\gamma\sum_{k\ne j}n^k$ is dropped from profit (so that $\lambda$ affects nothing), would make the goal trivial and is not this theorem.
• Lean conventions. Platforms are indexed by Fin J; $\lambda$ is called lam; $J$ is cast to $\mathbb R$ in the symmetric closed forms nSym, phiSym, xi.
• Infrastructure. The proofs need the Logit derivatives, a one-variable concavity argument through the change of variables $t \mapsto n^j$ (a strictly decreasing bijection $\mathbb R \to (0,1)$), the bound $\min_{n\in(0,1)} 1/(n(1-n)^2) = 27/4$, continuity of $\xi$ and Mathlib's intermediate value theorem. The Logit and concavity lemmas are shared with the other two missions of this series and are reusable for any Logit oligopoly with network effects. Proofs of any milestone, and alternative routes to the goal, are welcome.

Selected references

• M. Ekmekci, A. White, L. Wu, Platform Competition and Interoperability: The Net Fee Model, Management Science, 2025; accepted working-paper version of December 12, 2024. https://doi.org/10.1287/mnsc.2023.02810
• S. P. Anderson, N. Erkal, D. Piccinin, Aggregative Games and Oligopoly Theory: Short-run and Long-run Analysis, The RAND Journal of Economics 51(2), 470–495, 2020.
• A. Caplin, B. Nalebuff, Aggregation and Imperfect Competition: On the Existence of Equilibrium, Econometrica 59(1), 25–59, 1991. https://doi.org/10.2307/2938238
• Regulation (EU) 2022/1925 (Digital Markets Act), Article 7. https://eur-lex.europa.eu/eli/reg/2022/1925/oj

Motivation

Linear opinion models describe how individuals in a social network revise their views by averaging what their neighbours think, what external media tell them, and what they themselves believed a moment ago. The last ingredient, an autoregressive or memory term, appears in the Friedkin–Johnsen family of models and in its stochastic variants. Fraiman, Lin and Olvera-Cravioto (arXiv:2209.00969, Mathematics of Operations Research, 2025) study such a model on large directed random graphs with vertex attributes and random media signals. They show that the opinion of a typical vertex has a stationary law that is described, in the large-graph limit, by a recursion on a marked Galton–Watson tree.

A natural question is what the memory term does to that stationary law. Simulations in the paper (Section 5.4, Figures 6–7) suggest that memory smooths individual trajectories and makes the stationary opinion less dispersed. Proposition 6 turns this into a theorem: on a Galton–Watson limit, the stationary opinion with memory has variance at most that of a no-memory recursion that keeps the same relative weights of neighbours and media.

Setting

Nodes of the limiting tree are labelled by finite words $\mathbf i=(i_1,\dots,i_k)$, the root being $\varnothing$; $(\mathbf i,j)$ is the $j$-th child of $\mathbf i$. Each node carries a mark $\mathcal X_{\mathbf i}$, from which the model reads an in-degree $\mathcal N_{\mathbf i}$, weights $\mathcal C_{(\mathbf i,1)},\mathcal C_{(\mathbf i,2)},\dots\in[0,1]$ summing to $c$ when $\mathcal N_{\mathbf i}\ge1$, and an internal opinion $\mathcal Q_{\mathbf i}\in[-1,1]$. Parameters satisfy $c\in[0,1)$, $d\in(0,1]$, $c+d\le1$. The tree is a delayed marked Galton–Watson tree: marks are independent, and all non-root marks have the same law.

Each node receives media signals $\mathcal Z_{\mathbf i}^{(k)}\in[-1,1]$, $k\ge0$, conditionally i.i.d. given its mark and conditionally independent across nodes, and the external signal

$$\mathcal W_{\mathbf i}^{(k)}=d\,\mathcal Z_{\mathbf i}^{(k)}+\mathcal Q_{\mathbf i}\Big(c-\sum_{j=1}^{\mathcal N_{\mathbf i}}\mathcal C_{(\mathbf i,j)}\Big).$$

The general recursion (8) and the no-memory recursion (9) are

$$\mathcal M_{\mathbf i}^{(k+1)}=\sum_{j=1}^{\mathcal N_{\mathbf i}}\mathcal C_{(\mathbf i,j)}\mathcal M_{(\mathbf i,j)}^{(k)}+\mathcal W_{\mathbf i}^{(k)}+(1-c-d)\mathcal M_{\mathbf i}^{(k)},\qquad \mathcal R_{\mathbf i}^{(k+1)}=\sum_{j=1}^{\mathcal N_{\mathbf i}}\frac{\mathcal C_{(\mathbf i,j)}}{c+d}\mathcal R_{(\mathbf i,j)}^{(k)}+\frac{\mathcal W_{\mathbf i}^{(k)}}{c+d}.$$

Writing $\Delta$ for the linear map on the right-hand side without the signal, the limiting root opinion is the series $\sum_{s\ge0}(\Delta^s\mathcal W^{(s)})(\varnothing)$; it is $\mathcal M^*$ for (8) and $\mathcal R^*$ for (9). The moments

$$\rho_1^*=E\Big[\sum_{i=1}^{\mathcal N_\varnothing}\mathcal C_i\Big],\quad \rho_1=E\Big[\sum_{i=1}^{\mathcal N_1}\mathcal C_{(1,i)}\Big],\quad \rho_2^*=E\Big[\sum_{i=1}^{\mathcal N_\varnothing}\mathcal C_i^2\Big],\quad \rho_2=E\Big[\sum_{i=1}^{\mathcal N_1}\mathcal C_{(1,i)}^2\Big]$$

and the series $p_m=\sum_{s\ge0}\binom{s+m}{s}^2(1-c-d)^{2s}(c+d)^{2(m+1)}$ enter every formula below.

Formalization targets

Goal: Proposition 6

If $c,d>0$, $c+d<1$ and $P(\mathcal N_\varnothing>0)=P(\mathcal N_1>0)=1$, then

$$\mathrm{Var}(\mathcal M^*)\le\mathrm{Var}(\mathcal R^*).$$

The goal asserts the comparison only, not the closed forms, so it is the weakest statement the paper's computation supports.

Milestones

1. Theorem 8 (pp. 32–33): closed forms for $E$ and $\mathrm{Var}$ of the limiting opinions of the root and of a neighbour, in terms of $\rho_1^*,\rho_1,\rho_2^*,\rho_2$, $\mathcal Y_{\mathbf i}=E[\mathcal W_{\mathbf i}\mid\mathcal X_{\mathbf i}]$, $\mathcal V_{\mathbf i}=\mathrm{Var}(\mathcal W_{\mathbf i}\mid\mathcal X_{\mathbf i})$ and a Geometric expectation of $p_T$.
2. Remark 10.2 (pp. 33–34): the specialisation to the Section 5.1 signals with $\mathcal N_\varnothing,\mathcal N_1>0$ a.s.; it expresses $\mathrm{Var}(\mathcal M^*)$ through $\mathrm{Var}(\mathcal Z)$ and $E[\mathrm{Var}(\mathcal Z\mid\mathcal X)]$.
3. (15) (p. 31): $\mathrm{Var}(\mathcal R^*)=\frac{d^2}{(c+d)^2}\mathrm{Var}(\mathcal Z_\varnothing)+\frac{\rho_2^*d^2}{(c+d)^2((c+d)^2-\rho_2)}\mathrm{Var}(\mathcal Z_1)$.
4. Coefficient bound (pp. 31–32): $p_m\in(0,1)$ and $\frac{1}{1-\rho_2}E[(c+d)^{-2(T+2)}p_{T+1}]\le\frac{1}{(c+d)^2((c+d)^2-\rho_2)}$, $T$ Geometric with success probability $1-\rho_2$.

Additional item (not a milestone): Lemma 9 (p. 34), the mean and variance of $\mathcal R^{(k+1)}$ for the general recursion with general signals, started from $0$, at the root and at non-root nodes; it is the finite-time step behind Theorem 8.

Significance

The proposition isolates the effect of memory on dispersion: with the same proportional influence of neighbours and media, adding inertia never increases the variance of the stationary opinion of a typical individual. In the paper's interpretation, slower updating produces less polarised stationary opinions, which matters when the model is used to compare network interventions or media exposure. Theorem 8 and Lemma 9 go further and give exact first and second moments of the stationary opinion on Galton–Watson limits with possibly stubborn (in-degree zero) vertices and arbitrary mark-dependent signals; such closed forms are rare for models of this kind.

The results are proved in the paper. None of them has a machine-checked proof. Formalizing them produces a Lean development of moment computations for linear recursions on marked Galton–Watson trees (conditioning on independent subtrees, laws of total variance along generations, and negative-binomial series), which is reusable for other smoothing-transform and branching-recursion problems. Two printed slips are corrected along the way (see Formalization scope).

Difficulty

The difficulty is not the comparison itself but the exact variance of $\mathcal M^*$. With memory, a signal emitted at time $s$ by a node at depth $l$ reaches the root with coefficient $\binom{s}{l}(1-c-d)^{s-l}$ times the product of weights along the path, so its contributions spread over all later times. The variance then involves the squared coefficients $\sum_s\binom{s}{l}^2(1-c-d)^{2(s-l)}$, which do not factor as the coefficients do in the no-memory case. The obvious route, comparing the two recursions pathwise or coupling them, fails: the two root opinions are not ordered, and only their variances are. The comparison emerges only after the conditional variances of the media signals are separated from the variance of their conditional means, and after the Geometric average of $p_{T+1}$ is bounded.

Formalization scope

• Model. The tree is encoded with Ulam–Harris labels List ℕ (0-based children; the paper's node $1$ is [0]), and marks are read through measurable maps $\mathcal N$, $\mathcal C$, $\mathcal Q$ on a measurable space $M$. The media signals are $\zeta(\mathcal X_{\mathbf i},U_{\mathbf i}^{(k)})$ with i.i.d. uniforms independent of the marks. This quantile representation is equivalent in law to the paper's conditional i.i.d. assumption and is the paper's own device (p. 25). The general signals of Theorem 8 and Lemma 9 are $\xi(\mathcal X_{\mathbf i},U_{\mathbf i}^{(k)})$ with $|\xi|\le d+c-\sum_j\mathcal C_{(\mathbf i,j)}$.
• Limit tree, not graph sequence. The paper's statements assume "the assumptions of Theorem 2" with the Galton–Watson tree as local limit. Those assumptions only identify the tree's root opinion with the large-graph typical opinion; every claim here is about the tree. All statements are made on the tree under the Section 5 standing assumptions, which is a generalization.
• Conventions. Limiting opinions are the absolutely summable series $\sum_s(\Delta^s\mathcal W^{(s)})(\mathbf i)$; $E$ is the Bochner integral, Var/Cov are Mathlib's variance/covariance, conditional moments are condExp/condVar given $\sigma(\mathcal X_{\mathbf i})$; the Geometric expectation is the explicit series $\sum_k\rho^k(1-\rho)g(k)$.
• Corrections. Remark 10.2's printed mean lacks a factor $d$; the corrected mean is stated. Lemma 9's root variance is stated for $k\ge1$ (it fails at $k=0$) and its root mean under $\rho_1>0$. Equation (15) is Proposition 4 applied to recursion (9) after rescaling.
• No trivialization. Every random variable involved is bounded, so no variance, integral or series takes a junk value; the denominators $c+d-\rho_1$, $(c+d)^2-\rho_2$, $1-\rho_2$ are positive under the standing assumptions, and the goal's hypotheses are satisfied by, e.g., the path tree ($\mathcal N\equiv1$, $\mathcal C\equiv c$), where both variances are positive.
• Infrastructure. Useful contributions include: summability and boundedness of the opinion series; independence of subtrees in Ulam–Harris encodings; the law of total variance (integral_condVar_add_variance_condExp in Mathlib); the identities $\sum_s\binom{s}{l}x^{s-l}=(1-x)^{-(l+1)}$ and the negative-binomial bound $p_m<1$.

Selected references

• N. Fraiman, T.-C. Lin, M. Olvera-Cravioto, Opinion dynamics on directed complex networks, arXiv:2209.00969v2, 2024; Mathematics of Operations Research, 2025. https://arxiv.org/abs/2209.00969
• N. E. Friedkin, E. C. Johnsen, Social influence and opinions, Journal of Mathematical Sociology 15(3–4), 1990. https://doi.org/10.1080/0022250X.1990.9990069
• M. H. DeGroot, Reaching a consensus, Journal of the American Statistical Association 69(345), 1974. https://doi.org/10.1080/01621459.1974.10480137

Motivation

Stochastic matching with patience models kidney exchange, online dating and labour platforms: every edge of a graph is present only with some probability, the only way to learn whether it is present is to probe it, and a probed edge that turns out to be present must be added to the matching. Each vertex $v$ also has a patience $t_v$, a limit on how many of its edges may be probed. The goal is a probing strategy whose expected matched weight is a large fraction of what the best adaptive strategy obtains. Since the best strategy is hard to compute, algorithms are compared with the value of a linear program (LP (3) below), which upper-bounds every probing strategy (Bansal, Gupta, Li, Mestre, Nagarajan, Rudra, Algorithmica 2012).

Bansal et al. gave a $1/3$-approximation for stochastic bipartite matching. Brubach, Grammel, Ma, MacRury and Srinivasan (Mathematics of Operations Research, 2025; arXiv:2106.06892v3) single out the case in which one side of the bipartition has unit patience, $t_u=1$ for every $u\in V_1$. This case contains "Problem A" of Hikima et al. (AAAI 2021), whose approximation ratio transfers to their integrated two-stage problem ISPCB; Hikima et al. obtained $1/3$ from the bound of Bansal et al. For the special case in which one side has arbitrary patience and the other unlimited patience, Borodin and MacRury had already obtained the same $(1-1/e)$ guarantee through an online problem.

Setting

Let $G=(V_1\cup V_2,E)$ be a finite bipartite graph; $\delta(x)$ denotes the set of edges at a vertex $x$. Each edge $e$ has a weight $w_e\ge 0$ and an activation probability $p_e\in[0,1]$, independently across edges. Every $u\in V_1$ has patience $1$; every $v\in V_2$ has a patience $t_v\in\mathbb N\cup\{\infty\}$.

LP (3). A vector $(y_e)_{e\in E}$ is feasible when $0\le y_e\le 1$ and, for every vertex $x$,

$$\sum_{e\in\delta(x)}y_ep_e\le 1,\qquad \sum_{e\in\delta(x)}y_e\le t_x .$$

Write $z_e=y_ep_e$ and $\mathsf{OPT}(v)=\sum_{e\in\delta(v)}w_ez_e$.

The algorithm. A dependent rounding (Gandhi, Khuller, Parthasarathy, Srinivasan, J. ACM 2006) turns $y$ into a random set $\hat E=\{e:Y_e=1\}$ of rounded edges with $\Pr[Y_e=1]=y_e$, at most one rounded edge at each $u\in V_1$, at most $t_v$ at each $v\in V_2$, and the negative correlation property (2): for $v\in V_2$, $S\subseteq\delta(v)$ and $b\in\{0,1\}$,

$$\Pr\Big[\bigcap_{e\in S}(Y_e=b)\Big]\le\prod_{e\in S}\Pr[Y_e=b].$$

In the rounded graph every $v\in V_2$ is the centre of a star. Each $v$ probes its rounded edges in decreasing order of weight and is matched to the first active one; $W(v)$ is the weight of that edge ($0$ if none), and $\mathbb E[\mathsf{ALG}]=\mathbb E[\sum_{v\in V_2}W(v)]$.

Formalization targets

Goal: Theorem 2 (p. 18)

For every feasible $y$, every rounding with the properties above and every decreasing-weight probing order,

$$\mathbb E[\mathsf{ALG}]\ \ge\ \Big(1-\frac1e\Big)\sum_{v\in V_2}\sum_{e\in\delta(v)}w_ep_ey_e .$$

Milestones

1. The proof of Lemma 7 (p. 17) expresses $W(v)$ as $\mathbb E[\sum_i w_iY_iP_i\prod_{j<i}(1-Y_jP_j)]$ and bounds $\mathbb E[\prod_{j\le i}(1-Y_jP_j)]\le\prod_{j\le i}(1-y_jp_j)$ using (2).
2. Lemma 7 (p. 16): $\mathbb E[W(v)]\ge\sum_{i=1}^k w_iz_i\prod_{j=1}^{i-1}(1-z_j)$ for the edges of $\delta(v)$ labelled by decreasing weight.
3. Eq. (29) (p. 18): the bound $F(i)\ge1-e^{-F^*(i)}\ge(1-1/e)F^*(i)$. The summation-by-parts identity (27) on the same page is included as a supporting lemma.
4. Lemma 8 (p. 17): $\sum_i w_iz_i\prod_{j<i}(1-z_j)\ge(1-1/e)\sum_iw_iz_i$ when $z_i\in[0,1]$, $\sum_iz_i\le1$ and $w_1\ge\cdots\ge w_k\ge0$.
5. Lemma 9 (p. 18): $\mathbb E[W(v)]\ge(1-1/e)\,\mathsf{OPT}(v)$ for every $v\in V_2$.

The paper's proofs are in §4, pp. 16–19.

Significance

Combined with the LP upper bound (Lemma 1 of the paper, from Bansal et al.), Theorem 2 is a $(1-1/e)$-approximation for stochastic matching on bipartite graphs with a unit-patience side, improving and generalizing the $1/3$ guarantee of Hikima et al. for Problem A and, through their reduction, for ISPCB. By the paper's account (§1.1, p. 4), the guarantee rests on a new ingredient, a $(1-1/e)$-balanced ordered contention resolution scheme for rank-1 matroids under negative correlation, in which the algorithm chooses the order: the per-star bound of Lemmas 7 and 9 holds for every rounding satisfying (2), not only for independent activations.

The result is proved in the paper; none of it has been machine-checked. This mission formalizes the per-star analysis and the theorem for an abstract rounding described by its properties, which is reusable for any algorithm that probes stars after a negatively correlated rounding.

Difficulty

If the rounded indicators $Y_e$ at a vertex were independent, Lemma 7 would be an equality and the remaining work would be the deterministic inequality of Lemma 8. They are not: the rounding is dependent, and Example 1 (p. 19) shows that this dependence can raise the probability that a particular edge is blocked to $1/2$, so that no correlation-agnostic contention resolution scheme is better than $1/2$-balanced. A per-edge guarantee, of the kind a contention resolution scheme that ignores correlation provides, is therefore unavailable: the bound of Theorem 2 holds only for the total weight collected at each $v$, and the negative correlation property (2) is one-sided, so it can be used only in the direction in which it holds.

Formalization scope

• All randomness is finite. The rounding is a probability vector $\mu$ on subsets of $E$; the activeness pattern $P:E\to\{0,1\}$ is independent with product weights. Every expectation is an explicit finite sum.
• The rounding of Gandhi et al. is represented by its properties: $\mu\ge0$, $\sum\mu=1$, the marginals $\Pr[Y_e=1]=y_e$, at most one rounded edge at each $u\in V_1$, at most $t_v$ at each $v\in V_2$, and (2) on the rounded indicators for every $v\in V_2$, $S\subseteq\delta(v)$, $b\in\{0,1\}$. The goal holds for every such $\mu$, so it covers the paper's rounding; formalizing the rounding procedure itself is a separate project.
• $W(v)$ is defined from the run (the first active edge in $v$'s probe list), not by the formula of Lemma 7; the identity between the two is a milestone.
• Standing assumptions, disclosed: $w_e\ge0$ (with a negative weight the bound fails), $p_e\in[0,1]$, patience $\infty$ is allowed on $V_2$, and parallel edges are allowed. The goal is stated for every feasible $y$, a stronger statement than the paper's "optimal" $y$, since the proof never uses optimality. The phrase "yielding a $(1-1/e)$-approximation" is not formalized: it needs Lemma 1 of Bansal et al.
• Ruled out: defining $W(v)$ as $\sum_iw_iY_iP_i\prod_{j<i}(1-Y_jP_j)$, as the best active edge regardless of the rounding, or stating the goal for one specific (independent) rounding or "for some rounding" would each be a different, weaker theorem.
• Useful infrastructure: finite expectations over product measures, a negative-correlation inequality for products, Abel summation (Finset.sum_range_by_parts), and $1-x\le e^{-x}$. Proofs of any milestone, and of the theorem from the milestones, are welcome.

Selected references

• B. Brubach, N. Grammel, W. Ma, C. MacRury, A. Srinivasan, Improved Guarantees for Offline Stochastic Matching via New Ordered Contention Resolution Schemes, Mathematics of Operations Research, 2025. arXiv:2106.06892v3. https://arxiv.org/abs/2106.06892
• R. Gandhi, S. Khuller, S. Parthasarathy, A. Srinivasan, Dependent rounding and its applications to approximation algorithms, Journal of the ACM 53(3):324–360, 2006. https://doi.org/10.1145/1147954.1147956
• N. Bansal, A. Gupta, J. Li, J. Mestre, V. Nagarajan, A. Rudra, When LP is the cure for your matching woes: improved bounds for stochastic matchings, Algorithmica 63(4):733–762, 2012. https://doi.org/10.1007/s00453-011-9511-8
• Y. Hikima, Y. Akagi, H. Kim, M. Kohjima, T. Kurashima, H. Toda, Integrated optimization of bipartite matching and its stochastic behavior: new formulation and approximation algorithm via min-cost flow optimization, The Thirty-Fifth AAAI Conference on Artificial Intelligence (AAAI 2021) (reference [28] of the paper; no link).
• A. Borodin, C. MacRury, Online bipartite matching in the probe-commit model, Mathematical Programming, 2025, pp. 1–54 (reference [9] of the paper; no link).