Operations Research

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

A minimum support price (MSP) guarantees farmers a unit sale price at least as high as an announced floor. It can protect farmers when the market price is low, but the same guarantee can require a government payment and can change how much crop is produced. Policy evaluation therefore needs to account for farmers, consumers, and public expenditure together. Chintapalli and Tang examine these effects when the market price is uncertain and farmers decide whether to sow before that price is known (SSRN manuscript, §§3–4). This mission takes the paper's market uncertainty model and its joint assessment of farmer net benefit and net social value. The result is already proved in the paper; the work here is to formalize its definitions and claims in Lean.

Setting

The farmer population has total mass one. Each farmer can produce one unit and has a cultivation cost $c$ uniformly distributed on $[0,1]$. A farmer is small enough to take the eventual market price as given. At total production $q$, the inverse demand price is $p(q,\epsilon)=a-q+\epsilon$, where $a$ is market potential and the shock $\epsilon$ is uniform on $[-\theta,\theta]$. The government announces an MSP $m$ before sowing. A participating farmer receives the effective price $\hat p(m,q,\epsilon)=\max\{m,p(q,\epsilon)\}$: the market price when it exceeds the guarantee and the guaranteed price otherwise (manuscript, pp. 6–8).

Farmers are risk averse according to the paper's value-at-risk participation rule. A farmer with cost $c$ finds the crop lucrative when the probability that effective price is no greater than cost is at most $\alpha$:

$$\Pr\{\hat p(m,q,\epsilon)\le c\}\le\alpha.$$

The equilibrium quantity $q(m)$ equals the mass of farmers whose costs make cultivation lucrative when aggregate production is $q(m)$. The model does not prescribe this quantity in advance. Write $\tau_0=(a-(1-2\alpha)\theta)/2$ for production without an effective guarantee and $\tau(m)=\min\{1,\max\{m,\tau_0\}\}$ for the quantity identified by Theorem 1. The paper considers admissible MSPs $m\in\mathcal M$: the guarantee lies between the lowest and highest possible market price at its equilibrium quantity, or $a-q(m)-\theta\le m\le a-q(m)+\theta$ (manuscript, eqs. (7) and (9), pp. 8–10).

Let $F(m)$ be aggregate expected farmer surplus, computed from the effective sale price less each participating farmer's cost. Let $E(m)$ be government expenditure on the positive difference between the guarantee and the market price. Let $C(m)$ be consumer surplus, the area between inverse demand and the market price over units consumed. The paper evaluates a guarantee through net benefit $B(m)=F(m)-E(m)$ and net social value $V(m)=F(m)+C(m)-E(m)$ (manuscript, pp. 7 and 11–12).

Formalization targets

The milestone path first identifies individual participation and the unique equilibrium quantity, then establishes the paper's explicit formulas for $F$, $E$, and $C$. Two identities in the proof of Proposition 1 summarize the resulting policy values for admissible $m$:

$$B(m)=\tau(m)\left(a-\frac32\tau(m)\right),\qquad V(m)=\tau(m)\bigl(a-\tau(m)\bigr).$$

The goal is Proposition 1 in full. When $a\le3/2$ and $\tau_0\le m\le1$, it states $B(m)\ge0$ if and only if $m\le2a/3$. It identifies an admissible maximizer of net benefit at $m_B=\max\{\tau_0,\min\{1,a/3\}\}$ and says net benefit is independent of $m$ in each of the regions $m\le\tau_0$ and $m\ge1$. It also states $V(m)>0$ for every admissible $m$ and identifies an admissible maximizer at $m_V=\min\{1,a/2\}$ (manuscript, Proposition 1, p. 13). A maximizer is a price attaining the largest value; the proposition does not require uniqueness.

Significance

The two metrics answer different policy questions. Net benefit asks whether farmers' aggregate surplus exceeds the public cost of the support guarantee. Net social value adds consumer surplus to that accounting. Proposition 1 identifies which MSP maximizes each measure and states that the broader value remains positive throughout the admissible range. These conclusions are specific to the paper's linear inverse demand, continuous uniform cost and price shock, and risk-based sowing rule; they do not claim the same price choices for other agricultural markets (manuscript, §4.3).

Formalizing the result requires a machine-checkable account of the continuum of farmer costs, the uniformly distributed market shock, a fixed-point equilibrium, and integrals defining all three welfare components. The manuscript gives a proof; the Lean theorem files in this proposal state open proof obligations. A completed development would make the integral formulas, equilibrium characterization, and optimality claims reusable for related support-price models, while exposing exactly which modeling assumptions they need.

Difficulty

