All missions

Motivation

A manufacturer that receives evidence of a product defect must decide whether to disclose it. A regulator that receives a report must decide whether to investigate immediately. The regulator's announcement can itself change consumer demand while the investigation is under way, so a policy intended to reveal defects may change the manufacturer's incentive to report. Cho, DeMiguel, and Hwang study this interaction for vehicle defects, comparing a U.S. policy that announces an investigation with a U.K. policy that keeps it confidential. Their analytic model identifies circumstances in which the manufacturer conceals a signal even though the expected harm is substantial. This mission formalizes the U.S. equilibrium characterization in Proposition 2 of the authors' accepted manuscript.

Setting

A product is either defective, $D$, or nondefective, $N$. The prior probability of defect is $P_D$. A manufacturer receives a private signal $\widetilde D$ indicating a possible defect. Its reliability is $\rho\in[0,1]$, and after this signal the manufacturer's posterior probability of defect is

$$P(D\mid\widetilde D)=\rho+(1-\rho)P_D.$$

The product sells at price $p$ over a unit-length life cycle. Consumers arrive at unit rate and have valuations uniformly distributed on $[0,\bar v]$. A defective unit causes expected harm $h\in(0,\bar h]$. The ordinary demand rate is $d(p)=1-p/\bar v$. When the U.S. regulator announces an investigation, consumers account for possible harm during its mean duration $l$, so the temporary demand rate is $d(p,h)=1-(p+h)/\bar v$. The model assumes $\bar v>p+\bar h$, ensuring positive demand even during an announcement. These choices follow §3 of the manuscript.

After a positive signal, the manufacturer chooses report ($R$) or no report ($NR$). After a report, the regulator chooses immediate investigation ($I$) or no immediate investigation ($NI$). A later voluntary investigation can occur if the product is defective. Its time has constant density $h/((1-l)\bar h)$ on $[0,1-l]$, while the probability of no such investigation is $1-h/\bar h$. An investigation costs the regulator $C$. If a defect is found, the manufacturer recalls previously sold units at unit cost $r$ and compensates consumer harm. A discovered cover-up carries penalty $K_1h+K_2$ with discovery probability $\theta$. If no investigation takes place, the manufacturer bears fraction $\alpha$ of consumer harm. These payoffs determine three U.S. manufacturer profits, $\pi^{US}_{R,I}$, $\pi^{US}_{R,NI}$, and $\pi^{US}_{NR}$, from equations (1), (3), and (5) of the manuscript.

The regulator maximizes social welfare $W=\pi+S-\Gamma$, the manufacturer's profit plus consumer surplus minus investigation cost. The two welfare values after a report are $W^{US}_{R,I}$ and $W^{US}_{R,NI}$. The regulator chooses $I$ when these values tie. The manufacturer chooses $R$ when its profits tie. The regulator's action after $NR$ is $NI$, since there is no report to investigate at time zero. These conventions are stated in §§4–5 and the proof of Proposition 2 of the manuscript.

Formalization targets

The regulator's threshold result, the U.S. half of Proposition 1, says that there are $h_I^{US}\in(0,\bar h)$ and a curve $\rho_I^{US}$ on $[h_I^{US},\bar h]$, with values in $[0,1]$ and $\rho_I^{US}(h_I^{US})=1$, such that

$$I\quad\Longleftrightarrow\quad h\ge h_I^{US}\ \text{and}\ \rho\ge\rho_I^{US}(h).$$

Proposition 2 adds $h_R^{US}\in(0,\bar h)$ and a reporting curve $\rho_R^{US}$ with the analogous domain and endpoint value. The goal is the unique subgame perfect equilibrium for every admissible $h$ and $\rho$:

$$\begin{array}{ll} (R,I), & h\ge\max\{h_I^{US},h_R^{US}\},\quad \rho\ge\max\{\rho_I^{US}(h),\rho_R^{US}(h)\};\\ (R,NI), & h<h_I^{US}\quad\text{or}\quad h\ge h_I^{US},\ \rho<\rho_I^{US}(h);\\ (NR,I), & h_I^{US}\le h<h_R^{US},\ \rho\ge\rho_I^{US}(h),\\ & \quad\text{or}\quad h\ge h_R^{US},\ \rho_I^{US}(h)\le\rho<\rho_R^{US}(h). \end{array}$$

The last profile records the regulator's response if a report had arrived; on the realized path the regulator does not investigate immediately. The milestone list follows the source's two welfare and profit identities, the two harm thresholds, Proposition 1's U.S. response, and the reporting rule in Step 1 of Proposition 2's proof. Each formula comes from the accepted manuscript, pp. 13, 15, 28, and 30–31.

Significance

The characterization locates the cover-up region in the harm–reliability plane. Under the U.S. announcement policy, a report can depress sales during an immediate investigation, while concealment risks a later penalty. The model shows how these forces produce an intermediate-reliability band in which the manufacturer conceals even a high-harm signal. The result can therefore be used to compare disclosure incentives under investigation policies using the same payoff primitives. The authors prove the result in the paper; the remaining task here is to formalize its stated assumptions, integral payoffs, threshold identities, and equilibrium claim in Lean. The local prior-art search found no existing formalization of this particular game.

Difficulty

The regulator's and manufacturer's choices each depend on a difference between payoffs defined by several integrals. The closed forms are cubic expressions in harm, and the threshold claims require their signs to be controlled on the full interval $[0,\bar h]$. Checking a few parameter values does not establish those interval-wide claims. At the equilibrium boundaries, both actors' tie rules matter: without them, the claimed unique strategy profile is not determined. The proof must also keep the thresholds independent of the point $(h,\rho)$ being classified.

Formalization scope

The development uses real numbers for all model parameters and values. One Params record contains $p,\bar v,\bar h,r,K_1,K_2,\theta,\alpha,C,l,P_D$; neither $h$ nor $\rho$ is a field of that record. Params.Standing collects the source's sign and range restrictions, including $0<r<p$, $0<l<1$, $\theta,\alpha\in[0,1]$, $K_1,K_2\ge0$, and $\bar v>p+\bar h$. It also requires $0<P_D<1$: the paper's definition of reliability divides by $2P_D(1-P_D)$, and its threshold fractions divide by $1-P_D$.

Profit and consumer-surplus expressions use intervalIntegral for the manuscript's valuation and voluntary-investigation integrals. Their integrands are polynomials or constants on finite intervals, so the usual nonintegrability default is irrelevant here. The posterior formula represents the signal law at the point needed by the theorem; the full joint signal distribution is not reconstructed. Likewise, the investigation lead time enters through its mean $l$, as it does in the paper's expected-payoff formulas. The polynomial closed forms are named separately and linked to the primitive payoffs by milestone theorems.

IsSPNE is the tie-broken sequential best-response condition for the two decisions, with $A_3=NI$ fixed after no report. Proposition 2 quantifies the four thresholds before all $h$ and $\rho$, constrains their relevant domains, and characterizes every equilibrium profile in each region. This prevents thresholds chosen separately at each point, a vacuous regulator curve, or an existence-only restatement. The reusable work is the interval-integral algebra and interval-wide polynomial threshold arguments. Contributions on those identities, the threshold theorems, and their equilibrium assembly are all within scope. The U.K. equilibrium and later welfare comparisons are separate results in the paper.

Selected references

• Soo-Haeng Cho, Victor DeMiguel, and Woonam Hwang, Cover-Up of Vehicle Defects: The Role of Regulator Investigation Announcements, Management Science 67(6), 2021, 3834–3852. DOI: 10.1287/mnsc.2020.3672. This mission cites the authors' accepted manuscript, LBS Research Online eprint 1396, with its own printed page numbers.

Motivation

