Missions · Prove2Me

Completed

On complementary channels and the additivity problemResearch Paper

Motivation

We explore complementarity between output and environment of a quantum channel (or, more generally, CP map), making an observation that the output purity characteristics for complementary CP maps coincide. Hence, validity of the mutiplicativity/additivity conjecture for a class of CP maps implies its validity for complementary maps. The class of CP maps complementary to entanglement-breaking ones is described and is shown to contain diagonal CP maps as a proper subclass, resulting in new class of CP maps (channels) for which the multiplicativity/additivity holds. Covariant and Gaussian channels are discussed briefly in this context.

This mission is the statement-level formalization of On complementary channels and the additivity problem (arXiv:quant-ph/0509101v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: complementary transfer of multiplicativity, additivity and superadditivity (Theorem 1: complementary transfer of multiplicativity, additivity and superadditivity, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

4 results of the paper are not stated yet, because the library lacks an interface they need:

Two-mode attenuation Bogoljubov dilation and its marginals: Complete self-adjoint quadratic two-mode Fock generator, its actual unitary evolution, and both all-trace-class marginal identities. (hard)
Two-mode amplification Bogoljubov dilation and its marginals: Complete self-adjoint quadratic two-mode Fock generator, its actual unitary evolution, and both all-trace-class marginal identities. (hard)
Convex mixtures and constrained Holevo-capacity claim: Specified mixture construction, common output identifications/flags, and the constrained-Holevo product-constraint convention for the four listed classes. (source-ambiguity)
Literal true-complement identification of Gaussian environmental marginal: Purity of the Gaussian environment, or retention of its omitted purifying subsystem in the true complement. (source-ambiguity)

Selected references

On complementary channels and the additivity problem, arXiv:quant-ph/0509101v3, https://arxiv.org/abs/quant-ph/0509101v3

34 thms3 active usersReviewed

Quantum Information·Captain: Goku

Public and private resource trade-offs for a quantum channelResearch Paper

Motivation

Collins and Popescu realized a powerful analogy between several resources in classical and quantum information theory. The Collins-Popescu analogy states that public classical communication, private classical communication, and secret key interact with one another somewhat similarly to the way that classical communication, quantum communication, and entanglement interact. This paper discusses the information-theoretic treatment of this analogy for the case of noisy quantum channels. We determine a capacity region for a quantum channel interacting with the noiseless resources of public classical communication, private classical communication, and secret key. We then compare this region with the classical-quantum-entanglement region from our prior efforts and explicitly observe the information-theoretic consequences of the strong correlations in entanglement and the lack of a super-dense coding protocol in the public-private-secret-key setting. The region simplifies for several realistic, physically-motivated channels such as entanglement-breaking channels, Hadamard channels, and quantum erasure channels, and we are able to compute and plot the region for several examples of these channels.

This mission is the statement-level formalization of Public and private resource trade-offs for a quantum channel (arXiv:1005.3818v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Private dynamic capacity: operational region equals the regularized entropic region (Theorem 1, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

1 results of the paper are not stated yet, because the library lacks an interface they need:

Lemma 1: The scope of additivity needed to infer regularized single-letterization from a channel-pair equality. (source-ambiguity)

Selected references

Public and private resource trade-offs for a quantum channel, arXiv:1005.3818v3, https://arxiv.org/abs/1005.3818v3

39 thms3 active usersReviewed

Completed

Quantum Information·Captain: Goku

Improving fidelity of continuous-variable teleportation via local operationsResearch Paper

Motivation

We study the Braunstein-Kimble setup for teleportation of quantum state of a single mode of optical field. We assume that the sender and receiver share a two-mode Gaussian state and we identify optimum local Gaussian operations that maximize the teleportation fidelity. We consider fidelity of teleportation of pure Gaussian states and we also introduce fidelity of the teleportation transformation. We show on an explicit example that in some cases the optimum local operation is not a simple unitary symplectic transformation but some more general completely positive map.

This mission is the statement-level formalization of Improving fidelity of continuous-variable teleportation via local operations (arXiv:quant-ph/0202102v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Dissipative Gaussian preprocessing strictly beats every Bob symplectic unitary (Abstract; §IV, Fig.1, pp.6–7, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

3 results of the paper are not stated yet, because the library lacks an interface they need:

§III, paragraph after Eq.(42): A proved unrestricted diagonal-optimality theorem for arbitrary diagonal A,B,C,D. (source-ambiguity)
§III, claim after Eq.(47): A specified complete analytic diagonal root-search algorithm covering exceptional denominators and filtering squared roots. (source-ambiguity)
Appendix A, Eqs.(A1)–(A6), continuation p.8: A well-defined renormalized bosonic process score on the accepted full separable state domain, with a fixed momentum-transpose convention, swap trace pairing, and agreement with regular Wigner slices. (hard)

Selected references

Improving fidelity of continuous-variable teleportation via local operations, arXiv:quant-ph/0202102v3, https://arxiv.org/abs/quant-ph/0202102v3

14 thms3 active usersReviewed

Quantum Information·Captain: Goku

The Capacity of the Quantum Multiple Access ChannelResearch Paper

Motivation

We define classical-quantum multiway channels for transmission of classical information, after recent work by Allahverdyan and Saakian. Bounds on the capacity region are derived in a uniform way, which are analogous to the classically known ones, simply replacing Shannon entropy with von Neumann entropy. For the single receiver case (multiple access channel) the exact capacity region is determined. These results are applied to the case of noisy channels, with arbitrary input signal states. A second issue of this work is the presentation of a calculus of quantum information quantities, based on the algebraic formulation of quantum theory.

This mission is the statement-level formalization of The Capacity of the Quantum Multiple Access Channel (arXiv:quant-ph/9807019v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exact capacity region of a finite-dimensional quantum multiple-access channel (Theorem 10, PDF p. 6). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

2 results of the paper are not stated yet, because the library lacks an interface they need:

§VII, product-input converse: Operational product-input quantum multiway codes, their intrinsic-algebra block-channel action and all-large-length average-error capacity region (hard)
§VII, 1-separable capacity region: Independent operational product-input and per-sender fully temporally separable-input MAC regions, with finite-ensemble information union (hard)

Selected references

The Capacity of the Quantum Multiple Access Channel, arXiv:quant-ph/9807019v3, https://arxiv.org/abs/quant-ph/9807019v3

16 thms3 active usersReviewed

Completed

Analysis Control Theory Operations Research·Captain: mikedeng1

Optimal Dynamic Momentum Strategies: For Horizons Within the Look-Back Period, the Optimal Weight Is the Mean-Variance Weight Plus a Hedging Term Weighted Toward Recent ReturnsResearch Paper

Motivation

Time-series momentum is the empirical regularity that an asset's recent excess return predicts its future excess return. It has been documented across equity indices, currencies, commodities and bonds (Moskowitz, Ooi & Pedersen 2012), and momentum portfolios are among the most widely traded systematic strategies. Most of that literature builds portfolios from a single signal: the average return over a look-back window. Li and Liu (Operations Research 2022) ask what a long-horizon investor who rebalances should do when expected returns really are driven by such a moving average. Their answer has a structural feature that a Markovian model such as Merton's (Merton 1971) cannot produce. The optimal weight depends on the whole recent price path, not only on the current momentum.

Setting

A risky asset has price $S_t$ and log price $s_t=\ln S_t$ , with

\frac{dS_t}{S_t} = [\alpha m_t + (1-\alpha)\mu + r]\,dt + \sigma\,dB_t,\qquad m_t = \frac1\tau\int_{t-\tau}^{t}\Big(\frac{dS_u}{S_u} - r\,du\Big),

where $B$ is a Brownian motion. Momentum $m_t$ is the equally weighted moving average of excess returns over a look-back window of length $\tau>0$ . The parameter $0<\alpha<1$ measures how strongly momentum enters the expected return, $\mu$ is the unconditional risk premium, $r$ is the constant short rate and $\sigma>0$ is the volatility. Because the drift depends on $s_t - s_{t-\tau}$ , the price is not Markov: the state at time $t$ is the whole path on $[t-\tau,t]$ .

An investor with constant relative risk aversion $\gamma>0$ maximizes expected utility of terminal wealth at a horizon $T$ by trading the asset and a riskless bond. The mission works in the paper's short-horizon regime $0\le T\le\tau$ , with the investor standing at time $0$ , so the realized path $s$ on $[-\tau,0]$ is known.

The paper's analysis (Appendix A.2) produces the following objects:

the market price of risk at time $0$ , $\theta_0 = [(1-\alpha)\mu - \alpha(r-\sigma^2/2) + \frac\alpha\tau(s_0-s_{-\tau})]/\sigma$ ;
functions $A_1, A_2$ on $[0,T]$ that solve a Riccati equation and a linear equation, the system (A.9), with $A_1(T)=A_2(T)=0$ and forcing term $s_{u-\tau}$ ;
the optimal weight $\phi^*_0 = \theta_0/(\gamma\sigma) + A_{1,0}s_0 + A_{2,0}$ of (A.11);
explicit functions $C_0$ , $\hat\omega$ , the weight $\omega$ on $[-\tau,0]$ and a constant $C_1$ , all of (A.14).

The Lean development names them theta0, SolvesA9, phiStar, C0, omegaHat, omega and C1 in the namespace DynMomentum.ShortHorizon.

Formalization targets

Goal: Proposition 3.3

For every solution $(A_1,A_2)$ of (A.9),

\phi^*_0 = \underbrace{\frac{\alpha}{\gamma\sigma^2}\int_{-\tau}^{0}\frac1\tau\Big(\frac{dS_v}{S_v}-r\,dv\Big) + \frac{(1-\alpha)\mu}{\gamma\sigma^2}}_{\phi^M_0} + \underbrace{\frac{(1-\gamma)\alpha}{\gamma\sigma^2}\int_{-\tau}^{0}\omega_v\Big(\frac{dS_v}{S_v}-r\,dv\Big) + C_1}_{\phi^H_0}. \tag{3.8}

Moreover, $\omega$ is positive on $(-\tau,0]$ when $T>0$ , strictly increasing on $[-\tau,T-\tau]$ , and constant on $[T-\tau,0]$ . The first summand $\phi^M$ is the myopic mean-variance weight; the second, $\phi^H$ , is the hedging demand.

Milestones

(A.9) solves (A.8). The ansatz $f(x,t)=\exp\{A_{1,t}x^2/2+A_{2,t}x+A_{3,t}\}$ solves the Feynman–Kac PDE (A.8) whenever $(A_1,A_2,A_3)$ solve (A.9).
(A.13), $A_1$ . The closed form $A_{1,t}=\alpha(\gamma-1)(1-e^{2\alpha(T-t)/(\sqrt\gamma\tau)})/(\gamma\sigma^2\tau D(T,t))$ solves the Riccati equation with $A_{1,T}=0$ .
(A.13), $A_2$ . For any solution $A_1$ , the variation-of-constants integral for $A_2$ solves the linear equation with $A_{2,T}=0$ .
(A.14). $\hat\omega_u>0$ for $u\in[-\tau,-\tau+T]$ .
Proposition 3.3, last sentence. The positivity and shape of $\omega$ , stated on its own.

Significance

The result. Proposition 3.3 shows that a momentum investor who rebalances should not trade on momentum alone. The hedging demand weights past returns unequally, with more weight on recent ones, so two price paths with identical momentum lead to different optimal positions. This is the paper's explanation of why path dependence is intrinsic to optimal momentum trading. It underlies the paper's later comparisons with momentum-only strategies, the horizon extension of Proposition 6.3, and the closed-form expansions of Online Appendix III.

Formalizing it. The proof's analytic half, from (A.9) to (3.8), is summarized in the paper by the phrase "after some manipulations". Writing that step out yields a checked identity between an ODE-defined weight and an explicit integral formula. Doing so has already caught an error. The constant $C_1$ printed in (A.14) is wrong: it differs from the true value by a path-independent amount, and it becomes correct after deleting both occurrences of $-\sigma^2/2$ (a numerical solution of (A.9) agrees with the corrected formula to $10^{-10}$ ). The proposition is proved in the paper. As far as is known, no part of it has been machine-checked.

Difficulty

Each milestone is a direct calculus statement; the goal is not. The obvious approach is to substitute the closed forms (A.13) into (A.11) and simplify. That leaves $A_{2,0}$ as a double integral of the past path $s$ against two nested exponential kernels written in the ODE's own parameterization, while (3.8) is a single integral of returns $dS/S$ against the weight $\omega$ of (A.14), which is written in a different parameterization. The paper gives no derivation of the match. The path is only continuous, so no step may differentiate $s$ . Separately, the Riccati closed form divides by a quantity that vanishes for small $\gamma<1$ , so every step has to track where that denominator is positive.

Formalization scope

What is formalized. Everything from (A.9) to (3.8). The stochastic layer is not formalized: Lemmas 3.1–3.2 (martingale method), the measure change, the Feynman–Kac representation and the volatility matching (A.10)–(A.12) need stochastic integration, Itô's formula and martingale representation, which Mathlib does not have at this revision. Equation (A.11) is therefore taken as the definition of the optimal weight: $\phi^*_0 := \theta_0/(\gamma\sigma) + A_{1,0}s_0 + A_{2,0}$ .
Time. The statement is at $t=0$ with horizon $0\le T\le\tau$ and the path on $[-\tau,0]$ , as in Appendix A.2. The model is time-homogeneous, so a general $t$ is a shift.
ODEs. "Solves (A.9)" means a derivative within $[0,T]$ at every point of $[0,T]$ , plus the terminal conditions. At $T=0$ the derivative clause is vacuous; that is the paper's zero-horizon case.
Admissibility. The hypothesis $D(T,0)=(\sqrt\gamma-1)e^{2\alpha T/(\sqrt\gamma\tau)}+(\sqrt\gamma+1)>0$ is added. It holds automatically for $\gamma\ge1$ . Without it, the Riccati solution blows up for small $\gamma<1$ and the goal would be vacuous.
Pathwise returns. The return integral $\int_{-\tau}^0 w_v(dS_v/S_v - r\,dv)$ , for a deterministic absolutely continuous weight $w$ with derivative $w'$ , is read as $w_0s_0 - w_{-\tau}s_{-\tau} - \int_{-\tau}^0 w'_vs_v\,dv + (\sigma^2/2-r)\int_{-\tau}^0 w_v\,dv$ . This is its value by Itô's formula and the product rule. With $w\equiv1/\tau$ it gives back $m_0$ of (2.3).
Corrections. $C_1$ is the corrected constant described above. The positivity of $\omega$ is stated on $(-\tau,0]$ under $T>0$ , because $\omega_{-\tau}=0$ and $\omega\equiv0$ when $T=0$ .
What a correct formalization rules out. The goal is not obtained by definition. $\phi^*$ is (A.11), never $\phi^M+\phi^H$ . The functions $\omega$ , $\hat\omega$ , $C_0$ and $C_1$ are the explicit formulas of (A.14), never derived from the ODE solution. The goal quantifies over every solution of (A.9), not over the closed forms.
Infrastructure. The development uses Mathlib's HasDerivWithinAt, interval integrals, Real.exp and Real.sqrt. Two lemmas are reusable well beyond this mission: the closed form of a constant-coefficient scalar Riccati equation, and variation of constants for a scalar linear ODE with merely continuous forcing. Contributions of those lemmas, of uniqueness for (A.9), and of the integration-by-parts step are welcome.

Selected references

K. Li and J. Liu, Optimal Dynamic Momentum Strategies, Operations Research, 2022. https://doi.org/10.1287/opre.2021.2254
R. C. Merton, Optimum consumption and portfolio rules in a continuous-time model, Journal of Economic Theory 3(4), 1971. https://doi.org/10.1016/0022-0531(71)90038-X
T. J. Moskowitz, Y. H. Ooi and L. H. Pedersen, Time series momentum, Journal of Financial Economics 104(2), 2012. https://doi.org/10.1016/j.jfineco.2011.11.003

7 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Product Selling vs. Pay-Per-Use Service: A Strategic Analysis of Competing Business Models: Pay-Per-Use Out-Earns Selling in Duopoly Equilibrium Iff the Delivery Cost Is Below a ThresholdResearch Paper

Motivation

A firm can sell a product outright or charge customers each time they use it. Selling collects one payment and transfers the asset to the customer. Pay-per-use service (PPU) keeps control of the asset, earns revenue from each use, and incurs a delivery or operating cost each time. These arrangements coexist for equipment, vehicles, and other products whose useful life contains many potential uses. A firm choosing between them needs to know how production cost and delivery cost affect the profit it can earn in competition. Ladas, Kavadias, and Loch study that question in a two-stage game and derive a threshold for which business model earns more in an asymmetric duopoly equilibrium.

The threshold is a result about competitive earnings, not just customer preference. A service provider can attract customers who need few uses, while a seller can attract customers who expect to use the product often. Each firm's price changes the boundary between those groups. The mission focuses on the paper's base model and its Proposition 3: the comparison of the seller's and service provider's equilibrium profits. The paper proves the result in its 2021 SSRN manuscript; this mission asks for a machine-checked account of that known result.

Setting

There are two firms. One sells a product for a single price $p_s$ and pays a production cost $c>0$ for each unit sold. The other charges a price $p_u$ per use. Under the paper's strong pooling assumption, one asset supplies its full capacity of $q_m>0$ uses, so the provider allocates production cost over those uses. Its effective cost per use is $c_u=c/q_m+\delta$ , where $\delta\ge0$ is delivery cost per use. The willingness to pay for one use is $a>0$ . The base model assumes that all customers have this same value but differ in desired lifetime usage $q$ , uniformly distributed over $[0,q_m]$ with density $1/q_m$ . Sections 2.1–2.3 set out these assumptions.

The customer utilities are $U_s(q;p_s)=qa-p_s$ from buying and $U_u(q;p_u)=q(a-p_u)$ from service. A customer belongs to the seller's segment if buying gives nonnegative utility and at least as much utility as service. A customer belongs to the provider's segment if service gives nonnegative utility and at least as much utility as buying. These conditions define the market segments at every price pair, including prices far from equilibrium. The paper writes both comparisons weakly, so a customer at a tie belongs to both segments. In the relevant equilibria, such ties have zero measure.

The seller's profit is its margin $p_s-c$ times the mass of its segment. The provider's profit is the average over its segment of usage $q$ times margin $p_u-c_u$ . Both averages use the uniform density $1/q_m$ . Firms first select business models and then set prices simultaneously. This mission fixes the asymmetric subgame with one seller and one service provider. A price equilibrium is a pair at which neither firm can increase its profit by changing its own price; the provider's price is constrained by $p_u\le a$ . The comparison is made where the provider is admissible, $c_u\le a$ , as the paper specifies before Proposition 3 and when discussing infeasibility in Section 3.2. The model and game timing appear on manuscript pages 7–9.

Formalization targets

Equilibrium profit comparison

Write $\Pi_s(p_s,p_u)$ and $\Pi_u(p_s,p_u)$ for the integral-defined profits at an equilibrium. Proposition 3 gives a production-cost-dependent delivery threshold:

\bar\delta(c)= \begin{cases} \dfrac{c}{2q_m}, & c\le\dfrac{aq_m}{3},\\ a-\dfrac{c}{q_m}-2a\left(\dfrac{aq_m-c}{aq_m+c}\right)^2, & c>\dfrac{aq_m}{3}. \end{cases}

The goal asserts that an equilibrium exists and that every price equilibrium has the stated comparison:

\Pi_s(p_s,p_u)\le\Pi_u(p_s,p_u) \quad\Longleftrightarrow\quad \delta\le\bar\delta(c).

For delivery cost above the threshold, the seller's equilibrium profit is strictly larger. The milestone list follows the paper's Appendix A.2.1 profit and equilibrium table and Appendix A.2.4's two threshold regimes. Proposition 3, manuscript page 14 states the comparison.

Significance

The result separates two drivers of the business-model choice. Production cost creates a possible pooling advantage for the provider, because many uses can share one asset's cost. Delivery cost erodes that advantage on every use. The threshold states exactly when the provider's equilibrium earnings exceed the seller's, under the base model's assumptions. It also provides a benchmark for the paper's later analyses of usage uncertainty, heterogeneous valuation, and queueing inefficiencies. Those extensions change the model and are outside this mission. Sections 3–6 develop the base result and its extensions.

The result is already proved in the cited manuscript. The formalization would make explicit the price game, its whole strategy spaces, and the passage from the model's utility-defined market segments to equilibrium profits. It would also establish that the comparison is valid at every equilibrium in the admissible region, including boundary parameter values. No machine-checked proof of this model or Proposition 3 is being reused here; the platform search found related duopoly models with different customers, prices, and cost conventions. The definitions of the segments and profit integrals can be reused for later formalizations of this paper's variants.

Difficulty

The paper computes an indifferent customer's usage and then obtains price candidates from an interior first-order condition and a constrained KKT calculation. Those calculations alone do not establish a global equilibrium: a deviation can put all customers on one side of the indifferent point, leave a firm with no customers, or use a nonpositive price. The profit formulas derived for an interior split do not describe those cases. A formal equilibrium statement must compare each firm with every permitted price, rather than treating the stationary equations as a definition of equilibrium.

The boundary $c=aq_m,\delta=0$ also matters. At that point the seller can have several equilibrium prices with the same zero profits, so uniqueness of prices is too strong. The goal concerns profits at every equilibrium. Appendix A.2.4 switches the algebraic profit comparison according to the provider's price regime, while Proposition 3 switches its threshold formula at $c=aq_m/3$ ; the two switches have to describe the same profit ordering over the whole admissible region.

Formalization scope

Lean represents $a,q_m,c,\delta,p_s,p_u$ , and customer usage $q$ as real numbers. The parameter predicate records $a>0$ , $q_m>0$ , $c>0$ , $\delta\ge0$ , and $c/q_m+\delta\le a$ . The last condition is the paper's service admissibility condition; it implies $c\le aq_m$ . Customer mass is real Lebesgue measure restricted to the utility-defined segment and divided by $q_m$ ; service profit integrates $q$ over its segment and divides by the same $q_m$ . These segments are bounded and measurable, so their measures and integrals have the intended finite values. The threshold and table formulas only use divisions whose denominators are positive under admissibility.

The paper's weak market inequalities are retained, including their treatment of ties. Seller deviations range over all real prices because no duopoly seller-price bound is imposed in the source. Provider deviations range over all prices at most $a$ , matching its stated constraint. The equilibrium predicate requires global profit comparisons. The goal asserts existence before saying what holds at every equilibrium, so an empty equilibrium set cannot satisfy it. Profits in the goal are calculated from customer segments and integrals at an equilibrium; they are not defined by the table. The paper's Appendix A.2.1 table provides a separate milestone proving those values, and the global best-response and equilibrium-profit statements are identified as stronger than the printed calculations.

This mission needs Mathlib's real measure, set integral, and real algebra libraries, plus the paper-specific definitions of utility, market segments, profits, equilibrium, the two pricing regimes, and $\bar\delta(c)$ . Contributions that establish the closed-form integrals, global best responses, equilibrium table, all-equilibrium profit identity, and regime comparisons are within scope. The earlier monopoly benchmark, the full business-model choice game, and the later heterogeneous, uncertain-usage, and queueing models are separate targets.

Selected references

K. Ladas, S. Kavadias, and C. Loch, Product Selling vs. Pay-Per-Use Service: A Strategic Analysis of Competing Business Models, authors' SSRN manuscript, 2021, SSRN 3356458; published in Management Science, doi:10.1287/mnsc.2021.4125. This mission cites manuscript pages 7–9, 13–14, 36–37, and 42.

10 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

I Don’t “Recall”: The Decision to Delay Innovation Launch to Avoid Costly Product Failure: Neither, Both, or Exactly One of Two Identical Firms Tests, by Failure-Probability CutoffsResearch Paper

Motivation

Product recalls are frequent and costly. A firm that launches an innovation without thorough quality assurance testing gains time on the market but risks a recall, which brings direct costs (repairs, refunds, legal settlements) and lasting damage to the product's reputation. Testing removes the risk but delays the launch, and while a firm tests, a rival can take the market with its own innovation. Kim, Koenigsberg and Ofek (SSRN 3492105, November 2019; published in Management Science, 2022, doi:10.1287/mnsc.2022.4303) model this trade-off as a two-period game and ask when competing firms test and when they rush to market. Their answer for two identical firms, Proposition 2, is the goal of this mission: depending on the failure probability of an untested product, neither firm tests, both test, or exactly one tests.

Setting

Two firms each hold an innovation. The mature product has quality $V>0$ and the innovation quality $V+B$ , with $B>0$ . Production costs nothing. There are two periods, $t=1,2$ .

Before $t=1$ , each firm chooses its testing decision $QA\in\{0,1\}$ simultaneously. A firm that tests ( $QA=1$ ) sells its mature product at $t=1$ and a fail-proof innovation at $t=2$ . A firm that does not test ( $QA=0$ ) launches its innovation at $t=1$ . The untested innovation fails during that period with probability $\theta\in(0,1)$ , independently across firms. On failure the firm pays a recall cost $\Delta=\rho+\delta\,\pi_1$ , where $\rho>0$ is a fixed cost, $\delta\in(0,1]$ a penalty per unit of first-period revenue and $\pi_1$ the firm's first-period profit, and at $t=2$ it sells a recalled innovation of quality $(V+B)(1-\gamma)$ , with reputation damage $\gamma\in(0,1)$ .

In each period a new unit mass of consumers arrives, with tastes $\phi$ uniform on $[0,1]$ . A consumer of taste $\phi$ gets utility $\phi\,q-p$ from a product of quality $q$ at price $p$ and buys the product of greatest utility if that utility is nonnegative. Given the two products on offer, the firms set prices; the pricing subgame is the one-period price game, and its equilibrium profit for quality $q$ against $q'$ is written $\pi(q,q')$ . The testing game is the simultaneous $2\times2$ game in which a firm choosing $a$ against a rival choosing $b$ earns the expected two-period payoff $\Pi^{a,b}$ , and an equilibrium is a pure Nash equilibrium of it.

Formalization targets

Goal: Proposition 2

With the cutoffs of the paper's appendix,

\tilde\theta^{st}=\frac{4B(V+B)^2(3+\gamma)^2}{(V+B)\big(4B(V+B)(3+\gamma)^2\delta-(3V+4B)^2(1-\gamma)\gamma\big)+(3V+4B)^2(3+\gamma)^2\rho},

and $\tilde\theta^{nt}=[\underline{\tilde\theta}^{nt},\overline{\tilde\theta}^{nt}]$ , the interval between the two roots of the quadratic in $\theta$ given by (A.3):

\text{no firm tests}\iff\theta\in\tilde\theta^{nt},\qquad \text{both test}\iff\theta\ge\tilde\theta^{st},\qquad \text{exactly one tests}\iff\theta\le\tilde\theta^{st}\ \text{and}\ \theta\notin\tilde\theta^{nt},

and the two symmetric equilibria never coexist.

Milestones

Lemma 1 (three bullets): the equilibrium prices and profits of the pricing subgame, namely mature product against innovation, innovation against recalled innovation, and Bertrand pricing at equal qualities.
The four payoffs $\Pi^{1,1}=0$ , $\Pi^{0,1}$ , $\Pi^{1,0}$ , $\Pi^{0,0}$ in closed form (proof of Proposition 2).
(A.3) and (A.4): the best-response conditions $\Pi^{0,0}\ge\Pi^{1,0}\iff\theta\in\tilde\theta^{nt}$ and $\Pi^{1,1}\ge\Pi^{0,1}\iff\theta\ge\tilde\theta^{st}$ .
(A.5) and the $\tilde\rho^{nt}$ bound: the recall-cost thresholds under which each cutoff lies in $(0,1)$ .
Corollary 3: a dual-firm-test equilibrium requires $\rho\ge\tilde\rho^{st}$ , and $\tilde\rho^{st}>\tilde\rho^{nt}$ .

Significance

Proposition 2 is the paper's main result for competition. It shows that competition changes the testing decision in two directions. A rival's early launch makes simultaneous rushing less costly, because identical products earn nothing in the first period and the revenue-based recall penalty then vanishes. Firms also try to differentiate their timing, which produces the asymmetric equilibrium in which one firm tests and the other does not. Comparing the result with the monopoly benchmark (Proposition 1) gives the paper's managerial conclusions: duopolists may skip a test that a monopolist would run (Corollary 2), and both firms test only when the fixed recall cost is large (Corollary 3).

The proofs in the paper are algebraic and partly omitted ("tedious algebra … available from the authors"). A formal development checks every case of the price equilibria, including the global deviations that the first-order conditions do not cover, and the exact boundaries of each equilibrium region. It also settles the boundary behaviour the paper leaves implicit: the regions are disjoint only off their boundaries. No machine-checked proof of any result of this paper is known.

Difficulty

Most of the work is in Lemma 1. The first-order conditions of the price game give the stated prices, but an equilibrium must also survive non-local deviations: the low-quality firm may undercut to take the whole market, and the high-quality firm may price below the region where both firms sell. Demand is piecewise in the prices, with kinks where one firm's market vanishes and a tie-splitting rule at equal qualities, so each best response is a maximization over several branches. The uniqueness half of the Bertrand bullet needs an undercutting argument. The cutoff characterizations then require sign control of a quadratic in $\theta$ whose discriminant can be negative, and of a denominator in $\tilde\theta^{st}$ that is negative for small $\rho$ .

Formalization scope

All quantities are real numbers. The parameters are a structure with fields $V,B,\rho,\delta,\gamma,\theta$ , and a predicate bundles the standing assumptions $V>0$ , $B>0$ , $\rho>0$ , $0<\delta\le1$ , $0<\gamma<1$ , $0<\theta<1$ . The page writes neither $V>0$ nor $B>0$ ; both are implicit and are made explicit here.

Demand is the Lebesgue measure of the set of tastes in $[0,1]$ that buy the product, with indifferent consumers counted with weight $\tfrac12$ . A price equilibrium allows deviations to every nonnegative price. The period profit $\pi(q,q')$ is revenue at the prices computed in the proof of Lemma 1, $2q(q-q')/(4q-q')$ for the higher quality, $q(q'-q)/(4q'-q)$ for the lower and $0$ for equal qualities. It is computed from demand, so Lemma 1's profit formulas are theorems. The untested firm's objective $(1-\theta\delta)\,p\,d-\theta\rho$ of (A.1) is a positive affine transform of revenue and has the same best responses, so the price game is posed on revenue.

Lemma 1 identifies the unique price equilibrium for each of the two differentiated quality pairs as well as for equal qualities. The payoff $\Pi^{a,b}$ is built from the recall events, each failing independently with probability $\theta$ , and from the period profits. Testing decisions are Booleans (true = test). Equilibria of the testing game are pure Nash equilibria with weak best responses, using the published agt_games predicate AGT.IsPureNash.

The cutoffs are written exactly as on p. 37. Every statement that uses $\tilde\theta^{st}$ requires its denominator to be positive, and every statement that uses $\tilde\theta^{nt}$ requires the discriminant to be nonnegative; when these fail, the corresponding region is empty. The paper calls its regions "mutually exclusive", but at the boundaries a symmetric and an asymmetric equilibrium coexist, so the goal asserts exclusivity only between the two symmetric equilibria.

Trivializing formalizations are ruled out. Defining the payoffs by the four closed forms of the paper's proof, or the period profits by Lemma 1's formulas, would make the milestones definitional and the goal pure algebra. Here both are built from consumer choice.

Not in scope: the monopoly benchmark (Proposition 1, Corollary 1), Corollary 2 (proved only in a limit), the comparative statics of Corollary 4, the conditions $B<\tilde B^{nt}$ and $\tilde\gamma^{nt}$ of (A.3), and the extensions of §5. Contributions are welcome on any milestone. Lemma 1's analysis of the vertical-differentiation price game with uniform tastes is reusable for other quality-competition models.

Selected references

B. Kim, O. Koenigsberg, E. Ofek, I Don’t “Recall”: The Decision to Delay Innovation Launch to Avoid Costly Product Failure, SSRN working paper 3492105, November 2019. https://ssrn.com/abstract=3492105 — published in Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4303
A. Shaked, J. Sutton, Relaxing Price Competition Through Product Differentiation, Review of Economic Studies 49(1), 1982. https://doi.org/10.2307/2297136
J. Tirole, The Theory of Industrial Organization, MIT Press, 1988.

12 thms3 active usersReviewed

Algorithmic Game Theory Economics·Captain: mikedeng1

Interactive Information Design: Every Information Design Game with Finite Message Sets Admits a Subgame Perfect EquilibriumResearch Paper

Why this game matters

An information designer can change what others know without choosing their actions. When several designers disclose information at once, each designer's experiment affects the incentives faced by agents who receive messages from all of them. The resulting strategic problem appears in competing disclosures, advice, and mediated decisions. Koessler, Laclau, and Tomala study this interaction in a finite-state model and ask whether the designers and agents can play consistently at every continuation of the game. Their working paper proves an existence result for this general model before examining special splitting, corporation, and multi-period games.

The existence question has a specific obstacle. After seeing the designers' experiments, agents may have several optimal continuation behaviors. A designer's payoff can jump as those behaviors change with the experiment profile. The paper's Example 5 shows that some ways of selecting an agent equilibrium at each profile yield an induced game between designers with no approximate equilibrium. The continuation behavior must therefore be part of what the equilibrium chooses; a fixed arbitrary rule cannot be presumed adequate. The paper invokes the equilibrium-selection result of Simon and Zame (1990) for this step. The example and the proof are in the working paper, pp. 6–7 and 21–23.

Finite information design games

Let $N$ be a nonempty finite set of designers and $K$ a nonempty finite set of agents. Designer $i$ holds a component $\theta_i$ of the state, drawn with a common prior $p^0$ on $\Theta=\prod_{i\in N}\Theta_i$ . The prior is general: its coordinates may be dependent. Agent $j$ chooses an action in a nonempty finite set $A_j$ , and the action profile lies in $A=\prod_{j\in K}A_j$ . Designer $i$ and agent $j$ receive real payoffs $u_i(a;\theta)$ and $v_j(a;\theta)$ respectively. The primitive model appears in §2, p. 5.

Designer $i$ can send agent $j$ a message in a finite set $M_i^j$ . The designer's full message profile is $m_i\in M_i=\prod_jM_i^j$ . A statistical experiment is a rule $x_i:\Theta_i\to\Delta(M_i)$ : at each value of the designer's state component it specifies a lottery on full message profiles. The designers choose their experiments simultaneously from $X_i=\Delta(M_i)^{\Theta_i}$ . Each agent observes the whole experiment profile $x=(x_i)_i$ , but later sees only his own messages $m^j=(m_i^j)_i$ . The signal $\omega$ , uniformly distributed on $[0,1]$ , is public to all agents and may coordinate their action lotteries. Nature draws the state from $p^0$ ; conditional on it, each designer's experiment draws a message profile. This sequence is Definition 1 and the game timeline, pp. 5–6.

For fixed $x$ , the agents play a Bayesian continuation game $G_M(x)$ . Its equilibrium-outcome correspondence $E_M(x)\subseteq\Delta(A)^M$ consists of conditional distributions of action profiles given all messages that can arise from Bayes Nash behavior using the public signal. The agents' incentive test is ex ante: each agent may replace his entire private-message-to-action-lottery rule while the others keep theirs. Private messages with zero probability impose no incentive restriction. Public randomization allows convex combinations of equilibrium outcomes. As stated in §2, p. 6, $E_M(x)$ is nonempty and convex and is the set of public correlated equilibrium outcomes.

An equilibrium selection $\tau$ chooses one $\tau(x)\in E_M(x)$ at every $x$ and is Borel measurable. For a selected outcome, designer $i$ receives

U_i^\tau(x)=\sum_{\theta\in\Theta}\sum_{m\in M}\sum_{a\in A}p^0(\theta) \left(\prod_{i'\in N}x_{i'}(m_{i'}\mid\theta_{i'})\right) \tau(x)(a\mid m)u_i(a;\theta).

The designers may themselves mix: designer $i$ chooses a Borel probability measure $\zeta_i$ on $X_i$ , and the profile law is the product of these measures. By Definition 2, p. 6, an equilibrium of $G_M$ is a selection $\tau$ together with a mixed Nash equilibrium $\zeta$ of the designers' induced game. Selection at every $x$ gives the agents equilibrium behavior in every continuation subgame.

Formalization targets

The goal is Theorem 1, p. 6: for every finite profile of message sets, the game admits an equilibrium. With $X=\prod_iX_i$ and $\mathcal U(x)=\{(U_i(x,y))_i:y\in E_M(x)\}$ , the statement is

\exists\,\tau:X\to\Delta(A)^M,\ \zeta\in\prod_i\Delta(X_i) \quad\text{such that}\quad \tau(x)\in E_M(x)\ (\forall x),\quad \tau\text{ is Borel measurable},\quad \zeta\text{ is a mixed Nash equilibrium for }U^\tau.

The milestone list follows the assertions used in the paper's proof. It first records the nonemptiness, convexity, and public-correlation characterization of $E_M(x)$ ; then the compact convex values and upper hemicontinuity of $E_M$ and $\mathcal U$ . The final two milestones record a Borel measurable payoff selection $U^*(x)\in\mathcal U(x)$ whose designers' game has a mixed equilibrium, and a Borel measurable continuation selection $\tau$ that realizes that selected payoff. These statements are on pp. 6–7.

What the result establishes

Theorem 1 guarantees that the general finite-message model has at least one consistent profile of information design and agent continuation behavior. It permits multiple designers, arbitrary correlation in the prior, messages sent privately to different agents, and mixed experiment choices. The result supports the paper's later analysis by ensuring that the baseline game has an equilibrium even though an arbitrary continuation selection need not support one. The theorem is proved in the paper; the machine-checked proof and reusable formal infrastructure are the work of this mission.

Formalizing the result adds a precise interface for finite statistical experiments, agent continuation equilibria with public correlation, set-valued payoff maps, measurable selections, and mixed deviations over spaces of experiments. The finite-game lottery predicate from the published agt_games definition and its proved Nash-existence theorem are available as prerequisites. The remaining public-device, continuity, and selection material can serve other Bayesian-game formalizations.

Where the proof is difficult

The obvious first step is to choose one equilibrium outcome of the agents' game at each experiment profile and then seek a Nash equilibrium of the designers' game. That step fails because the chosen continuation outcome may change discontinuously with the experiments. In the paper's Example 5, a particular legitimate selection gives an induced zero-sum game with a gap between maxmin and minmax payoffs, so it has no approximate equilibrium. An argument that assumes every measurable selection works would be false. The existence theorem needs a selection compatible with mixed strategic behavior, and it needs that selection realized by actual agent equilibrium outcomes. Both demands are represented in the last two milestones.

Formalization scope

The Lean model uses finite nonempty designer, agent, state, action, and message types. Nonempty message sets are an explicit addition to the printed hypotheses: if one such set were empty, that designer would have no experiment and the existence claim would fail. The paper's printed action-product index $N$ is read as $K$ , the agent index, because actions belong to agents. The common prior is a lottery on the whole state profile, without a product assumption.

Finite lotteries are nonnegative real weight functions summing to one. The experiment spaces inherit the finite-dimensional product topology and Borel sigma algebra. The public signal has Lebesgue probability law on $[0,1]$ ; its strategy process is measurable and Bayes Nash at almost every signal value. The outcome correspondence is constructed from these processes, with no free outcome variable unrelated to agent incentives. Upper hemicontinuity uses the open-neighborhood definition. Designer mixed profiles are independent Borel probability measures, and deviations range over every such measure. Integrability is required for the mixed payoff and every deviating payoff, avoiding Lean's default value for a nonintegrable Bochner integral.

The target requires an existential Borel selection $\tau$ that belongs to $E_M(x)$ at every $x$ . A fixed selection, a nonmeasurable selection, or an unconstrained outcome map would alter the theorem. Contributions that establish compactness, upper hemicontinuity, measurable selection, and the mixed-equilibrium conclusion for these exact definitions are in scope. The separate results on splitting games, corporations, and multi-period play are outside this mission.

Selected references

F. Koessler, M. Laclau, and T. Tomala, Interactive Information Design, SSRN working paper 3171992, version of April 25, 2018; published in Mathematics of Operations Research, 2021. Working paper.

9 thms3 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

When Should the Off-Grid Sun Shine at Night? Optimum Renewable Generation and Energy Storage Investments: Storage Pays iff c_K/e < g − √(2c_Q g), So Technologies Rank by Cost-to-Efficiency RatioResearch Paper

Motivation

Islands, remote villages and mining sites that are not connected to a power grid have traditionally run on diesel generators. Solar panels can replace part of that fuel, but the sun shines only during the day, and demand continues at night. Pairing solar capacity with energy storage lets daytime surplus serve nighttime demand, at the price of an additional investment and of energy lost in each charge–discharge cycle. Many storage technologies compete for this market (lithium-ion and sodium batteries, pumped hydro, hydrogen), each with its own capital cost and cycle efficiency. A planner therefore faces two coupled questions: how much solar and storage capacity to install, and which storage technology to install at all.

Kaps, Marinesi and Netessine (SSRN 3761397; Management Science, 2023, doi:10.1287/mnsc.2021.04129) study these questions in a stochastic capacity-investment model. Their answer to the second question is a closed-form rule: technologies are ranked by a single number, the storage-cost-to-efficiency ratio $c_K/e$ , and a technology pays off exactly when this ratio is below an explicit function of the solar cost and the fuel cost.

Setting

A firm serves $T\ge 1$ periods. Each period has a day with deterministic demand $D_H>0$ and a night with deterministic demand $D_L>0$ . The firm installs solar capacity $Q\ge 0$ at per-period unit cost $c_Q>0$ , and storage able to discharge $K\ge 0$ units at per-period unit cost $c_K/e$ , where $c_K\ge 0$ and $0<e\le 1$ is the cycle efficiency. Day generation $q_t$ is uniform on $[0,Q]$ , independently across periods; nothing is generated at night. Any demand not covered by solar or storage is met by a fossil backup at marginal cost $g$ , with $2c_Q<g$ . Every unit of renewable energy served therefore saves $g$ . Write $(a)^+=\max[0,a]$ .

The tracking model follows the stored charge $x_t$ , starting from $x_0=0$ :

x_t=\Bigl(\min\bigl[\bigl(x_{t-1}+e(q_t-D_H)^+-(D_H-q_t)^+\bigr)^+,K\bigr]-D_L\Bigr)^+,

and its expected profit is

\Pi_{TR}(Q,K)=g\,E\Bigl[\sum_{t=1}^T\Bigl(\min[x_{t-1}+q_t,D_H]+\min\bigl[\bigl(x_{t-1}+e(q_t-D_H)^+-(D_H-q_t)^+\bigr)^+,K,D_L\bigr]\Bigr)\Bigr]-T\tfrac{c_K}{e}K-Tc_QQ.

The full-discharge model assumes all stored energy is used within the period:

\Pi_F(Q,K)=T\Bigl(g\,E\bigl[\min[q,D_H]+\min[e(q-D_H)^+,K]\bigr]-\tfrac{c_K}{e}K-c_QQ\Bigr),\qquad q\sim U[0,Q].

A plan is optimal if it maximizes the model's profit over all $Q,K\ge 0$ . For a technology $j=(e^j,c_K^j)$ , $\Gamma^j$ is the set of market parameters $(c_Q,D_H,D_L,g)$ at which the optimal tracking storage $K^*_{TR}$ is positive. Technology $A$ is preferred to $B$ when $\Gamma^A\supsetneq\Gamma^B$ (Definition 1). The threshold is

g_0=c_Q+\frac{c_K}{e}+\sqrt{c_Q^2+\frac{2c_Qc_K}{e}} .

Formalization targets

Goal: Theorem 2

A\text{ preferred to }B\iff \frac{c_K^A}{e^A}<\frac{c_K^B}{e^B},\qquad K^*_{TR}>0\iff \frac{c_K}{e}<g-\sqrt{2c_Qg}.

The goal concerns the tracking model, the paper's primary object, and not its approximation.

Milestones

$\Pi_{TR}\le\Pi_F$ for every plan (A.4.3).
$\Pi_{TR}=\Pi_F$ when $K\le D_L$ (eq. (30)).
The closed form (20) of $\Pi_F$ on $Q\ge D_H+K/e$ .
Joint concavity of the full-discharge profit $\Pi_F$ over all plans $Q,K\ge 0$ (Theorem 3, first sentence).
The no-storage optimum $Q_0=D_H\sqrt{g/(2c_Q)}$ and the marginal value of storage there, $T(g-\sqrt{2c_Qg}-c_K/e)$ (eq. (25)).
If $g\le g_0$ , $(Q_0,0)$ is optimal in both models, with equal profits (Theorem 4, first bullet).
$K^*_{TR}>0\iff g>g_0$ (Lemma 1, first bullet).
$g_0$ depends on $(c_K,e)$ only through $c_K/e$ and is strictly increasing in it (Lemma 1, second bullet).
$g_0<g\iff c_K/e<g-\sqrt{2c_Qg}$ , and the boundary form (19).

A supporting item, with no paper counterpart, asserts that an optimal tracking plan exists.

Significance

The theorem reduces the comparison of storage technologies, each described by two parameters, to a one-dimensional ranking that holds uniformly over all demand levels, solar costs and backup costs. It also gives a profitability test that uses only $c_K/e$ , $c_Q$ and $g$ . Neither statement involves $T$ , $D_H$ or $D_L$ . Lemma 1 locates the transition from "no storage" to "some storage" in the tracking model exactly, although that model has no closed-form solution. The intermediate results establish when the tractable full-discharge model is an exact surrogate for the tracking model.

The results are proved in the paper, by first-order conditions of the full-discharge model and a comparison argument. No machine-checked proof exists. This mission produces one: a Lean formalization of a multi-period storage recursion with uniform generation, its expected profit, and the threshold structure of its optimizers. Several printed statements are corrected along the way (see Formalization scope), so the formal versions also serve as an erratum.

Difficulty

The tracking model couples periods through the stored charge, so its expected profit has no closed form, and optimal plans cannot be computed. Everything about $K^*_{TR}$ has to be derived indirectly, by sandwiching the tracking profit between quantities of the one-period full-discharge model. The sandwich rests on two facts: $\Pi_{TR}\le\Pi_F$ everywhere, and $\Pi_{TR}=\Pi_F$ for $K\le D_L$ .

The obvious first idea, first-order conditions of the closed form (20), needs care: (20) equals $\Pi_F$ only where $Q\ge D_H+K/e$ , and plans outside that region must be handled too. Theorem 3's printed optimal capacity ignores $K\ge 0$ and is wrong whenever no storage is optimal. Optimal plans need not be unique: at $g=g_0$ with $e=1$ a whole segment of plans is optimal. A proof must therefore argue about optimality, not about the uniqueness of a stationary point. The existence of a tracking optimum also needs an argument when $c_K=0$ , because the profit is then not coercive in $K$ .

Formalization scope

Parameters form a structure with $D_H,D_L,e,c_K,c_Q,g\in\mathbb R$ and $T\in\mathbb N$ , constrained by a predicate Standing. The paper states $D_H,D_L>0$ , $0<e\le1$ and $2c_Q<g$ . Three conditions are added, and each is disclosed: $c_Q>0$ and $c_K\ge0$ (unit costs; with $c_Q=0$ the problem is unbounded) and $T\ge1$ (with $T=0$ every profit vanishes). Storage starts empty (footnote 3, p. 15). Generation is encoded as $q_t=Qu_t$ with $u$ uniform on $[0,1]^T$ , which is Lebesgue measure restricted to the unit cube. Expectations are Bochner integrals of bounded continuous functions. Everything is real-valued.

" $K^*_{TR}>0$ " is formalized as an optimal tracking plan exists and every optimal tracking plan has $K>0$ . The existence clause rules out the vacuous reading. Definition 1's $\supset$ is read as a proper superset, without which the "only if" direction of Theorem 2(a) fails for equal ratios. $\Gamma^j$ ranges over tuples with $c_Q,D_H,D_L>0$ and $2c_Q<g$ , for a fixed $T$ .

One printed statement is restated. Theorem 4's first bullet asserts that $(Q_0,0)$ is optimal in both models, not that optima are unique, and uses $Q_0$ from eq. (25) rather than Theorem 3's formula. Eqs. (20) and (25) are per period in the paper and carry the factor $T$ here.

The tracking profit is the $T$ -period expectation of the charge recursion. Defining it through the closed form (20), through $\Pi_F$ , or defining $\Gamma$ or optimality through $g_0$ , would make the goal a statement about the full-discharge model or a restatement of milestone 9, and is excluded.

Not in scope: Theorem 1 (strategic complements), Theorem 3's closed-form optimal decisions, Theorem 4's second and third bullets ( $g_F$ ), the partial-discharge model (Theorems 5–6), the capacitated generator (Theorem 7) and the numerical study. The recursion and the unit-cube encoding of i.i.d. uniform generation are reusable for related storage and inventory models. Contributions are welcome for any milestone and for the existence of an optimal tracking plan.

Selected references

C. Kaps, S. Marinesi, S. Netessine, When Should the Off-Grid Sun Shine at Night? Optimum Renewable Generation and Energy Storage Investments, SSRN 3761397, version of May 11, 2023. https://ssrn.com/abstract=3761397
C. Kaps, S. Marinesi, S. Netessine, same title, Management Science, 2023. https://doi.org/10.1287/mnsc.2021.04129

11 thms3 active usersReviewed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Shareholder Short-Termism, Corporate Control and Voluntary Disclosure: The Manager Discloses Good and Bad News Below a Short-Termism Threshold and Only Good News Above ItResearch Paper

Why disclosure can change control decisions

A manager's voluntary report can change more than investors' estimate of a firm. It can change what a controlling shareholder does to the firm. Jia and Menon study a shareholder who privately knows the value of an alternative strategy and may replace the current strategy. Investors observe intervention but do not observe that private value. A shareholder who expects to sell soon therefore weighs the market price after intervention along with the eventual liquidation value. The manager can influence that choice by disclosing or withholding the value of the current strategy. The question matters for accounting and corporate governance because withholding information can improve the firm's eventual value even when the manager has no direct preference for a higher short-term stock price. Jia and Menon, authors' manuscript, §§1–2.

The paper's Proposition 1 identifies a change in the form of equilibrium disclosure as the shareholder puts more weight on the interim price. The same model gives full disclosure when that weight is zero, disclosure of both low and high values at moderate weight, and disclosure only of high values at greater weight. This mission targets that proposition, with its intervention and Bayes equations as intermediate statements. Jia and Menon, Proposition 1, p. 18 of the authors' manuscript.

The disclosure and intervention game

The current firm value $v$ is uniformly distributed on $[\underline v,\bar v]$ . With probability $p$ , the manager privately learns its realization. An informed manager may truthfully disclose $v$ or remain silent; an uninformed manager cannot disclose or reveal that he is uninformed. A controlling shareholder privately observes an alternative value $\mu$ , uniformly distributed on $[0,\bar\mu]$ , then chooses whether to intervene. Intervention makes the liquidation value $V$ equal to $\mu$ ; otherwise $V=v$ . Investors see the manager's disclosure decision $d$ and the shareholder's intervention decision $a$ , and set a competitive price $P=E[V\mid d,a]$ . Jia and Menon, §2, pp. 6–8.

The shareholder's utility is $\eta P+(1-\eta)V$ , where $\eta\in[0,1]$ measures the weight on the interim stock price. The manager in the main model maximizes $V$ . The paper writes $\lambda=\eta/(2-\eta)$ for shareholder short-termism. Assumption 1 requires $\bar\mu/2<\underline v<\bar v<\bar\mu$ , so intervention is a live option at every current value. Jia and Menon, §2 and Assumption 1, pp. 7–8.

An equilibrium specifies the informed manager's disclosure set $D$ , the belief $N=E[v\mid ND]$ after no disclosure, and a shareholder intervention threshold after each disclosure decision. Here $ND=[\underline v,\bar v]\setminus D$ . Truthful disclosure reveals $v$ , so the intervention threshold after that announcement uses belief $v$ . After silence, investors and the shareholder account for both informed managers who withheld and uninformed managers who could not disclose. The shareholder best responds to either belief. The informed manager compares expected liquidation values under the resulting interventions and discloses when indifferent. Jia and Menon, §§2–4, pp. 7–18.

Formalization targets

The goal is Proposition 1. There is a $\lambda^*\in(0,1)$ , fixed by the model parameters before $\eta$ is chosen, for which an equilibrium exists for every $\eta\in[0,1]$ . Every equilibrium has the corresponding disclosure region:

ND=\begin{cases} \varnothing,&\lambda=0,\\ (v_1,v_2),&0<\lambda\le\lambda^*,\\ [\underline v,v'),&\lambda^*<\lambda\le1. \end{cases}

In the two-tailed regime, $v_2=N$ and $v_1=\frac{1+\lambda}{1-\lambda}v_2-\frac{2\lambda}{1-\lambda}\bar\mu$ . In the upper-tailed regime, $v'=N$ . The common belief and shareholder intervention threshold are

N=\frac{p\Pr(v\in ND)E[v\mid v\in ND]+(1-p)E[v]}{p\Pr(v\in ND)+1-p}, \qquad \mu^*(d)=(1+\lambda)E[v\mid d]-\lambda\bar\mu.

The supporting targets are the paper's Lemma 1 for the shareholder threshold, equations (7)–(8) for the manager's expected value, the zero-short-termism benchmark, equation (14) for the disclosure decision, and equations (15), (18), and (19) for the two Bayes fixed points and the lower threshold. The milestone list retains the source's labels and text. Jia and Menon, Proposition 1, pp. 18–20, and Appendix, pp. 36–39.

What the result establishes

The proposition separates two reasons to disclose: a low current value can prompt beneficial intervention, while a high current value can deter intervention that would destroy value. As the shareholder cares more about the price effect of intervention, the low-value disclosure region disappears. The result therefore gives a precise condition under which voluntary silence can protect liquidation value, despite the manager's exclusive concern for that value. The paper also uses the equilibrium in its later analysis of market reactions and comparative statics. Jia and Menon, §§4–5.

The result is proved in the cited paper; the remaining task here is a machine-checked Lean proof of the stated model, its best-response and Bayes identities, and Proposition 1. The proposal contains proof targets with sorry, not completed machine-checked proofs. Definitions of threshold responses and Bayes beliefs should remain reusable for other disclosure games, provided their priors and tie conventions are checked against those games.

Where the mathematical work lies

The manager's choice cannot be inferred from the current value alone. Disclosure changes the shareholder's belief, the probability of intervention, and the conditional alternative value revealed to investors by intervention. Comparing only the chance of intervention misses the price effect that makes the shareholder act too often. Comparing only the two conditional means misses how often each action occurs. Jia and Menon, §§3–4.

The equilibrium also imposes a fixed-point condition: the withholding interval determines the belief after silence, while that belief determines which values a manager withholds. The form of the interval changes at $\lambda^*$ . At the boundary, the low endpoint is a manager indifference point and remains disclosed. The challenge is to establish existence in each regime and characterize every equilibrium with those endpoint conventions, including the extreme shareholder weight $\eta=1$ . Jia and Menon, Proposition 1 and Appendix proof, pp. 18, 36–39.

Formalization scope

Lean uses real values and interval integrals against the two uniform laws. The lower support endpoint of $\mu$ is zero, as in the paper. The Standing predicate includes Assumption 1 and the explicit added restriction $0<p<1$ : the source says "with probability $p$ " but does not give strict bounds, while its Bayes formulas and nondisclosure regions need a nondegenerate informed population. The shareholder weight is quantified over $\eta\in[0,1]$ ; $\lambda$ is derived from it. Set integrals on a withholding region are used only when equilibrium makes the region measurable and contained in the bounded support. The conditional mean at the zero-probability endpoint $t=\bar\mu$ is assigned its limiting value so total real functions do not introduce a zero-over-zero artifact.

The shareholder's best-response condition is weak at indifference, while the manager's tie-break requires disclosure. Equation (14) prints a strict inequality even though the paper says an indifferent manager discloses; the Lean decision condition uses $\ge0$ . The target requires an equilibrium for every admissible $\eta$ and describes every equilibrium, so its universal characterization cannot hold vacuously. The shareholder threshold and manager payoff are defined from utility and integrals, rather than by the closed formulas being posed as milestones. The goal covers the paper's long-term manager case $\gamma=0$ ; Proposition 3 and the later comparative statics are outside this mission.

Selected references

X. Jia and R. Menon, Shareholder Short-Termism, Corporate Control and Voluntary Disclosure, authors' post-review manuscript, SSRN 4029096, 2023. Manuscript.
X. Jia and R. Menon, Shareholder Short-Termism, Corporate Control and Voluntary Disclosure, Management Science, 2023. DOI:10.1287/mnsc.2022.4357.

9 thms3 active usersReviewed

Control Theory Operations Research Probability+1·Captain: mikedeng1

On System-Wide Safety Staffing of Large-Scale Parallel Server Networks: Positive SWSS Makes the Limiting Diffusion Exponentially Ergodic, Negative SWSS Makes It Transient Under Every Markov ControlResearch Paper

Motivation

Large service systems such as call centres, hospital wards and cloud server farms route several customer classes to several server pools, with each pool trained for only some of the classes. Staffing such a network sits between two failure modes: too few servers make queues explode, and too many waste capacity. In the Halfin–Whitt (quality-and-efficiency-driven) regime, arrival rates and pool sizes grow like $n$ and the staffing surplus or deficit of each pool is of order $\sqrt n$ . Whether those $O(\sqrt n)$ surpluses can be scheduled into a stable system is a question about the network as a whole: a surplus in one pool can serve a deficit elsewhere only through the compatibility graph.

Hmedi, Arapostathis and Pang (arXiv:2009.01942, v3, 2021; Operations Research 2023) answer this for networks whose compatibility graph is a tree and that have no abandonment. They introduce one number, the system-wide safety staffing (SWSS) $\vartheta_p$ , the value of a small linear program. They prove that its sign decides stability.

Timeline.

Atar (2005) derived the limiting diffusion of tree networks under complete resource pooling.
Arapostathis and Pang (2016) obtained the triangular form of its drift.
Hmedi, Arapostathis and Pang (2019) characterized uniform stability through the "spare capacity" $-\langle e,B_1^{-1}h\rangle$ , for networks with one non-leaf pool.
The present paper (2021) treats general trees and identifies the spare capacity with $\vartheta_p$ .

Setting

There are $I$ classes and $J$ pools. Write $i\sim j$ if pool $j$ can serve class $i$ , and assume the bipartite graph $G$ with these edges is a tree. The first-order rates are $\lambda_i>0$ , $\nu_j>0$ and $\mu_{ij}>0$ , and the second-order corrections are $\hat\lambda_i,\hat\nu_j,\hat\mu_{ij}\in\mathbb R$ . Complete resource pooling (CRP) means that the linear program "minimize $\max_j\sum_i\xi_{ij}$ subject to $\sum_j\mu_{ij}\nu_j\xi_{ij}=\lambda_i$ , $\xi\ge0$ on the edges" has a unique solution $\xi^*$ , with $\sum_i\xi^*_{ij}=1$ and $\xi^*>0$ on every edge. Put $z^*_{ij}=\xi^*_{ij}\nu_j$ and $\theta_j=\hat\nu_j+\sum_i(\hat\mu_{ij}/\mu_{ij})z^*_{ij}$ .

For a positive probability vector $p$ , the SWSS parameter $\vartheta_p$ is the optimal value of

\text{(LP}')\quad \max\ \vartheta\quad\text{s.t.}\quad \hat\lambda_i\le\sum_{j}\mu_{ij}\kappa_{ij}-\vartheta p_i\ \ \forall i,\qquad \sum_i\kappa_{ij}=\theta_j\ \ \forall j,

over $\vartheta\in\mathbb R$ and $\kappa$ supported on the edges.

Let $\Psi(\alpha,\beta)$ be the unique array on the edges with row sums $\alpha$ and column sums $\beta$ (defined when $\langle e,\alpha\rangle=\langle e,\beta\rangle$ ). Let $h_i=\hat\lambda_i-\sum_j(\mu_{ij}\xi^*_{ij}\hat\nu_j+\hat\mu_{ij}z^*_{ij})$ . The limiting controlled diffusion is

dX_t=b(X_t,U_t)\,dt+\Sigma\,dW_t,\qquad b_i(x,u)=h_i-\sum_j\mu_{ij}\Psi_{ij}\big(x-\langle e,x\rangle^+u^c,\,-\langle e,x\rangle^-u^s\big),

with $\Sigma=\mathrm{diag}(\sqrt{2\lambda_i})$ and $W$ a standard Brownian motion. Here $\langle e,x\rangle^+$ is the total queue, $\langle e,x\rangle^-$ the number of idle servers, and the control $u=(u^c,u^s)\in\Delta_I\times\Delta_J$ says how queued customers are split among classes and idle servers among pools. A stationary Markov control is a Borel map $v:\mathbb R^I\to\Delta_I\times\Delta_J$ , used as $U_t=v(X_t)$ .

Formalization targets

Goal: Theorem 1 (limiting-diffusion clauses), p. 9

(a) If $\vartheta_p>0$ , then for every edge $(\hat\imath,\hat\jmath)$ , under the constant control $\bar v=(e_{\hat\imath},e_{\hat\jmath})$ , the diffusion has a unique invariant probability measure $\pi$ . Moreover there are $c\in\mathbb R^I$ , $S\succ0$ and $\varepsilon>0$ such that, with $V(x)=\exp\big(\varepsilon\|x-c\|_S^2(1+\|x-c\|_S^2)^{-1/2}\big)$ ,

\int V\,d\pi<\infty,\qquad \|P_t(x,\cdot)-\pi\|_V\le C\,V(x)\,e^{-\gamma t}\quad\forall x,\ t\ge0 .

(b) If $\vartheta_p<0$ , then under every stationary Markov control $|X_t|\to\infty$ almost surely. If $\vartheta_p=0$ , then under every stationary Markov control there is no invariant probability measure.

Milestones

Atar's uniqueness of $\Psi$ on a tree (p. 17).
Proposition 2: the drift equals $h-B_1(x-\langle e,x\rangle^+u^c)+\langle e,x\rangle^-B_2u^s$ , with $B_1$ triangular.
Theorem 2: closed form of $\vartheta_p$ through path gains $d$ .
Remark 1: the sign of $\vartheta_p$ does not depend on $p$ .
Theorem 3: $d(i,\ell)=(e^{\mathsf T}B_1^{-1})_\ell/(e^{\mathsf T}B_1^{-1})_i$ .
Theorem 4: $\vartheta_p=-\langle e,B_1^{-1}h\rangle/\langle e,B_1^{-1}p\rangle$ .
Lemma 1.
Theorem 5: the instability half of the goal.
Remark 8: the recentring shift $\zeta$ .
The Dieker–Gao Lyapunov matrix (p. 25).
Theorem 7: the Foster–Lyapunov inequality (57) and exponential ergodicity (58).

Significance

The theorem turns a stochastic stability question into the sign of a linear-program value computable from the network data. Positive SWSS is the condition under which a staffing rule with $O(\sqrt n)$ safety capacity can be made stable by scheduling, and the proof exhibits a simple stabilizing control. The identity $\vartheta_p\langle e,B_1^{-1}p\rangle=-\langle e,B_1^{-1}h\rangle$ links the LP value to the drift of the diffusion. It extends earlier uniform-stability results from networks with a single non-leaf pool to arbitrary trees.

The results are proved on paper. This mission produces machine-checked statements, and eventually proofs, of the limiting-diffusion half. That requires:

a general tree-network model;
its flow map $\Psi$ and drift;
the linear-algebraic identities between path gains and $B_1^{-1}$ ;
a notion of transience for diffusions;
an exponential-ergodicity statement for a piecewise-linear drift.

No part of this is formalized elsewhere. The existing platform layers for Halfin–Whitt diffusions concern single-pool networks.

Difficulty

The linear-algebra half is a genuine induction on trees, not an unfolding of definitions. Theorem 2 eliminates leaves class by class. Theorem 3 identifies the gains with the entries of $e^{\mathsf T}B_1^{-1}$ , which forces $B_1$ to be invertible and $e^{\mathsf T}B_1^{-1}$ to be positive. Theorem 4 then rewrites the LP value through the drift.

The probabilistic half is harder:

Transience for $\vartheta_p<0$ must hold under every Borel control. The drift is then discontinuous, so the argument must work with a bounded test function whose generator has a sign uniformly in the control, and with the recurrence–transience dichotomy for nondegenerate diffusions.
The case $\vartheta_p=0$ is a borderline case that no single Lyapunov function settles.
For $\vartheta_p>0$ , the drift under $\bar v$ is linear on each of two half-spaces. One quadratic form must decrease along both pieces, and one piece has a zero eigenvalue. A naive choice of $S$ (for instance the identity) fails there.
The ergodic statement needs a Foster–Lyapunov theorem for diffusions, which is not available in Mathlib.

Formalization scope

Classes are Fin I and pools Fin J, and the tree is SimpleGraph.IsTree on Fin I ⊕ Fin J. States are EuclideanSpace ℝ (Fin I), and control values are pairs of vectors in Mathlib's stdSimplex. Strong solutions, standard Brownian motion, invariant measures, the generator and the weighted total-variation norm are the published EthierKurtz, GPhNGIDiffusion.EMError and UnifErgHW.Diffusion definitions. The weighted norm uses the weight $1+V$ , which is equivalent to the paper's $V$ -norm up to a factor $2$ .

Conventions committed to:

$\vartheta_p$ is the supremum of the feasible values of (LP′); it is never defined by a closed formula.
$\Psi$ is chosen as the unique solution of (37), with junk value $0$ off $D$ .
$B_1$ , $B_2$ are defined for a chosen pool $\hat\jmath$ by eliminating $\beta_{\hat\jmath}$ .
The drift is (42) of the network data. Its triangular form (43) is Proposition 2, a theorem.
Transience is $|X_t|\to\infty$ a.s. for every strong solution.
"Not positive recurrent" is the absence of an invariant probability measure.

The statement admits trivializations, each ruled out:

(a) asserts the existence of strong solutions, so its transition probability is not an arbitrary choice.
(b) quantifies over every Borel control and every strong solution.
The ergodic bound has its constants ordered $\exists c,S,\varepsilon$ , then $\exists\gamma,C$ , then $\forall t,x$ , with $S\succ0$ and $\varepsilon>0$ .

For the instability clauses, strong solutions exist and are pathwise unique for every Borel control (a theorem of Veretennikov, 1981, and its locally bounded extensions; the drift is locally bounded with linear growth and the noise is additive and nondegenerate). This is background, not a claim of the mission.

Out of scope: the clauses of Theorem 1 about the diffusion-scaled $n$ th systems (Theorems 6 and 8), and the $\vartheta^n_p$ half of Theorem 4. They need a controlled continuous-time Markov chain layer with work-conserving action sets, which does not exist on the platform.

Welcome contributions:

proofs of the tree identities (Theorems 2–4, Lemma 1, Proposition 2);
a reusable Foster–Lyapunov-to-exponential-ergodicity theorem for diffusions with additive noise;
a reusable transience criterion via bounded submartingales.

Selected references

H. Hmedi, A. Arapostathis, G. Pang, On system-wide safety staffing of large-scale parallel server networks, arXiv:2009.01942v3, 2021; Operations Research (2023). https://arxiv.org/abs/2009.01942
R. Atar, A diffusion model of scheduling control in queueing systems with many servers, Annals of Applied Probability 15(1B) (2005). https://doi.org/10.1214/105051604000000963
R. Atar, Scheduling control for queueing systems with many servers: asymptotic optimality in heavy traffic, Annals of Applied Probability 15(4) (2005). https://doi.org/10.1214/105051605000000601
A. Arapostathis, G. Pang, Ergodic diffusion control of multiclass multi-pool networks in the Halfin–Whitt regime, Annals of Applied Probability 26(5) (2016). https://doi.org/10.1214/16-AAP1171
A. B. Dieker, X. Gao, Positive recurrence of piecewise Ornstein–Uhlenbeck processes and common quadratic Lyapunov functions, Annals of Applied Probability 23(4) (2013). https://doi.org/10.1214/12-AAP870
H. Hmedi, A. Arapostathis, G. Pang, Uniform stability of a class of large-scale parallel server networks, arXiv:1907.04793, 2019. https://arxiv.org/abs/1907.04793
S. P. Meyn, R. L. Tweedie, Stability of Markovian processes III: Foster–Lyapunov criteria for continuous-time processes, Advances in Applied Probability 25 (1993). https://doi.org/10.2307/1427522

24 thms3 active usersReviewed

Completed

Analysis Economics Operations Research·Captain: mikedeng1

Dual Moments and Risk Attitudes: The Rank-Dependent Utility Risk Premium of a Small Risk Is Variance Times Utility Risk Aversion Plus Maxiance Times Probability-Weighting Risk AversionResearch Paper

Motivation

The Pratt–Arrow risk premium is the basic local measure of risk aversion under expected utility (EU): a decision-maker with a twice differentiable utility $U$ facing a small zero-mean risk $\tilde\varepsilon$ at wealth $w_0$ pays approximately

\pi \simeq \frac{\sigma^2}{2}\left(-\frac{U''(w_0)}{U'(w_0)}\right),

variance times the index of absolute risk aversion (Pratt 1964; Arrow 1965). It is used throughout portfolio theory, insurance pricing and decision analysis, wherever a risk attitude has to be summarised by one number.

Much of decision theory since the 1980s replaces EU by rank-dependent utility (RDU, Quiggin 1982), which distorts cumulative probabilities by a probability weighting function $h$ . Its special case with linear utility is Yaari's dual theory (DT, Yaari 1987). Under these models risk aversion comes from two sources, the curvature of $U$ and the curvature of $h$ , and the variance alone no longer measures how much a small risk costs. Eeckhoudt and Laeven (arXiv:1612.03347v2, published in Operations Research, 2022) identify the missing measure: the second dual moment, or maxiance, the expected best of two independent draws of the risk. They show that under DT the local risk premium is proportional to the maxiance, and that under RDU it is the sum of a variance term and a maxiance term.

Setting

A finite lottery lists outcomes $x_1 \le \dots \le x_n$ in increasing order with unconditional probability masses $\pi_1, \dots, \pi_n$ . Write $F_i = \pi_1 + \dots + \pi_i$ and $F_0 = 0$ . The masses need not sum to one: the risks below are attached to one branch of a lottery and carry only that branch's mass. An RDU decision-maker with utility $U$ and weighting function $h$ evaluates a lottery by (4.1):

\int U(x)\,\mathrm dh(F(x)) = \sum_{i=1}^n U(x_i)\bigl(h(F_i) - h(F_{i-1})\bigr).

DT is the case $U(x) = x$ (3.1). The paper assumes that $U$ is twice continuously differentiable with $U' > 0$ , and that $h : [0,1] \to [0,1]$ is twice continuously differentiable with $h(0) = 0$ , $h(1) = 1$ , $h' > 0$ .

For a risk with cumulative distribution $F$ and mean $m = \int x\,\mathrm dF(x)$ , the unconditional variance and maxiance are

m_2 = \int (x - m)^2\,\mathrm dF(x), \qquad \bar m_2 = \int (x - m)\,\mathrm d(F(x))^2,

and $\Pr$ denotes the total unconditional mass. For a probability distribution, $\bar m_2 = \mathbb E[\max(\tilde\varepsilon^{(1)}, \tilde\varepsilon^{(2)})] - \mathbb E[\tilde\varepsilon]$ (2.1).

Fix $0 < p_0 < 1$ , $0 < \varepsilon_1 < \min\{p_0, 1 - p_0\}$ , $\varepsilon_2 > 0$ and initial wealth $w_0$ . Lottery $C$ pays $w_0 - \varepsilon_2$ with probability $p_0$ and $w_0 + \varepsilon_2$ with probability $1 - p_0$ . Lottery $D$ takes mass $\varepsilon_1$ from each branch of $C$ and puts the released mass $2\varepsilon_1$ on a middle outcome $w_0 + y$ with $-\varepsilon_2 < y < \varepsilon_2$ . The RDU risk premium is $\lambda = 0 - y$ for the $y$ that makes the decision-maker indifferent between $C$ and $D$ , that is, the solution of (4.2). The spread from $D$ with $y = 0$ to $C$ attaches to the middle branch the risk $\tilde\varepsilon_{12}$ , which takes the values $\pm\varepsilon_2$ each with unconditional probability $\varepsilon_1$ . The DT construction with lotteries $A$ , $B$ , outcomes $\pm1$ , premium $\rho$ and risk $\tilde\varepsilon_1$ ( $\pm1$ with probability $\varepsilon_1$ each) is the same with $\varepsilon_2 = 1$ and $U(x) = x$ .

Formalization targets

Goal: the RDU risk premium, (4.3)

As $(\varepsilon_1, \varepsilon_2) \to (0^+, 0^+)$ jointly, with $m_2$ , $\bar m_2$ , $\Pr$ the moments of $\tilde\varepsilon_{12}$ ,

\lambda = \frac{m_2}{2\Pr}\left(-\frac{U''(w_0)}{U'(w_0)}\right) + \frac{\bar m_2}{2\Pr}\left(-\frac{h''(p_0)}{h'(p_0)}\right) + o\!\left(\frac{m_2}{\Pr} + \frac{\bar m_2}{\Pr}\right).

Milestones

The moments of $\tilde\varepsilon_1$ : $\bar m_2 = 2\varepsilon_1^2$ , $\Pr = 2\varepsilon_1$ (§3, p. 6).
The moments of $\tilde\varepsilon_{12}$ : $m_2 = 2\varepsilon_1\varepsilon_2^2$ , $\bar m_2 = 2\varepsilon_1^2\varepsilon_2$ , $\Pr = 2\varepsilon_1$ (footnote 21).
DT indifference between $A$ and $B$ is equation (3.2).
The explicit DT premium (3.3): $\rho = \dfrac{(h(p_0) - h(p_0 - \varepsilon_1)) - (h(p_0 + \varepsilon_1) - h(p_0))}{h(p_0 + \varepsilon_1) - h(p_0 - \varepsilon_1)}$ .
The DT approximation (3.4): $\rho = \dfrac{\bar m_2}{2\Pr}\left(-\dfrac{h''(p_0)}{h'(p_0)}\right) + o\!\left(\dfrac{\bar m_2}{\Pr}\right)$ as $\varepsilon_1 \to 0^+$ .
RDU indifference between $C$ and $D$ is equation (4.2), and it has exactly one solution $\lambda$ with $-\varepsilon_2 < \lambda < \varepsilon_2$ .

Significance

The result. Formula (4.3) shows that, for a small zero-mean risk, an RDU decision-maker's premium splits additively into an EU part (variance times utility risk aversion $-U''/U'$ ) and a DT part (maxiance times probability-weighting risk aversion $-h''/h'$ ). Variance and maxiance appear on an equal footing, so the maxiance is the natural second risk measure for non-EU preferences, as the variance is for EU. The DT index $-h''(p_0)/h'(p_0)$ plays the role of the Arrow–Pratt coefficient in the probability plane. The paper builds its global comparative risk aversion result (Proposition 5.1), its examples with Prelec's weighting function and its portfolio application on this local index.

Formalizing it. The result is proved in the paper by Taylor expansion, with " $\simeq$ " left informal. This mission fixes the precise asymptotic meaning: a little-o remainder in the joint limit. It also makes definite the claims the paper takes for granted: that the premium exists and is unique, and that the moments of $\tilde\varepsilon_1$ and $\tilde\varepsilon_{12}$ take the stated values. No part of this development, nor any rank-dependent utility evaluation, is formalized on the platform or, as far as is known, elsewhere.

Difficulty

The obvious argument expands both sides of (4.2) and keeps "the second-order terms". This needs care on two counts. First, the premium is defined only implicitly, so its size has to be controlled before $U(w_0 - \lambda)$ is expanded: the $\lambda^2$ term is negligible only once $\lambda = O(\varepsilon_2^2 + \varepsilon_1\varepsilon_2)$ is known. Second, the two leading terms have different orders, $\varepsilon_2^2$ and $\varepsilon_1\varepsilon_2$ , and the remainder must be uniformly small relative to their sum in a two-parameter limit. The tempting reading "small variance and small maxiance" (p. 4) with $\varepsilon_1$ fixed is false: at fixed $\varepsilon_1$ the dual term carries a relative error of order $\varepsilon_1$ that does not vanish as $\varepsilon_2 \to 0$ . The DT step (3.4) needs the explicit solution (3.3) and the strict positivity of $h(p_0 + \varepsilon_1) - h(p_0 - \varepsilon_1)$ .

Formalization scope

All quantities are real. A lottery is a pair of vectors indexed by $\mathrm{Fin}\,n$ ; the evaluation (4.1) is the finite rank-dependent sum, with cumulative masses computed from the vector. The sum equals the Stieltjes integral only for outcomes in increasing order, so the premium predicates keep the page's ranges $-1 < x < 1$ and $-\varepsilon_2 < y < \varepsilon_2$ , which order $B$ and $D$ . Initial wealth $w_0$ is added to every outcome.

Committed conventions:

$U$ is $C^2$ on $\mathbb R$ with $U' > 0$ everywhere (footnote 1). $h$ is $C^2$ on $[0,1]$ , maps $[0,1]$ into itself, satisfies $h(0) = 0$ , $h(1) = 1$ , and has positive one-sided derivative within $[0,1]$ (p. 5, footnote 12). These are the page's hypotheses, kept although local differentiability at $w_0$ and $p_0$ would suffice.
$U''(w_0)$ , $h'(p_0)$ , $h''(p_0)$ are ordinary iterated derivatives; $p_0$ is interior.
Pinned reading of " $\simeq$ ". (4.3) is a little-o statement along the filter of $(0,0)$ restricted to $(0,\infty)^2$ , relative to $m_2/\Pr + \bar m_2/\Pr$ ; (3.4) is the one-variable analogue as $\varepsilon_1 \to 0^+$ , relative to $\bar m_2/\Pr$ .
The premium is any function of $(\varepsilon_1, \varepsilon_2)$ satisfying the indifference on the feasible region; milestone 6 shows it exists and is unique.
The moments $m_2$ , $\bar m_2$ , $\Pr$ in the goal are computed from $\tilde\varepsilon_{12}$ by the definitions, not written as $2\varepsilon_1\varepsilon_2^2$ , $2\varepsilon_1^2\varepsilon_2$ , $2\varepsilon_1$ . $\Pr = 2\varepsilon_1 > 0$ on the filter, so no division by zero enters.

A formalization that defined the premium by its Taylor polynomial, replaced $\lambda$ by the leading terms, or took the limit in $\varepsilon_2$ alone would be trivial or false; the goal quantifies over every solution of the indifference and uses the joint limit.

Not formalized: the equivalence of (2.1) with the Stieltjes form, Proposition 5.1 (global comparative risk aversion), the examples of §6, the portfolio application of §7 and the non-binary generalisation of Appendix A.

Needed infrastructure: finite rank-dependent sums, Taylor expansion of $C^2$ functions with little-o remainders (Mathlib's taylor_mean_remainder family and Asymptotics), and the intermediate value theorem. Contributions welcome: proofs of the milestones, and a general Stieltjes-integral version of (4.1) for finitely supported distributions that would let later missions treat non-binary risks.

Selected references

L. R. Eeckhoudt, R. J. A. Laeven, Dual Moments and Risk Attitudes, arXiv:1612.03347v2, 2018 (the version formalized here; later published in Operations Research, 2022). https://arxiv.org/abs/1612.03347v2
J. W. Pratt, Risk Aversion in the Small and in the Large, Econometrica 32, 1964. https://doi.org/10.2307/1913738
J. Quiggin, A Theory of Anticipated Utility, Journal of Economic Behavior & Organization 3, 1982. https://doi.org/10.1016/0167-2681(82)90008-7
M. E. Yaari, The Dual Theory of Choice under Risk, Econometrica 55, 1987. https://doi.org/10.2307/1911158
K. J. Arrow, Aspects of the Theory of Risk-Bearing, Yrjö Jahnssonin Säätiö, Helsinki, 1965.

8 thms3 active usersReviewed

Bandit Algorithms Probability Statistics·Captain: mikedeng1

Asymptotically Optimal Sequential Design for Rank Aggregation: The ε-Greedy Generalized-Likelihood-Ratio Ranking Policies Attain the Minimal Bayes Risk as the Comparison Cost Tends to ZeroResearch Paper

Motivation

Rank aggregation turns many local comparisons into one global ordering. In a sequential setting, the experimenter chooses which two items to compare next, sees a noisy binary answer, and decides when enough evidence has been collected. More comparisons can improve the ranking, but each comparison has a cost. This tradeoff appears in preference elicitation and pairwise choice studies, where comparisons are easier to obtain than an entire ranking. Chen, Chen, and Li study how to make that tradeoff when comparison outcomes follow a parametric probability model and the per-comparison cost tends to zero (preprint, §§1–3).

The paper states a lower bound on the minimum Bayes risk among all sequential ranking policies, upper bounds for two explicit policies, and a corollary that the policies attain the minimum asymptotically. The central question is therefore precise: can a comparison rule that learns which pairs are informative achieve the same leading Bayes risk as a policy that may use any admissible adaptive selection, stopping, and ranking procedure? This mission targets that corollary in the arXiv version 1710.06056v1, including the supplemental proofs (paper and supplement).

Setting

There are $K=m+1\ge2$ items. Their latent scores are $\theta_1=0,\theta_2,\ldots,\theta_K$ ; fixing the first score removes the otherwise unidentifiable common shift. The parameter $\theta$ has a prior density $\rho$ on $\mathbb R^m$ , with support $W$ . Each available arm is a pair $(i,j)$ with $i<j$ . A comparison of that pair produces $X\in\{0,1\}$ with probability mass function $f^{i,j}_\theta(x)$ ; $X=1$ favors item $i$ . The Bradley–Terry–Luce model is one example, but the result allows a broader family of positive comparison mass functions (§2, pp. 5–6).

A sequential ranking policy $\pi=(A,T,R)$ consists of an adaptive randomized pair-selection rule $A$ , a stopping time $T$ for the observed comparison history, and a terminal permutation $R$ . The permutation induces pair decisions $R_{ij}=1$ when item $i$ is ranked ahead of item $j$ . Its Kendall loss counts pairwise errors against the strict ordering of the latent scores. A comparison costs $c>0$ , so the policy's Bayes risk is

V_c(\rho,\pi)=\mathbb E_{\rho,\pi}\bigl[L_K(\theta,R)+cT\bigr], \qquad V_c^*(\rho)=\inf_{\pi\text{ admissible}} V_c(\rho,\pi).

The infimum covers every adaptive randomized pair selector, stopping time, and ranking measurable at stopping. A policy that never stops pays infinite comparison cost. These are the objects of equations (2.2)–(2.5) (§2, pp. 6–7).

For each candidate parameter, the comparison log likelihood $l_n(\theta)$ sums the log probabilities of the first $n$ observed outcomes. The two proposed generalized likelihood ratio stopping times $T_1,T_2$ compare the best log likelihoods on opposite sides of each pair-ordering boundary. Both use the threshold $h(c)=|\log c|(1+|\log c|^{-\alpha_h})$ , $0<\alpha_h<1$ , and start checking after the first comparison. At stopping, $R$ ranks a maximum likelihood estimate $\hat\theta^{(T)}$ (§3.1, pp. 8–10).

The pair-selection rule uses the max–min information value $D(\theta)$ : among probability distributions on comparison pairs, it maximizes the minimum weighted KL divergence to a parameter that induces a different ranking. It mixes a maximizing allocation evaluated at the current MLE with uniform exploration. The mixing probability is $p(c)=C|\log c|^{-1/2+\delta_0}$ asymptotically, where $C>0$ and $0<\delta_0<1/2$ (§3.1–3.2, pp. 8–13).

Formalization targets

The goal is Corollary 4: for each $i=1,2$ , the concrete policy $\pi_i=(A_p,T_i,R)$ exists and its risk satisfies

\lim_{c\downarrow0}\frac{V_c(\rho,\pi_i)}{V_c^*(\rho)}=1.

The mission's milestones state the paper's information bound for the least distinguishable alternative (Lemma 13), the maximal Azuma–Hoeffding inequality (Lemma 8), a level-crossing bound for Lipschitz random fields (Lemma 9, stated with a guard that the printed version omits and without which it is false), the unrestricted Bayes-risk lower bound (Theorem 1), the stopped likelihood-ratio tail estimate (Lemma 11), the bound $\mathbb P_\theta(T_i\ge\tau)\le c^2$ for $\tau$ of order $|\log c|^3$ (Lemma 10), the expected Kendall-loss bound (Theorem 2), the within-ranking regularity of $D$ (Lemma 14), the expected sample-size bound (Theorem 3), and the paper's claim that the ε-greedy selection rule satisfies the exploration and allocation conditions A6 and A8. Theorems 1–3 separate the lower benchmark, error cost, and sampling cost; the corollary combines them as a statement about the true policy risk and the true unrestricted infimum (pp. 12–13, 22–23, 25, 38, 42).

Significance

The result identifies a pairwise-comparison procedure whose Bayes risk has the best possible leading order when comparisons become cheap. A lower bound alone does not identify a usable procedure; an upper bound for the two proposed rules alone does not show that a better adaptive policy cannot improve the leading risk. Together they explain the value of balancing uniform exploration against information-directed pair selection in this model (Theorems 1–3 and Corollary 4).

The analytic results are proved in the paper; they are not yet machine checked in this mission. The published Lean bandit definitions already supply a reusable randomized interaction law, natural filtration, and stopping-time notion. A complete formalization would add the paper-specific ranking loss, KL allocation problem, GLR procedures, and asymptotic analysis on top of that substrate. The probability and decision-theoretic pieces can also be reused for other sequential identification problems.

Difficulty

The likelihood-maximizing parameter and information-maximizing allocation both depend on observed data, while the pairs selected next depend on those estimates. This feedback prevents replacing the adaptive experiment with a fixed independent sample sequence. The stopping rules also inspect likelihood maxima over sets of parameters with opposing pair orders, so a pointwise likelihood estimate does not by itself control the stopping event uniformly over those sets. Finally, comparing the policy risk with $c\,\mathbb E t_c(\Theta)$ is insufficient: the corollary must compare it with the infimum over all admissible policies (§6 and supplemental Appendices A–I).

Formalization scope

Parameters are functions Fin m → ℝ, with item 1 fixed at score zero; Lean's item index is one less than the paper's. Pair arms use the published StochasticBandit, BanditPolicy, and BanditTrajectory definitions. Binary comparison outcomes are rewards $0$ and $1$ . The norm on the finite parameter space is the sup norm, and A2's balls are centered in $W$ . A maximum likelihood estimate and a max–min allocation are represented by arbitrary measurable selectors satisfying the page's maximizing properties. Their existence is a mathematical obligation; the goal also asserts existence of the resulting exact policy family, so an empty policy class cannot make it true.

The Bayes risk, expected loss, expected stopping time, and optimal risk use $[0,\infty]$ . This retains the infinite cost of nontermination and avoids turning a nonintegrable expectation into zero. The supremum and infimum defining $D(\theta)$ range over exactly the probability simplex and the set of rank alternatives in $W$ , and the likelihood suprema over the nonempty compact sets $W_{i,j}$ , so no default value of an empty or unbounded real supremum enters. Limits are from positive $c$ ; the exploration probability is clipped at $1$ away from zero. Ties in estimated scores are resolved by item index, and terminal rankings are required to be permutations. A4 is a uniform positive KL separation of differently ranked parameters of $W$ and, as the page's remark on A4 requires, $W$ contains no parameter with two tied scores. A6's exponent is existential, as printed; A8 is read uniformly over finite histories after the first uniformly sampled comparison. The prior is required to be a measurable probability density, and each binary comparison probability is positive so its logarithm is defined.

Contributions to the ten milestones, proofs of selector existence, a complete nonvacuity example, and reusable facts about stopped likelihoods and finite max–min KL problems are in scope. Lemmas 5, 6, 7 and 12 remain available as supporting work; the proposal lists only the source results whose statements have been pinned down here. The proposed goal is the explicit Corollary 4 ratio, never mere existence of a value function or a ratio against its own constructed benchmark.

Selected references

X. Chen, Y. Chen, and X. Li, Asymptotically optimal sequential design for rank aggregation, arXiv:1710.06056v1, 2017 preprint; published in Mathematics of Operations Research, 2022. arXiv version used for all pages and theorem numbers.
T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, §4.6 and §33.2. Open book.

15 thms3 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Government Loan Guarantees, Market Liquidity, and Lending Standards: Loan Insurance Raises the Price of Uninsured Loans and Lowers Screening in the Liquid EquilibriumResearch Paper

Motivation

Mortgage lenders in the United States and Canada can insure a loan against default when it is originated. In the US the guarantee is typically provided by government-sponsored enterprises, in Canada by government-backed mortgage insurers. Such guarantees are usually discussed as risk-sharing devices, or criticized because they weaken lenders' incentives to screen borrowers. Ahnert and Kuncl (Bank of Canada Staff Working Paper 2019-47; published as Government Loan Guarantees, Market Liquidity, and Lending Standards, Management Science, 2024) isolate a different channel. Loans are later sold in a secondary market where buyers cannot tell good loans from bad ones, the lemons problem of Akerlof (1970). Insurance bought at origination changes which loans reach that market, and therefore its price and its liquidity.

The model is deliberately risk-neutral, so insurance has no risk-sharing value. Every effect comes from the interaction of screening incentives, private information at the interim date, and market segmentation between insured and uninsured loans. This mission formalizes the paper's characterization of the liquid equilibrium with loan insurance (Proposition 2, existence and parts 1–2) and the results that the paper's proof uses.

Setting

There are dates $t=0,1,2$ and a continuum of lenders $i\in[0,1]$ , each with one loan. A loan pays $A>0$ at $t=2$ with probability $\mu\in(0,1)$ , or $\psi\in(\mu,1)$ if the lender screens at $t=0$ , and $0$ otherwise. Screening costs lender $i$ a private amount $\eta_i$ , distributed with distribution function $F$ supported on $[0,\bar\eta]$ . At $t=1$ each lender privately learns the quality $A_i\in\{0,A\}$ of its loan and a liquidity shock $\lambda_i\in\{1,\lambda\}$ , $\lambda>1$ , with $\Pr\{\lambda_i=\lambda\}=\nu\in(0,1)$ . Its utility is $\lambda_ic_{i1}+c_{i2}-\eta_is_i$ , so a shocked lender values interim consumption more.

At $t=0$ a lender may insure its loan for a fee $k$ . Insurance guarantees $A$ , so an insured loan pays the safe amount $\pi=A-k$ . At $t=1$ loans can be sold to competitive outside financiers who do not observe screening, shocks or quality, but do observe insurance. There are therefore two markets, for insured loans at price $p_I$ and for uninsured loans at price $p_U$ .

Write $\kappa=\nu\lambda+1-\nu$ . Lenders use a threshold rule: those with cost $\eta_i\le\eta$ screen. The market for uninsured loans is liquid when shocked lenders sell good loans, $\lambda p_U\ge A$ (condition (2)). A liquid equilibrium (Definition 1) consists of screening and insurance choices, prices and a fee such that:

every lender's choices are optimal, with $t=1$ sales chosen optimally;
the insurer and the buyers in both markets break even;
condition (2) holds.

Without insurance, the break-even price (4) and the marginal lender's indifference (5) characterize the benchmark equilibrium of Lemma 1.

Formalization targets

Goal: Proposition 2, existence and parts 1–2

Assume $\psi>\underline\psi=\lambda\mu/(\lambda\mu+\kappa(1-\mu))$ , $\lambda\ge\tilde\lambda_L=\frac1{2\mu}+\sqrt{\frac1{4\mu^2}+\frac{(1-\mu)(1-\nu)}{\mu\nu}}$ , and condition (35), which is equivalent to $\mu>\tilde\mu_I$ . Then a liquid equilibrium exists in which a share $m^*\in(0,1)$ of high-cost lenders insures, with

\eta^*=\frac{(1-\nu)(1-\mu)(\psi-\mu)\kappa A}{\nu\lambda+(1-\nu)(1-\mu)},\qquad p^*_U=\frac{\nu\lambda\mu A}{\nu\lambda+(1-\nu)(1-\mu)}\in\Big[\frac A\lambda,\,p^*_I\Big),

m^*=1-\frac{(\kappa(1-\mu)\psi-(1-\psi)\lambda\mu)F(\eta^*)}{\mu(\lambda-1)(1-\nu)(1-\mu)(1-F(\eta^*))},

fee $(1-\mu)A$ and $p^*_I=\mu A$ . Moreover, the price of uninsured loans is higher and the screening threshold lower than in every solution $(\eta_0,p_0)$ of the no-insurance system (4)–(5):

p_0<p^*_U,\qquad \eta^*<\eta_0.

Milestones

In attack order:

Lemma 1, the no-insurance benchmark.
Proposition 1 (liquid case), which gives the insurance fee and the price of insured loans, and bounds the share of insuring high-cost lenders below one.
The indifference condition (8), which pins down $p^*_U$ .
The screening condition (5), which pins down $\eta^*$ .
The root condition behind $\tilde\lambda_L$ .
Equations (34)–(35): $m^*$ , and when insurance is used.
Equation (38): more insurance raises $p_U$ and lowers $\eta$ .
Equation (37): the bound $\tilde\mu_I$ is unique.

Significance

The result is the paper's positive case for loan guarantees. Insured loans are removed from the uninsured market in two ways. Shocked lenders who insure hold average-quality loans. Unshocked high-cost lenders who insure give up the option to sell their lemons later. Both effects improve the pool of uninsured loans traded, so $p_U$ rises, and the liquid equilibrium survives for smaller liquidity shocks: $\tilde\lambda_L$ replaces the benchmark bound $\underline\lambda_L$ . The cost is lower lending standards ( $\eta^*<\eta_0$ ). The paper's welfare analysis (Proposition 4) and its regulation results (Proposition 5) start from this trade-off.

On the formal side, the paper's arguments are informal derivative computations and limit arguments in Appendix B. As far as is known, nothing in this model is machine-checked. Formalizing the result requires the equilibrium to be posed as a genuine fixed point: optimality among all screening and insurance choices, with $t=1$ sales chosen optimally, and break-even prices. The closed forms then become theorems, not definitions. The comparative statics in part 3 of Proposition 2 remain open for later work.

Difficulty

The closed forms follow quickly once one assumes the equilibrium structure: screeners do not insure, high-cost lenders are exactly indifferent about insurance, and the marginal screener is indifferent about screening. The work is in deriving that structure from Definition 1 and then exhibiting the equilibrium.

Fee. The fee is pinned down by break-even only if a positive mass of loans is insured.
Pooling price. The price of uninsured loans pools screened and unscreened loans, so it depends on the threshold through $F$ . The threshold in turn depends on the price.
Comparison with the benchmark. Showing that the benchmark fixed point lies on the other side of $(\eta^*,p^*_U)$ needs the monotonicity of (4) in the threshold, combined with (35).
The bound $\tilde\mu_I$ . Its uniqueness rests on single crossing along a curve whose right side involves $F(\eta^*(\mu))$ . The paper's appeal to "continuity in $\mu$ " fails when $F(\eta^*(\mu))$ reaches $1$ , which is why the milestone carries a heterogeneity assumption.

Formalization scope

Everything is defined in the namespace LoanInsurance.Liquid, in one definitions file LoanInsurance.Liquid.Model. The conventions are:

Parameters. These are a structure Params with fields A, μ, ψ, ν, lam (the paper's $\lambda$ ), etaBar ( $\bar\eta$ ) and F. The standing assumptions of §2 form the predicate Standing. The density $f>0$ on $[0,\bar\eta]$ is replaced by what the paper uses: $F$ is continuous and strictly increasing on $[0,\bar\eta]$ , $0$ below $0$ , and $1$ above $\bar\eta$ .
Profiles. Strategy profiles are threshold–share profiles: the threshold $\eta$ , the share $m_L$ of screeners who insure, the share $m$ of high-cost lenders who insure, $p_I$ , $p_U$ and $k$ . This is the paper's own reduction (p. 10).
Payoffs. Payoffs use $\max$ , so $t=1$ sales are optimal by construction. The break-even condition for uninsured loans uses the sales (3), which (2) licenses.
Derived quantities. $\kappa$ , $\underline\psi$ , $\tilde\lambda_L$ , $\eta^*$ , $p^*_U$ , $m^*$ , the prices (4) and (33), and condition (35) are definitions computed from the parameters, never free variables.
Goal hypotheses. The goal carries $\psi>\underline\psi$ (the paper's standing focus from p. 14) and (35) in place of $\mu>\tilde\mu_I$ ; their equivalence is milestone 8.
Milestone 8. It adds the heterogeneity assumption $(1-\nu)\psi A\le\bar\eta$ . Without it the claim can fail.

A trivializing formalization is ruled out: the equilibrium is never defined by the equations (5), (8) and (33) or by the closed forms. It is optimality among all four choices $(s,\ell)$ plus break-even. Neither $k=(1-\mu)A$ nor $p_I=\mu A$ is built into the definition. The goal is an existence statement whose witness must satisfy Definition 1.

A complete development needs elementary real analysis: monotonicity of linear-fractional functions, the intermediate value theorem for the fixed points (6) and (37), and case analysis on $\max$ . Lemmas about the prices (4) and (33) are reusable across the milestones. Proofs of any milestone, and alternative formulations of Definition 1 that are proved equivalent, are welcome.

Selected references

T. Ahnert and M. Kuncl, Loan Insurance, Market Liquidity, and Lending Standards, Bank of Canada Staff Working Paper 2019-47 (last updated August 2020). https://www.bankofcanada.ca/2019/12/staff-working-paper-2019-47/
T. Ahnert and M. Kuncl, Government Loan Guarantees, Market Liquidity, and Lending Standards, Management Science, 2024. https://doi.org/10.1287/mnsc.2022.01571
G. A. Akerlof, The Market for "Lemons": Quality Uncertainty and the Market Mechanism, Quarterly Journal of Economics 84(3), 1970. https://doi.org/10.2307/1879431

10 thms3 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Delegation of Stocking Decisions Under Asymmetric Demand Information: With Two Demand States, Early Stock-Out Inspection Makes the Store Manager Order the Principal's Optimal QuantityResearch Paper

Motivation

Retail chains routinely delegate replenishment decisions to store managers. The manager sees signals the head office does not: local events, weather, the mood of the neighbourhood. The head office (the principal) knows only the probabilities of these demand states. It also cannot observe lost sales directly, because unmet demand leaves no record, so it cannot simply pay the manager (the agent) on the true newsvendor cost. What it can observe is leftover stock and whether the shelf was empty when someone checked.

Alp and Şen (M&SOM 23(1):55–69, 2021) study performance measures built from these observable quantities. Under scheme $[M]$ , the agent is charged for leftover stock and pays a lump-sum penalty $M$ if the shelf is empty at the end of the period. One value of $M$ aligns the agent's order with the principal's optimal order in every demand state only when all states have the same demand variability (their Corollary 1). The paper's response is early inspection: scheme $[M,t]$ checks the shelf at an earlier time $t<1$ . Its Proposition 2 shows that with two demand states, a suitable inspection time and one penalty restore perfect alignment, even though the principal does not know the state.

The question belongs to the literature on sales-force and inventory incentives (e.g. F. Chen, Sales-force incentives and inventory management, M&SOM 2(2):186–202, 2000), where the agent's private information about demand is the central obstacle.

Setting

There is one period of length $1$ and two demand states $j\in\{1,2\}$ . The agent knows $j$ ; the principal does not. In state $j$ , cumulative demand is a Wiener process with drift $\mu_j$ and standard deviation $\sigma_j>0$ . So the period demand is $D_j\sim N(\mu_j,\sigma_j^2)$ and the demand up to time $t$ is $Y_{t,j}\sim N(t\mu_j,t\sigma_j^2)$ . Write $\Phi$ and $\varphi$ for the standard normal distribution function and density, and $k_j=\mu_j/\sigma_j$ .

The stock starts at a level $I\ge0$ and is raised to an order-up-to level $S\ge I$ . Leftover stock costs $c_o>0$ per unit and lost demand $c_u>0$ per unit, so the principal's expected cost is the newsvendor cost

\mathrm{ETC}_j(S)=c_o\,\mathbb E[(S-D_j)^+]+c_u\,\mathbb E[(D_j-S)^+].

Let $\hat z$ be the critical fractile, $\Phi(\hat z)=c_u/(c_o+c_u)$ . The principal's optimal level is $\mu_j+\hat z\sigma_j$ .

Under scheme $[M,t]$ with unit weight on leftover stock, the agent's expected score, eq. (4) of the paper, is

\mathrm{ETPM}_j(S)=\mathbb E[(S-D_j)^+]+M\,\mathbb P\{Y_{t,j}\ge S\}.

Its derivative in $S$ , at $S=\mu+z\sigma$ , is the function of eq. (9):

\omega(z)=\Phi(z)-\frac{M}{\sqrt t\,\sigma}\varphi\!\left(\frac{k(1-t)+z}{\sqrt t}\right).

In Lean these objects are agentCost, Φ, φ, omega, incentiveM, inspectionLHS and argminFrom in EarlyInspect.Align.Model. The principal's cost is the published InventoryControl.newsboyCost co cu μ σ.

Formalization targets

Goal: Proposition 2 (with one disclosed hypothesis)

Assume $0<\sigma_2<\sigma_1$ , $k_2>k_1$ and $\mu_1+\hat z\sigma_1\ge0$ . Then there is $\tau\in(0,1)$ with

e^{-\frac12\left[\frac{(k_2(1-\tau)+\hat z)^2-(k_1(1-\tau)+\hat z)^2}{\tau}\right]}=\frac{\sigma_2}{\sigma_1},

and the penalty

M=\frac{\Phi(\hat z)}{\varphi\!\left(\frac{k_1(1-\tau)+\hat z}{\sqrt\tau}\right)}\sqrt\tau\,\sigma_1=\frac{\Phi(\hat z)}{\varphi\!\left(\frac{k_2(1-\tau)+\hat z}{\sqrt\tau}\right)}\sqrt\tau\,\sigma_2

achieves the following with inspection time $t=\tau$ . For every $I\ge0$ and both $j$ ,

\operatorname*{argmin}_{S\ge I}\mathrm{ETPM}_j(S)=\{\max(I,\mu_j+\hat z\sigma_j)\}=\operatorname*{argmin}_{S\ge I}\mathrm{ETC}_j(S).

Milestones

The newsvendor optimum: $\mathrm{ETC}$ has the unique minimizer $\mu+\hat z\sigma$ , and over $S\ge I$ the unique minimizer $\max(I,\mu+\hat z\sigma)$ .
Eq. (9): $\mathrm{ETPM}'(S)=\omega((S-\mu)/\sigma)$ .
Lemma 1: the shape of $\omega$ on either side of the threshold $e^{-\frac12k^2(1-t)}\sqrt t\,\sigma/k$ .
Theorem 3 part 1: if $M>\Phi(-k)\sqrt t\,\sigma/\varphi(-k\sqrt t)$ , $\omega$ has a unique root $z'\ge-k$ , and the agent's optimum is $z^*=\max(z',(I-\mu)/\sigma)$ .
The first part of Proposition 2: existence of $\tau$ , and the agreement of the two expressions for $M$ .

Significance

The result shows that when the principal inspects is an incentive instrument in its own right. With end-of-period inspection, one penalty cannot align a manager across states that differ in variability. Moving the inspection earlier changes the stock-out probability differently in each state, and with two states that extra freedom is enough to make the manager's privately optimal order equal the principal's in both. Proposition 2 is the paper's headline claim, stated in the abstract and the conclusion. The paper generalizes its second consequence in Theorem 4: for more than two states, some $[M,t]$ with $t<1$ yields lower expected cost for the principal than scheme $[M]$ .

The paper states its results without proofs in the journal text; all proofs are in an online appendix. This mission states the goal and the results it rests on as machine-checkable statements. Two of them needed repair. As printed, Proposition 2 is false without a sign condition: in the paper's own case $\mu_1=\mu_2$ , $\sigma_1>\sigma_2$ , with $\hat z=-2$ , no $\tau$ exists. Theorem 3's "unique root" holds only on the feasible region $z\ge-k$ . None of these results has been formalized before.

Difficulty

The principal's problem is the convex newsvendor problem. The agent's is not convex. The score $\mathrm{ETPM}$ adds a decreasing Gaussian tail $M\,\mathbb P\{Y_t\ge S\}$ to a convex function, and its derivative $\omega$ can change sign more than once on the real line. The obvious argument, " $\omega(\hat z)=0$ by the choice of $M$ , hence $\hat z$ is the agent's optimum", fails twice. First, a stationary point need not be a minimizer: the agent's choice is the argmin of the score over $[I,\infty)$ , and that requires the sign pattern of $\omega$ on all of $[-k,\infty)$ , which is Lemma 1 and Theorem 3. Second, the same $M$ must serve both states, and the condition of §4.2.2 under which the root is unique has to hold at the constructed $(\tau,M)$ in each state. The existence of $\tau$ is an intermediate-value argument whose sign condition is exactly the added hypothesis.

Formalization scope

All quantities are real. Only the two normal marginals of the demand process are used, so the Wiener process is not formalized. The normal law is the published InventoryControl.newsboyDemand m s (mean $m$ , standard deviation $s$ ), and $Y_t$ is newsboyDemand (t * μ) (Real.sqrt t * σ), with variance $t\sigma^2$ . The agent's weight $\hat c_o$ is fixed to $1$ , as in Proposition 2. The principal's cost follows the text (leftover $c_o$ , lost demand $c_u$ ), not eq. (1), which prints the coefficients swapped. $\hat z$ is characterized by $\Phi(\hat z)=c_u/(c_o+c_u)$ .

The following hypotheses are added and disclosed in the items. $0\le\mu_1+\hat z\sigma_1$ appears in Proposition 2 and in milestone 5. $\mu>0$ and $M\ge0$ appear in Lemma 1, whose threshold divides by $k$ and whose second clause fails for negative $M$ . $I\ge0$ (nonnegative starting stock) appears in Theorem 3 and the goal. Standing hypotheses $\sigma>0$ and $t,\tau\in(0,1)$ appear throughout.

The goal cannot be trivialized by defining the agent's choice as a root of $\omega$ or as $\max(z',z^I)$ . Both choices are stated as sets of minimizers of the expected costs, and these sets are claimed to be singletons, so no vacuous reading is possible. A sorry-free check shows that the goal's hypotheses are satisfiable.

Useful infrastructure includes derivatives of Gaussian expectations of $(S-x)^+$ and of Gaussian tails, monotonicity and convexity of $\Phi$ and $\varphi$ , and the uniqueness of the critical fractile. These are reusable for any newsvendor-type model with normal demand. Proofs of individual milestones are welcome, as are proofs of the remaining results of the paper (Corollary 1, Theorem 3 parts 2–3, Theorem 4) as new statements.

Selected references

O. Alp, A. Şen, Delegation of Stocking Decisions Under Asymmetric Demand Information, Manufacturing & Service Operations Management 23(1):55–69, 2021. https://doi.org/10.1287/msom.2019.0810
F. Chen, Sales-force incentives and inventory management, Manufacturing & Service Operations Management 2(2):186–202, 2000.

8 thms3 active usersReviewed

Economics Operations Research·Captain: mikedeng1

Investment Strategies for Sourcing a New Technology in the Presence of a Mature Technology: When Equity Induces a Higher Probability of Technical Success Than a LoanResearch Paper

Motivation

Manufacturers that depend on a component often fund a new supplier whose technology could replace the incumbent one, while keeping the incumbent as a backup. Apple's 2013 prepayment to GT Advanced Technologies for sapphire production, which ended in the supplier's bankruptcy, and Intel's 2012 equity stake in ASML to accelerate extreme-ultraviolet lithography are the two cases that motivate Zhang and Lee (SSRN 3269249; Management Science, 2021, doi:10.1287/mnsc.2021.4078). Such a funder chooses between two instruments: a loan, repaid only up to what a failed supplier still holds, and an equity stake, which shares the supplier's value. The question the paper answers is which instrument induces the higher probability of technical success (PTS), once the existing supplier's reaction is taken into account.

The comparison sits between two literatures. Corporate finance knows the cost-shifting effect of debt under limited liability: a borrower who does not bear the cost of failure takes more risk (Brander and Lewis, 1986). Supply-chain work on collaborative development studies cost and effort sharing with a single supplier (Bhaskaran and Krishnan, 2009). The paper adds the incumbent supplier, whose cost reduction changes how much the manufacturer values the new technology.

Setting

Three firms play. The new supplier has no wealth. Reaching a PTS $\theta\in[0,1]$ requires the verifiable investment $K(\theta)=\theta^2/a$ and the unverifiable effort $G(\theta)=\theta^2/b$ , with capabilities $a,b>0$ ; a larger $a$ means a more mature technology. The manufacturer sells $D$ units of an end product at price $R>1$ and offers a contract: an upfront investment $B$ , a cap $B^G$ on effort expenses, and an expected procurement payment $P$ , plus an equity share $\gamma$ under equity. The supplier chooses $\theta$ and a filed effort expense $S$ subject to

G(\theta)\le S\le B^G,\qquad S+K(\theta)\le B,\qquad \theta\le\min\{G^{-1}(B^G),G^{-1}(aB/(a+b))\}.

Under equity the supplier's value is $\Pi^N_E=[B-K(\theta)-S]+\theta P$ , it earns $(1-\gamma)\Pi^N_E+[S-G(\theta)]$ , and the share is the fair valuation $\gamma\,\Pi^N_E=B$ . Under a loan (interest normalized to $0$ ) it earns $[B-K-S]+[S-G]+\theta(P-B)-(1-\theta)\min\{B-S-K,B\}$ . The manufacturer maximizes its payoff over contracts subject to incentive compatibility (the supplier's choice maximizes its payoff) and participation.

If the new technology fails, the manufacturer buys from the existing supplier, which can lower its unit cost from $1$ to $\varphi\le1$ at cost $c(1-\varphi)^2$ and keeps the share $1-\beta$ of the surplus $(R-\varphi)D$ ; $\beta\in[0,1]$ is the manufacturer's bargaining power. It maximizes $(1-\theta)(1-\beta)(R-\varphi)D-c(1-\varphi)^2$ . The manufacturer and the existing supplier play a static game, and $\theta^*_E$ , $\theta^*_L$ denote the PTS of its Nash equilibria under equity and under a loan. Two quantities drive the equilibrium:

W(\beta)=[(1-\beta)R+\beta]D,\qquad L(\beta)=\frac{D^2(1-\beta)\beta}{2c},

and the paper assumes $W(\beta)>L(\beta)$ .

Formalization targets

Goal: Proposition 1

For equilibria with an uncertain R&D ( $\theta<1$ ):

\text{(i)}\quad \text{given }\beta:\qquad \theta^*_E>\theta^*_L\iff a>\bar a_T(\beta),

\text{(ii)}\quad \text{given }a:\qquad \theta^*_E>\theta^*_L\iff \beta<\bar\beta_L(a)\ \text{or}\ \beta>\bar\beta_H(a),\qquad \bar\beta_L(a)\le\bar\beta_H(a).

The goal asserts only the threshold shape; it does not fix the thresholds' values, so it is stated about the equilibria of the two games, not about formulas.

Milestones

The existing supplier's best response $\hat\varphi(\theta)=1-D(1-\beta)(1-\theta)/(2c)$ (A-5).
Fair valuation forces the equity share $\hat\gamma=\big(3(a+b)-\sqrt{9a^2+10ab+b^2}\big)/(4b)$ .
Lemma A.1: given $\varphi$ , the manufacturer's optimal PTS is $\hat\theta_E(\varphi)$ (A-3) under equity and $\hat\theta_L(\varphi)$ (A-4) under a loan.
Lemma 1: the equilibrium PTS is $\theta^*_E$ (6), $\theta^*_L$ (7), with existence when these lie in $(0,1)$ .
The proof of Proposition 1: a rewriting of $\theta^*_L$ ; the equivalence $\theta^*_E\ge\theta^*_L\iff F\ge0$ for an explicit $F$ ; and the facts that $\hat\gamma$ decreases in $a$ , $F$ increases in $a$ , and $F$ is a convex quadratic in $\beta$ .

Significance

The result locates the boundary between two effects. Under a loan, limited liability makes the supplier invest more (cost shifting), but the incentive fades as success becomes likely. Under equity the manufacturer shares the supplier's value and is willing to pay more for success (profit sharing). Proposition 1 says profit sharing wins when the technology is mature enough, and that the incumbent's bargaining position acts non-monotonically: equity wins when the existing supplier is either weak or strong. The second part has no analogue when the incumbent's cost is exogenous, which is why the backup supplier matters. Proposition 2 of the paper, on the manufacturer's payoff, is stated in terms of the threshold $\bar a_T(\beta)$ .

The paper's proofs are pen-and-paper and partly informal: the contract analysis (pp. Appendix-18–23) proceeds by first-order conditions across case regions, and the comparison squares an inequality without treating the case where one side is negative. A machine-checked development would certify that the closed forms are the equilibria of the game as stated, including the participation and incentive constraints, and that the threshold structure holds without gaps. None of these results has a machine-checked proof on the platform.

Difficulty

The obstacle is Lemma A.1, not the algebra of Proposition 1. The manufacturer's problem is a moral-hazard contract design problem with a non-smooth agent: the supplier's choice of $S$ switches between the expense cap and the budget, the constraint set (3) has two caps, and under a loan the repayment is a minimum. Each candidate contract induces a best response that must be computed globally, not only from a first-order condition, and the optimal contract must be compared against every incentive-compatible alternative, including those with slack caps. Under equity the share $\gamma$ is itself pinned by a fixed point with the induced PTS. A proof that only checks first-order conditions in the region where the paper's contract lives does not establish optimality.

A second difficulty is the equilibrium layer: the manufacturer's optimum depends on $\varphi$ , and $\varphi$ on the PTS, so the equilibrium PTS solves a fixed-point equation, and boundary equilibria ( $\theta=0$ or $\theta=1$ ) must be excluded by the hypotheses $W(\beta)>L(\beta)$ and $\theta<1$ .

Formalization scope

All quantities are real numbers. The parameters $a,b,c,D,R,\beta$ form a record with the standing assumptions $a,b,c>0$ , $R>1$ , $\beta\in[0,1]$ and, added, $D>0$ . The loan's interest is dropped, following the paper's normalization $r=0$ . An outcome of each game is a contract together with the supplier's response; it is admissible when the response maximizes the supplier's payoff over (3) (the maximizer is chosen with the contract, the standard principal–agent tie-break), participation holds, $B,B^G\ge0$ , and, under equity, $\gamma\in[0,1]$ with $\gamma\,\Pi^N_E=B$ . The equilibrium is the platform's generic pure Nash equilibrium with feasible sets (CarbonDoubleCount.Planner.IsPureNash), instantiated with the manufacturer (admissible outcomes) and the existing supplier ( $\varphi\le1$ ).

The goal quantifies over all equilibria with $\theta<1$ ; the Lemma 1 milestones assert that such equilibria exist when $\theta^*_E,\theta^*_L\in(0,1)$ , so the goal is not vacuous. Substituting the closed forms (6), (7) for the equilibrium PTS in the goal would trivialize it into the proof-of-Proposition-1 milestones and is ruled out. In (i) only $a$ varies, with $b$ fixed; the paper's remark that $a\propto b$ is not imposed. In (ii) the thresholds are real numbers. The printed proposition puts them in $[0,1]$ , while its proof explicitly allows them to lie outside that interval when a region disappears; the formal statement follows the proof. The derivative claims of Lemma 1, Proposition 2 and the benchmark models of §5 are out of scope.

A complete development needs a global analysis of the agent's best response under (3), optimization of a concave function over $[0,1]$ , and real-algebra lemmas about square roots. Contributions on any milestone are welcome; milestones 1 and 5 are independent of the contract analysis.

Selected references

W. Zhang and H.-H. Lee, Investment Strategies for Sourcing a New Technology in the Presence of a Mature Technology, Management Science, 2021. SSRN version of 23 Mar 2021: https://ssrn.com/abstract=3269249 ; https://doi.org/10.1287/mnsc.2021.4078
J. A. Brander and T. R. Lewis, Oligopoly and Financial Structure: The Limited Liability Effect, American Economic Review 76(5), 1986. https://www.jstor.org/stable/1816460
S. R. Bhaskaran and V. Krishnan, Effort, Revenue, and Cost Sharing Mechanisms for Collaborative New Product Development, Management Science 55(7), 2009. https://doi.org/10.1287/mnsc.1090.1010

12 thms3 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

How Complementors Benefit from Taking Competition to the System Level: Squeezing the Complementor Makes Launching an Integrated System Profitable Even When the System Itself Loses MoneyResearch Paper

Motivation

Customers often need several complementary products, such as hardware and software, cars and financing, or jet engines and maintenance, sold by specialist firms that are complementors to one another. A recurring strategic move is for one complementor to launch an integrated system: a single offering that competes with the multi-component system its complementor still helps to supply. The paper's examples are AT&T's bundles of internet and entertainment services after the Time Warner merger, BMW's financing and leasing, Rolls-Royce's "power-by-the-hour" package of engines with maintenance, and Apple's music service competing with Spotify.

Reisinger, Schmidt and Stieglitz (Management Science, 2021) ask when such a move pays, and why it is observed even when the integrated system is neither better than the two-component system nor aimed at a different customer segment. Their answer separates the entrant's incremental profit into a direct effect (market expansion and conversion of customers to the integrated system) and a strategic effect: once an integrated system competes with the two-component system, the rival complementor cuts its component price while the entrant raises its own. The entrant thereby squeezes its complementor's margin. This decomposition follows the direct/strategic-effect analysis of Bulow, Geanakoplos and Klemperer (1985) and Fudenberg and Tirole (1984).

Setting

Two complementors $A$ and $B$ each sell one component of a two-component system with gross utility $U_C>0$ . Either may launch an integrated system with gross utility $U_I>0$ by paying an investment $K\ge0$ . Production costs are zero. The parameter $\gamma\in(0,1)$ measures substitutability between systems. Inverse demand is linear:

P_{C_A}+P_{C_B}=U_C-Q_C-\gamma\textstyle\sum_i Q_{I_i},\qquad P_{I_i}=U_I-Q_{I_i}-\gamma\big(Q_C+Q_{I_{-i}}\big),

a system that is not offered having quantity zero. The model restricts $\gamma$ to an admissible range: $\gamma\le U_C/(2U_I-U_C)$ if $U_I\ge U_C$ , and $\gamma\le\bar\gamma:=(\sqrt{U_C^2+3U_I^2}-U_C)/U_I$ if $U_I<U_C$ .

The game has two stages. In stage 1 the complementors decide simultaneously whether to launch an integrated system. In stage 2 they set prices. This gives three price subgames: no entry (i), accommodation (ii), in which only $A$ enters, and escalation (iii), in which both enter. A price equilibrium of a subgame is a pure Nash equilibrium in which a firm selling two products may change both prices at once. In stage 1, $A$ 's benefit of entering when $B$ stays out is $\Pi_A^{(ii)}-K-\Pi_A^{(i)}$ , and $B$ 's benefit of entering when $A$ is in is $\Pi_B^{(iii)}-K-\Pi_B^{(ii)}$ . The thresholds $\bar K$ and $\underline K$ are the values of $K$ at which these vanish.

$A$ 's incremental profit from entry splits into three parts:

\Delta\Pi_A^Z=(Q_{I_A}^{(ii)}+Q_C^{(ii)}-Q_C^{(i)})P_{I_A}^{(ii)},\quad \Delta\Pi_A^Y=(Q_C^{(i)}-Q_C^{(ii)})(P_{I_A}^{(ii)}-P_{C_A}^{(i)}),\quad \Delta\Pi_A^X=Q_C^{(ii)}(P_{C_A}^{(ii)}-P_{C_A}^{(i)}).

These are the profits from market expansion, from conversion of customers to the integrated system, and from squeezing the complementor.

Formalization targets

Goal: Proposition 3

In the accommodation equilibrium, for every admissible $\gamma>0$ :

U_I<U_C\ \Rightarrow\ \Delta\Pi_A^X>\Delta\Pi_A^Y,\qquad U_I>U_C\ \Rightarrow\ \Delta\Pi_A^Y>\Delta\Pi_A^X .

Moreover, when $U_I<U_C$ there is a threshold $\hat\gamma<\bar\gamma$ such that for every admissible $\gamma>\hat\gamma$ some $K\ge0$ makes the stage-1 outcome accommodation while

P_{I_A}^{(ii)}Q_{I_A}^{(ii)}-K<0,

that is, $A$ enters although its integrated system loses money. The goal states this existence claim and does not fix the threshold.

Milestones

The no-entry equilibrium: $P_{C_i}^{(i)}=U_C/3$ and profit $U_C^2/9$ .
The accommodation equilibrium: $P_{C_A}^{(ii)}=U_C/3+\gamma U_I/6$ , $P_{C_B}^{(ii)}=U_C/3-\gamma U_I/3$ , $P_{I_A}^{(ii)}=U_I/2$ , with both profits.
The escalation equilibrium and its symmetric profit.
Proposition 1 (i): $0<\underline K<\bar K$ , accommodation exactly for $\underline K<K\le\bar K$ , and escalation for $K\le\underline K$ .
Closed forms of $\Delta\Pi_A^X$ and $\Delta\Pi_A^Y$ .
The identity $\Delta\Pi_A^X-\Delta\Pi_A^Y=\gamma(U_C-U_I)(U_I(3+\gamma)-2\gamma U_C)/(18(1-\gamma)(1+\gamma))$ , whose second factor is positive.
The split of $A$ 's accommodation profit into component and integrated-system profit.
The equivalence of (8) and (9), $\gamma\ge U_CU_I/(2U_C^2-U_I^2)$ , and the fact that this threshold lies below $\bar\gamma$ .

Significance

The result gives a rationale for entry with an integrated system that is unprofitable on its own terms. The value of entry can lie entirely in the entrant's old business, through the margin it takes from its complementor. This matters for reading platform and ecosystem strategy, where launches of "first-party" hardware or bundles are often judged by their own profitability, and for competition policy, where the same move lowers the rival complementor's price and changes how the gains of the system are divided. Proposition 1, which the goal relies on, also shows that the asymmetric outcome, where one complementor integrates and the other does not, occurs for an intermediate band of entry costs, so the asymmetry arises endogenously between identical firms.

The paper proves these statements with computer-algebra-style calculations on closed forms. As far as is known, none of it is formalized. A complete development checks every equilibrium derivation, including uniqueness of the equilibria under joint deviations, and the inequalities that the paper's appendix treats briefly. The positivity of $\bar K-\underline K$ (Proposition 1 (i)) is argued in the appendix through a monotonicity claim that does not hold as written, and the two displayed formulas listed under Formalization scope contain misprints. The formal record settles these points.

Difficulty

The equilibrium computations are linear algebra, but each is stated as an equivalence: a profile is an equilibrium if and only if it equals the closed form. The "only if" direction needs strict concavity of each firm's two-price profit in both prices jointly. The comparison $\Delta\Pi_A^X$ versus $\Delta\Pi_A^Y$ needs the admissible range: the factor $U_I(3+\gamma)-2\gamma U_C$ is positive only because $\gamma\le\bar\gamma$ , and this has to be extracted from a square-root bound. The loss-making-entry claim needs more than $A$ 's entry benefit being nonnegative. $B$ must also stay out, so $K$ has to lie in $(\underline K,\bar K]$ and above $A$ 's integrated-system profit at the same time. That is why the goal depends on Proposition 1 (i), whose central inequality $0<\underline K<\bar K$ is a polynomial inequality in three variables over a region bounded by a square root. Plugging in boundary values of $U_I$ , as the appendix does, does not by itself establish it.

Formalization scope

All objects are over $\mathbb R$ in the namespace SystemSqueeze.Accommodation, in one definition file:

Standing UC UI γ bundles $U_C>0$ , $U_I>0$ , $0<\gamma<1$ and Admissible UC UI γ. Positivity of $U_C, U_I$ and $K\ge0$ are added; the paper uses them without stating them.
Prices range over $\mathbb R$ , and the direct demands are the untruncated linear expressions of §4.2. This is the paper's first-order approach; equilibrium prices are nonnegative on the admissible range as a consequence, not an assumption.
IsNoEntryEq, IsAccEq and IsEscEq are pure Nash equilibria with joint deviations in a firm's two prices.
Entry benefits, $\Delta\Pi_A^X$ , $\Delta\Pi_A^Y$ and $\Delta\Pi_A^Z$ are computed from equilibrium profiles passed as arguments. Every statement quantifies over the equilibrium predicates, so substituting the closed-form prices into the goal is ruled out: that would turn Proposition 3 into its own lemmas.
In stage 1 an indifferent firm enters, as in the proof of Proposition 1. The entering complementor is called $A$ , as by the paper's selection rule.
The de novo entrant of §5 is absent: its quantity is zero throughout.
Three printed slips are corrected: $\Pi_B^{(ii)}$ (a stray factor $1-\gamma$ ), the interval $[\bar K,\underline K)$ of Proposition 1 (i) (the proof has $\underline K<K\le\bar K$ ), and $\Delta\Pi_A^Y$ (an extra factor $U_I$ and a flipped sign).

The equilibrium lemmas are reusable for any linear-demand analysis of this model, including Propositions 2 and 4–8 of the paper, which are not part of this mission. Contributions of proofs for any milestone are welcome, as are alternative proofs of $\underline K<\bar K$ .

Selected references

M. Reisinger, J. Schmidt, N. Stieglitz, How Complementors Benefit from Taking Competition to the System Level, Management Science 67(5), 2021. https://doi.org/10.1287/mnsc.2020.3771
J. Bulow, J. Geanakoplos, P. Klemperer, Multimarket Oligopoly: Strategic Substitutes and Complements, Journal of Political Economy 93(3), 1985. https://doi.org/10.1086/261312
D. Fudenberg, J. Tirole, The Fat-Cat Effect, the Puppy-Dog Ploy, and the Lean and Hungry Look, American Economic Review 74(2), 1984. https://www.jstor.org/stable/1816385
L. Cabral, J. M. Villas-Boas, Bertrand Supertraps, Management Science 51(4), 2005. https://doi.org/10.1287/mnsc.1040.0337

10 thms3 active usersReviewed

Completed

Analysis Economics Operations Research·Captain: mikedeng1

Following the Customers: Dynamic Competitive Repositioning: For Small Repositioning Costs, the Thresholds Rise Infinitely Fast, Increase with σ², Decrease with δ, and Become Independent of rResearch Paper

Motivation

Firms reposition their products as consumer tastes drift: car makers redesign models, retailers change assortments, media outlets shift their editorial line. Each move costs money, and competitors respond to it. Ning and Villas-Boas (2020) study when two competing firms should incur a fixed cost to move toward consumers whose preferred position follows a random path. The answer is a pair of repositioning thresholds. The paper characterizes them through a system of two transcendental equations and, for small repositioning costs, derives explicit asymptotic expansions. Those expansions give the paper's comparative statics in volatility, attribute importance and patience.

This mission formalizes that small-cost analysis: Proposition 2 of the paper, together with the chain of identities and limits in its appendix that leads to it.

Setting

Consumers have preferences $(x,z)\in[0,1]^2$ . All consumers share the same position $x_t$ on the repositionable attribute, and they are uniformly spread on the fixed attribute $z$ . The position $x_t$ follows a driftless Brownian motion with variance $\sigma^2$ , reflected at $0$ and $1$ . Two firms sit at the ends of $[0,1]$ in $x$ , and at opposite ends in $z$ . A consumer buying from a firm at distance $x$ gets utility $v-\delta x-z-p$ , so $\delta>0$ measures how much the repositionable attribute matters. A firm may jump to the other end of the $x$ -line at a cost $K>0$ . Firms discount at rate $r>0$ . All these parameters are standing assumptions.

Under price competition, a firm earns the flow profit $\pi_s=\tfrac12$ when both firms are on the same side. When they are on different sides and the firm is at distance $x$ from the consumers, it earns

\pi_d(x)=\tfrac12\Big(1+\frac{\delta(1-2x)}{3}\Big)^2 .

Write $\lambda=\sqrt{2r/\sigma^2}$ . In the symmetric equilibrium, a firm on the far side repositions when its distance reaches a threshold $x^*$ . Firms on the same side reposition at a positive hazard rate on $(\underline x,x^*)$ . Value matching and smooth pasting of the value functions

V_d(x)=\frac{\pi_d(x)}{r}+\frac{4\delta^2}{9r\lambda^2}+Ae^{\lambda x}+Be^{-\lambda x},\qquad V_s(x)=\frac{\pi_s}{r}+C\big(e^{\lambda x}+e^{-\lambda x}\big)

give five conditions (5)–(9). Eliminating $A,B,C$ leaves the threshold system (14)–(15) in $(\underline x,x^*)$ alone. With $G=e^{\lambda(x^*+\underline x-1)}$ :

G=\frac{\pi_d(x^*)-\pi_s+\pi_d'(x^*)/\lambda+rK+\frac{4\delta^2}{9\lambda^2}}{\pi_d(1-\underline x)-\pi_s+\pi_d'(1-\underline x)/\lambda-rK+\frac{4\delta^2}{9\lambda^2}},\qquad G=\frac{\pi_d(1-\underline x)-\pi_s-\pi_d'(1-\underline x)/\lambda-rK+\frac{4\delta^2}{9\lambda^2}}{\pi_d(x^*)-\pi_s-\pi_d'(x^*)/\lambda+rK+\frac{4\delta^2}{9\lambda^2}} .

A threshold pair at cost $K$ is a solution of (14)–(15) with $\tfrac12<\underline x<x^*<1$ and $\delta(2x^*-1)<3$ . A solution branch is a pair of functions $K\mapsto(\underline x(K),x^*(K))$ that is a threshold pair for every sufficiently small $K>0$ . The appendix uses the prices $p^*=(3+\delta-2\delta x^*)/3$ and $\underline p=(3-\delta+2\delta\underline x)/3$ , and their sum $y=p^*+\underline p$ .

Formalization targets

Goal: Proposition 2

For every solution branch, as $K\to0^+$ :

the thresholds rise infinitely fast:

\frac{x^*(K)-\tfrac12}{K}\to\infty,\qquad\frac{\underline x(K)-\tfrac12}{K}\to\infty;

comparing two parameter tuples with equal $r,\delta$ and $\sigma_1^2<\sigma_2^2$ , for all small $K$ ,

x_1^*<x_2^*,\qquad\underline x_1<\underline x_2,\qquad x_1^*-\underline x_1<x_2^*-\underline x_2;

comparing equal $r,\sigma^2$ and $\delta_1<\delta_2$ , for all small $K$ , both thresholds decrease and the gap increases:

x_2^*<x_1^*,\qquad\underline x_2<\underline x_1,\qquad x_1^*-\underline x_1<x_2^*-\underline x_2;

comparing equal $\sigma^2,\delta$ and arbitrary $r_1,r_2$ ,

\frac{x_1^*-x_2^*}{x_1^*-\tfrac12}\to0,\qquad\frac{\underline x_1-\underline x_2}{\underline x_1-\tfrac12}\to0 .

The goal fixes no constant. It asserts only the directions and the vanishing relative effect of $r$ , so it survives any refinement of the expansions.

Milestones

In attack order:

(14)–(15) follow from (5)–(9);
Proposition 1, existence part: a solution branch exists;
the polynomial form (x)–(xi) of (14)–(15);
the identities (xii) and (xiii);
the limit (xviii): $\lim_{G\to1}\big(\log G-2\tfrac{G-1}{G+1}\big)/(G-1)^3=\tfrac1{12}$ ;
convergence $\underline x,x^*\to\tfrac12$ ;
the limits (xix): $(G-1)^3/K\to36r\lambda/\delta$ , and (xx): $(y-2)/(G-1)^2\to-\delta^2\sigma^2/(54r)$ ;
the expansions (16)–(18):

x^*=\tfrac12+\sqrt[3]{\tfrac{9\sigma^2}{4\delta}}K^{1/3}+\tfrac12\sqrt[3]{\tfrac{\delta\sigma^4}{18}}K^{2/3}+o(K^{2/3}),\quad \underline x=\tfrac12+\sqrt[3]{\tfrac{9\sigma^2}{4\delta}}K^{1/3}-\tfrac12\sqrt[3]{\tfrac{\delta\sigma^4}{18}}K^{2/3}+o(K^{2/3}),\quad \frac{x^*-\underline x}{K^{2/3}}\to\sqrt[3]{\tfrac{\delta\sigma^4}{18}} .

Significance

The result. Proposition 2 is the paper's main qualitative statement about cheap repositioning. More volatile tastes make firms wait longer before moving: with high $\sigma^2$ the consumers are likely to drift back. A more important repositioning attribute makes them move sooner. In both cases the band $(\underline x,x^*)$ , in which same-side firms randomize, widens. Patience, by contrast, drops out to first order. The $K^{1/3}$ law also quantifies how strongly repositioning reacts to its cost: a small cost has a large effect on behaviour.

Formalizing it. The result is proved in the paper by an asymptotic computation in its appendix. As far as a search of the Prove2Me catalog shows, none of it is formalized. The mission produces a checked version of every step, in the paper's own notation. Two places need more than transcription. The printed (16)–(17) have right sides that still depend on $K$ , so they are restated as two-term expansions. The paper also never states that solutions of (14)–(15) exist for small $K$ ; the existence milestone supplies that.

Difficulty

The thresholds are defined only implicitly, as solutions of a transcendental system, and the goal is about every solution branch. Nothing is known in advance about such a branch: not continuity, not uniqueness, not a closed form. The natural first idea, to substitute the expansions (16)–(18) and compare coefficients, assumes what has to be shown. The expansions must be derived from (14)–(15) for an arbitrary branch.

The derivation is delicate because the leading behaviour cancels. The left side of (xii) vanishes to third order at $G=1$ , so the rate of $G-1$ is the cube root of a ratio of small quantities. The gap $x^*-\underline x$ is of order $K^{2/3}$ , one order below the thresholds' own displacement. Clause 4 of the goal needs the leading coefficient to be independent of $r$ , and clauses 2–3 need strict inequalities between leading coefficients.

Formalization scope

All quantities are real. The parameters are a structure with fields r, σ2 (the variance $\sigma^2$ itself) and δ, and Standing requires all three to be positive. Primes are deriv evaluated at the point, and $\pi_d'$ is the derivative of pid, not a hand-coded formula. Equations (14)–(15) keep the paper's ratio form: since $G>0$ , a vanishing denominator makes them false, not vacuously true. The milestone deriving (14)–(15) from (5)–(9) states the displayed ratios with both denominators nonzero.

Commitments beyond the printed text:

The region. A threshold pair must satisfy $\tfrac12<\underline x<x^*<1$ , the paper's own description of the thresholds, and $\delta(2x^*-1)<3$ , which keeps the far firm's Hotelling price positive. The latter is not a global restriction on $\delta$ : the paper's examples use $\delta=4$ .
Small $K$ . "For a small $K$ " and "K not too large" mean "for all sufficiently small $K>0$ ". Limits are along $K\to0^+$ .
Infinitely fast. This is divergence of the chord slope $(x^*(K)-\tfrac12)/K$ , since no differentiability in $K$ is established.
The effect of $r$ . Its vanishing is relative to the displacement of the threshold from $\tfrac12$ .
(16)–(17) are two-term expansions.

Two readings are ruled out as trivializing. Defining the thresholds by formulas, or assuming (16)–(18) for the branch, would make the goal a computation; the goal instead quantifies over every branch. Stating clause 4 as $x_1^*-x_2^*\to0$ would be contentless, because both thresholds tend to $\tfrac12$ .

The development needs real asymptotics: Taylor control of $\log$ near $1$ , cube roots as real powers, and filters on $(0,\infty)$ . It needs no stochastic calculus, since the value functions enter only through their closed forms. The limit (xviii) and the asymptotic analysis of an implicitly defined branch are reusable beyond this paper. Contributions to any milestone are welcome. Not formalized: the hazard rate (13), the verification that the thresholds form a Markov perfect equilibrium, Propositions 3–6, the asymmetric equilibrium and the limit $r\to0$ .

Selected references

Z. Eddie Ning and J. Miguel Villas-Boas, Following the Customers: Dynamic Competitive Repositioning, SSRN working paper 3695318, December 2020. https://ssrn.com/abstract=3695318
Z. Eddie Ning and J. Miguel Villas-Boas, Following the Customers: Dynamic Competitive Repositioning, Management Science, published version. https://doi.org/10.1287/mnsc.2021.3962
Harold Hotelling, Stability in Competition, The Economic Journal 39(153), 41–57, 1929. https://doi.org/10.2307/2224214

12 thms3 active usersReviewed

Completed

Economics Operations Research Probability·Captain: mikedeng1

Ranking Distributions When Only Means and Variances Are Known: Y Dominates X by First-Order Almost Stochastic Dominance for γ ≥ 1/(1 + 2t(t + √(t² + 1))), t = (μ_Y − μ_X)/(σ_Y + σ_X)Research Paper

Motivation

Decision analysts routinely have to rank two risky prospects, with returns $X$ and $Y$ , when nothing is known about them beyond a mean and a standard deviation for each. The classical tools are of two kinds. First-order stochastic dominance (FSD) ranks $Y$ above $X$ for every increasing utility, but it can never be certified from means and variances alone: with only the first two moments fixed, the admissible laws of $X$ and $Y$ include pairs that FSD does not rank. Mean–variance rules such as the Sharpe ratio rank everything, but lack a general expected-utility justification. Müller, Scarsini, Tsetlin and Winkler (Ranking distributions when only means and variances are known, Operations Research 69(3), 2021; SSRN 3440103) close the gap by restricting the utilities: they bound the ratio of marginal utilities, and they ask how strong that bound must be for every pair of laws with the given moments to be ranked.

The relevant order between the two extremes is almost first-order stochastic dominance (AFSD), introduced by Leshno and Levy (Management Science, 2002) to rule out "pathological" utilities that FSD must accommodate. Müller, Scarsini, Tsetlin and Winkler (Management Science, 2017) discuss that this symmetric case of their order is AFSD, i.e. the order generated by utilities whose marginal utilities differ at most by a fixed factor. Leshno and Levy computed the smallest parameter for which one given pair of laws is ranked; the present mission concerns a bound that holds for all pairs with prescribed means and variances.

Setting

Fix $\gamma_{cv},\gamma_{cx}\in\mathbb R$ . The utility class $\mathcal U_{\gamma_{cv},\gamma_{cx}}$ consists of continuously differentiable $u:\mathbb R\to\mathbb R$ with

0\le\gamma_{cv}\,u'(y)\le u'(x)\quad\text{and}\quad0\le\gamma_{cx}\,u'(x)\le u'(y)\qquad\text{for all }x\le y.

For $0\le\gamma_{cv},\gamma_{cx}\le1$ and real random variables $X,Y$ , $Y$ dominates $X$ by $(1+\gamma_{cv},1+\gamma_{cx})$ -SD, written $X\le_{(1+\gamma_{cv},1+\gamma_{cx})}Y$ , if $\mathbb E\,u(X)\le\mathbb E\,u(Y)$ for every $u\in\mathcal U_{\gamma_{cv},\gamma_{cx}}$ . The symmetric case $\gamma_{cv}=\gamma_{cx}=\gamma$ is $\varepsilon$ -AFSD with $\varepsilon=\gamma/(1+\gamma)$ : $\gamma=0$ gives FSD, and $\gamma=1$ gives the increasing affine utilities, i.e. ranking by means. Increasing $\gamma$ shrinks $\mathcal U_{\gamma,\gamma}$ and makes the order easier to satisfy.

Write $\mu_X,\mu_Y$ for the means and $\sigma_X,\sigma_Y$ for the standard deviations, and

t=\frac{\mu_Y-\mu_X}{\sigma_Y+\sigma_X},\qquad \gamma^*=\frac{1}{1+2t\big(t+\sqrt{t^2+1}\big)}.

The quantity $t$ is a standardized advantage of $Y$ over $X$ ; $\gamma^*$ decreases from $1$ at $t=0$ towards $0$ as $t\to\infty$ .

The proof works with the piecewise-linear utilities $u_U(x;\delta)=\gamma(x-\delta)+(1-\gamma)(x-\delta)_+$ and $u_L(x;\delta)=\gamma(x-\delta)-(1-\gamma)(\delta-x)_+$ , with $x_+=\max\{x,0\}$ , and with the closed forms

B(\gamma,\delta)=\gamma(\mu_X-\delta)+(1-\gamma)\tfrac12\Big(\mu_X-\delta+\sqrt{\sigma_X^2+(\mu_X-\delta)^2}\Big),\quad A(\gamma,\delta)=\gamma(\mu_Y-\delta)-(1-\gamma)\tfrac12\Big(\delta-\mu_Y+\sqrt{\sigma_Y^2+(\mu_Y-\delta)^2}\Big),

the paper's worst-case values of $\mathbb E\,u_U(X;\delta)$ and $\mathbb E\,u_L(Y;\delta)$ given the moments, and the point $\delta^*=(\mu_X\sigma_Y+\mu_Y\sigma_X)/(\sigma_Y+\sigma_X)$ .

Formalization targets

Goal: Theorem 7 (p. 6)

For square-integrable $X,Y$ with $\mu_Y>\mu_X$ ,

\gamma^*\le\gamma\le1\ \Longrightarrow\ X\le_{(1+\gamma,1+\gamma)}Y.

The goal quantifies over all $X,Y$ with the given moments; nothing about their laws is fixed. The upper bound $\gamma\le1$ is the domain of the order in Definition 1(b).

Milestones (proof of Theorem 7, pp. 6–8)

Every $v\in\mathcal U_{\gamma,\gamma}$ with $0<\gamma\le1$ is $a\,u+b$ with $a\ge0$ , $u(\delta)=0$ and $\gamma\le u'\le1$ .
Such a $u$ satisfies $u_L(x;\delta)\le u(x)\le u_U(x;\delta)$ .
Lemma 4 (Scarf's bound) $\mathbb E\,X_+\le\frac12\big(\mu+\sqrt{\sigma^2+\mu^2}\big)$ — already proved on the platform as PricingRM.DetHeuristic.gallego_bound (the case $C=0$ ).
$\mathbb E\,u_U(X;\delta)\le B(\gamma,\delta)$ and 5. $\mathbb E\,u_L(Y;\delta)\ge A(\gamma,\delta)$ .
$\dfrac{f(-t)}{2t+f(-t)}=\dfrac{-t+\sqrt{1+t^2}}{t+\sqrt{1+t^2}}=\gamma^*$ , with $f(z)=z+\sqrt{1+z^2}$ .
$A(\gamma,\delta^*)\ge B(\gamma,\delta^*)$ for all $\gamma\ge\gamma^*$ .
$\delta^*$ is the unique minimizer of $h(\delta)=\sigma_Y f\big(\frac{\delta-\mu_Y}{\sigma_Y}\big)+\sigma_X f\big(\frac{\mu_X-\delta}{\sigma_X}\big)$ for $\sigma_X,\sigma_Y>0$ .

Significance

The result. Theorem 7 turns two summary statistics into an expected-utility guarantee: once $(\mu_Y-\mu_X)/(\sigma_Y+\sigma_X)$ exceeds the value making $\gamma^*\le\gamma$ , every decision maker whose marginal utility varies by at most the factor $1/\gamma$ prefers $Y$ , concave or not. It complements the paper's Theorems 3 and 6, which restrict to concave and to convex utilities and give tight bounds in $(\mu_Y-\mu_X)/\sigma_Y$ and $(\mu_Y-\mu_X)/\sigma_X$ ; the class $\mathcal U_{\gamma,\gamma}$ contains utilities that are neither, and both standard deviations enter. The paper's Example 8 shows the practical use: with $\gamma=0.37$ the rule " $t>0.53$ " settles a project choice for a whole team with heterogeneous, non-concave preferences. The authors note that the bound of Theorem 7 is not tight; the tight constant is open in the paper (Remarks 9–10).

Formalizing it. The result is proved in the paper; none of it is formalized. A formal development produces a reusable definition of the bounded-marginal-utility-ratio class and of AFSD in Mathlib's probability language, distribution-free bounds on expectations of piecewise-linear functions of a square-integrable variable, and a machine-checked version of the threshold. The Scarf/Gallego bound, which the proof uses twice, is already proved on the platform.

Difficulty

The obvious argument fails at the first step: a stochastic dominance relation is usually checked through distribution functions, but nothing about the distribution functions of $X$ and $Y$ is known. For concave utilities (Theorem 3) Jensen's inequality disposes of $X$ entirely, which is why that bound ignores $\sigma_X$ ; for the symmetric class no such step is available, both variables must be controlled at once, and the worst case over all laws with given moments must be computed in closed form for a family of utilities rather than for a single one. On the formal side, the normalization step needs the boundedness of $u'$ to be derived from the ratio condition (there is no supremum hypothesis), the bounds need integrability of $u(X)$ for an unbounded $u$ , and the threshold computation is real algebra with nested square roots.

Formalization scope

Random variables are measurable functions $X,Y:\Omega\to\mathbb R$ on one probability space $(\Omega,P)$ , with MemLp X 2 P and MemLp Y 2 P in the goal; only their laws matter. Means are Bochner integrals and $\sigma_X=\sqrt{\operatorname{Var}X}$ with Mathlib's variance, never free reals in the goal. "Continuously differentiable" is ContDiff ℝ 1 and $u'$ is deriv u. The order SDle carries $0\le\gamma_{cv},\gamma_{cx}\le1$ and integrability of $X$ and $Y$ , because the identity utility is in the class. It compares the expectations for every utility in the class for which both compositions are integrable. This excludes Lean's zero value for a non-integrable integral from a comparison, while keeping the order reflexive when $\gamma=0$ ; every class utility is integrable under the goal's hypotheses. Divisions follow Lean's $a/0=0$ ; when $\sigma_X=\sigma_Y=0$ the paper's $t$ is undefined, Lean gives $t=0$ and $\gamma^*=1$ , and the goal then asserts dominance for increasing affine utilities only, which is true. The worst-case quantities $B$ and $A$ are stated as the inequalities the proof uses; attainment (the two-point laws) is not formalized.

A trivializing formalization is ruled out: the goal is stated for every $u$ in the class, not only for $u_U,u_L$ or at a fixed $\delta$ ; for every pair $X,Y$ with the moments as hypotheses, not for chosen laws; and with $\gamma\le1$ , since for $\gamma>1$ the class contains only constants.

A complete development needs: the mean value inequality for deriv; integrability of Lipschitz functions of an $L^2$ variable; the Gallego bound (available); and elementary real algebra with Real.sqrt. The utility class, the order, and the bounds on $\mathbb E\,u_U$ , $\mathbb E\,u_L$ are reusable for Theorems 3 and 6 of the same paper and for other almost-dominance results. Proofs of any milestone, alternative proofs of the goal, and formalizations of Theorems 3 and 6 are welcome.

Selected references

A. Müller, M. Scarsini, I. Tsetlin, R. L. Winkler, Ranking distributions when only means and variances are known, Operations Research 69(3), 2021; INSEAD Working Paper 2020/36/DSC, 2020. https://ssrn.com/abstract=3440103
A. Müller, M. Scarsini, I. Tsetlin, R. L. Winkler, Between first- and second-order stochastic dominance, Management Science 63(9):2933–2947, 2017.
M. Leshno, H. Levy, Preferred by "all" and preferred by "most" decision makers: almost stochastic dominance, Management Science 48(8):1074–1085, 2002.
H. Scarf, A min-max solution of an inventory problem, in K. J. Arrow, S. Karlin, H. Scarf (eds.), Studies in the Mathematical Theory of Inventory and Production, pp. 201–209, Stanford University Press, 1958.
J. R. Birge, J. H. Dulá, Bounding separable recourse functions with limited distribution information, Annals of Operations Research 30:277–298, 1991.

10 thms3 active usersReviewed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

The Role of Problem Specification in Crowdsourcing Contests for Design Problems: A Theoretical and Empirical Analysis: Unique Symmetric Equilibrium and Participation Monotone in Disclosed ObjectivesResearch Paper

Motivation

Firms increasingly source design work (logos, packaging, product sketches) through crowdsourcing contests: a seeker posts a problem statement and an award, independent designers submit entries, and the best entry wins. The problem statement is the seeker's main lever. It can list conceptual objectives (what the design should convey) and execution guidelines (fonts, colours, shapes to use). Practitioners disagree on how much to specify: more detail tells designers what the seeker values, but also raises the effort needed to take part.

Jiang, Huang and Beil (SSRN 3260862, 2018; Manufacturing & Service Operations Management, 2021, doi:10.1287/msom.2020.0873) model this trade-off and test it on data from a design-contest platform. Their theory builds on the contest model of Terwiesch and Xu (Management Science 54(9):1529–1543, 2008), in which designers generate several trials with Gumbel-distributed quality shocks and free entry fixes the number of participants. The new ingredient is the problem statement: the number $S_r$ of disclosed objectives and the number $S_g$ of execution guidelines enter designers' costs and the quality of their designs. Theorem 1 of the paper describes how designers respond. This mission formalizes that theorem.

Setting

A seeker offers an award $A>0$ and discloses $S_r\ge0$ conceptual objectives and $S_g\ge0$ execution guidelines. A designer who takes part chooses the number $r_i\ge0$ of objectives to incorporate and the number $m_i>0$ of design trials to generate. Objectives beyond the $S_r$ disclosed must be guessed.

Quality. Each incorporated disclosed objective adds $w>0$ to a design's baseline quality, and each guessed one adds $\nu w$ with $\nu\in(0,1)$ : $v(r)=rw$ for $r\le S_r$ and $v(r)=S_rw+(r-S_r)\nu w$ for $r>S_r$ . A trial's quality is $v(r_i)$ plus an independent zero-mean Gumbel shock of scale $\mu>0$ , and only a designer's best trial counts.
Cost (equation (1)):

C_i(r_i,m_i)=c_g(r_i-S_r)^+ + c_1S_r + c_2(1/p)^{r_i} + c_3m_i,\qquad c_3=h(S_g).

Here $c_g>c_1\ge0$ are the unit costs of guessing and of understanding an objective, $p\in(0,1)$ is the probability that a sampled concept meets one objective (so $(1/p)^{r_i}$ attempts are expected, each costing $c_2>0$ ), and $h$ is decreasing.

Win probability (A.1). Against $N-1$ opponents playing $(r,m)$ ,

\Pr(i\text{ wins})=\frac{m_ie^{v(r_i)/\mu}}{m_ie^{v(r_i)/\mu}+(N-1)me^{v(r)/\mu}},

and a participant's expected utility is $\Pr(i\text{ wins})\cdot A-C_i(r_i,m_i)$ . Not taking part yields the outside option $s>0$ .

Equilibrium. Given $N$ participants, $(r,m)$ is a symmetric equilibrium when no participant gains from any deviation $(r_i,m_i)$ . The free-entry level $N^*$ is the number of participants at which the $N$ -th designer's equilibrium utility equals $s$ and every additional designer's would fall below $s$ .
Thresholds. With $L=\ln(1/p)$ :

\bar r=\tfrac1L\ln\!\Big(\tfrac{N-1}{N^2}\tfrac{w}{\mu}\tfrac{A}{c_2}\tfrac1L\Big),\qquad \bar r^g=\tfrac1L\ln\!\Big(\tfrac{N-1}{N^2}\tfrac{\nu w}{\mu}\tfrac{A}{c_2}\tfrac1L-\tfrac{c_g}{c_2}\tfrac1L\Big).

Formalization targets

Goal: Theorem 1 (p. 9)

Given $N>1$ , every symmetric equilibrium is

r^*=\begin{cases}\bar r^g,&S_r<\bar r^g,\\S_r,&\bar r^g\le S_r\le\bar r,\\\bar r,&S_r>\bar r,\end{cases}\qquad m^*=\frac{A(N-1)}{N^2c_3}.

$N^*$ does not depend on $S_g$ .
$N^*$ strictly increases with $S_r$ where designers guess ( $S_r<\bar r^g$ ) and does not increase where they do not.
At a fixed $N$ , more execution guidance strictly raises $m^*$ and leaves $r^*$ unchanged (p. 10).

Milestones (Appendix A)

The win probability (A.1) from Gumbel shocks; the marginal winning chance; the trial-effort condition (A.3); $\bar r^g<\bar r$ ; the equilibrium characterization (A.2)–(A.3) at fixed $N$ ; $\Pr(i\text{ wins})=1/N$ and an entry utility free of $c_3$ ; the closed forms (A.5) $N_1^*=\sqrt{A/(s+c_1S_r+c_2(1/p)^{S_r})}$ and (A.6) $N_2^*=(\sqrt{4Y(X+1)+X^2}-X)/(2Y)$ ; the rise of the entry utility with $S_r$ in Region 0; and the decrease of $N_1^*$ and $N_2^*$ in $S_r$ .

Significance

Theorem 1 is the paper's theoretical core. It predicts an inverted-U relation between disclosed objectives and participation, and no effect of execution guidelines on participation, only on effort. Section 4 turns these predictions into hypotheses, and §5 tests them on contest data. The seeker's optimal disclosure (Proposition 1) is derived from the same characterization.

The theorem is published with a proof in the appendix, but nothing in it has been machine-checked. A formal development makes three of the paper's choices explicit. It separates the parts of the proof that are first-order algebra from the parts that need a global argument. It states the free-entry level as a condition, not as a root of a formula. And it isolates the claims the proof does not support (see Formalization scope). The contest model (logit win probability, cost (1), free entry) is shared with other crowdsourcing models built on Terwiesch and Xu (2008), and its definitions can be reused for them.

Difficulty

The payoff is not concave in the designer's choices. The win probability (A.1) is a logistic function of $v(r_i)$ , convex while $\Pr(i\text{ wins})<1/2$ , so first-order conditions do not identify best responses. A newcomer's first idea, "solve the first-order conditions and invoke concavity", fails. Uniqueness survives because any equilibrium must satisfy the first-order conditions, but at the kink $r=S_r$ only one-sided conditions are available, and they must be combined into the three regions of (A.2).

The monotonicity of $N^*$ is a second difficulty. The entry utility $U(N;S_r)$ is not monotone in $N$ , so $U=s$ can have several roots and $N^*$ can jump as $S_r$ varies. The region-0 formula (A.4) is implicit, because $\bar r^g$ depends on $N$ . Comparing $N^*$ at two values of $S_r$ therefore needs the largest-root description of free entry, not a closed form.

Formalization scope

Everything is real-valued, as the paper allows (p. 9). The namespace is ProblemSpec.Equilibrium. A single definition file holds the parameters, the standing assumptions, $v$ , $C_i$ , (A.1), the expected utility, the symmetric equilibrium, $\bar r$ , $\bar r^g$ , $r^*$ , $m^*$ , the entry utility, the free-entry condition and the closed forms $N_1^*$ , $N_2^*$ . The win probability is (A.1) itself, for real $m_i,m$ , as in the paper. The milestone (A.1) connects it to i.i.d. Gumbel shocks for integer trial counts, using the published Gumbel law of AssortSearch.Cannibal.Model.

The formalization commits to the following conventions and additions:

$0<p<1$ (the page has $p\in[0,1]$ , where $(1/p)^r$ or $\ln(1/p)$ degenerate);
$s>0$ ((A.6) divides by $Y$ );
$h>0$ and strictly decreasing (the page says "decreasing"; strictness makes $m^*$ strictly increase in $S_g$ , as p. 10 states);
$\bar r(N)\ge0$ wherever an equilibrium is characterized (the page's " $w$ is not trivially small"), which excludes the corner $r=0$ ;
"Designers guess" means the argument of the logarithm in $\bar r^g$ is positive and $S_r<\bar r^g$ ;
a symmetric equilibrium is a global best response over $r_i\ge0$ , $m_i>0$ , never a first-order condition;
$N^*$ is the free-entry level of App. p. 2 (equality at $N$ , strict loss for every $N'>N$ ), never a closed form. Defining $N^*$ by (A.5)/(A.6), or the equilibrium by its first-order conditions, would make the goal close to trivial, and both are excluded.

Two claims of the page are not stated. Existence is false. Theorem 1 says $(r^*,m^*)$ is the symmetric equilibrium. At $A=314.768$ , $s=3.492$ , $p=0.841$ , $c_2=4.437$ , $\mu=7.369$ , $w=0.808$ , $c_1=2.694$ , $c_g=3.724$ , $\nu=0.93$ , $h\equiv4.832$ , $S_r=0$ , the free-entry level is $N^*\approx6.3007$ , with $r^*=0$ , $\bar r\approx10.35$ , $m^*\approx8.698$ and equilibrium utility $s=3.492$ . A designer who deviates to $r_i=9.925$ , $m_i\approx16.28$ earns about $14.74$ . The goal therefore states uniqueness only. The "first … then" ordering is stated region by region. Monotonicity holds on the points where designers guess and on the points where they do not, but the guessing points need not form an initial segment of $S_r$ values, because $N^*$ can jump. "Decreases" is weak, since with $c_1=0$ , $N_2^*$ is constant.

Not in scope: Lemma 1, Proposition 1 and Lemmas 2–8 (the seeker's problem and extensions), and the empirical sections.

Welcome contributions: proofs of the milestones, especially the uniqueness argument at the kink $r=S_r$ , the Gumbel computation (A.1), and the comparison of free-entry levels in the goal's part 3.

Selected references

Z. Jiang, Y. Huang, D. R. Beil, The Role of Problem Specification in Crowdsourcing Contests for Design Problems: A Theoretical and Empirical Analysis, SSRN 3260862 (version of 30 Oct 2019); Manufacturing & Service Operations Management, 2021. https://ssrn.com/abstract=3260862, https://doi.org/10.1287/msom.2020.0873
C. Terwiesch, Y. Xu, Innovation Contests, Open Innovation, and Multiagent Problem Solving, Management Science 54(9):1529–1543, 2008. https://doi.org/10.1287/mnsc.1080.0884
D. Fudenberg, J. Tirole, Game Theory, MIT Press (cited by the paper, as the 2000 printing, for existence of a pure-strategy equilibrium; its Theorem 1.2 assumes quasi-concave payoffs). https://mitpress.mit.edu/9780262061414/game-theory/

13 thms3 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Information Acquisition, Decision Making, and Implementation in Organizations: Homogeneous Organization Optimal for Weak Signals, Heterogeneous Optimal Above a Threshold in k for Strong SignalsResearch Paper

Motivation

In most organizations the person who decides is not the person who carries the decision out. A board ratifies a product and engineers build it; a studio approves a film and a director makes it. The implementer usually also knows more, or can learn more, about which course of action will work. A long literature in organizational economics asks whether such an organization should be staffed with people who share the decision maker's preferences or with people who disagree with her: Aghion and Tirole (1997) on formal and real authority, Dessein (2002) on communication, Van den Steen (2010) on homogeneity, and Landier, Sraer and Thesmar (2009) on "optimal dissent" between a decision maker and an implementer.

Itoh and Morita add endogenous information acquisition to the decision–implementation setting of Landier et al. The implementer chooses how much effort to spend learning which project is efficient, and that choice responds to whether his preferences agree with the decision maker's. Their main result (Proposition 2) says when the principal, who only cares about success, should prefer a heterogeneous organization (one where the two agents disagree) to a homogeneous one.

Setting

A principal employs a decision maker (DM) and an implementer (IM). There are two projects $d\in\{1,2\}$ and two equally likely states $\theta\in\{1,2\}$ ; project $d$ is efficient iff $\theta=d$ . A project succeeds iff it is efficient and IM exerts implementation effort, which costs him a random $\tilde c$ with CDF $F$ and density $f$ , where $F(0)=0$ , $F$ is strictly increasing on $[0,\infty)$ and $F(b_H)\le1$ . Success is worth $1$ to the principal.

On success, DM receives $B_H$ from her favourite project 1 and $B_L<B_H$ from project 2. IM receives $b_H$ from his favourite project and $b_L<b_H$ from the other. The organization is homogeneous if IM's favourite is project 1 and heterogeneous if it is project 2. Write $\Gamma=B_H/B_L$ and $\gamma=b_H/b_L$ for the two biases.

Before the project is chosen, IM picks information effort $\pi\in[0,1]$ at cost $\pi^2/(2k)$ , $k>0$ . With probability $\pi$ he observes a signal $\sigma\in\{1,2\}$ that points to the efficient project with probability $\alpha\in(1/2,1]$ ; otherwise $\sigma=\phi$ . The signal is public. The posterior that project $d$ is efficient is $1/2$ after $\phi$ , $\alpha$ after $\sigma=d$ , and $1-\alpha$ after $\sigma\ne d$ .

Moves are solved backwards:

IM implements iff $\tilde c$ is at most his expected benefit, so the success probability is $p(b,d,\sigma)=\Pr[\theta=d\mid\sigma]\,F(\Pr[\theta=d\mid\sigma]\,b)$ .
DM chooses the project with the larger $p(b,d,\sigma)B$ , and project 1 when indifferent.
IM chooses $\pi$ to maximize his expected net benefit minus $\pi^2/(2k)$ .
The principal's payoff $V_{hom}(\alpha,k)$ or $V_{het}(\alpha,k)$ is the resulting success probability.

Three thresholds in $\alpha$ appear: $\alpha_{hom}$ , $\alpha_{het}$ and $\hat\alpha$ , the solutions of

\alpha F(\alpha b_L)=(1-\alpha)F((1-\alpha)b_H)\Gamma,\quad \alpha F(\alpha b_H)=(1-\alpha)F((1-\alpha)b_L)\Gamma,\quad \alpha F(\alpha b_L)=(1-\alpha)F((1-\alpha)b_H).

DM follows a signal for project 2 iff $\alpha>\alpha_{hom}$ (homogeneous) or $\alpha>\alpha_{het}$ (heterogeneous). Let $\hat\alpha_{het}=\max\{\alpha_{het},\hat\alpha\}$ , and let $\bar k_h(\alpha)$ be the least $k$ at which IM's optimal effort in organization $h$ reaches $1$ .

The paper's assumptions are:

Assumption 1, $\Gamma\ge F(b_H/2)/F(b_L/2)$ ;
Assumption 2, $\Gamma\ge\gamma$ ;
Assumption 3, $xf(x)$ weakly increasing on $x>0$ .

Formalization targets

Goal: Proposition 2

Under Assumptions 1–3:

\alpha\in(1/2,\alpha_{het}]\ \Longrightarrow\ V_{het}(\alpha,k)<V_{hom}(\alpha,k)\quad\text{for all }k>0,

and for $\alpha\in(\hat\alpha_{het},1]$ there is $k(\alpha)\in(0,\bar k_{het}(\alpha))$ with

V_{het}(\alpha,k)<V_{hom}(\alpha,k)\ (k<k(\alpha)),\qquad V_{het}(\alpha,k)\ge V_{hom}(\alpha,k)\ (k\ge k(\alpha)),

strictly for $k\in(k(\alpha),\bar k_{hom}(\alpha))$ . The threshold $k(\alpha)$ is existential, not a formula.

Milestones

In attack order:

Lemma 1: $1/2\le\alpha_{het}<\alpha_{hom}<1$ , and DM's choice in the three $\alpha$ -regions.
IM's net benefit equals $K(x)=\int_0^xF$ , which is increasing and strictly convex (§3.3, p. 17).
IM's optimal effort is $\min\{k\cdot(\text{marginal benefit}),1\}$ (pp. 18–20).
Lemma 2: the reactive homogeneous effort is positive.
Proposition 1: the comparison of the two efforts.
The closed forms of $V_{hom},V_{het}$ (Appendix A3).
Lemmas A1, A2, A3: the three regions of Proposition 2.

Significance

The result. Proposition 2 identifies a channel through which disagreement between a decision maker and an implementer raises an organization's success probability: the implementer, anticipating that without information the decision maker will pick his unfavourite project, invests more in information (the paper's "ignorance-avoiding effect"). Against this, a heterogeneous implementer is less willing to execute the decision maker's default. The proposition says exactly when each force wins: never for weak signals, and above a cost threshold $k(\alpha)$ for informative ones. Corollary 1 and the comparative statics of Proposition 3 build on it.

Formalizing it. The result is proved in the paper; this mission formalizes the statement from the primitives (DM's argmax, IM's maximizer, success probability) rather than from the closed forms, and then the paper's chain of lemmas. Two of the paper's arguments need repair along the way: the proofs of Lemmas A2 and A3 claim the payoff difference is increasing in $k$ , which fails once the heterogeneous effort saturates at $1$ , although the lemma statements remain true. No part of this model is formalized elsewhere.

Difficulty

The comparison is between two maximizers of different concave programs, each built on a different branch of DM's decision rule, so the obvious argument of differentiating $V_{het}-V_{hom}$ in $k$ has to handle kinks: the efforts are $\min\{k\cdot\text{const},1\}$ and saturate at different $k$ , and DM's choice switches at different $\alpha$ . The single-crossing property in $k$ (one sign change of $V_{het}-V_{hom}$ ) is not monotonicity of the difference on the whole half-line; on the interval where only the heterogeneous effort is saturated the difference is not increasing, and the sign has to be read off directly. For $\alpha\in(\alpha_{het},\alpha_{hom}]$ DM reacts in one organization and not the other, and the positivity of the relevant brackets rests on the definition of $\hat\alpha$ and on Assumption 3.

Formalization scope

All quantities are real. The model is one definition file, OrgDiversity.Optimal.Model:

Parameters. A record of $b_L,b_H,B_L,B_H,F,f$ , with the standing assumptions as one predicate.
Density and regularity. The paper calls $f$ the density of $F$ ; Standing makes this precise by requiring $f$ to be integrable on every $[0,x]$ and $F(x)=\int_0^x f(c)\,dc$ for $x\ge0$ . The formalization also assumes $F$ is continuous on $[0,\infty)$ and $F'=f$ on $(0,\infty)$ .
Domain of $F$ . " $F$ strictly increasing" is read on $[0,\infty)$ , which is the only reading consistent with $F(0)=0$ .
Signal. It is encoded by the posteriors the paper states, not by a joint law.
Thresholds. $\alpha_{hom},\alpha_{het},\hat\alpha$ are passed as solutions of their equations, in the intervals $(1/2,1)$ , $[1/2,1)$ and $(1/2,1)$ . Each solution is unique, and existence of the first two is part of Lemma 1.
The bound $\bar k_h(\alpha)$ . " $k<\bar k_h(\alpha)$ " is encoded as "the optimal effort is $<1$ ".
Tie-breaks. DM chooses project 1 when indifferent; IM implements when indifferent.
IM's net benefit. It is defined as on p. 17, $p\,b-\int_0^{x}c f(c)\,dc$ ; the identity with $\int_0^xF$ is a milestone.

$V$ is never defined by its closed form, and optimal efforts are arbitrary maximizers of IM's payoff on $[0,1]$ , not the formula $\min\{k\cdot\text{const},1\}$ ; stating the goal about the closed forms would reduce it to elementary inequalities and is ruled out.

Contributions of any milestone are welcome; the convexity lemma for $K$ and the maximizer of a concave quadratic on $[0,1]$ are reusable beyond this mission. Corollary 1, Proposition 3, §4 and the cheap-talk extension of §5 are not part of this mission.

Selected references

Hideshi Itoh and Kimiyuki Morita, Information Acquisition, Decision Making, and Implementation in Organizations, Management Science, 2022. https://doi.org/10.1287/mnsc.2022.4373 — read in the SSRN version of August 5, 2019, https://ssrn.com/abstract=2751969
Augustin Landier, David Sraer and David Thesmar, Optimal Dissent in Organizations, Review of Economic Studies 76, 761–794, 2009.
Wouter Dessein, Authority and Communication in Organizations, Review of Economic Studies 69, 811–838, 2002.
Philippe Aghion and Jean Tirole, Formal and Real Authority in Organizations, Journal of Political Economy 105, 1–29, 1997.
Eric Van den Steen, Culture Clash: The Costs and Benefits of Homogeneity, Management Science 56, 1718–1738, 2010.

11 thms3 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Curbing Emissions: Environmental Regulations and Product Offerings Across Markets: Horizontal Negotiation Unifies a Split Market at the Exact Global Standard and Lowers Total EmissionsResearch Paper

Motivation

Energy-efficiency and emission standards for products such as vehicles and appliances are set by regulators whose jurisdictions overlap a single manufacturer's markets. The best-known case is United States fuel-economy regulation. California has long been allowed to set stricter vehicle standards than the federal government, and the 2019 dispute between California and the federal administration over a single "50-state" standard put the question of split versus unified markets on the policy agenda. A manufacturer facing two different standards can sell two product versions (a split market), sell one version that meets the stricter standard everywhere (a unified market), or withdraw from the stricter market.

Han, Hu and Dawande (Curbing Emissions: Environmental Regulations and Product Offerings Across Markets, Manufacturing & Service Operations Management, 2022) model this as a game between an environmentally concerned regulator, an environmentally agnostic regulator, and a monopolist. They ask when the market splits, and whether negotiation between the regulators can unify a split market and lower total emissions. This mission formalizes their answer for one negotiation format, the exact global standard (§4.1.1), together with the base-model results it rests on. Citations refer to the authors' accepted manuscript of 28 July 2022, including its Online Appendices.

Setting

A monopolist sells in two markets $M_1, M_2$ of sizes $m_1, m_2 > 0$ . Regulator $R_i$ sets a minimum efficiency standard $s_i \ge 0$ for products sold in $M_i$ . Consumers' valuations are uniform on $[0, \bar u]$ . A consumer with valuation $u$ who buys a product of efficiency $e$ at price $p$ receives $u - p + \gamma e$ , where $\gamma$ is the efficiency bonus, and buys when this is positive. Producing efficiency $e$ costs $c e$ per unit plus a fixed setup cost $r > 0$ per product.

Regulator $R_1$ maximizes consumer utility in $M_1$ minus $h_1 \sum_i (b - e_i)\cdot\text{sales}_i$ . Here $b$ is a benchmark efficiency, $h_1$ is the perceived per-unit environmental impact, and the sum runs over both markets. Regulator $R_2$ maximizes consumer utility in $M_2$ only and therefore sets $s_2 = 0$ . The total emissions are $\sum_i (b - e_i)\cdot\text{sales}_i$ .

Given $s_1$ , the firm chooses among three strategies: $D$ (differentiated products at $s_1$ and $0$ ), $U$ (one unified product at $s_1$ in both markets), and $S$ (one product at $0$ , sold in $M_2$ only). Each product is priced at $p^* = [(c+\gamma)e + \bar u]/2$ . A base-model outcome is a standard $s_1 \ge 0$ together with a profit-maximizing strategy of the firm, such that $R_1$ cannot do better with another standard paired with any profit-maximizing response.

In the exact-standard negotiation, $R_1$ and $R_2$ agree on one standard $s_e$ for both markets and a transfer $t_h$ from $R_1$ to $R_2$ . Their total utility is $T_h(s_e)$ (eq. (4)). The disagreement point $(D_1, D_2)$ is the pair of utilities at the split-market base outcome, and the negotiated pair maximizes the Nash product $(\Pi_1 - D_1)(\Pi_2 - D_2)$ over the feasible pairs that split the gain equally.

Formalization targets

Goal: Proposition 3 (p. 19)

Assume condition (1) of Lemma A.1, where $\bar x$ is the larger root of an auxiliary quadratic:

0<r\le\min\Big\{\tfrac{m_2\bar u}{4}-\tfrac{m_2[\bar u-b(c-\gamma)]^2}{\bar u(4-\frac{c-\gamma}{h_1})^2},\ \tfrac{m_1[\bar u-b(c-\gamma)]^2}{\bar u(4-\frac{c-\gamma}{h_1})^2},\ \tfrac{m_2}{4\bar u}(\bar u^2-\bar x^2)\Big\}.

Then a split-market base outcome $(s_1, D)$ exists. For every such outcome, the negotiation has a Nash bargaining solution, and every solution has standard

s^*_e=\frac{2h_1[\bar u+b(c-\gamma)]-(c-\gamma)\bar u}{(c-\gamma)[4h_1-(c-\gamma)]}.

The regulators' total utility at $s^*_e$ strictly exceeds $D_1 + D_2$ , and total emissions at $s^*_e$ are strictly lower than at the split-market outcome.

Milestones

The optimal price $p^*$ (§3.1, p. 12).
Lemma 1 (p. 12): the firm's best response is $U$ for $s_1 \le \tau_U$ , $D$ for $\tau_U \le s_1 \le \tau_S$ , and $S$ for $s_1 \ge \tau_S$ .
The constant $\bar x$ is well defined (proof of Lemma A.1, Online Appendix p. 12).
Lemma A.1(1): under condition (1), $(s^*_{1D}, D)$ is a base-model outcome, and every split outcome has $s_1 = s^*_{1D}$ .
The arbitrator's optimal standard $s^*_a$ for eq. (3) (p. 16).
The reduction of the Nash bargaining solution to maximizing $T_h$ (§4.1.1, p. 19).
The closed-form gain $T_h(s^*_e) - D_1 - D_2$ (proof of Proposition 3, Online Appendix p. 13).
Proposition 2, split-market half (p. 16): a split outcome emits more than the arbitrator outcome.

Significance

The result. Proposition 3 shows that, whenever the base model predicts a split market under the paper's sufficient condition, two regulators who negotiate an exact global standard with side payments always reach agreement. The agreed standard unifies the market and lowers total emissions. The negotiated standard coincides with the standard a neutral arbitrator would choose. This makes the exact global standard the benchmark against which the paper compares its other negotiation formats (a baseline global standard, and vertical negotiation with the firm). It also qualifies the policy debate: unification through an exact standard requires the stricter regulator to give up its power to exceed the common standard.

Formalizing it. The proofs in Online Appendix C are short computations in which several steps are "straightforward" or "easy to show". In particular, the existence and use of $\bar x$ , the comparison between strategies at the regime boundaries, and the truncated branch of Proposition 2 are argued only briefly. A machine-checked development fixes the equilibrium notion, including how ties between strategies are treated, and verifies every inequality. To our knowledge none of these results has been formalized before.

Difficulty

The algebra of each step is elementary, but the base equilibrium is a bilevel object. $R_1$ optimizes over $s_1$ against a firm response that switches between three regimes at $\tau_U$ and $\tau_S$ , and $R_1$ 's utility is a different concave quadratic in each regime. Showing that the split outcome sits at $s^*_{1D}$ requires comparing the maximum over the $D$ regime with the maxima over the $U$ and $S$ regimes. Only the third term of condition (1), through the implicitly defined $\bar x$ , controls the $U$ comparison. Simply substituting the closed forms of Lemma A.1 into the negotiation does not prove the goal: the goal quantifies over every split-market base outcome, so the characterization of the base equilibrium must actually be established. The emissions comparison also needs a strict inequality. At $s^*_e = s^*_{1D}$ the emissions in $M_1$ are equal and only $M_2$ changes, and the case $s^*_e = 0$ must be excluded using condition (1).

Formalization scope

All quantities are real numbers in one parameter record $(c, \gamma, h_1, m_1, m_2, \bar u, b, r)$ , and every statement assumes the standing assumptions of §3: $c > 0$ , $r > 0$ , $h_1 \ge (c-\gamma)/2$ , and $\bar u \ge \max\{4r(m_1+m_2)/(m_1 m_2),\ b(c-\gamma)\}$ . The formalization departs from or adds to the page in these places:

the page's $c \ge \gamma$ is strengthened to $c > \gamma$ , because every threshold divides by $c - \gamma$ ;
$m_1, m_2 > 0$ and $b \ge 0$ are made explicit;
$\gamma$ 's sign is left free;
$s_2 = 0$ is fixed, as on p. 11;
the buying share is clipped to $[0,1]$ and the margin $\bar u - (c-\gamma)e$ at $0$ . On $[0, \bar u/(c-\gamma)]$ every quantity equals the page's formula, and above it a negative margin cannot square into a positive profit;
profits, sales and consumer utilities are the closed forms at $p^*$ ;
the firm's best response is not tie-broken, and a base-model outcome must beat $R_1$ 's utility at every alternative standard paired with every best response there. This makes the equilibrium value independent of tie-breaking;
$\bar x$ enters as the greatest element of the root set of $\pi_{1D}(s^*_{1D}) = \pi_{1U}((\bar u - x)/(c-\gamma))$ , and a milestone shows that this greatest element exists;
under condition (1) with equalities, a unified outcome can tie with the split outcome for $R_1$ , so Lemma A.1(1) is stated as " $(s^*_{1D}, D)$ is an outcome, and every split outcome has $s_1 = s^*_{1D}$ ", not as uniqueness of the outcome;
the page's positivity argument for the gain fails when $2h_1[\bar u + b(c-\gamma)] = (c-\gamma)\bar u$ , so positivity is stated under condition (1), which excludes that case.

A trivializing formalization is ruled out: the goal does not take the disagreement point from Lemma A.1's closed form or compare two formulas. It reads the disagreement point off an arbitrary split-market base outcome, asserts that one exists, and characterizes the negotiated standard through the Nash-product maximization. A sorry-free verification file checks that the goal's hypotheses hold together at a concrete parameter point ( $c = 1$ , $\gamma = 1/2$ , $h_1 = 1$ , $m_1 = m_2 = 1/2$ , $\bar u = 1000$ , $b = 100$ , $r = 20$ ).

The development needs only real algebra: quadratics, square roots and case analysis over three strategies. The lemmas on piecewise-quadratic best responses, and on the reduction of a transferable-utility Nash bargaining problem to total-utility maximization, may be reused for other regulator–firm models. Proofs of any milestone are welcome. Propositions 4 and 5 (baseline global standard, vertical negotiation) and the unified half of Proposition 2 are outside this mission.

Selected references

Z. Han, B. Hu, M. Dawande, Curbing Emissions: Environmental Regulations and Product Offerings Across Markets, Manufacturing & Service Operations Management, 2022. https://doi.org/10.1287/msom.2022.1141
J. F. Nash, The Bargaining Problem, Econometrica 18(2), 155–162, 1950. https://doi.org/10.2307/1907266

10 thms3 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Reciprocity in Dynamic Employment Relationships: Effort and Bonus Weakly Decrease and the Upfront Wage Weakly Increases over the Course of EmploymentResearch Paper

Motivation

Most employment relationships rely on incentives that no court enforces. A relational contract is a self-enforcing promise: the employer pays a discretionary bonus after observing effort, and keeps the promise because reneging would destroy the value of the future relationship (Bull 1987; MacLeod and Malcomson 1989; Levin 2003). This mechanism has a well-known weakness. When the relationship has a known last period, no bonus is credible in that period, and backward induction removes it from every earlier period as well.

A second source of incentives is reciprocity. Workers respond to a generous upfront wage with higher effort, the "gift exchange" of Akerlof (1982), a pattern documented in many laboratory and field studies. Fahn (Reciprocity in Dynamic Employment Relationships, Management Science 2023, doi:10.1287/mnsc.2022.4657; working paper CRC TRR 190 Discussion Paper No. 198, 2019) combines the two in a finite-horizon principal–agent model. In this model the agent's reciprocity is tied to the relational contract and vanishes if the principal reneges. Because reciprocity is valuable even in the last period, the employer has something to lose by reneging at every date, so bonuses stay credible despite the known end date.

The paper's main dynamic result, Proposition 1, describes how the two incentive instruments evolve over the relationship. This mission formalizes that result, together with the lemmas its proof uses, in the reduced optimization problem the paper derives. All page references are to the 2019 working paper.

Setting

There is one principal and one agent, both risk neutral, over periods $t=1,\dots,T$ with $1<T<\infty$ . Effort $e\ge0$ costs the agent $c(e)=e^3/3$ and yields output $e\theta$ to the principal, with productivity $\theta>0$ . The reciprocity parameter $\eta\ge0$ measures how strongly the agent responds to an upfront wage, and the two parties share a discount factor $\delta\in(0,1]$ .

In each period the principal pays an upfront wage $w\ge0$ before effort is chosen and may pay a bonus afterwards. An agent who reacts only to the wage chooses the deviation effort $\tilde e=\sqrt{\eta w\theta}$ . The paper reduces the equilibrium analysis (its Lemma 2) to the following per-period problem. To implement effort $e$ at wage $w$ , the principal must pay the bonus

b(e,w)=\frac{e^3}{3}-\eta w\theta e+\frac23\big(\sqrt{\eta w\theta}\big)^3 ,

and her per-period profit is $\pi(e,w)=e\theta-b(e,w)-w$ . A promised bonus is credible only if it does not exceed what the principal would lose by reneging. This is the dynamic enforcement constraint

b(e,w)\le\delta\,\Pi_{t+1},\tag{DE}

where $\Pi_{t+1}$ denotes the principal's continuation profit from period $t+1$ on, and $\Pi_{T+1}=0$ . A profit-maximizing path $(e_t,w_t,\Pi_t)_{t=1}^{T}$ is one in which, for every $t$ , the pair $(e_t,w_t)$ maximizes $\pi$ over $e,w\ge0$ subject to (DE), and $\Pi_t=\pi(e_t,w_t)+\delta\Pi_{t+1}$ . The bonus paid in period $t$ is $b_t=b(e_t,w_t)$ . In the last period the bound is $0$ , so the problem becomes the reciprocity spot contract, in which no bonus is paid.

The first-best levels maximize $\pi$ without (DE). (DE) is said to bind in period $t$ when no first-best pair satisfies it. Two reciprocity thresholds appear in the results: $\bar\eta=\sqrt{1/\theta^3}$ , and, for a (DE) multiplier $\lambda$ , $\tilde\eta=\sqrt{1/(\theta^3(1+\lambda))}$ .

Formalization targets

Goal: Proposition 1 (p. 20)

Along every profit-maximizing path, for $2\le t\le T$ :

e_t\le e_{t-1},\qquad w_t\ge w_{t-1},\qquad b_t\le b_{t-1}.

Moreover, whenever $t+1\le T$ , strict changes propagate forward and equalities propagate backward:

e_t<e_{t-1}\Rightarrow e_{t+1}<e_t,\qquad e_{t+1}=e_t\Rightarrow e_t=e_{t-1},

(w_t>w_{t-1}\wedge b_t<b_{t-1})\Rightarrow(w_{t+1}>w_t\wedge b_{t+1}<b_t),\qquad (w_{t+1}=w_t\wedge b_{t+1}=b_t)\Rightarrow(w_t=w_{t-1}\wedge b_t=b_{t-1}).

The goal is stated for every $\theta>0$ , $\eta\ge0$ , $\delta\in(0,1]$ and $T\ge2$ , and contains no closed-form expression.

Milestones

These follow the paper's proof order:

the deviation effort (p. 16);
the existence of a profit-maximizing path (Lemma 2, existence part);
the spot contract $w=\eta\theta^3/4$ , $e^*=\eta\theta^2/2$ (Lemma 1);
the first-best levels and the threshold $\bar\eta$ (Lemma 3);
the binding case, in which effort falls below first best, the wage rises, and the threshold drops to $\tilde\eta<\bar\eta$ (Lemma 4);
strictly declining continuation profits, $\Pi_{t-1}>\Pi_t$ (Lemma 5);
the forward propagation of a binding (DE) constraint (p. 20);
the signs $\partial w/\partial\lambda>0$ and $\partial e^*/\partial\lambda<0$ ;
the comparison of the last period with every earlier one;
the bonus formula and its decrease in $\lambda$ (pp. 43–44).

Significance

Proposition 1 predicts the shape of incentive pay over a finite employment spell. Effort, wage and bonus are flat early on, while the future is valuable enough that (DE) does not bind. Once it binds, the bonus falls and the upfront wage rises in every remaining period, and effort declines because the substitution is incomplete. Relational and reciprocity-based incentives are therefore dynamic substitutes. The paper relates this to observed effort patterns near the end of employment relationships and to the experimental evidence of Boosey and Goerg (2018).

The result is proved in the paper, with an argument that mixes first-order conditions, the implicit function theorem, and an induction on continuation profits. To our knowledge none of it has been machine-checked. A formal proof would check the case split between zero and positive wages and between slack and binding periods, which the paper's proof treats in prose. It would also establish the uniqueness and existence facts that the phrase "the equilibrium" presupposes. The milestones are reusable on their own: they give the explicit optimizers of a one-period contracting problem with a cubic cost and a square-root reciprocity term.

Difficulty

The obvious approach is comparative statics. Treat each period's problem as a parametric program in the bound $K=\delta\Pi_{t+1}$ , show that its solution moves monotonically in $K$ , and combine this with $\Pi_t$ decreasing in $t$ . Two steps of this approach fail as stated.

First, the profit $\pi(e,w)$ is not jointly concave on the feasible set: the term $\frac23(\eta w\theta)^{3/2}$ and the cross term $\eta w\theta e$ make the Hessian indefinite where $e<\sqrt{\eta w\theta}$ . In addition, the wage has a corner at $w=0$ that is active for some parameters and not for others. Uniqueness of the optimum, and the regularity needed to differentiate it, have to be obtained rather than assumed.

Second, the bound $K$ is not exogenous. It is the discounted value of the next period's problem, so monotonicity in $t$ requires an induction that runs backward through the value functions (Lemma 5). The step from monotone bounds to monotone wages and bonuses must also handle the switch between the zero-wage and positive-wage branches.

The strict-propagation clauses are sharper than plain monotonicity: they also require that the solution responds strictly to $K$ whenever (DE) binds.

Formalization scope

The Lean development formalizes the reduced problem of p. 17, not the paper's game. Histories, strategies, the norm function $\eta_t$ and subgame norm-perfect equilibrium do not appear, and Lemma 2's reduction from the game to the per-period problem is not part of the mission. The conventions are as follows:

All quantities are real numbers; periods are natural numbers, and paths are functions $\mathbb N\to\mathbb R$ of which only the indices $1,\dots,T+1$ carry meaning, with $\Pi_{T+1}=0$ .
Optimality means that the pair is feasible and that every feasible pair has weakly smaller profit. No supremum is taken over the reals.
"(DE) binds" means that no first-best pair satisfies the period's constraint. No multiplier enters the goal.
The standing assumptions $\theta>0$ , $\eta\ge0$ , $\delta\in(0,1]$ , $T\ge2$ are bundled in one predicate. Milestones whose formulas divide by $\eta$ , together with Lemma 5, add $\eta>0$ . The goal keeps $\eta\ge0$ , because at $\eta=0$ the only profit-maximizing path is identically zero and the statement still holds.
The printed last clause of Proposition 1 (" $w_{t+1}=w_t$ and $b_{t+1}=b_t$ imply $w_{t+1}=w_t$ and $b_t=b_{t-1}$ ") repeats its own premise. The goal uses $w_t=w_{t-1}$ , in parallel with the effort clause and with the paper's proof.

A formalization that fixes the path by closed forms in a given multiplier sequence, or that assumes (DE) slack or binding throughout, would make the goal a computation. The goal therefore quantifies over every profit-maximizing path, and a separate milestone shows that such a path exists.

A complete development needs elementary real analysis (one-variable calculus, monotonicity from derivatives, and existence of maximizers of continuous coercive functions) and an induction over the finite horizon. All of this is available in Mathlib. Proofs of any milestone are welcome, as are alternative routes to the goal that avoid multipliers.

Selected references

M. Fahn, Reciprocity in Dynamic Employment Relationships, Management Science, 2023. doi:10.1287/mnsc.2022.4657. Working paper: CRC TRR 190 Discussion Paper No. 198, 2019 (the version cited here).
G. A. Akerlof, Labor contracts as partial gift exchange, Quarterly Journal of Economics 97(4):543–569, 1982. doi:10.2307/1885099
C. Bull, The existence of self-enforcing implicit contracts, Quarterly Journal of Economics 102(1):147–159, 1987. doi:10.2307/1884684
W. B. MacLeod and J. M. Malcomson, Implicit contracts, incentive compatibility, and involuntary unemployment, Econometrica 57(2):447–480, 1989. doi:10.2307/1912562
J. Levin, Relational incentive contracts, American Economic Review 93(3):835–857, 2003. doi:10.1257/000282803322157115
M. Dufwenberg and G. Kirchsteiger, A theory of sequential reciprocity, Games and Economic Behavior 47(2):268–298, 2004. doi:10.1016/j.geb.2003.06.003
L. Boosey and S. Goerg, The timing of discretionary bonuses: Effort, signals, and reciprocity, IZA Discussion Paper No. 11580, 2018. IZA DP 11580

12 thms3 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Plumbing of Securities Markets: The Impact of Post-trade Fees on Trading and Welfare: Neither Uniform nor Trade-Specific Post-Trade Fees Maximize Welfare at Every Post-Trade CostResearch Paper

Why post-trade fees matter

Securities traders commonly pay for clearing and settlement after a trade is executed. A fee that is the same for every transaction is simple to administer, but processing a transaction between customers of the same broker can cost less than processing one between brokers. Degryse, Van Achter, and Wuyts ask whether charging everyone the same fee, or charging each transaction its processing cost, leads traders to make the trades that create the most total value. Their answer depends on the processing cost and on how traders' choice of limit-order quotes changes the next trader's choice. The October 2016 working paper develops this question in a single-security limit-order market; this mission uses its preprint page and result numbering.

Market and fee setting

In each period, one risk-neutral trader arrives. She is a buyer with probability $1/2$ and values the security at $V_h$ , or a seller with probability $1/2$ and values it at $V_l$ , where $V_h>V_l\ge0$ . Each trader belongs to one of $N>1$ brokers, with equal arrival shares. A limit order offers one unit at a quoted bid or ask. It remains available for one period, so only the next trader can accept it. A market order accepts the standing quote immediately. The next trader may instead post her own limit order. Broker affiliations are visible, so a trader can choose a quote that attracts counterparties at every broker, called the all strategy, or only counterparties at her own broker, called the own strategy. The market description and tie rules appear in §3 of the working paper, pp. 8–9.

A trade within one broker is internalized; its processing cost is normalized to zero. A trade across brokers costs the post-trade service provider $c>0$ per leg. The uniform fee structure charges $(N-1)c/N$ on each leg of every trade, while the trade-specific structure charges zero on an internalized leg and $c$ on a cross-broker leg. These are the fee schedules analyzed in §4, pp. 10–13. They alter the gains from accepting a standing quote, and therefore the quotes that traders choose to post. A trader indifferent between a market order and a new limit order chooses the market order; a limit-order trader indifferent between attracting all brokers and only her own chooses all brokers.

The model tracks three possible actions in an order-flow chain: posting a limit order, executing an internalized market order, and executing a non-internalized market order. A stationary distribution $\varphi=(\varphi_0,\varphi_1,\varphi_2)$ gives their long-run frequencies. A trade's price transfers value between buyer and seller, while processing uses real resources. Thus expected welfare per period is

W(\varphi)=\varphi_1(V_h-V_l)+\varphi_2(V_h-V_l-2c).

This is the stationary-distribution form of Equation (6) in §5 and the Appendix, pp. 14–15 and Appendix pp. 1–2. It also gives welfare zero if no trade occurs.

Formalization targets

The goal is Corollary 3 of the working paper, p. 16. Two cost thresholds divide the outcomes:

c_1=\frac{2N(N-1)(V_h-V_l)}{(2N+1)(2N-1)},\qquad c_2=\frac{N(V_h-V_l)}{2N+1}.

For $c\le c_1$ , the all strategy gives strictly higher welfare than own, and both fee structures induce all. For $c_1<c\le c_2$ , all gives at least as much welfare; uniform fees induce all, while trade-specific fees induce own. For $c>c_2$ , own gives strictly higher welfare; trade-specific fees induce own and realize higher welfare than uniform fees. At $c=c_2$ , all and own have equal welfare. The two fee structures still induce different strategies there. The paper says that only uniform fees achieve the maximum in its middle range; at the equality endpoint, both welfare values attain the same maximum, so the formal statement preserves the equality and the distinct strategy choices.

Seven milestones support this target, in the paper's order. Equation (1) is the indifference system that optimal limit-order quotes satisfy. Proposition 1 classifies the equilibrium strategy under uniform fees, Equation (5) locates the cost $c_1$ at which the limit-order profits of all and own coincide under trade-specific fees, and Proposition 2 classifies the trade-specific equilibrium. Appendix Equation (A3) gives the stationary distributions of the two order-flow chains, Equation (7) their trading rates, internalization rates and welfare, and Equation (8) the cost at which the two welfare levels agree. The proposition milestones also identify the resulting quotes and spreads; the welfare goal retains the paper's comparison of actual equilibrium outcomes.

What the result establishes

The distinction between the privately chosen strategy and the socially preferred one is operational: trade-specific fees can steer traders toward broker-only trading before that is best for total welfare, while uniform fees can leave them targeting every broker after broker-only trading becomes preferable. The theorem identifies the exact cost ranges in which each mismatch occurs. Its thresholds depend on the number of brokers and the spread in buyer and seller valuations. These claims, including the fact that neither fee schedule is best for the whole cost range, are stated in Corollary 3 and the discussion following it, pp. 16–17.

The result is proved in the paper. The remaining task here is to formalize its equilibrium classification and stationary welfare comparison in Lean, then give the published mathematical statements machine-checked proofs. The mission reuses a published finite-chain stationary-distribution definition; its three-state welfare accounting can serve related trading models, while the exact fee schedules and quote formulas belong to this paper's setting.

Main mathematical difficulty

The equilibrium cannot be found by comparing the welfare formulas alone: traders maximize their own expected limit-order profits. Whether a quote is accepted changes discretely when it crosses a counterparty's market-order threshold, and the value of posting the counterparty's new limit order is itself an equilibrium value. A quote attractive to all brokers and a quote attractive only to the same broker may each be optimal in different cost ranges. The analysis must also respect the paper's tie rules at both switching thresholds. Once the strategies are classified, the two three-state chains have different stationary trading frequencies, so a fee comparison at a fixed trade volume would not answer the question.

Formalization scope

Lean represents $N$ as a natural number with $1<N$ and all money amounts as real numbers. The standing assumptions are $0\le V_l<V_h$ and $c>0$ ; the latter expresses that the zero internalized cost is lower than the non-internalized cost. Division in threshold and quote formulas uses the real cast of $N$ . A market order is chosen at equality, and an optimal all-broker quote is preferred at an all-versus-own tie. An equilibrium is a stationary pair of buyer and seller continuation values, each an attained greatest expected limit-order profit given the other. Optimal quotes determine the strategy; strategy labels are not defined by the cost thresholds.

The transition matrix has state indices $0,1,2$ for limit, internalized market, and non-internalized market orders. A stationary distribution uses the published finite-chain definition: it is nonnegative, sums to one, and is a fixed row vector of that matrix. The printed third row of Appendix (A2) is all zeros even though the text calls the matrix stochastic. The formal matrix sends that unreachable state back to state $0$ ; this changes no stationary probability in (A3). Welfare is calculated from the stationary distribution and true processing costs, not assigned one of the closed formulas in Equation (7). The goal quantifies over equilibrium continuation values and stationary distributions, while the milestones assert their existence and identify the distributions. Contributions that establish these equilibrium, finite-chain, and threshold results are within scope.

Selected references

Hans Degryse, Michael Van Achter, and Gunther Wuyts, Plumbing of Securities Markets: The Impact of Post-Trade Fees on Trading and Welfare, SSRN working paper 2023597, October 2016. SSRN.
Hans Degryse, Michael Van Achter, and Gunther Wuyts, Plumbing of Securities Markets: The Impact of Post-Trade Fees on Trading and Welfare, Management Science, 2021. DOI. The source used for formalization is the October 2016 working paper.

10 thms3 active usersReviewed

Economics Operations Research Probability·Captain: mikedeng1

Insider Trading, Competition, and Real Activities Manipulation: With Subsequent Kyle Insider Trading, a Monopoly Has a Unique Linear Equilibrium, with Output E[a|s]/2 + (1/(4ω))√(ΣuΣaΣθ/(Σa+Σθ))Research Paper

Motivation

Managers who run a firm also trade its stock. Accounting and finance research has long asked how the opportunity to trade on private information changes what managers do inside the firm. Real activities manipulation means that a manager distorts operating choices (production, investment, discretionary spending) rather than accounting numbers. The usual concern is that insider trading pushes such choices away from value maximization (Roychowdhury, J. Accounting and Economics, 2006).

Chen and Jorgensen (SSRN 2358668; Management Science, 2021, doi:10.1287/mnsc.2020.3915) combine a product-market decision with the one-period insider trading model of Kyle (Econometrica 53, 1985). The trading stage is Kyle's linear equilibrium: an informed trader, noise traders and a competitive market maker. What is new is that the variance of the asset's value is not exogenous. The manager chooses it through the firm's output. Their basic result, Proposition 1, determines the equilibrium output of a monopolist whose manager will later trade. The later sections (Cournot duopoly, cross-trading, the board's choice of the manager's stake) all reuse this computation.

Setting

A monopolist faces the inverse demand $p = \tilde a - q$ , where $q \in \mathbb R$ is output and marginal cost is $0$ . The demand intercept has prior $\tilde a \sim N(m_a, \Sigma_a)$ . Before producing, the manager observes and publicly discloses a signal $\tilde s = \tilde a + \tilde\theta$ , with $\tilde\theta \sim N(0, \Sigma_\theta)$ . Given the realized $s$ , the demand intercept has the posterior

(a\mid s) \sim N\!\left(E[a|s],\ \frac{\Sigma_a\Sigma_\theta}{\Sigma_a+\Sigma_\theta}\right),\qquad E[a|s] = \frac{\Sigma_a s + \Sigma_\theta m_a}{\Sigma_a + \Sigma_\theta}.

After the manager chooses $q$ , the firm value is $V = q(a - q)$ . The manager learns $a$ and submits a demand $d$ for the firm's shares. Noise traders submit $\tilde u \sim N(0, \Sigma_u)$ , independent of $a$ . A market maker sees only the total order flow $D = d + u$ and sets the price $P(D) = E[V \mid D]$ . Strategies are linear: the manager's demand is $d(V) = \alpha + \beta V$ and the price is $P(D) = \mu + \lambda D$ .

A linear equilibrium of the trading stage at $q$ is a pair of such strategies with two properties. For every realized $a$ , the demand maximizes the insider's expected profit $E[(V - P(d + \tilde u))\,d]$ over all $d$ . And the price equals $E[V\mid D]$ almost surely. The manager owns a stake $0 < \omega \le 1$ in the firm and chooses $q$ to maximize

\omega\,E[V(q)] + E[\Pi(q)],\qquad E[\Pi(q)] = E\big[(V - P(D))\,d(V)\big].

A linear equilibrium is a quantity $q$ together with a trading-stage equilibrium at $q$ , such that no other quantity $q'$ , followed by any trading-stage equilibrium at $q'$ , does better. Write $\kappa = \sqrt{\Sigma_u\Sigma_a\Sigma_\theta/(\Sigma_a+\Sigma_\theta)}$ .

Formalization targets

Goal: Proposition 1

Under $\Sigma_a, \Sigma_\theta, \Sigma_u > 0$ , $0 < \omega \le 1$ and $E[a|s] > 0$ , there is exactly one linear equilibrium. Its output is

\hat q = \frac12 E[a|s] + \frac{1}{4\omega}\sqrt{\frac{\Sigma_u\Sigma_a\Sigma_\theta}{\Sigma_a+\Sigma_\theta}},

and its trading strategies are

\alpha = -\frac{\sqrt{\Sigma_u}}{\sqrt{\frac{\Sigma_a\Sigma_\theta}{\Sigma_a+\Sigma_\theta}}}(E[a|s]-\hat q),\quad \beta = \frac{\sqrt{\Sigma_u}}{\hat q\sqrt{\frac{\Sigma_a\Sigma_\theta}{\Sigma_a+\Sigma_\theta}}},\quad \mu = \hat q(E[a|s]-\hat q),\quad \lambda = \frac{\hat q}{2\sqrt{\Sigma_u}}\sqrt{\frac{\Sigma_a\Sigma_\theta}{\Sigma_a+\Sigma_\theta}}.

The goal is stated as an equivalence: a pair is an equilibrium if and only if it is this one.

Milestones

These are the steps of the paper's proof in Appendix A:

the insider's best response to a linear price;
the Gaussian law of $V$ ;
the market maker's update (30);
the trading stage solved for $q > 0$ ;
the price (31) and demand (32);
the expected trading profit (33), $E[\Pi] = \tfrac{|q|}{2}\kappa$ , in every trading equilibrium;
the production stage (34), whose unique maximizer is $\hat q$ .

Significance

Without insider trading the manager would choose $q^* = \tfrac12 E[a|s]$ (§2.1). Proposition 1 gives $\hat q = q^* + \kappa/(4\omega) > q^*$ . When the manager can trade, the firm overproduces. The distortion shrinks as the stake $\omega$ grows, and it grows with the noise-trading variance and with the residual demand uncertainty. The paper's consumer-welfare remark, the comparative statics in Corollaries 1.1–1.2, and the contracting analysis of §4 all start from these closed forms. So do the duopoly results (Propositions 2–4), which repeat the same computation with two firms.

The result is proved in the paper, by a first-order-condition argument. As far as we know it has no machine-checked proof. The formal development adds two things to the paper's argument. First, the trading-stage equilibrium is unique among all linear pairs, not only the one the first-order conditions produce. Second, the production choice is compared against every real quantity, including negative ones (footnote 7), each followed by any of its trading equilibria. The paper's appeal to "the first-order condition" leaves both checks implicit.

Difficulty

The algebra of the closed forms is routine. The work is in the trading stage, where the price is a conditional expectation. To identify $E[V\mid D]$ with an affine function of $D$ , one needs the regression formula for a jointly Gaussian pair $(V, D)$ built from independent normals. One also needs uniqueness: two affine functions of a non-degenerate Gaussian that agree almost surely have the same coefficients. Mathlib has the one-dimensional Gaussian law and conditional expectation, but no ready-made Gaussian conditioning lemma of this form.

Uniqueness of the trading-stage equilibrium also requires ruling out $\lambda \le 0$ . In that case the insider's quadratic payoff has no maximizer for some realized value. Finally, the production comparison runs over all real quantities. The insider's gain is $\tfrac{|q|}{2}\kappa$ , not $\tfrac q2\kappa$ , so the objective has two concave branches. The global maximizer is $\hat q$ only when $E[a|s] > 0$ .

Formalization scope

Everything is real-valued and lives in the namespace KyleProduction.Monopoly. The variances are named Sa, Sθ, Su and $\lambda$ is lam. The model is analysed conditional on the realized signal $s$ :

the law of $a$ is the paper's posterior gaussianReal (postMean P) (postVar P).toNNReal;
$u$ is gaussianReal 0 Su.toNNReal;
$(a, u)$ has the product law.

Deriving the posterior from the prior and the signal is not part of the mission. Market efficiency (4) is stated with Mathlib's condExp with respect to the σ-algebra generated by the order-flow map, almost surely under the joint law. Insider optimality (3) is required for every realization of $a$ . Quantities range over $\mathbb R$ .

The formalization commits to these hypotheses and conventions:

$\Sigma_a, \Sigma_\theta, \Sigma_u > 0$ , implicit in the paper's normal laws;
$0 < \omega \le 1$ , from p. 5;
$E[a|s] > 0$ , which makes footnote 7's " $m_a$ sufficiently large" precise and is needed for $\hat q$ to be the global maximizer over all real quantities;
in milestones 6 and 7, the paper's $\hat q/2$ is read as $|q|/2$ for negative quantities.

Three printed slips are corrected in the Lean statements and kept as printed in the milestone texts:

the order flow $\alpha + \beta(\tilde V + \tilde u)$ , which should read $\alpha + \beta\tilde V + \tilde u$ ;
the denominator of $\lambda$ in (30), which is missing the factor $\Sigma_a\Sigma_\theta/(\Sigma_a+\Sigma_\theta)$ ;
the bracket of (33), whose second term should be $\hat q(E[a|s]-\hat q)$ .

A trivial formalization would define the price by the regression formulas, or define the objective by the closed form $\tfrac q2\kappa$ in place of the trading profit of an equilibrium. The first makes milestone 3 a tautology. The second collapses the goal to milestone 7. Neither is done here: the price is the conditional expectation, and the objective integrates the realized trading profit.

The work needs a lemma for the conditional expectation of a Gaussian given an affine Gaussian observation, together with the a.s. identification of affine functions of a non-degenerate Gaussian. Both are reusable beyond this mission, for other Kyle-type and rational-expectations models. Contributions of these lemmas, of the trading-stage uniqueness and of the production comparison are all welcome.

Selected references

H. Chen and B. N. Jorgensen, Insider Trading, Competition, and Real Activities Manipulation, SSRN working paper 2358668, version of February 2016; published in Management Science 67, 2021. https://ssrn.com/abstract=2358668, https://doi.org/10.1287/mnsc.2020.3915
A. S. Kyle, Continuous Auctions and Insider Trading, Econometrica 53(6), 1315–1335, 1985. https://doi.org/10.2307/1913210
S. Roychowdhury, Earnings management through real activities manipulation, Journal of Accounting and Economics 42(3), 335–370, 2006. https://doi.org/10.1016/j.jacceco.2006.01.002

9 thms3 active usersReviewed

All missions

On complementary channels and the additivity problemResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Public and private resource trade-offs for a quantum channelResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Improving fidelity of continuous-variable teleportation via local operationsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

The Capacity of the Quantum Multiple Access ChannelResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Optimal Dynamic Momentum Strategies: For Horizons Within the Look-Back Period, the Optimal Weight Is the Mean-Variance Weight Plus a Hedging Term Weighted Toward Recent ReturnsResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3.3

Milestones

Significance

Difficulty

Formalization scope

Selected references

Product Selling vs. Pay-Per-Use Service: A Strategic Analysis of Competing Business Models: Pay-Per-Use Out-Earns Selling in Duopoly Equilibrium Iff the Delivery Cost Is Below a ThresholdResearch Paper

Motivation

Setting

Formalization targets

Equilibrium profit comparison

Significance

Difficulty

Formalization scope

Selected references

I Don’t “Recall”: The Decision to Delay Innovation Launch to Avoid Costly Product Failure: Neither, Both, or Exactly One of Two Identical Firms Tests, by Failure-Probability CutoffsResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Interactive Information Design: Every Information Design Game with Finite Message Sets Admits a Subgame Perfect EquilibriumResearch Paper

Why this game matters

Finite information design games

Formalization targets

What the result establishes

Where the proof is difficult

Formalization scope

Selected references

When Should the Off-Grid Sun Shine at Night? Optimum Renewable Generation and Energy Storage Investments: Storage Pays iff c_K/e < g − √(2c_Q g), So Technologies Rank by Cost-to-Efficiency RatioResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Shareholder Short-Termism, Corporate Control and Voluntary Disclosure: The Manager Discloses Good and Bad News Below a Short-Termism Threshold and Only Good News Above ItResearch Paper

Why disclosure can change control decisions

The disclosure and intervention game

Formalization targets

What the result establishes

Where the mathematical work lies

Formalization scope

Selected references

On System-Wide Safety Staffing of Large-Scale Parallel Server Networks: Positive SWSS Makes the Limiting Diffusion Exponentially Ergodic, Negative SWSS Makes It Transient Under Every Markov ControlResearch Paper

Motivation

Setting

Formalization targets