The farmer's sowing decision depends on the distribution of the effective price, and the effective price changes at the support threshold. At the same time, the market price depends on the aggregate number of farmers who sow. Directly inserting a guessed production quantity would skip the equilibrium question. The welfare formulas add a second layer: they must integrate the same participation rule and price guarantee, then compare policies only within the admissible set. Theorem 1's printed farmer-level biconditional also has a boundary cost that requires care, even though a single cost has zero mass under the uniform distribution (manuscript, Theorem 1 and its proof, pp. 10 and 37).

Formalization scope

Lean represents prices, costs, probabilities, and welfare values in $\mathbb R$. The cost distribution is Lebesgue measure on $[0,1]$; the shock law is normalized Lebesgue measure on $[-\theta,\theta]$. The standing assumptions are $0<\alpha<1/2$, $\theta>0$, $1+\theta<a$, and $\tau_0<1$. Positivity of $\theta$ is explicit in Lean because the uniform law and its expectation divide by $2\theta$. The paper treats it implicitly when it specifies a nondegenerate uniform shock. The lucrative rule uses weak inequalities on both the loss event and the probability bound, following the numbered model equations (manuscript, eqs. (1), (5), and (6)).

An MSP's admissibility is evaluated at an equilibrium quantity, not at an arbitrary guessed quantity. Equilibrium is defined as a fixed point of the mass of lucrative farmers; it is not defined to equal $\tau(m)$. Farmer surplus, expenditure, and consumer surplus are integrals, not the later closed forms. This prevents the goal from becoming a substitution exercise. Theorem 1 is restricted to admissible MSP values; its premise evaluates admissibility at the proposed equilibrium $\tau(m)$, which the theorem then identifies as the actual equilibrium. Its farmer-level clause excludes the one threshold cost at which the manuscript's biconditional is inaccurate. Aggregate equilibrium remains the same. The mission covers the single-crop market uncertainty model in §§3–4; the paper's yield uncertainty and two-crop extensions are separate results. Contributions to the fixed-point, measure, integration, and policy-optimization steps are all within scope.

Selected references

• P. Chintapalli and C. S. Tang, The Value and Cost of Crop Minimum Support Price: Farmer and Consumer Welfare and Implementation Cost, Management Science 67 (2021), doi:10.1287/mnsc.2020.3831. The formalized statements and page numbers follow the authors' SSRN manuscript 3681588.

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

Temporal-difference (TD) learning is the basic algorithm of reinforcement learning for estimating the value function of a fixed policy from a single stream of experience. With a linear function approximation $V_\theta(s)=\phi(s)^\top\theta$, TD(0) is the evaluation step inside many policy-iteration and actor–critic methods, and its behaviour governs how much data such methods need.

The asymptotic theory is classical. Tsitsiklis and Van Roy (1997) proved that TD(λ) with linear features converges almost surely along a single trajectory of an ergodic Markov chain, to the unique solution $\theta^*$ of the projected Bellman equation, under Robbins–Monro step sizes. Their proof uses the ODE method, which says nothing about how fast the iterates approach $\theta^*$, nor how the rate depends on the step size, on the conditioning of the features, or on how quickly the chain mixes.

Finite-time results came later and mostly for independent samples. Dalal, Szörényi, Thoppe and Mannor (2018) and Lakshminarayanan and Szepesvári (2018) analysed TD(0) when the observed transitions are drawn i.i.d. from the stationary distribution. Bhandari, Russo and Singal (2018) gave a short analysis in the i.i.d. model and, for a projected variant of TD, the first finite-time bounds when the transitions come from one trajectory of the Markov chain, so that consecutive observations are strongly correlated. This mission formalizes that Markovian result, Theorem 3 of the paper.

Setting