An experiment may compare two ways to select initial participants in a social network. Each selected seed set can lead to a different outcome, and the experiment observes only the outcome for the seed set actually selected. Chin, Eckles and Ugander study how known selection probabilities let observations from one experimental design estimate the outcomes of two other seeding strategies. Their setting includes one hop targeting and random targeting, but their statistical results apply to any two stochastic strategies with known probabilities. The central result here is their Proposition 2: the Hájek estimator, which normalizes the observed importance weights separately for the two strategies, is consistent and asymptotically normal. These properties are needed to interpret a large experiment's estimated difference and its uncertainty. Chin, Eckles and Ugander, §§2–3.3 and Proposition 2.

Setting

Let $\Omega$ be a countable space of possible seed sets, including any network information that varies across the superpopulation. Strategies $A$ and $B$ give probability mass functions $p_A$ and $p_B$ on $\Omega$. An experimental design distribution $p_\Delta$ gives the law of each observed seed set. A fixed function $y:\Omega\to\mathbb R$ records the potential outcome for each possible seed set. For a draw $S$, the observed outcome is $Y=y(S)$. The design supplies independent draws $S_0,S_1,\ldots$ with common law $p_\Delta$; the outcome is a deterministic function of each draw. The paper allows outcomes such as counts and fractions and does not require a finite seed space. Chin, Eckles and Ugander, pp. 8–9.

The strategy means are $\mu_A=\mathbb E_A[Y]$ and $\mu_B=\mathbb E_B[Y]$. Their difference is the superpopulation contrast $\tau_{\mathrm{sp}}=\mu_A-\mu_B$. For a seed set $s$ with positive design probability, its importance weights are $w_A(s)=p_A(s)/p_\Delta(s)$ and $w_B(s)=p_B(s)/p_\Delta(s)$. Write $\bar w_{A,N}=N^{-1}\sum_{i<N}w_A(S_i)$, with analogous notation for $B$. The paper's estimator in equation (7) separately normalizes the two sets of weights:

$$\widetilde\tau_N=\frac1N\sum_{i<N}\left(\frac{w_A(S_i)}{\bar w_{A,N}}-\frac{w_B(S_i)}{\bar w_{B,N}}\right)y(S_i).$$

The design can be a mixture of $p_A$ and $p_B$, but the proposition also addresses other designs. The formal statement therefore leaves $p_\Delta$ general. Chin, Eckles and Ugander, equations (2), (4), (5), (7), pp. 9–10.

Formalization targets

The first targets are the weight moment identities, the limits of the four sample averages, and almost sure consistency of $\widetilde\tau_N$. The joint central limit theorem for those averages and the variance identity connect these to the goal. These targets follow the displays and sentences in the proof of Proposition 2, Appendix A.2. Chin, Eckles and Ugander, pp. 39–40.

The goal is the corrected full strength of Proposition 2. Under full support of the design on the support of either strategy and finite second moments for the four weighted coordinates,

$$\widetilde\tau_N\longrightarrow\tau_{\mathrm{sp}}\quad\text{almost surely},\qquad \sqrt N(\widetilde\tau_N-\tau_{\mathrm{sp}})\Rightarrow\mathcal N(0,V_{\widetilde\tau}),$$

where the variance is the value specified by the paper's equation (15),

$$V_{\widetilde\tau}=\mathbb E_\Delta\!\left[ \left(\frac{\mu_Ap_A(S)-\mu_Bp_B(S)-y(S)(p_A(S)-p_B(S))}{p_\Delta(S)}\right)^2 \right].$$

The variance is determined by the two strategies, the design, and the outcomes; it is not a free variance parameter. The almost sure limit records the strong form supplied by the sample average law. Chin, Eckles and Ugander, Proposition 2 and equation (15), p. 14.

Significance

The result identifies both the value approached by the normalized estimator and its leading large sample variance. The two normalized terms are correlated because a single observed seed set contributes information about both strategies. Equation (15) retains that dependence, so the uncertainty of their difference is not obtained by adding two separate variance formulas. The paper uses this result to motivate inference for a superpopulation contrast rather than a finite collection of villages, for which a single observation per village does not identify each village's variance. Chin, Eckles and Ugander, §3.3, p. 14.

The mathematical result is published in the cited preprint. This mission asks for a machine checked statement and proof of its corrected version, plus reusable facts about weighted moments, strong laws for transformed samples, and a four coordinate central limit theorem. The proof infrastructure can serve other comparisons of two policies under a common sampling design. The Horvitz–Thompson result in Proposition 1 is related but is a separate theorem and is outside this mission. No proof of Proposition 2 is currently included in the mission's local formalization.

Difficulty

The estimator is a difference of two random ratios. At small sample sizes, either normalizing sum can vanish, and the two ratios are dependent. Applying a variance formula for one self normalized estimate twice would discard their covariance. There is also a source level obstacle: the printed positivity assumption permits the design to omit a seed set on which both strategies assign equal positive probability. Such a set does not affect the strategy contrast pointwise, but it changes the separate means and the normalizing weight expectations. The printed hypothesis therefore does not imply the moment identity used in Appendix A.2. Chin, Eckles and Ugander, Assumption 1, p. 11, and proof of Proposition 2, p. 40.

For example, take three seed sets with $p_A=(1/2,0,1/2)$, $p_B=(0,1/2,1/2)$, $p_\Delta=(1/2,1/2,0)$ and $y=(1,0,0)$. The paper's Assumption 1 holds, but $\tau_{\mathrm{sp}}=1/2$ and the Hájek estimator approaches $1$. This mission labels the replacement support condition as a correction. The printed intermediate expansion of the delta method variance also has a sign error in a cross term; equation (15) itself is retained. Chin, Eckles and Ugander, pp. 11, 14, 40.

Formalization scope

Lean represents $\Omega$ by an arbitrary countable type with measurable singletons, $p_A,p_B,p_\Delta$ by PMF, and the sample by measurable independent maps from one probability space, each with law $p_\Delta$. The natural number $N$ is the number of sampled villages: Lean uses draws $S_0,\ldots,S_{N-1}$ in place of the paper's $S_1,\ldots,S_N$. Probabilities enter real arithmetic through ENNReal.toReal; a PMF assigns finite mass to each point. Full positivity says $p_\Delta(s)>0$ whenever $p_A(s)>0$ or $p_B(s)>0$. It is stronger than the paper's contrastive Assumption 1 and is needed for the separate means and normalization identities.

The four second moment conditions apply to $w_A$, $w_B$, $w_Ay$, and $w_By$ under $p_\Delta$. They make the joint covariance finite even when $y$ is unbounded. The consistency milestone uses only the first moments it needs. The variance is the real integral from equation (15), then converted to a nonnegative real variance for Mathlib's Gaussian law. Lean's total division assigns zero weight when $p_\Delta(s)=0$; such a seed set is not observed under the design. The estimator is zero at $N=0$, and a finite sample with a zero normalizing sum uses Lean's division by zero value. The almost sure and distributional limits address the paper's asymptotic claim.

The intended statement includes every countable seed space and every qualifying independent sample. Restricting to a finite seed space, assuming the estimator's limit or a central limit theorem, or selecting an arbitrary Gaussian variance would change the claim. The development needs Mathlib's probability measures, integration, strong law, Gaussian laws, distributional convergence, and moment theory. Contributions that establish the listed milestones or develop the general joint limit and ratio tools are in scope.

Selected references

• Chin, Alex, Dean Eckles, and Johan Ugander. Evaluating Stochastic Seeding Strategies in Networks. arXiv:1809.09561v3, 2020. Preprint.

Motivation

Traffic, packet and evacuation networks are often studied with atomic dynamic flows: individual agents move through a network over time, queue at congested links, and each wants to reach its destination as early as possible. The deterministic queuing (Vickrey) model makes the queue at every link explicit: a link has a capacity, and agents beyond it wait in a queue. In the atomic, discrete-time version, simultaneous arrivals at a queue must be ordered by some tie-breaking rule, and that rule decides whether the resulting routing game has an equilibrium.

Hoefer, Mirrokni, Röglin and Teng (2009, 2011) and Werth, Holzhauser and Krumke (2014) studied atomic routing over time in deterministic queuing models, and found non-existence of equilibria and computational hardness in several variants; Harks, Peis, Schmand, Tauer and Vargas Koch (2018) studied competitive packet routing with priority lists. Scarsini, Schröder and Tomala (Operations Research, 2018) proved that a Nash equilibrium exists when priorities are placed on agents, in single-origin, single-destination networks. Cao, Chen, Chen and Wang (Operations Research 2021) showed that with agent priorities and several origins an equilibrium can fail to exist (their Example 3, a rock–paper–scissors cycle). They proposed instead to break ties by edge priorities at each vertex, and proved that equilibria then always exist. This mission formalizes that existence theorem.

Setting

A network instance consists of the following data.

• A finite acyclic directed multigraph $G=(V,E)$ with a destination $d$; every vertex has a path to $d$. Every edge has unit capacity and unit length.
• At each vertex $v$, a complete priority order $\prec_v$ on the edges entering $v$.
• At time $0$, an initial ranked queue $Q^0_e$ on each edge $e$.
• At each time $r\ge1$ and vertex $v$, a finite ranked set $\Delta_{r,v}$ of agents entering at origin $v$.

The agent set $\Delta$ is the disjoint union of all these, and may be infinite.

Each agent $i$ chooses at time $0$ a path $P_i$ from his starting vertex to $d$. For $i\in Q^0_e$ the path must begin with $e$; this is his strategy set $\mathcal P_i$. At every time unit only the head of the queue on an edge leaves it, and it reaches the head of the edge one unit later. Agents entering an edge are ranked by the edge-priority DQ rule, applied in this order:

• (R0) initial-queue order;
• (R1) an earlier entry ranks higher;
• (R2) among simultaneous entries through different edges, higher priority under $\prec_{u_e}$ ranks higher;
• (R3) an agent starting at $u_e$ ranks above through-traffic entering at the same time;
• (R4) agents with the same origin keep their original ranks.

$t^v_i(p)$ denotes the time agent $i$ reaches vertex $v$ under the profile $p$, and is $\infty$ if he never does.