A finite Markov reward process consists of a finite state space $S$, a stochastic matrix $P$ with $P(s,s')$ the probability of moving from $s$ to $s'$, transition rewards $R(s,s')$ with $|R(s,s')|\le r_{\max}$, and a discount factor $0\le\gamma<1$. The chain has a stationary distribution $\pi$ ($\pi P=\pi$), and the observed trajectory $s_0,s_1,\dots$ starts from $\pi$, so it is a stationary sequence.

Each state carries a feature vector $\phi(s)\in\mathbb{R}^d$ with $\|\phi(s)\|_2\le1$. The steady-state feature covariance $\Sigma=\sum_s\pi(s)\phi(s)\phi(s)^\top$ has full rank, and $\omega>0$ is its minimum eigenvalue. Value functions are compared in the steady-state seminorm $\|V_\theta\|_D^2=\sum_s\pi(s)(\phi(s)^\top\theta)^2$.

At a transition $(s,s')$ the TD direction is $g(\theta;s,s')=\big(R(s,s')+\gamma\phi(s')^\top\theta-\phi(s)^\top\theta\big)\phi(s)$. Its steady-state mean is $\bar g(\theta)=\sum_{s,s'}\pi(s)P(s,s')\,g(\theta;s,s')$, and the TD fixed point $\theta^*$ is the vector with $\bar g(\theta^*)=0$. Projected TD(0) with radius $R\ge\|\theta^*\|_2$ starts from $\|\theta_0\|_2\le R$ and iterates

$$\theta_{t+1}=\Pi_{2,R}\big(\theta_t+\alpha_t\,g(\theta_t;s_t,s_{t+1})\big),$$

where $\Pi_{2,R}$ is the Euclidean projection onto the ball of radius $R$. The averaged iterate is $\bar\theta_T=T^{-1}\sum_{t=0}^{T-1}\theta_t$.

The chain mixes uniformly (Assumption 1): there are $m>0$ and $\rho\in(0,1)$ with $\sup_s d_{TV}(P^t(s,\cdot),\pi)\le m\rho^t$ for all $t\ge0$. The mixing time is $\tau_{\mathrm{mix}}(\epsilon)=\min\{t\ge0: m\rho^t\le\epsilon\}$. Write $G=r_{\max}+2R$.

Formalization targets

Goal: Theorem 3 (pp. 17–18)

All three bounds are stated together, with $\mathbb{E}$ the expectation over the stationary trajectory:

(a) for $T\ge1$ and $\alpha_t\equiv1/\sqrt T$,

$$\mathbb{E}\|V_{\theta^*}-V_{\bar\theta_T}\|_D^2\le\frac{\|\theta^*-\theta_0\|_2^2+G^2\big(9+12\tau_{\mathrm{mix}}(1/\sqrt T)\big)}{2\sqrt T(1-\gamma)};$$

(b) for a constant $\alpha_t\equiv\alpha_0\in\big(0,\,1/(2\omega(1-\gamma))\big)$,

$$\mathbb{E}\|\theta^*-\theta_T\|_2^2\le e^{-2\alpha_0(1-\gamma)\omega T}\|\theta^*-\theta_0\|_2^2+\alpha_0\frac{G^2\big(9+12\tau_{\mathrm{mix}}(\alpha_0)\big)}{2(1-\gamma)\omega};$$

(c) for $\alpha_t=1/(\omega(t+1)(1-\gamma))$ and $T\ge1$,

$$\mathbb{E}\|V_{\theta^*}-V_{\bar\theta_T}\|_D^2\le\frac{G^2\big(9+24\tau_{\mathrm{mix}}(\alpha_T)\big)}{T(1-\gamma)^2\omega}(1+\log T).$$

Milestones

The milestones are the paper's own lemmas, in the order the proof in Appendix A uses them: norm equivalence $\sqrt\omega\|\theta\|_2\le\|V_\theta\|_D\le\|\theta\|_2$ (Lemma 1); the descent inequality $(\theta^*-\theta)^\top\bar g(\theta)\ge(1-\gamma)\|V_{\theta^*}-V_\theta\|_D^2$ (Lemma 3); the gradient bound $\|g_t(\theta)\|_2\le r_{\max}+2\|\theta\|_2$ (Lemma 6); the pathwise error recursion (Lemma 8); the coupling bound $|\mathbb{E}v(X,Y)-\mathbb{E}v(X',Y')|\le2\|v\|_\infty m\rho^\tau$ (Lemma 9); boundedness and Lipschitz continuity of the gradient error $\zeta_t$ (Lemma 10); and the bias bound $\mathbb{E}[\zeta_t(\theta_t)]\le G^2(4+6\tau_{\mathrm{mix}}(\alpha_T))\alpha_{t^*}$ (Lemma 11).

Significance

Theorem 3 gives explicit, non-asymptotic mean-squared-error bounds for TD(0) with linear features under Markovian sampling. Part (a) does not depend on the conditioning $\omega$, part (b) shows exponential convergence to a neighbourhood whose radius scales with $\alpha_0G^2\tau_{\mathrm{mix}}(\alpha_0)$, and part (c) gives an $\tilde O(1/T)$ rate. Compared with the i.i.d. bounds, the only change is a factor of order $\tau_{\mathrm{mix}}$: roughly, one mixing time of correlated observations is worth one independent sample. The same argument carries over, in the paper itself, to projected TD(λ) (Theorem 4) and to Q-learning for optimal stopping (§10), so the lemmas formalized here are the core of all of its Markovian results.

The result is proved on paper but has not been machine-checked. The mission provides a Lean statement of the theorem and of each lemma of its proof, all built on one model. The trajectory-level definitions (path law, total-variation mixing, mixing time, projected iterates) can be reused by later formalizations of Markovian stochastic approximation.

Difficulty

The obvious approach, from the i.i.d. analysis, takes expectations in the error recursion of Lemma 8 and uses $\mathbb{E}[\zeta_t(\theta_t)]=0$. Under Markov sampling this fails: $\theta_t$ is a function of $s_0,\dots,s_t$ and is correlated with the observation $(s_t,s_{t+1})$ at which it is evaluated, so the gradient is biased and the noise is not a martingale difference. Bounding that bias needs a quantitative decorrelation between the iterate $\tau$ steps back and the current observation, which is a total-variation estimate on the joint law of a path (Lemma 9). It also needs control of how far the iterates drift in $\tau$ steps, which is where the projection and the uniform gradient bound $G$ enter. The rest of the proof then combines telescoping, a geometric recursion and harmonic sums, with every constant ($9+12\tau$, $9+24\tau$) tracked exactly.

Formalization scope

• State space and expectation. $S$ is a Fintype. The expectation over the stationary trajectory is the finite sum $\sum_{w\in S^{T+1}}\pi(w_0)\prod_iP(w_i,w_{i+1})\,F(w)$, the exact law of $(s_0,\dots,s_T)$ for a finite chain started from $\pi$, so no measure theory is used. The paper itself works with a finite $S$ (p. 5).
• Coupling lemma. Lemma 9 uses probability measures for the conditional laws of $X,Y$ given $s_t,s_{t+\tau}$; their factorization expresses $X\to s_t\to s_{t+\tau}\to Y$. The variables may take values in arbitrary measurable spaces, including the iterates and observations used in the proof.
• Norms. Parameters and features live in EuclideanSpace ℝ (Fin d) with $d\ge1$, so every $\|\cdot\|$ is Euclidean.
• Standing hypotheses, added or made explicit: $0\le\gamma$ (the paper writes $\gamma<1$; the proof of Lemma 3 needs $\gamma\ge0$). $\omega$ is the least value of $\theta^\top\Sigma\theta$ on the unit sphere, that is $\lambda_{\min}(\Sigma)$, together with $\omega>0$ (full rank). $\pi$ is a stationary probability vector, and no separate irreducibility hypothesis is added, since Assumption 1 implies ergodicity. $\theta^*$ is given as a vector with $\bar g(\theta^*)=0$. The implicit conditions are explicit: $T\ge1$ in (a) and (c), $\alpha_0>0$ in (b), $\alpha_T>0$ in Lemma 11, and $\alpha_t\ge0$ in Lemma 8.
• Conventions. $\Pi_{2,R}$ is defined by the rescaling formula of p. 16. $\bar\theta_T$ averages $\theta_0,\dots,\theta_{T-1}$, as in the text and the proof (Algorithm 1's averaging recursion is a slip). $\tau_{\mathrm{mix}}$ is sInf over $\mathbb{N}$ and is only evaluated at positive thresholds, where it is a true minimum. "With probability 1" is stated for every path or transition.
• No trivialization. The expectation must start from $\pi$, never from an arbitrary state. $\theta_t$ and the observation must come from the same trajectory. $\omega$ must be $\lambda_{\min}(\Sigma)$, not an arbitrary positive constant, since it fixes the step size in (c). A formalization with independent samples, with the sup norm on $\mathbb{R}^d$, or with a junk-valued $\tau_{\mathrm{mix}}(0)=0$ would prove a different statement.
• Not in scope. Theorem 1 (mean-path TD), Theorem 2 (i.i.d. model), Theorem 4 (projected TD(λ)) and §10 (Q-learning for optimal stopping) are separate results. Theorem 3's proof does not use them.
• Welcome contributions. Proofs of the milestones, and general lemmas on finite path sums (marginalisation of the trajectory law, the variational form of total variation, nonexpansiveness of the ball projection).

Selected references

• J. Bhandari, D. Russo, R. Singal, A Finite Time Analysis of Temporal Difference Learning With Linear Function Approximation, arXiv:1806.02450v2, 2018; Operations Research 69(3), 2021. https://arxiv.org/abs/1806.02450
• J. N. Tsitsiklis, B. Van Roy, An Analysis of Temporal-Difference Learning with Function Approximation, IEEE Transactions on Automatic Control 42(5), 1997. https://doi.org/10.1109/9.580874
• G. Dalal, B. Szörényi, G. Thoppe, S. Mannor, Finite Sample Analyses for TD(0) with Function Approximation, AAAI 2018. https://arxiv.org/abs/1704.01161
• C. Lakshminarayanan, C. Szepesvári, Linear Stochastic Approximation: How Far Does Constant Step-Size and Iterate Averaging Go?, AISTATS 2018. http://proceedings.mlr.press/v84/lakshminarayanan18a.html
• R. S. Sutton, Learning to Predict by the Methods of Temporal Differences, Machine Learning 3, 1988. https://doi.org/10.1007/BF00115009
• D. A. Levin, Y. Peres, Markov Chains and Mixing Times, 2nd ed., AMS, 2017. https://doi.org/10.1090/mbk/107

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