The normal-form game $\Gamma^N$ has players $\Delta$, strategies $\mathcal P_i$, and cost $t^d_i$. A profile $p$ is a Nash equilibrium (NE) if $t^d_i(p)\le t^d_i(P'_i,p_{-i})$ for all $i$ and $P'_i\in\mathcal P_i$. It is an iteratively dominant NE (IDNE) if the agents can be reindexed $1,2,\dots$ such that for every $k$, every vertex $v$ on $P_k$ and every profile $q$ of the agents outside $[k]=\{1,\dots,k\}$,

$$t^v_k(p_{[k]},q)=\min\{t^v_j(p_{[k-1]},r): j\notin[k-1],\ r \text{ a profile of }\Delta\setminus[k-1]\}.$$

Formalization targets

Goal: Theorem 1 (p. 12)

$$\text{every } \Gamma^N \text{ admits a path profile } p \text{ that is an IDNE, and hence an NE.}$$

The goal makes no finiteness assumption on $\Delta$ and fixes no constants.

Milestones

1. Selection step (§4.1, p. 14). Given the first $k-1$ agents of the construction, the pruning (S1)–(S3) leaves exactly one candidate pair $(j,P_j)$.
2. Lemma EC.2 (p. ec6). For the selected $(k,P_k)$, any $S\subseteq\Delta\setminus[k-1]$, $j\in S$, $v\in P_k$ and any profile $q$,

$$t^v_k(p_{[k]},q_{S\setminus\{k\}})=\ell^v_k[\![k-1]\!]\le t^v_j(p_{[k-1]},q_S).$$

3. Reindexing (p. ec3). The selection can be iterated so that every agent receives an index.
4. Theorem EC.2 (p. ec8). The profile so constructed (a special IDNE) is an IDNE.
5. IDNE ⇒ NE (§4.1, p. 11).

Significance

The result. Theorem 1 gives an equilibrium for every network with edge priorities: multiple origins, initial queues and an unbounded stream of inflows are all allowed. With agent priorities, equilibrium can fail to exist in exactly this setting. The IDNE carries more structure than an NE. Arrival times along each agent's path are independent of later agents' choices, and no agent who enters later at the same origin overtakes an earlier one. The paper uses these properties in its study of subgame-perfect equilibria for adaptive agents (p. 12; §5).

Formalizing it. The result is proved in the paper; nothing here is open mathematically. To our knowledge no part of it is formalized in any proof assistant. The mission produces:

• a reusable, executable model of discrete-time deterministic queuing with priority tie-breaking;
• a formal proof of the constructive existence argument.

The paper proves Lemma EC.2 in a transformed game $\bar\Gamma^N$ on an infinite graph (Lemma EC.1). The mission instead states everything directly in $\Gamma^N$, so a complete development must either carry out the transfer or reprove the lemma natively. For infinitely many agents, the claim that every agent is eventually indexed (milestone 3) is asserted in the paper without a separate argument; the formal proof has to supply one.

Difficulty

The obvious argument fails at the no speed-up property. Adding agents to a network can make some other agent arrive earlier. The paper's Example 4 (pp. 15–16) has such a chain effect: removing an agent delays another. So the claim that agent $k$'s arrival times are unaffected by everyone after him is not monotonicity of congestion. It holds only for the specific order and paths produced by the selection procedure, and it must be proved by an induction that carries invariance (equality in (EC.2)) and domination (inequality in (EC.2)) together.

The tie-breaking is the second difficulty. The selection compares candidates backwards from $d$: by arrival time, then by incoming-edge priority, then one edge further back. The argument has to show that this order matches the queue rule (R0)–(R4) at every vertex, including (R3) for agents starting mid-network.

Formalization scope

Everything lives in the namespace AtomicDynFlow.IDNE.

• Network and agents. Instance V E A carries the graph as finite types V, E with tail, head, d, and the priorities as lists inc v of incoming edges, highest priority first. Initial queues Q0 e are listed head first, and inflows inflow r v highest original rank first. The standing hypotheses are fields:

  • acyclicity, as a height function;
  • reachability of $d$;
  • no inflow at time $0$;
  • every agent lies in exactly one source list.

  The agent type A is arbitrary and may be infinite.

• Dynamics. queue π s e is a computable, list-based simulation of the queue on each edge at each time, under a partial profile π : A → Option (List E), where none means the agent is absent. arrival π i v : ℕ∞ is $t^v_i$, with ⊤ for $\infty$ (p. ec4). The starting-vertex time is $0$ for initial-queue agents and $r$ for $\Delta_{r,v}$ (Algorithm 1, Step 2).

• Equilibria. The reindexing of Definition 2 is an injective $\sigma:\Delta\to\mathbb N$ whose range is an initial segment, with agent $a$ receiving index $\sigma(a)+1$. Definition 2 quantifies over every vertex of the path, the starting vertex included.

• Selection. The pruning (S1)–(S3) is a backward pairwise comparison of candidate pairs (Before, IsSelected). Milestones 2 and 4 are $\Gamma^N$-native versions of the e-companion statements, and Lemma EC.1 is not formalized.

Ruled out. Three encodings would trivialize the goal, and none is used:

• arrival times that ignore queuing, under which every profile would be an IDNE;
• a profile in which removed agents are frozen rather than absent;
• a reindexing that skips agents.

A sorry-free check of the paper's Example 2 shows that agent $i$ waits at $y_1$ and reaches $d$ at time $6$, and that removing agent $g$ lets him arrive at $5$.

Welcome contributions: proofs of the milestones in any order. Milestone 5 needs only the definitions. Milestones 1 and 2 are the technical core, and general lemmas about the queue simulation (FIFO within an edge, monotonicity in entry times) are reusable throughout.

Selected references

• Z. Cao, B. Chen, X. Chen, C. Wang, Atomic dynamic flow games: adaptive versus nonadaptive agents, Operations Research, 2021; accepted manuscript Oct. 2020, WRAP 143835. https://doi.org/10.1287/opre.2021.2105
• M. Scarsini, M. Schröder, T. Tomala, Dynamic atomic congestion games with seasonal flows, Operations Research 66(2):327–339, 2018.
• T. Werth, M. Holzhauser, S. Krumke, Atomic routing in a deterministic queuing model, Operations Research Perspectives 1(1):18–41, 2014.
• T. Harks, B. Peis, D. Schmand, B. Tauer, L. Vargas Koch, Competitive packet routing with priority lists, ACM Transactions on Economics and Computation 6(1):4, 2018.
• M. Hoefer, V. S. Mirrokni, H. Röglin, S.-H. Teng, Competitive routing over time, Theoretical Computer Science 412(39):5420–5432, 2011.
• W. Vickrey, Congestion theory and transport investment, American Economic Review 59(2):251–260, 1969.

Motivation

A firm's accounting disclosure affects what traders know. The price produced by their orders can then affect the firm's own investment decision. In this setting, the timing of bad news changes both the speculator's incentive to trade and the information conveyed by market prices. Chen, Huang, Jiang, Zhang and Zhang study this interaction in a finite trading game, asking how timely loss recognition changes gross trading profits and the ranges of trading costs that support trading or no trading. Their result is Proposition 4 of the held working paper, later published under a different title in Management Science (published article).

The model builds on the feedback-effect framework of Edmans, Goldstein and Jiang (AER 2015), in which a firm learns from its own stock's order flow and, as a result, a speculator gains less from selling on bad news than from buying on good news; their firm has no private information of its own. The present paper adds a privately informed firm whose reporting system may disclose good and bad news with different timeliness, a theme of the accounting literature on conservatism. The paper relates its profit comparisons to the strategic-trading intuition of Kyle (Econometrica 1985).

The comparison matters because a disclosure rule that makes bad news public more often also changes what a null disclosure means. A null report can alter the market maker's valuation, while order flow can lead an uninformed firm to change investment. The question is therefore about prices and real decisions together, under the same reporting rule.

Setting

The underlying state is either good, $H$, or bad, $L$, each with prior probability $1/2$. The firm may increase investment, decrease investment, or keep its current level. A correct change adds $x$ to terminal value and costs $c$; a wrong change loses $x$ and costs $c$. Without a change, terminal value is $R_H$ or $R_L$. The model assumes $0<c<x$ and $R_H-x>R_L+x$.

The firm privately learns the state with probability $f$; otherwise it has a null signal. An informed firm discloses its state with probability $\beta_H$ in state $H$ and $\beta_L$ in state $L$. Write $\beta=(\beta_H+\beta_L)/2$ and $\xi=(\beta_L-\beta_H)/2$, so $\beta_H=\beta-\xi$ and $\beta_L=\beta+\xi$. Positive $\xi$ means bad news is disclosed more promptly than good news. A feasible disclosure rule has $0\leq\beta\pm\xi\leq1$.

After a null report, a speculator may buy one share, sell one share, or abstain. She learns the state with probability $\lambda$; otherwise her private signal is null. An independent noise trader submits an order of $-1$, $0$, or $1$ with equal probability. The market maker sees only the total order flow $X$ and prices the share at expected terminal firm value conditional on the report and $X$. The firm also observes the order flow before its investment decision. When it has no private state signal, it invests only if its posterior exceeds $\bar\mu=1/2+c/(2x)$, divests only if it falls below $\underline\mu=1/2-c/(2x)$, and otherwise keeps its investment.

Two speculator strategies are compared. Under no trading (NT) she abstains; $\pi^{NT}_{buy}$ and $\pi^{NT}_{sell}$ are gross profits from deviating to a buy on good news or a sale on bad news. Under trading (T) she buys on good news and sells on bad news; $\pi^T_{buy}$ and $\pi^T_{sell}$ are the corresponding gross profits. Each profit averages over the three noise orders and uses the market maker's Bayesian price and the firm's response under that strategy. Let $\kappa^T=\min\{\pi^T_{buy},\pi^T_{sell}\}$ and $\kappa^{NT}=\max\{\pi^{NT}_{buy},\pi^{NT}_{sell}\}$. These are the trading cost thresholds reported by Propositions 1 and 2 of the working paper.

Formalization targets

The goal is Proposition 4. For every feasible $\xi$, selling on bad news becomes more profitable as $\xi$ rises, under both profiles:

$$\frac{d\pi^T_{sell}}{d\xi}>0,\qquad \frac{d\pi^{NT}_{sell}}{d\xi}>0.$$

In a neighborhood of neutral reporting, the trading threshold rises with $\xi$:

$$\frac{d\kappa^T}{d\xi}>0\quad\text{near }\xi=0.$$

For every feasible $\widehat\xi>0$, the no-trading threshold under timely loss recognition exceeds both the neutral threshold and the threshold under the mirrored timely gain policy:

$$\kappa^{NT}(\widehat\xi)>\kappa^{NT}(0),\qquad \kappa^{NT}(\widehat\xi)>\kappa^{NT}(-\widehat\xi).$$

The milestone chain establishes the firm's investment rule, the null-report posterior and the probability of an informed firm behind that report, the relevant trading-profile posteriors, the two profiles' gross profit formulas, and the neutral-policy comparisons. The target does not assert that $\kappa^T$ increases across the entire feasible range: the smaller of buying and selling profits can switch away from selling as $\xi$ grows.

Significance

The first claim identifies a strict incentive effect of asymmetric reporting on trading against bad news. The second concerns the trading threshold locally around symmetric reporting, and the third compares the no-trading threshold with neutral reporting and its mirror policy. Together they express how a reporting choice can change the regions of trading cost in which the two profiles are candidates for equilibrium (Chen et al.).

The result is proved in the held working paper. The formalization task is to connect it to an explicit finite Bayesian trading model in Lean. This includes the order-flow likelihoods, the market maker's posterior expected value, the firm's posterior investment rule, and the gross profits averaged over noise orders. Those definitions can support later work on the paper's other trading profiles and on disclosure choices. No machine-checked proof of this mission's goal is claimed here.

Difficulty

The reporting parameter changes more than the posterior probability of $H$ after a null report. It also changes the probability that a firm which made a null report privately knows the state, and hence the value traders expect after the firm's investment decision. The same order flow affects the market maker's price and an uninformed firm's investment. A direct comparison of null-report beliefs alone therefore does not establish the profit inequalities. The minimum defining $\kappa^T$ adds a local regime change: near $\xi=0$ selling is the smaller profit, but that need not remain true at a larger feasible $\xi$.

Formalization scope

The Lean development uses two finite state constructors, three investment decisions, integer order flows, and real-valued probabilities, values and profits. Disclosure and order-flow posteriors are explicit Bayes ratios. Off-path order flows with zero Bayesian denominator receive the paper's belief convention: $H$ at positive $X$, $L$ at negative $X$. The firm's tie-break chooses the status quo at either investment threshold. The speculator's trading cost is excluded from gross profit, as in the paper.

Every theorem carries the paper's standing restrictions $0<c<x$, $R_H-x>R_L+x$, $0<\beta<1$, and $\lambda>2c/(x+c)$. The formalization also makes explicit $0<f<1$ and $\lambda<1$: both are probabilities, and endpoint choices destroy strict conclusions used here. Claims about a given $\xi$ require $0\leq\beta\pm\xi\leq1$. The neighborhood claim is stated as a positive derivative throughout some open interval about zero. In particular, the profits are calculated from the Bayesian prices and the firm's response; they are not defined to equal the closed forms that the milestones ask solvers to prove.

Reusable work includes finite likelihoods, posterior calculations, the optimal investment rule, and algebraic profit reductions. Contributions toward the source-labelled milestone statements and the full derivative comparison are welcome. The held source is the authors' 2018 working paper; its pages and numbering have not been reconciled with the retitled 2021 journal article.

Selected references

• Q. Chen, Z. Huang, X. Jiang, G. Zhang and Y. Zhang, The Role of Asymmetric Disclosure When Price Efficiency Affects Real Efficiency, working paper, 2018, held PDF pp. 7–22 and 33–39; published as Asymmetric Reporting Timeliness and Informational Feedback, Management Science, 2021. DOI.
• A. Edmans, I. Goldstein and W. Jiang, Feedback Effects, Asymmetric Trading, and the Limits to Arbitrage, American Economic Review 105(12), 3766–3797, 2015. DOI.
• A. S. Kyle, Continuous Auctions and Insider Trading, Econometrica 53(6), 1315–1335, 1985. DOI.

Motivation

Durable life-improving products such as solar lamps, water filters and clean cookstoves reach few households in the base of the pyramid (BOP), the low-income markets of developing economies. Two frictions explain much of the gap. Customers cannot afford the product (low ability to pay, ATP), and they are uncertain whether an unfamiliar product is worth its price; being poor, they are also risk averse. Distributors and the foundations that fund them must decide how to spend a fixed budget: on subsidies that make the product affordable, on marketing and demonstrations that inform customers, or on return policies that remove the risk of trying.

Calmon, Jue-Rajasingh, Romero and Stenson (M&SOM 24(4), 1887–1905, 2022; accepted manuscript SSRN 2882402) model this decision, motivated by the Indian distributor Essmart. Their headline finding concerns a funder's dilemma: in the BOP, the allocation that maximizes the distributor's profit is often the one that gives customers the lowest average consumer surplus, and the misalignment disappears when the ATP is high. This mission formalizes that finding and the chain of results the paper proves on the way.

Setting

A unit mass of customers values the product at $v_h$ with probability $\beta\in(0,1)$, and lower otherwise. A fraction $\theta$ of customers is informed and knows its valuation. The rest know only the population distribution. Customers have CARA utility with risk aversion $\alpha>0$, and all of them can pay at most $m$, the homogeneous ATP. A distributor buys at wholesale cost $w$, salvages returned units at $y$, and values consumer surplus with weight $\gamma\in[0,1)$.

The distributor has a budget $b$ per customer. It can raise the ATP by a subsidy $x\in[0,v_h-m]$, and it can raise the education level from $\theta_0$ to $\theta\le1$ at marginal cost $c_\theta$. A downstream retailer then sets prices and refunds. The resulting pricing outcome is given in closed form by the paper's Proposition B.1:

• pricing strategy (a) sells only to informed high-value customers, without returns;
• pricing strategy (b) sells to everyone and accepts returns, with the minimum refund

$$r_\alpha(m)=\max\Big(0,\ m-\tfrac1\alpha\ln\tfrac{1-\beta e^{-\alpha(v_h-m)}}{1-\beta}\Big).$$

Each strategy has its profit $\Pi^a_D,\Pi^b_D$ and consumer surplus $CS^a,CS^b$. The budget constraint is $c_\theta(\theta-\theta_0)+xB\le b$, where the demand $B$ is $\theta\beta$ under (a) and $\beta+(1-\theta)(1-\beta)$ under (b).

Theorem 1 reduces the allocation problem to four strategies:

• F: subsidy first, pricing (a);
• M: education first, pricing (a);
• FR: subsidy first, pricing (b);
• MR: education first, pricing (b).

Each strategy has an explicit allocation $(x^i,\theta^i)$, profit $\Pi^i$ and consumer surplus $CS^i$. The ATP thresholds are

$$m^F=\frac{c_\theta/\beta+w-\gamma v_h}{1-\gamma},\quad m^{MR}=v_h-\frac{(1-\beta)(w-y)-c_\theta}{(1-\gamma)\beta},\quad \bar m^{MR}=v_h-\frac{\beta v_h+(1-\beta)y-w}{(1-\gamma)\beta},$$

and the parameter bounds are $\bar w=\beta v_h+(1-\beta)y$ and $\bar c_\theta=(1-\beta)(w-y)$.

Formalization targets

Goal: Corollary 1 with Proposition 2

There is a threshold $a^{cs}_F(m)\in[0,\infty]$ such that for every $\alpha>0$, MR maximizes consumer surplus with $CS^{MR}\ge CS^M\ge CS^F$, and

$$CS^F\le\min(CS^{MR},CS^M,CS^{FR})\iff\alpha\ge a^{cs}_F(m).$$

If $w\le\bar w$ and $c_\theta\le\bar c_\theta$, then $m^F\le m^{MR},\bar m^{MR}\le v_h$. There is also a threshold $a_F(m)$ such that

$$\Pi^F\ge\max(\Pi^M,\Pi^{FR},\Pi^{MR})\iff m\le m^F\ \text{and}\ \alpha\ge a_F(m),$$

and F is both profit-optimal and worst for consumers iff $m\le m^F$ and $\alpha\ge\max(a_F(m),a^{cs}_F(m))$. Finally, MR is profit-optimal for all $\alpha$ when $m\ge\max(m^{MR},\bar m^{MR})$.

Milestones

In attack order:

1. Theorem 1 in regime form: F/M solve the problem under pricing (a), and FR/MR under (b).
2. Monotonicity and range of the log term $\tfrac{1-\beta}{\alpha}\ln\tfrac{1-\beta e^{-\alpha(v_h-m)}}{1-\beta}$.
3. Lemma B.1, $\theta^M=\theta^{MR}\ge\theta^F\ge\theta^{FR}$.
4. Property 1, $\Pi^F\ge\Pi^M\iff m\le m^F$.
5. Property 4, a risk-aversion threshold for $\Pi^F\ge\Pi^{FR}$.
6. Property 6.
7. The second statement of Property 5.
8. The first bullet of Proposition 2.
9. The threshold for $CS^{FR}\ge CS^F$.

Significance

The result separates two regimes:

• BOP regime (low $m$, high $\alpha$): a profit-maximizing distributor subsidizes customers and refuses returns. Once risk aversion also exceeds $a^{cs}_F(m)$, this is the strategy with the lowest consumer surplus.
• High-ATP regime: education with returns maximizes both profit and surplus.

For a funder whose grant the distributor allocates (p. 10), this means that profit-seeking allocation serves customers well only outside the BOP. The paper's §4.3 goes on to show that an operational commitment, free returns, reduces the misalignment; that extension is not part of this mission.

The results are proved in the paper by direct case analysis; none of them has a machine-checked proof. A complete formalization would make the hypotheses explicit. For example, the paper's list of ATP thresholds includes $w\le m^F$, which fails for $\gamma>0$. The proof also claims that $m\ge m^{MR}$ alone makes MR more profitable than F; a counterexample before $\bar m^{MR}$ is recorded in the moderation notes. Formalization would pin down the tie-breaking and degenerate cases that the prose leaves implicit, and provide a reusable model of CARA-refund pricing with budgeted subsidy and education.

Difficulty

Each strategy value is a composition of positive parts, minima, indicator tie-breaks and a log-exponential refund. The comparisons in the strategy map are therefore piecewise in $(m,\alpha)$, and the obvious approach, writing the closed forms and comparing, breaks into many cases. The threshold statements are harder than inequalities. "F is optimal iff $\alpha\ge a_F(m)$" asserts that the set of good $\alpha$ is a closed upward ray, so one needs monotonicity in $\alpha$ of every competing value. That includes $\Pi^{FR}$, whose allocation jumps when the tie-break flips. One also needs closedness at the jump. The consumer-surplus threshold rests on $\theta^{FR}$ being non-decreasing in $\alpha$, and on the refund term staying within $[0,\beta(v_h-m)]$.

Formalization scope

Everything is real-valued, in the namespace BOPDistrib.Misalign, with the definitions in one file. The parameters are a structure Params with fields $v_h,\beta,w,y,c_\theta,b,\theta_0,\gamma$; $m$ and $\alpha$ are explicit arguments.

The formalization commits to the following conventions.

• Pricing stage. It is Proposition B.1's outcome; the retailer game is not re-derived.
• Refund. $r_\alpha(m)$ keeps its positive part, and $m-r_\alpha(m)$ stands wherever Proposition B.1 has it.
• Strategy values. They are evaluated at the allocations of the proof of Theorem 1, never taken as the closed forms (16)–(17).
• FR tie-break. FR's leftover budget is invested iff $y\le y_\theta$ with $y_\theta=w-(1-\gamma)(m-r_\alpha(m))-(v_h-m)$. This is the proof's indicator; the theorem's text has "$<$".
• Optimality. "Optimal" and "smallest" are weak inequalities.
• Thresholds. The risk-aversion thresholds are existential in $[0,\infty]$, with $\infty$ meaning never, and fixed before $\alpha$. The ATP thresholds are pinned to the proof's formulas.

Added standing hypotheses relative to the page:

• $\alpha>0$, since the refund divides by $\alpha$;
• $\gamma<1$, since $m^F$ divides by $1-\gamma$ and the paper treats only $\gamma\le1$;
• $0<\theta_0<1$ and $c_\theta>0$, which are divisors;
• $0\le m$, since ATP is nonnegative and the refund cannot exceed the customer price;
• $m<v_h$, $b>0$ and the strict homogeneous Assumption 1, $b<c_\theta(1-\theta_0)+\beta(v_h-m)$. At the boundary the F and M allocations coincide, and "F optimal only if $m\le m^F$" fails.

A formalization in which the thresholds are chosen after $\alpha$ (so that $\exists a$ is trivial), or in which $\Pi^F$ is compared with closed forms that build in the conclusion, would be vacuous; both are excluded by the statement shapes. The heterogeneous-ATP model of §5, the free-returns setting of §4.3, and the regime $w>\bar w$ or $c_\theta>\bar c_\theta$ are out of scope.

The work needs elementary real analysis: monotonicity of $\tfrac1\alpha\ln(\cdot)$ in $\alpha$, limits at $0^+$ and $\infty$, and piecewise-linear optimization over a polygon. Contributions of proofs of any milestone are welcome, as are lemmas on the monotonicity of the refund in $\alpha$, which every threshold uses.

Selected references

• A. P. Calmon, D. Jue-Rajasingh, G. Romero, J. Stenson, Operational strategies for distributing durable goods in the base of the pyramid, Manufacturing & Service Operations Management 24(4), 2022. https://doi.org/10.1287/msom.2022.1106 ; accepted manuscript https://ssrn.com/abstract=2882402

Motivation

Many digital goods are sold as bundles assembled from the output of many independent producers: a streaming service carries films from many studios, a music subscription carries many labels, a news or software aggregator carries many publishers. One retailer (the aggregator) prices the bundle and keeps a share of the revenue. The producers split the rest in proportion to how much content each contributes. Two questions follow. How much does each producer contribute when it competes with the others for the shared revenue? And how many producers can survive with positive output when their costs differ?

H. K. Bhargava's Bundling for Flexibility and Variety: An Economic Model for Multiproducer Value Aggregation (Management Science, 2021, doi:10.1287/mnsc.2020.3662) answers both questions in a stylized model with an explicit equilibrium. Its central result, Lemma 1, gives the retailer's price, the number $K$ of active producers, and every producer's output in closed form. The paper's propositions are then derived from these formulas: how outputs respond to costs, how participation responds to the bundle-size elasticity $\theta$, and the effects of mergers and of the revenue share $\gamma$. This mission formalizes Lemma 1 from the author's accepted manuscript (2020).

Setting

There are $I \ge 1$ producers, indexed in ascending order of unit cost, $0 < c_1 \le c_2 \le \dots \le c_I$. Producer $i$ chooses an output $Q_i \ge 0$, measured in value units. The bundle has size $Q = \sum_i Q_i$.

Retailer. For a bundle of size $Q$ the retailer charges a price $P$. Demand is

$$D(P,Q) = \sqrt{AQ^\theta - bP}, \qquad 0 < \theta < 2/3,\ b > 0,$$

with zero demand when $AQ^\theta < bP$. The retailer's distribution cost per unit of demand is $w^R(Q) = wQ^\theta$ (the paper writes this coefficient as $c$). The retailer keeps a fraction $1 - \gamma$ of the surplus, so its profit is

$$\Pi_R(P,Q) = (1-\gamma)\,(P - wQ^\theta)\,D(P,Q), \qquad 0 < \gamma < 1 .$$

The sharable surplus $S(Q)$ is the largest value of $(P - wQ^\theta)D(P,Q)$ over all prices $P$, which is the surplus at the retailer's optimal price. Throughout, $A - bw > 0$.

Producers. Producer $i$ receives the share $\gamma\,(Q_i/Q)\,S(Q)$ of the surplus and pays $c_iQ_i$, so its profit is

$$\pi_i = \gamma\,\frac{Q_i}{Q}\,S(Q) - c_iQ_i .$$

Producers choose their outputs simultaneously. A profile $(Q_1,\dots,Q_I)$ is a Nash equilibrium if no producer can increase its profit by changing its own output to any other $x \ge 0$.

Formalization targets

Write $\alpha = 1 - 3\theta/2$.

Goal: Lemma 1 (p. 14)

Let

$$K = \max\Bigl\{i : c_i \le \frac{c_1 + \dots + c_i}{i - \alpha}\Bigr\},\qquad Q^* = \Bigl[\frac{2\gamma}{b}\,\frac{K - \alpha}{c_1 + \dots + c_K}\Bigr]^{\frac{2}{2-3\theta}}\Bigl(\frac{A-bw}{3}\Bigr)^{\frac{3}{2-3\theta}},$$ $$Q^*_i = \Bigl[1 - c_i\,\frac{K-\alpha}{c_1 + \dots + c_K}\Bigr]\frac{2Q^*}{2-3\theta}\ (i \le K), \qquad Q^*_i = 0\ (i > K).$$

Then $1 \le K \le I$. The retailer's unique optimal price is $P^*(Q) = \frac{2A+bw}{3b}Q^\theta$. A profile is a Nash equilibrium if and only if it equals $(Q^*_1,\dots,Q^*_I)$. Moreover, $\sum_i Q^*_i = Q^*$, every $Q^*_i \ge 0$, and the producers with positive output are exactly those $i \le K$ with $c_i < (c_1+\dots+c_K)/(K-\alpha)$. When $K = 1$, $Q^*_1 = (3\gamma\theta/(bc_1))^{2/(2-3\theta)}((A-bw)/3)^{3/(2-3\theta)}$. When $I \ge 2$, $K = 1$ holds exactly when $c_2 > 2c_1/(3\theta)$.

Milestones

1. (3b)–(3e): the retailer's unique optimal price, demand, profit, and $S(Q) = \frac{2}{b}\bigl(\frac{A-bw}{3}Q^\theta\bigr)^{3/2}$.
2. (4a)–(4c): a positive output is a best response if and only if it solves the first-order condition (4c).
3. (4e): (4c) yields a nonnegative output if and only if $c_i \le \gamma S(Q)/Q$.
4. §3.3: in equilibrium, a producer is active if and only if $c_i < \gamma S(Q)/Q$.
5. Proof step (i): the active producers form an initial segment of the cost order.
6. (5a)–(5c): summing (4c) over the first $k$ producers pins down the aggregate output in closed form.
7. Downward closedness: if $k \ge 2$ satisfies the condition of (2a), so does $k - 1$, and $k = 1$ always does.
8. (6): at the aggregate (5c), the participation bound of the $k$-th producer is condition (2a).
9. (2b): (2c) is (5c) at $k = K$, and (4c) evaluated at $Q^*$ gives $Q^*_i$.

Significance

Lemma 1 is the basis of the paper's comparative statics. Its formulas show that output falls with a producer's own cost and rises with the revenue share. They also show that the number of active producers is set by a single threshold condition rather than by an iterative entry process. Under proportional sharing, several producers with different costs can all remain active, and the condition $c_2 \le 2c_1/(3\theta)$ for at least two active producers is the paper's headline insight about variety.

The paper establishes the closed form by summing first-order conditions. It does not argue that the stationary points are maximizers, that no inactive producer gains by entering, or that the equilibrium is unique. A machine-checked proof of the full characterization, uniqueness included, makes the model a verified base for the paper's later propositions and for variants with other demand curves or sharing rules. No formalization of this model was found on the platform.

Difficulty

The first-order conditions give each active producer's output as a function of the aggregate $Q$, and summing them over a guessed active set gives $Q$. The obvious argument stops there. Turning that computation into an equilibrium characterization requires several further facts.

1. Each producer's profit, viewed as a function of its own output, must be shown concave, so that (4c) describes the best response exactly.
2. The all-zero profile must be ruled out separately, because there the revenue share is $0/0$.
3. The active set of an arbitrary equilibrium must be shown to be an initial segment of the cost order.
4. The count $m$ of active producers in an arbitrary equilibrium must be matched with the $K$ of (2a). This step is delicate under ties: when $c_{m+1} = (c_1 + \dots + c_m)/(m - \alpha)$, index $m+1$ also satisfies the weak condition (2a), so $K$ exceeds $m$. Producer $m+1$ then has output $0$ by (2b), and the two descriptions must be shown to give the same profile.

Finally, $S$ is defined as a supremum over prices, so the closed form (3e) itself requires solving the retailer's problem, including prices above the choke price.

Formalization scope

Producers are Fin I with 0 < I, so Lean's producer i is the paper's producer $i+1$. The paper's distribution-cost coefficient $c$ is named w, and every $A - bc$ of the paper is A - b * w. Costs are ordered by Monotone c and are positive. The standing hypotheses are $b > 0$, $A - bw > 0$, $0 < \theta < 2/3$ and $0 < \gamma < 1$. The paper uses $c_i > 0$, $b > 0$ and $A - bw > 0$ implicitly; they are needed for the formulas to be finite and well-defined. All powers are real powers. Demand uses Real.sqrt, which returns $0$ above the choke price. Outputs are arbitrary nonnegative reals with no upper bound. The Nash equilibrium is the published predicate CachonCoord.Proportional.IsNash (nonnegative real strategies, unilateral deviations) applied to the producers' payoffs. Because the retailer's optimal surplus is folded into $S$, this is the subgame-perfect reading of the paper's backward solution. The share $Q_i/Q$ at $Q = 0$ evaluates to $0$ in Lean; the all-zero profile is still not an equilibrium.

Two readings of the page are fixed explicitly. "The equilibrium" means the unique Nash equilibrium. "The set of producers $1\dots K$ with positive output" is stated exactly, because with the weak inequality of (2a), a producer whose cost ties the threshold has output $0$. Three slips of the page are corrected rather than copied. The page calls $\bar c_{(K)} = \sum_i c_i$ "the average"; the formalization uses the average $(c_1+\dots+c_K)/K$. The share formula printed in the proof is wrong and is not formalized. The proof's "$LHS(i-1) < LHS(i)$" holds only weakly under ties.

The producers' payoff uses the surplus at the retailer's optimal price for the realized bundle size, a supremum over prices. It is not the closed form (3e), so none of the closed forms holds by definition. $K$, $Q^*$, $Q^*_i$ and $P^*$ are fixed by the page's formulas and are not quantified as arbitrary objects satisfying (6).

Everything needed beyond Mathlib is in one definitions file in CoProdBundle.Equil. Contributions are welcome on every milestone. The retailer's square-root pricing problem (milestone 1) and the concavity of the proportional-share payoff behind milestone 2 can be reused in other aggregative games with proportional revenue sharing.

Selected references

• H. K. Bhargava, Bundling for Flexibility and Variety: An Economic Model for Multiproducer Value Aggregation, Management Science, 2021 (author's accepted manuscript, 2020). doi:10.1287/mnsc.2020.3662
• Y. Bakos, E. Brynjolfsson, Bundling and Competition on the Internet, Marketing Science 19(1), 2000. doi:10.1287/mksc.19.1.63.15182
• G. P. Cachon, Supply Chain Coordination with Contracts, Handbooks in Operations Research and Management Science 11, 2003. doi:10.1016/S0927-0507(03)11006-7

Motivation

Diversification is the oldest prescription of decision theory. Bernoulli (1738) used the example of a merchant, Sempronius, who can send his goods on one ship or split them over two ships, and showed that an expected-utility maximizer with concave utility prefers to split. Portfolio choice, insurance and supply-chain sourcing all rest on the same principle: when the risk of loss is known, spreading exposure helps a risk-averse decision maker.

Most real diversification decisions are made without knowing the probability of loss. A common intuition in the ambiguity literature holds that ambiguity aversion, a dislike of not knowing the probabilities, should add a second motive to diversify on top of risk aversion. Epstein (2010) and Klibanoff, Marinacci and Mukerji (2012) debated whether the smooth ambiguity model of Klibanoff, Marinacci and Mukerji (2005) captures a preference for diversification at all.

Berger and Eeckhoudt (iRisk Working Paper 2021-iRisk-02; Management Science 67(3), 2021, doi:10.1287/mnsc.2020.3823) return to Bernoulli's two-ship problem with two experts who disagree about the probability that a ship perishes. They show that ambiguity can lower the value of diversification: under ambiguity neutrality it is below the value for the corresponding known risk (their Proposition 2), and in the smooth model, under constant or increasing absolute ambiguity aversion, it is below the ambiguity-neutral value (their Proposition 4.1). This mission formalizes the second result.

Setting

A decision maker has sure wealth $W_0\in\mathbb R$ and ships cargo of value $L>0$. A ship perishes with probability $p$. Her utility is $u:\mathbb R\to\mathbb R$. Shipping everything on one ship, or splitting the cargo over two ships that perish independently, gives the expected utilities

$$EU^{ND}=p\,u(W_0-L)+(1-p)\,u(W_0),\qquad EU^{D}=p^2u(W_0-L)+2p(1-p)\,u\!\left(W_0-\tfrac L2\right)+(1-p)^2u(W_0).$$

The value of diversification under risk is $VD_{risk}=EU^D-EU^{ND}$.

Under ambiguity, two experts $\theta\in\{1,2\}$ give probabilities $p_1,p_2\in[0,1]$. The decision maker holds the prior $\mu(1)=\mu$, $\mu(2)=1-\mu$ with $\mu\in[0,1]$. Write $\Delta(\theta)=EU^D(p_\theta)-EU^{ND}(p_\theta)$ for the value of diversification according to expert $\theta$. The ambiguity-neutral decision maker averages the experts' expected utilities, so that

$$VD_{AN}=\big[\mu EU^D(p_1)+(1-\mu)EU^D(p_2)\big]-\big[\mu EU^{ND}(p_1)+(1-\mu)EU^{ND}(p_2)\big].$$

The smooth ambiguity model aggregates them through an ambiguity function $\phi$ and takes the certainty equivalent:

$$EU^{j}_{smt}=\phi^{-1}\big(\mu\,\phi(EU^{j}(p_1))+(1-\mu)\,\phi(EU^{j}(p_2))\big),\qquad VD_{smt}=EU^D_{smt}-EU^{ND}_{smt}.$$

A concave $\phi$ expresses ambiguity aversion. A linear $\phi$ gives back $VD_{AN}$. The coefficient of absolute ambiguity aversion is $\lambda(x)=-\phi''(x)/\phi'(x)$. The decision maker exhibits DAAA, CAAA or IAAA (decreasing, constant or increasing absolute ambiguity aversion) when $\lambda$ is strictly decreasing, constant or strictly increasing.

Formalization targets

Goal: Proposition 4.1

Let $u$ be nondecreasing and concave, and let $\phi$ be $C^2$, concave, with $\phi'>0$. Suppose that (i) IAAA holds and $p_1=1-p_2$, or (ii) CAAA or IAAA holds and $p_1,p_2\ge\tfrac12$. Then

$$VD_{smt}\le VD_{AN}.$$

Milestones

1. The closed form $VD_{risk}=p(1-p)\big[2u(W_0-\tfrac L2)-u(W_0-L)-u(W_0)\big]$, (A.1).
2. Proposition 1: for continuous $u$, $VD_{risk}\ge0$ for all $W_0$, $L>0$, $p\in[0,1]$ if and only if $u$ is concave.
3. The closed form $VD_{AN}=\big[\mu p_1(1-p_1)+(1-\mu)p_2(1-p_2)\big]\big[2u(W_0-\tfrac L2)-u(W_0-L)-u(W_0)\big]$, (A.2).
4. Lemma 1, for a two-point lottery: under DAAA, CAAA or IAAA, shifting both expert utilities by $z>0$ moves the certainty equivalent by more than, exactly, or less than $z$.
5. If $p_1=1-p_2$ then $\Delta(1)=\Delta(2)$.
6. If $\tfrac12\le p_2\le p_1\le1$ and $u$ is concave then $\Delta(1)\le\Delta(2)$, strictly under strict concavity, $p_1>p_2$ and $L>0$.
7. For concave $\phi$, $x_1\le x_2$ and $d\ge0$: $\phi^{-1}(\mu\phi(x_1)+(1-\mu)\phi(x_2+d))\le\phi^{-1}(\mu\phi(x_1)+(1-\mu)\phi(x_2))+(1-\mu)d$.

Significance

Proposition 4.1 shows that the smooth model does not automatically turn ambiguity aversion into a stronger taste for diversification. Under CAAA, the exponential case $\phi(x)=-e^{-\lambda x}$ used throughout applied work, together with experts who both consider a loss at least as likely as not, the smooth value of diversification never exceeds the ambiguity-neutral one. Together with Proposition 2 this says that, in Bernoulli's own example, ambiguity weakly lowers the incentive to diversify. Applied models that use the smooth criterion to explain hedging or portfolio spreading by ambiguity aversion rely on the opposite comparison. The result marks the conditions on $\lambda$ and on the experts' beliefs under which that comparison fails.

The paper's proofs are short, but they compress several steps. Lemma 1 is Pratt's (1964) characterization of decreasing, constant and increasing absolute aversion through certainty equivalents, cited without proof. Case (ii) relies on the sentence "it is easy to show that, under the concavity of $\phi$, inequality (A.8) is satisfied if $\Delta(2)>\Delta(1)$", and (A.6)–(A.8) are stated through an expectation over a random $\tilde\Delta$ whose law is never specified. A formal proof fixes the exact hypotheses: risk aversion and monotonicity of $u$, the regularity of $\phi$, and the weak form of the conclusion. The mission also yields a reusable Lean statement of Pratt's comparative-statics lemma for two-point lotteries. As far as is known, none of these results has a machine-checked proof.

Difficulty

The algebra (milestones 1, 3, 5, 6) is routine. Lemma 1 is not: its hypothesis is a pointwise condition on $\lambda=-\phi''/\phi'$, a local quantity, while its conclusion compares certainty equivalents, which are global quantities involving $\phi^{-1}$. Mathlib has no theory of absolute risk aversion or of Pratt's comparison for this to rest on.

The natural first attempt at the goal applies Lemma 1 directly, but this only works when every expert's utility rises by the same amount, which is case (i). In case (ii) the shifts $\Delta(1)\neq\Delta(2)$ differ, and comparing $VD_{smt}$ with the weighted average $\mu\Delta(1)+(1-\mu)\Delta(2)$ requires knowing which expert gains more. It also requires that this expert is the one with the higher no-diversification utility, and that is where $p_\theta\ge\tfrac12$ and the monotonicity of $u$ enter.

Formalization scope

All quantities are real. The utility $u$ and the ambiguity function $\phi$ are functions $\mathbb R\to\mathbb R$, so outcomes $W_0-L<0$ are allowed and logarithmic utility is outside the model. The two experts are two real parameters $p_1,p_2$ with prior weights $\mu,1-\mu$, exactly as the proofs write them. $\phi^{-1}$ is Function.invFun φ. Every argument it receives is a $\mu$-mixture of two values of a continuous, strictly increasing $\phi$, so it lies in the range of $\phi$ and the inverse is the true one.

The following hypotheses are added to the page and disclosed in each item:

• $u$ nondecreasing and concave in the goal;
• $u$ continuous in Proposition 1;
• $\phi$ of class $C^2$ with $\phi'>0$;
• $L>0$;
• nondegeneracy ($x_1\neq x_2$, $0<\mu<1$) for the strict cases of Lemma 1.

IAAA, CAAA and DAAA are monotonicity of $\lambda$, not a sign condition on $\lambda'$. "Decreases the value of diversification" is the weak inequality $VD_{smt}\le VD_{AN}$, the comparison (A.4) of the proof. The strict inequality is false at $p_1=p_2$, at $\mu\in\{0,1\}$, or for linear $u$.

The values of diversification are defined as differences of expected utilities. The closed forms (A.1), (A.2) are milestones, so they cannot become definitions under which those milestones hold by rfl. IAAA is defined through $\lambda$, never through certainty equivalents, which is the conclusion of Lemma 1. Milestone 7 is a repaired two-expert reading of the (A.8) step, not (A.8) as printed.

Not formalized: Proposition 2, the $\alpha$-maxmin results (Propositions 3.1, 3.2), Proposition 4.2, the converse of Lemma 1 and its version for general random variables, and the numerical examples.

Welcome contributions: proofs of the milestones, a general Pratt comparison theorem for certainty equivalents in Lean, and the omitted companion results.

Selected references

• L. Berger, L. Eeckhoudt, Risk, ambiguity, and the value of diversification, Management Science 67(3), 2021; iRisk Working Paper 2021-iRisk-02, IÉSEG School of Management, 2021. https://doi.org/10.1287/mnsc.2020.3823
• D. Bernoulli, Specimen theoriae novae de mensura sortis, 1738; English translation Exposition of a new theory on the measurement of risk, Econometrica 22(1), 1954. https://doi.org/10.2307/1909829
• P. Klibanoff, M. Marinacci, S. Mukerji, A smooth model of decision making under ambiguity, Econometrica 73(6), 2005. https://doi.org/10.1111/j.1468-0262.2005.00640.x
• L. G. Epstein, A paradox for the "smooth ambiguity" model of preference, Econometrica 78(6), 2010. https://doi.org/10.3982/ECTA8689
• P. Klibanoff, M. Marinacci, S. Mukerji, On the smooth ambiguity model: a reply, Econometrica 80(3), 2012. https://doi.org/10.3982/ECTA9775
• J. W. Pratt, Risk aversion in the small and in the large, Econometrica 32(1/2), 1964. https://doi.org/10.2307/1913738