Missions · Prove2Me

Completed

Convex Optimization Numerical Analysis Operations Research+1·Captain: mikedeng1

Approximate Parametric Computation of Minimum-Cost Flows with Convex Costs: Linear Splines of the Marginal Costs with Bounded Step Sizes Give an (α, β)-Approximate Minimum-Cost Flow FunctionResearch Paper

Motivation

Flow networks model the movement of material, traffic, electricity, or gas through connected systems. In many such models, the required net flow at each vertex varies with a parameter, so the object of interest is a whole family of optimal flows rather than one solution. When edge costs are nonlinear, solving a new optimization problem for every parameter value gives no finite description of that family. Joachims, Klimm and Warode study two approximations of this parametric problem: one approximates each edge's marginal cost, and the other interpolates selected optimal flows. This mission concerns their marginal cost approximation result, Theorem 5.

The paper builds on an exact method for piecewise quadratic edge costs by Klimm and Warode. A piecewise linear approximation of each marginal cost has a piecewise quadratic integral, so it brings general convex costs into the class handled by that method. The question is how fine the linear interpolation mesh must be for the resulting flows to be close to optimal under the original costs. The paper gives local step size bounds involving the second derivative of each marginal cost. The target here is a corrected version of that guarantee, with the precise corrections stated below.

Setting

A network consists of finite sets of vertices $V$ and edges $E$ . Every edge has a tail and a head. The graph is strongly connected and has neither self loops nor parallel directed edges. For an edge flow $x\in\mathbb R^E$ , its net inflow at a vertex is the sum of flows entering that vertex minus the sum leaving it. Two balanced demand vectors $b^0,b\in\mathbb R^V$ determine a demand $b^0+\lambda b$ for $\lambda\in[0,\lambda^{\max}]$ . A flow is feasible when its net inflow equals that demand. In the directed case all edge flows are nonnegative; in the undirected case their signs are unrestricted.

Each edge $e$ has a marginal cost $f_e:\mathbb R\to\mathbb R$ that is strictly increasing, differentiable, nonpositive on negative arguments, and nonnegative on positive arguments. Its edge cost is $F_e(x)=\int_0^x f_e(s)\,ds$ . The total cost is the sum of edge costs, and $C(\lambda)$ is the minimum total cost of a feasible flow at parameter $\lambda$ . These sign conditions make the edge costs nonnegative. The paper calls them homogeneous marginal costs, although this is a sign condition rather than algebraic homogeneity. Section 5.2 gives the model and its approximation criterion.

For each edge, choose a strictly increasing mesh from $-x^{\max}$ to $x^{\max}$ , where

x^{\max}=\max_{0\le\lambda\le\lambda^{\max}}\frac12\sum_{v\in V}|b_v^0+\lambda b_v|.

The linear spline $s_{f_e}$ joins the values of $f_e$ at adjacent mesh points by straight chords. The minimum cost flow function $\widetilde x(\lambda)$ for these spline marginal costs is tested under the original costs: $\widetilde C(\lambda)=\sum_e F_e(\widetilde x_e(\lambda))$ . This convention is essential because a small optimal cost for the spline instance alone says nothing about the cost under $f_e$ .

Formalization targets

The milestones follow the paper's argument in order.

Edge-flow bound (§5.2.1, p. 16): every optimal edge flow satisfies $|x_e(\lambda)|\le x^{\max}$ .
Equation (17) (proof of Lemma 4, p. 16): the closeness condition (15) of marginal costs on $[-x^{\max},x^{\max}]$ gives

\frac{2}{1+\alpha}F_e(x)-\frac{\beta}{(1+\alpha)m}\le\widetilde F_e(x)\le\frac{2\alpha}{1+\alpha}F_e(x)+\frac{\beta}{(1+\alpha)m}.

The (16) case (proof of Lemma 4, p. 17): $|\widetilde f_e|\ge|f_e|$ and (16) give $F_e\le\widetilde F_e\le\alpha F_e+\beta/m$ .
Lemma 4 (p. 16): uniform control of $|\widetilde f_e-f_e|$ on $[-x^{\max},x^{\max}]$ in the sense (15) or (16) makes the minimum-cost flow function of the $\widetilde f$ instance an $(\alpha,\beta)$ -approximation.
Equation (18) (p. 17): the interpolation estimate

|f(x)-s_f(x)|\le\frac18\delta_i^2\max_{\xi\in[x_i,x_{i+1}]}|f''(\xi)|.

Spline domination under (ii) (proof of Theorem 5, p. 18): $|s_{f_e}(x)|\ge|f_e(x)|$ on $[-x^{\max},x^{\max}]$ .
Endpoint maximum under (ii) (proof of Theorem 5, p. 18): $\max_{[x_i,x_{i+1}]}|f_e''|=\max\{|f_e''(x_i)|,|f_e''(x_{i+1})|\}$ .

The goal is the corrected Theorem 5. It states that either of the paper's two explicit step size regimes, involving $\alpha>1$ , $\beta\ge0$ , $m=|E|$ , and $x^{\max}$ , makes the spline instance's minimum cost flow function satisfy

\widetilde C(\lambda)\le\alpha C(\lambda)+\beta\qquad(0\le\lambda\le\lambda^{\max}).

The first regime bounds each step by a local maximum of $|f_e''|$ and the magnitude of $f_e$ at a mesh endpoint. The second adds monotonicity and sign conditions on $f_e''$ and uses its endpoint values. The formal theorem retains the constants $2\sqrt2$ , the factor $1/8$ in (18), and both distinct denominators in Theorem 5. Theorem 5, pp. 17–18 is the source for the exact formulas.

Significance

The guarantee applies to an entire interval of demand parameters. It converts local numerical accuracy of the marginal cost splines into a bound on the original total cost at every parameter value, while preserving feasibility. The edge flow bound explains why it suffices to approximate marginal costs on a finite interval even when edge flows are otherwise real valued.

The paper proves the intended result by a paper argument, but its printed Theorem 5 has a counterexample when a mesh crosses zero without including zero: the spline can lose the marginal cost sign condition, and at zero demand the spline optimum can have positive original cost while the true optimum has cost zero. The corrected goal records a valid target for machine checked proof. Formalizing it also yields reusable definitions of finite flow networks, convex separable edge costs, parametric approximation, and chord splines. No machine checked proof of this theorem is claimed by this mission.

Difficulty

Pointwise closeness of marginal costs does not directly compare the two optimized flows, which may differ on every edge. A direct comparison at the spline optimum must also account for the original optimum and for how the edge costs accumulate across the network. The interpolation estimate alone does not settle this: a mesh interval crossing zero can change the sign of its chord at zero, even when every step size bound in the printed theorem holds. The shape condition in Theorem 5(ii), read literally with the third differentiability assumption, also forces the second derivative to vanish on the negative half line. The mission keeps that condition as printed rather than silently replacing it with a more symmetric one.

Formalization scope

Lean represents vertices and edges by finite types, net inflow by finite sums, and each edge cost by a real interval integral based at zero. A Boolean flag selects the directed case with $x_e\ge0$ or the undirected case with no sign constraint. The general finite lower and upper bounds of problem (14) are outside this mission. The optimal cost is the real infimum of feasible costs; the graph and balanced demand assumptions give feasible flows, and the sign assumptions bound their costs below. The spline is computed from its mesh values, with its end chords extended linearly outside $[-x^{\max},x^{\max}]$ . Meshes are indexed from zero in Lean, regardless of the paper's two indexing styles.

The corrected Theorem 5 requires zero to be a mesh point on every edge. In regime (i), it replaces $|f_e(x_i)|$ by $\min\{|f_e(x_i)|,|f_e(x_{i+1})|\}$ . In regime (ii), both entries of the factor $B$ are square roots of $|f_e''|$ ; this matches the equality $B^2=\max\{|f_e''(x_i)|,|f_e''(x_{i+1})|\}$ used in the printed proof. Lemma 4 and Theorem 5 explicitly require $x^{\max}>0$ , since both step-size bounds and (15), (16) divide by it (with zero demands, a one-point mesh and $\beta=0$ , Theorem 5 would otherwise fail), and its second marginal cost family is continuous, strictly increasing, and sign preserving. These conventions and corrections are recorded in the source analysis for Theorem 5.

A proof must use the chord spline determined by $f_e$ and the mesh; replacing it by an arbitrary close function would discard the numerical claim. Likewise, the bound $|\widetilde x_e(\lambda)|\le x^{\max}$ is never a hypothesis of Lemma 4 or of the goal: it is milestone 1, and assuming it would remove the combinatorial half of the argument. Milestone 6 is stated on $[-x^{\max},x^{\max}]$ rather than on all of $\mathbb R$ as printed, because the linearly extended end chord of a convex function lies below it. Contributions to the flow bound, Lemma 4, the spline estimate, or the final connection between them are all within scope. The flow and spline definitions can also support other approximation results beyond this theorem.

Selected references

Per Joachims, Max Klimm and Philipp Warode, Approximate Parametric Computation of Minimum-Cost Flows with Convex Costs, arXiv preprint, 2022. arXiv:2203.13146v1.
Max Klimm and Philipp Warode, Parametric Computation of Minimum-Cost Flows with Piecewise Quadratic Costs, Mathematics of Operations Research, articles in advance, 2021. DOI:10.1287/moor.2021.1151.

10 thms2 active usersReviewed

Economics Operations Research·Captain: mikedeng1

Skill Acquisition and Data Sales: Under Uncertain Skill Acquisition and Accurate Data, Higher Skill-Acquisition Costs Raise Data Clarity, Data Price and Price InformativenessResearch Paper

Motivation

Asset managers increasingly buy alternative data: satellite images, credit-card panels, web traffic. Raw data of this kind is worthless until someone has the skills to process it, and those skills are costly and uncertain to acquire. A fund can hire data scientists and still find that its models extract little. Huang, Xiong and Yang (Management Science, 2022) build an equilibrium model of a data seller who sells to investors who must first acquire such skills. They ask how the cost of acquiring skills feeds through the data market into the financial market: into how much the price reveals, the cost of capital and return volatility.

The model joins two lines of work. One is the classical noisy rational-expectations market of Grossman and Stiglitz (1980), in which prices partly reveal private information. The other is the literature on selling information started by Admati and Pfleiderer (1986, 1990), in which a monopolist seller degrades the information it sells to limit what the price leaks. The new feature is the "gold rush" of skill acquisition: an investor who pays the cost learns only afterwards whether her skill is high or low.

Setting

A risky asset pays $\tilde\theta\sim N(0,\tau_\theta^{-1})$ and there is noise demand $\tilde u\sim N(0,\tau_u^{-1})$ . A data seller observes $\tilde\theta+\tilde\eta$ with $\tilde\eta\sim N(0,\tau_\eta^{-1})$ ; the precision $\tau_\eta$ is the data accuracy. The seller chooses a clarity $x\in(0,\infty]$ and passes the data with personalized noise, so that a buyer of skill $z$ receives a signal of precision $xz$ about $\tilde\theta+\tilde\eta$ . The value $x=\infty$ means the data are sold "as is".

A continuum of CARA investors with risk aversion $\gamma$ is indexed by $i\in[0,1]$ . Investor $i$ can acquire data-processing skills at cost $C(c,i)$ , where $c>0$ is a cost parameter. The cost is continuous and strictly increasing in $i$ , with $C(c,0)=0$ and $C(c,i)\to\infty$ as $i\to1$ , and it is strictly increasing in $c$ . A skilled investor turns out high-skilled ( $Z_H$ ) or low-skilled ( $Z_L$ ) with probability $\tfrac12$ each, with $0<Z_L<Z_H$ . A mass $\lambda$ of investors becomes skilled.

In the asset market, the price reveals $\tilde\theta+\tilde\eta$ with precision $\alpha^2\tau_u$ , and $\alpha$ is pinned down by the market-clearing equation (14). Skilled investors buy the data at a Nash-bargained price $q=\beta G$ , where $G(x,\alpha)$ is the certainty-equivalent trading gain (15) and $\beta\in(0,1)$ is the seller's bargaining power. Investors acquire skills until the marginal investor is indifferent, $(1-\beta)G(x,\alpha)=C(c,\lambda)$ (19). The seller chooses $x$ to maximize the profit $\lambda q$ . An equilibrium is a clarity $x^*$ with its $(\lambda^*,\alpha^*)$ such that no other feasible clarity gives more profit.

The market outcomes are:

the data price $q^*$ ;
price informativeness $1/\operatorname{Var}(\tilde\theta\mid\tilde p)$ ;
the cost of capital $E(\tilde\theta-\tilde p)$ ;
return volatility $\sigma(\tilde\theta-\tilde p)$ ;
skilled investors' performance, the average certainty-equivalent advantage (21) of a skilled over an unskilled investor.

Formalization targets

Goal: Proposition 5

Fix $0<c_1<c_2$ . There is a threshold $T$ such that, for every data accuracy $\tau_\eta\ge T$ and every pair of equilibria at $c_1$ and $c_2$ , both clarities are finite and

\lambda^*_2<\lambda^*_1,\quad x^*_1<x^*_2,\quad q^*_1<q^*_2,\quad \frac{1}{\operatorname{Var}_1(\tilde\theta\mid\tilde p)}<\frac{1}{\operatorname{Var}_2(\tilde\theta\mid\tilde p)},

E_2(\tilde\theta-\tilde p)<E_1(\tilde\theta-\tilde p),\quad \sigma_2(\tilde\theta-\tilde p)<\sigma_1(\tilde\theta-\tilde p),\quad \mathrm{Performance}_1<\mathrm{Performance}_2 .

The paper writes these as signs of derivatives in $c$ . The goal states them as comparisons between two cost levels, which is what the prose of the proposition asserts.

Milestones

Proposition 1: for given $(\lambda,x)$ , equation (14) has a unique positive root $\alpha$ .
Proof of Proposition 2: for each finite clarity $x$ , a unique $(\lambda,\alpha)$ solves (14) and (19).
Proposition 2 (1): an equilibrium exists.
(C5): on feasible tuples the profit equals $\beta\lambda C(c,\lambda)/(1-\beta)$ .
Proposition 3: in equilibrium, $x^*<\infty$ if $\lambda^*\tau_\eta>\alpha^*\gamma$ and $x^*=\infty$ otherwise.
The clarity limit: as $\tau_\eta\to\infty$ , every solution $x$ of (14) tends to $2\alpha\gamma/(\lambda(Z_H+Z_L))$ .
The α limit: the equilibrium $\alpha^*$ tends to $\sqrt{\tau_\theta/\tau_u}$ .
(C18): the equilibrium $\lambda^*$ tends to a root of (C18).

Significance

The result. Proposition 5 is the paper's headline. When skills are uncertain, a rise in skill-acquisition costs makes prices more informative and lowers the cost of capital and return volatility. When skills are certain, these outcomes stay unchanged (Proposition 4). The mechanism is that the seller cannot tailor one clarity to buyers of unknown skill. To keep buyers interested as costs rise, she provides clearer data, and more information leaks into the price. The result separates the data market from a pure cost shock to information production. It gives empirical predictions for markets where skill acquisition is costlier, such as private or international equities.

Formalizing it. The proposition is proved in the paper by expansion in $w=1/\tau_\eta$ around $w=0$ . A machine-checked version must make "sufficiently high $\tau_\eta$ " precise, with a threshold that holds uniformly over all equilibria. It must also control the exact finite- $\tau_\eta$ equilibrium rather than its limit. The mission also contributes the first noisy rational-expectations model with a strategic data seller on the platform: posterior variances, the equilibrium equation (14), the certainty-equivalent gain, and the seller's choice between finite clarity and selling "as is". No part of the paper has been formalized before.

Difficulty

Several comparisons follow at leading order in $1/\tau_\eta$ . As $\tau_\eta\to\infty$ the equilibrium mass converges to the root of (C18), which is decreasing in $c$ , and the clarity, the data price and performance are, to first order, functions of that mass. The price-informativeness, cost-of-capital and volatility comparisons do not follow at leading order. At $\tau_\eta=\infty$ the ratio $\alpha^*$ tends to $\sqrt{\tau_\theta/\tau_u}$ whatever the cost, so these three outcomes are flat in $c$ to leading order. Their signs come from the $O(1/\tau_\eta)$ correction to $\alpha^*$ , and the correction must be controlled jointly with the seller's optimal clarity. A newcomer's first idea is to set $\tau_\eta=\infty$ in the equilibrium conditions and differentiate. That loses exactly the term that carries the result. A further difficulty is that the seller's optimum is defined by comparison with every feasible clarity, including selling "as is", not by a first-order condition.

Formalization scope

All quantities are real numbers. The parameters satisfy $\tau_\theta,\tau_u,\gamma>0$ , $0<\beta<1$ , $0<Z_L<Z_H$ and $\tau_\eta>0$ . Two of these go beyond the paper's §2 domains, and both are needed:

$\beta>0$ : with $\beta=0$ the profit is identically zero and every clarity is optimal;
$Z_L>0$ : this is the paper's own condition on p. 23.

The cost family is any admissible $C(c,i)$ : continuous and strictly increasing in $i$ on $[0,1)$ , $C(c,0)=0$ , $C(c,i)\to\infty$ as $i\to1^-$ , and strictly increasing in $c$ on $(0,1)$ . "Increasing" in the paper is read as strictly increasing. Clarity is either a finite $x>0$ or "as is". At "as is", (14) becomes $\gamma\alpha=\lambda\tau_\eta$ and both conditional variances given a signal equal $1/(\tau_\theta+\tau_\eta)$ . These are the $x\to\infty$ limits of the finite-clarity formulas. The value $x=0$ is excluded from the choice set because it gives no positive root of (14).

The posterior variances (8), (10), (12), the gain (15), the price coefficients (C1)–(C4), the cost of capital (C12), volatility (C13) and performance (21) are taken as closed-form definitions. Their CARA-normal derivation (Bayes' rule, market clearing, certainty equivalents) is not formalized. Equilibria are defined relationally: a feasible tuple whose profit is at least that of every feasible tuple, with no choice functions.

The goal concludes, rather than assumes, that the equilibrium clarities are finite. It quantifies over every equilibrium at each cost level. It does not define the equilibrium through the $\tau_\eta=\infty$ economy or through the paper's expansions, which would replace the theorem by its heuristic.

A complete development needs real analysis only: the intermediate value theorem, monotonicity, compactness on $(0,\infty]$ , and asymptotics in $1/\tau_\eta$ . Contributions are welcome on any milestone, on an independent proof of Proposition 4's $\Delta=0$ counterpart, and on a formal derivation of the closed forms from Gaussian conditioning and CARA utility, which would be reusable for other rational-expectations models.

Selected references

S. Huang, Y. Xiong, L. Yang, Skill Acquisition and Data Sales, Management Science 68(8), 2022; working paper version of July 2019. https://doi.org/10.1287/mnsc.2021.4117
S. J. Grossman, J. E. Stiglitz, On the Impossibility of Informationally Efficient Markets, American Economic Review 70(3), 1980. https://www.jstor.org/stable/1805228
A. R. Admati, P. Pfleiderer, A Monopolistic Market for Information, Journal of Economic Theory 39(2), 1986. https://doi.org/10.1016/0022-0531(86)90049-3
A. R. Admati, P. Pfleiderer, Direct and Indirect Sale of Information, Econometrica 58(4), 1990. https://doi.org/10.2307/2938330
N. Gârleanu, L. H. Pedersen, Efficiently Inefficient Markets for Assets and Asset Management, Journal of Finance 73(4), 2018. https://doi.org/10.1111/jofi.12696

11 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Managing Social Responsibility in Multitier Supply Chains: The Buyer's Optimal Strategy Is Control, Delegation or No Effort, Decided by Thresholds in the Loss-Adjusted Effort CostsResearch Paper

Why responsibility effort matters across tiers

A buyer can face public and financial losses when a remote supplier violates labor, safety, or environmental standards, even if the buyer did not cause the violation directly. The buyer and an intermediate supplier can spend resources to help the remote supplier reduce this risk. Their incentives depend on who pays for the effort and who bears the loss when a violation is detected. Huang, Song, and Swinney model these choices in a fixed three-tier supply chain and characterize which firm takes the downstream responsibility effort. Their result gives a precise threshold rule for when the buyer should act, let the intermediate supplier act, or leave both of them idle (Huang, Song, and Swinney, SSRN author version, 2021, §§3–4).

The mission concerns the paper's base model and Theorem 1. It is a known result with a proof in the online supplement to the paper. The formalization target is to reconstruct that result as a theorem about the sequential game itself, with the parameter assumptions and boundary cases stated explicitly. The paper also studies external stakeholder pressure, two-tier comparisons, and variants of the effort model; those later results are outside this mission.

Three firms, effort, and risk

A Tier 0 buyer sources from a Tier 1 supplier, which sources from a Tier 2 supplier. The buyer sells one product with deterministic demand $d$ . Each tier $i\in\{0,1,2\}$ has a fixed per-unit margin $m_i\ge0$ and chooses responsibility effort $x_i\ge0$ at linear cost $k_i x_i$ , with $k_i>0$ . Only Tier 2 can experience a responsibility violation. Tier 0 and Tier 1 efforts are substitutes: their combined contribution is $x_0+x_1$ . Tier 2 effort complements that contribution and also has a baseline return $b>0$ . The effective total effort is therefore $x_2(x_0+x_1+b)$ (§3.1, pp. 7–9).

An actual violation has probability $\lambda(x_0,x_1,x_2)=\exp[-x_2(x_0+x_1+b)]$ . Conditional on a violation, the public detects it with probability $\beta$ , so the probability of a detected violation is $\alpha=\beta\lambda$ . Each firm loses a fraction $\gamma\in(0,1)$ of demand times its margin, plus an indirect financial loss $a_i$ . Its total loss is $\ell_i=\gamma m_i d+a_i$ . The paper's expected profit and loss-adjusted effort cost are

\Pi_i(x_0,x_1,x_2)=m_i d-k_i x_i-\ell_i\alpha(x_0,x_1,x_2), \qquad \tau_i=\frac{k_i}{\ell_i}.

The ratio $\tau_i$ measures effort cost relative to the firm's loss from a detected violation. The paper assumes $b>\tau_2/\beta$ , which keeps Tier 2's best response positive even when the buyer and Tier 1 make no effort (§3.2, pp. 10–12, equation (1)).

The game is sequential. The buyer chooses $x_0$ first; Tier 1 observes it and chooses $x_1$ ; Tier 2 observes both and chooses $x_2$ . A best response at either supplier maximizes that supplier's expected profit among nonnegative efforts after the observed history. The buyer anticipates these responses and maximizes its resulting profit. The paper chooses positive effort when zero and a positive effort tie (§3.2, pp. 10–12).

Formalization targets

The central target is Theorem 1 on pp. 14–15. The selected buyer optimum has no outcome in which both the buyer and Tier 1 exert positive effort. Its effort choices fall into three Table 2 rows: control, in which Tier 0 acts and Tier 1 does not; delegation, in which Tier 1 acts and Tier 0 does not; and no effort, in which neither downstream firm acts. Tier 2 still exerts effort in each row. Table 2 specifies all three efforts, the actual violation probability $\lambda$ , and the detected probability $\alpha$ (Table 2 and Theorem 1).

The threshold rule is

g(\tau_0)=\left(\frac{b\tau_0}{2\sqrt{\tau_0}-\sqrt{\tau_1}}\right)^2, \qquad \begin{array}{ll} \tau_1<\tau_2/b^2:\!& \begin{cases} \text{control},&\tau_0\le\tau_1/4,\\ \text{control if }\tau_2\le g(\tau_0),\text{ otherwise delegation}, &\tau_1/4<\tau_0\le\tau_1,\\ \text{delegation},&\tau_0>\tau_1; \end{cases}\\[1em] \tau_1\ge\tau_2/b^2:\!& \text{control if }\tau_0\le\tau_2/b^2,\text{ otherwise no effort}. \end{array}

The milestone list follows the paper's two supplier best-response lemmas, the buyer's piecewise reduced profit in the proof of Theorem 1, and the comparisons that separate the candidate outcomes. Each milestone is stated about profits and best responses, rather than merely restating a Table 2 row (Lemma 1, p. 12; Lemma 2, p. 13; Online Supplement, p. 1).

What the result gives

The theorem identifies a buyer's optimal responsibility-management regime using the ratios $\tau_i$ , the Tier 2 baseline $b$ , and the model's risk parameters. The distinction matters because a buyer's direct effort can displace the Tier 1 supplier's effort: a low effort cost for the buyer alone does not settle which firm should act. Table 2 also turns the chosen regime into an explicit violation probability, so the result characterizes both private effort and the supply chain's responsibility outcome (Theorem 1 and discussion, pp. 14–15).

The source paper proves Theorem 1; the Lean declarations in this mission are open proof targets. Formalizing them will supply reusable definitions for a three-player sequential effort game and a checked route from the suppliers' optimality conditions to the buyer's full equilibrium classification. Later statements about stakeholder pressure and the two-tier comparison can build on the same model once the base theorem is proved.

Where the classification is difficult

Tier 1's best response changes at $x_0=\sqrt{\tau_2/\tau_1}-b$ : below that point it offsets some of the buyer's effort, while above it Tier 1 exerts zero effort. The buyer's reduced profit therefore changes form at the same boundary. Optimizing a single smooth expression across all nonnegative $x_0$ would miss that change. The equality cases also matter: at the control–delegation boundary the two choices have equal buyer profit, and the paper's convention selects positive buyer effort (§4.1 and Online Supplement §A, proof of Theorem 1).

Formalization scope

Lean represents all parameters, efforts, profits, and probabilities as real numbers. The three tier indices are explicit fields, and every player's feasible efforts are nonnegative. A separate sequential-game definition gives the argmax meaning of both supplier best responses and buyer optimality. The paper-specific model defines $\ell_i$ , $\tau_i$ , the exponential risk function, equation (1), the Table 2 rows, and $g$ . The goal quantifies over every pair of supplier best-response strategies; it does not define those strategies as the formulas to be proved in Lemmas 1 and 2. Buyer optimality ranges over every feasible effort, rather than over the three candidate rows.

The model's standing predicate records $d>0$ , $m_i\ge0$ , $a_i\ge0$ , $k_i>0$ , $\ell_i>0$ , $0<\gamma<1$ , $0<\beta\le1$ , $b>0$ , and $b>\tau_2/\beta$ . Positive demand, nonnegative indirect loss, positive total loss, and positive $\beta$ make economic sign and division conventions explicit where the source uses them without a separate assumption. The denominator of $g$ is positive in the only region where Theorem 1 uses it, $\tau_0>\tau_1/4$ . Real logarithms and square roots are used only with positive arguments in the applicable equilibrium rows. At $\tau_0=\tau_2/b^2$ , the control effort is zero and its row coincides with the no-effort outcome; the theorem retains the paper's weak inequality.

The initial reusable work is the sequential-game interface and the two best-response characterizations. Contributions that prove those results, the reduced-profit identity, the domination and comparison statements, or the full threshold classification all advance the mission. Statements obtained by assuming the Table 2 formulas are already optimal would bypass the result being formalized.

Selected references

L. Huang, J.-S. Song, and R. Swinney, Managing Social Responsibility in Multitier Supply Chains, SSRN author version dated October 2021, SSRN 2837332. This mission cites its pp. 7–15 and Online Supplement §A, pp. 1–2.
L. Huang, J.-S. Song, and R. Swinney, Managing Social Responsibility in Multitier Supply Chains, Manufacturing & Service Operations Management, doi:10.1287/msom.2021.1063. The mission's theorem indices and pages follow the held SSRN author version.

8 thms2 active usersReviewed

Completed

Economics Mechanism Design Operations Research·Captain: mikedeng1

Optimal Management of Evolving Hierarchies: Full Transfers to Immediate Predecessors Form the Unique Decentralized Socially Optimal Allocation SchemeResearch Paper

Motivation

Some organizations grow by asking each member to recruit a successor. The incentive facing a member depends on where the revenue generated by later members goes. A transfer rule may reward the recruiter, keep the revenue with the entrant, or divide it among several predecessors. Hougaard, Moreno-Ternero, and Østerdal ask which fixed rule gives the greatest total expected payoff when members choose recruitment investments for themselves. Their model covers a sequential hierarchy with no fixed terminal generation, so both incentives and the possibility of a very long hierarchy matter. The authors also discuss recruitment and blockchain rewards as interpretations of the same transfer problem. Hougaard et al.

The paper distinguishes a centralized benchmark from a decentralized design problem. In the centralized benchmark, investments can be chosen to maximize the hierarchy’s total value directly. In the decentralized problem, each agent chooses an investment privately after the allocation rule has been announced. The result targeted here is the paper’s Theorem 2 for the decentralized problem, in the authors’ Universidad Pablo de Olavide working-paper version dated August 3, 2021. Its page numbering and theorem labels refer to that version. Hougaard et al.

Setting

Agents are numbered $0,1,2,\ldots$ . Agent $0$ is present initially. If agent $i$ has arrived, she invests $x_i\geq0$ and recruits agent $i+1$ with probability $p(x_i)$ . The common technology $p$ is strictly increasing and strictly concave, starts at $p(0)=0$ , takes values below one, has an unbounded right derivative near zero, and has convex ratio $p/p'$ on positive investments. These conditions apply throughout the model. A member may invest any nonnegative amount; there is no budget ceiling. Hougaard et al., §2

Each arrival creates one unit of value. An allocation scheme $t$ has entry $t_{ij}$ for the share of agent $i$ ’s unit given to agent $j$ . Shares are between zero and one, shares to a later agent are zero, and each row sums to one: $\sum_{j\leq i}t_{ij}=1$ . Write $w_0(x)=1$ and $w_i(x)=\prod_{k<i}p(x_k)$ for the probability that agent $i$ arrives. Conditional on arriving, agent $i$ receives her own share, pays her investment, and may receive shares from later arrivals. The paper denotes this conditional expected payoff by $E_i(t,x)$ ; equation (1) gives its full series. Hougaard et al., pp. 7–9

A profile $x$ is a Nash equilibrium of a scheme if, for every agent $i$ and every alternative $y\geq0$ , changing only $x_i$ to $y$ cannot raise that agent’s conditional payoff. This includes agents reached with probability zero under the current profile: each is still a player in the induced game. The hierarchy’s expected length is $L(x)=\sum_{i\geq0}w_i(x)$ , and its expected investment is $I(x)=\sum_{i\geq0}w_i(x)x_i$ . Transfers cancel in the total, so the social value is associated with the profile rather than the scheme and equals $L(x)-I(x)$ when the series are finite. Hougaard et al., pp. 8–10

A scheme is decentralized socially optimal when at least one of its equilibria has social value at least as high as every equilibrium under every valid allocation scheme. This existential choice of a supporting equilibrium matters because a scheme can have more than one equilibrium. The comparison concerns outcomes agents can sustain in equilibrium, rather than all investment profiles, including those a planner could impose without incentives. Hougaard et al., pp. 10–12

Formalization targets

Goal: Theorem 2

Let $t^*$ keep agent $0$ ’s initial unit with agent $0$ and give the entire unit created by each later agent to that agent’s immediate predecessor:

t^*_{ij}=1\quad\Longleftrightarrow\quad i=j+1\ \text{or}\ i=j=0,

with every other entry zero. The goal asserts both existence and uniqueness:

t^*\text{ is decentralized socially optimal},\qquad t\text{ is decentralized socially optimal}\Longrightarrow t=t^*.

Equality is entrywise equality of schemes. The goal does not assert that every scheme has a unique equilibrium. Under $t^*$ , the supporting equilibrium is constant, $x_i=\chi$ , with $p'(\chi)=1$ . Hougaard et al., Theorem 2, p. 12; proof of Proposition 1, p. 27

Milestones

The milestone list follows the claims used in the paper’s proof: finite investment gives finite expected length; the best length at fixed expected investment is attained; a constant profile of the same length uses less investment than a nonconstant profile; a weighted gross-return identity accounts for all later arrivals; a nonconstant equilibrium is surpassed in social value by the unique constant profile of equal length, supported as an equilibrium; the equilibrium under $t^*$ is identified; and the two parts of Theorem 2 are established separately. The length and value comparisons use the source’s own quantities $L$ , $I$ , $V$ , and $E_i^*$ . Hougaard et al., proof of Theorem 2, pp. 20–27

Significance

Theorem 2 identifies the complete transfer table that gives the largest attainable social value under private investment choices. It rules out every other feasible scheme, including schemes that spread a successor’s revenue across several predecessors. The result also fixes a reference point for the paper’s comparison with centralized investment and for its later analysis of rules that optimize the initiator’s payoff instead. Those later results concern different objectives and are outside this mission. Hougaard et al., §§3–4

The paper proves the result on paper. The formalization task is to give a machine-checked proof of its exact claim, including the infinite-horizon payoffs and the quantifiers over all schemes and their equilibria. The definitions of nonnegative-action equilibrium, sequential survival weights, and extended-valued expected returns can also support later work on sequential incentive systems. No proof of this theorem is supplied by the draft statement itself.

Difficulty

The obvious hope is that a rule that fully rewards the immediate recruiter must produce the best outcome because it ties each payment to the next successful addition. That observation does not compare all possible equilibria: a different rule may redistribute receipts from several future arrivals and change investment at every stage. The hierarchy has no finite horizon, and an agent’s gross expected receipts can be infinite. A complete argument must control those series while comparing a nonconstant equilibrium to a constant one, then establish that no different transfer entry can support an equally good outcome. The paper’s proof organizes these obstacles in Steps 0–5. Hougaard et al., pp. 20–27

Formalization scope

Lean represents agents by natural numbers, with zero as the initial agent. Profiles and schemes are real-valued functions; validity requires nonnegative investments and row-stochastic, lower-triangular transfer shares. The technology structure carries every standing assumption of §2. Differentiability is stated on positive investments together with continuity at zero from the right, consistent with the paper’s infinite right derivative there. Hougaard et al., pp. 7–10

Expected length, expected investment, and gross receipts are sums in extended nonnegative reals. Conditional payoffs and social values use extended reals. The value convention assigns negative infinity when expected investment is infinite; otherwise it uses the finite real difference $L-I$ . Step 0 supplies the finiteness of $L$ in that latter case. The maximum-length function takes a supremum over profiles with exactly the specified expected investment, and its milestone includes finiteness and attainment. These choices retain the source’s possible infinite payoffs and avoid an accidental zero value for a divergent real series. Hougaard et al., footnote 8 and proof of Theorem 2, Step 0

Steps 2–3 require a disclosed boundary reading: “nonconstant” means differing investments among agents with positive probability of arrival, and the profile has finite expected length. Without these conditions, a profile can differ only after recruitment has stopped, or have infinite length, making the printed comparison false. The Step 3 identity carries the no-self-transfer condition used where the paper invokes it. The goal itself has no such extra conditions. The equilibrium definition ranges over every agent and every nonnegative unilateral deviation, and decentralized optimality compares every equilibrium of every valid scheme; neither class is empty by definition. Contributions proving the eight milestones, the goal, or reusable lemmas for their infinite sums and concavity claims are in scope. Hougaard et al., pp. 9–10, 24–27

Selected references

Jens Leth Hougaard, Juan D. Moreno-Ternero, and Lars Peter Østerdal, Optimal Management of Evolving Hierarchies, Universidad Pablo de Olavide WP ECON 21.15, August 3, 2021; published in Management Science (2022). DOI: 10.1287/mnsc.2021.4185.

11 thms2 active usersReviewed

Control Theory Operations Research Optimization·Captain: mikedeng1

Managing Self-Replicating Innovative Goods: Characterization of the Optimal Production and Sales Policies under Strong ReplicabilityResearch Paper

Why self-replicating goods

Some goods can only be made by copies of themselves. RepRap and Prusa 3D printers print the parts of new printers, seed stock is grown from seed, and livestock herds breed. For such a good the inventory is also the production capacity: a unit sold today is a unit that will not replicate tomorrow. A firm launching such a good has to decide, at every instant, how much of its stock to use for replication and how much demand to serve. Demand for an innovative good is not exogenous either. It diffuses through the market by word-of-mouth, so sales held back today also slow future demand.

B. Hu and Z. Sun (Management Science) model this as a deterministic optimal control problem. Their demand side is the Bass diffusion model (Bass, 1969) in the supply-constrained form of Ho, Savin and Terwiesch (2002) and Kumar and Swaminathan (2003), where cumulative sales rather than cumulative demand drive imitation. Hu and Sun add diminishing word-of-mouth. Their main structural result, Theorem 1, says that under a condition they call Strong Replicability the optimal policy switches only once and can be found by a one-dimensional search.

The model

Time runs over $[0,T]$ , where $T$ is the life cycle. The firm controls a production rate $p(t)$ and a sales rate $s(t)$ . The state consists of the cumulative demand $D(t)$ , the adjusted cumulative sales $S(t)$ and the inventory $I(t)$ . The demand rate is

d(t)=\Big[\alpha+\frac{\beta S(t)}{m}\Big]\big[m-D(t)\big],

where $m$ is the market size, $\alpha$ the coefficient of innovation and $\beta$ the coefficient of imitation. Problem (1) of the paper is

\max_{p,s}\int_0^T\big[\pi s(t)-cp(t)-hI(t)\big]e^{-\rho t}\,dt

subject to

D'=d,\quad S'=s-wS,\quad I'=p-s,\qquad 0\le p\le rI,\quad 0\le s\le d,\quad I(T)\ge0,

D(0)=S(0)=0,\qquad I(0)=I_L>0.

Here $\pi$ is the price, $c$ the unit replication cost, $h$ the holding cost rate, $r$ the replication rate, $\rho\ge0$ the discount rate and $w\ge0$ the rate at which word-of-mouth decays. Unmet demand is lost. The paper assumes $\pi>c$ and $r>\rho$ . Production is on when $p=rI$ and off when $p=0$ . Sales are on when $s=d$ and off when $s=0$ .

Strong Replicability is condition (2),

(r-\rho)\pi>cr+h.

It says that letting a unit replicate for a short time and selling the offspring later is worth more than selling the unit now.

Two levels of the launch inventory organise the answer. $\underline I$ is the level at which keeping production and sales always on depletes the inventory exactly at $T$ . $\overline I$ is the level at which keeping production off and sales on depletes it exactly at $T$ .

Formalization targets

Goal: Theorem 1

Assume Strong Replicability. Then:

(a) if $I_L<\underline I$ , the policy that keeps production always on and switches sales on once, at the time that depletes the inventory exactly at $T$ , is optimal;
(b) if $\underline I<I_L<\overline I$ , the policy that keeps sales always on and switches production on once, at the time that depletes the inventory exactly at $T$ , is optimal;
(c) if $I_L>\overline I$ , the policy that keeps sales always on and production off is optimal, and it leaves inventory at $T$ .

In each case, optimal means that the profit is at least

\int_0^T\big[\pi\tilde s-c\tilde p-h\tilde I\big]e^{-\rho t}\,dt

for every admissible trajectory $(\tilde D,\tilde S,\tilde I,\tilde p,\tilde s)$ , not only for policies of the stated shape. The switching times are not given in closed form, and the theorem asserts only that they exist.

Milestones

The thresholds are ordered, $\underline I<\overline I$ (preamble of Theorem 1).
Proposition 1. Once production is switched on, an optimal policy keeps it on until $T$ or inventory depletion.
Proposition 2, first half. Under Strong Replicability, every optimal trajectory has $I(t)>0$ for all $t<T$ , whatever $T$ is.

Significance

Theorem 1 turns an infinite-dimensional control problem into a choice of one switching time. Its managerial content is that a firm with a replicating good should, when stock is scarce, run replication at full capacity and hold back sales, losing some early customers, as long as the stock built up will eventually be sold. Proposition 2 says that under Strong Replicability the firm never sells out before the end of the life cycle. The paper's numerical study (§4) and its extensions (§5: backlogged demand, liquidity, stochastic diffusion) are built on this characterization.

The result has a published informal proof (pp. 36–37 of the manuscript), which applies necessary conditions from Pontryagin's maximum principle and then a perturbation and exchange argument. None of it is machine-checked. A complete formal proof would establish global optimality, against all integrable controls, for a nonlinear controlled ODE with mixed state–control constraints. That is a sufficiency statement, which the necessary conditions alone do not give.

Difficulty

The maximum principle gives necessary conditions only, and Problem (1) is not concave: the dynamics of $D$ are bilinear in $S$ and $D$ , and the constraint $p\le rI$ couples control and state. So the obvious route, solving the Pontryagin system and reading off the optimum, does not prove optimality. The paper's own argument is an exchange argument. It postpones sales or shifts production forward and claims each change improves profit, and it applies the change recursively ("by making the same argument recursively"). Making it rigorous requires comparison results for the Bass system under perturbed sales, which are delicate. Postponing sales lowers the adjusted sales $S$ , and with it all future demand. The existence of the switching times also needs a continuity argument on the depletion time as a function of the switch.

Formalization scope

The Lean development lives in the namespace SelfReplic.Strong and uses real numbers throughout.

Parameters form a structure Params with fields m, price, c, h, r, alpha, beta, rho, w, T, IL. The predicate Params.Standing collects the page's assumptions $I_L>0$ , $\pi>c$ , $r>\rho\ge0$ , $w\ge0$ . It adds the sign conditions $m>0$ , $T>0$ , $\alpha>0$ , $\beta\ge0$ , $c\ge0$ , $h\ge0$ , which the paper uses but never states. Params.StrongRepl is condition (2).
Admissible trajectories (IsAdmissible) have integrable controls $p,s$ and continuous states $D,S,I$ on $[0,T]$ . The three ODEs hold in integral form at every $t\in[0,T]$ , the constraints $0\le p\le rI$ , $0\le s\le d$ hold at every $t\in[0,T]$ , and $I(T)\ge0$ . The integral form is used because bang-bang controls are discontinuous. Continuity and integrability prevent any integral from silently taking Lean's default value $0$ . Nonnegativity of $I$ follows from $0\le p\le rI$ , as on p. 8.
Optimality (IsOptimal) compares the discounted profit with every admissible trajectory of the same parameters.
Policy shapes are pointwise statements on $[0,T]$ , and a switch instant counts as "on". The thresholds $\underline I,\overline I$ enter as real numbers with their defining property (IsLowLevel, IsHighLevel), evaluated at the same parameters with $I_L$ replaced.
Proposition 1 is read up to null sets ("production has run before $t_0$ ", conclusion almost everywhere). It carries the added hypothesis $\rho c+h>0$ , which the paper's proof uses. Without it ( $\rho=h=0$ ), pausing production is costless and the statement fails.

A formalization that states Theorem 1 inside its own policy class (the best policy of shape (a) is the best of shape (a)) would be empty. Here the competitor in every case ranges over all admissible trajectories.

Not formalized: Theorem 2 (Weak Replicability), whose closed form (3) for the production interval is inexact when $\rho>0$ ; Corollaries 1–2; the second half of Proposition 2, which fails when $I_L\ge m$ ; the unnumbered bang-bang claim of p. 9; Propositions 3–4 (§5).

Contributions that would be reusable beyond this mission include existence and uniqueness for the controlled Bass system in integral form, a comparison lemma for $D$ and $S$ under pointwise-ordered sales, and a sufficiency (verification) theorem for bang-bang controls of problems that are linear in the control.

Selected references

B. Hu, Z. Sun, Managing self-replicating innovative goods, Management Science (doi:10.1287/mnsc.2020.3936); authors' manuscript of 2020-10-18. https://doi.org/10.1287/mnsc.2020.3936
F. M. Bass, A new product growth for model consumer durables, Management Science 15(5), 215–227, 1969. https://doi.org/10.1287/mnsc.15.5.215
T.-H. Ho, S. Savin, C. Terwiesch, Managing demand and sales dynamics in new product diffusion under supply constraint, Management Science 48(2), 187–206, 2002. https://doi.org/10.1287/mnsc.48.2.187.255
S. Kumar, J. M. Swaminathan, Diffusion of innovations under supply constraints, Operations Research 51(6), 866–879, 2003. https://doi.org/10.1287/opre.51.6.866.24918
S. P. Sethi, Optimal Control Theory: Applications to Management Science and Economics, 3rd ed., Springer, 2019. https://doi.org/10.1007/978-3-319-98237-3

8 thms2 active usersReviewed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Supplier Encroachment in a Non-Exclusive Reselling Channel: The Encroaching Supplier May Sell Only Directly at a Positive Direct Cost, or Through Both Channels at a Negative OneResearch Paper

Why encroachment through a shared reseller matters

Manufacturers that sell through retailers increasingly also sell directly to consumers, through their own web stores or outlets. The operations literature calls this supplier encroachment. The classical analysis (Arya, Mittendorf and Sappington, 2007) assumes an exclusive reseller: the reseller carries only the encroaching supplier's product. In that setting a supplier whose direct channel costs more per unit than the reseller's still sells through the reseller, and a supplier whose direct channel is cheaper never does.

Real resellers are rarely exclusive. A retailer that carries one brand usually carries competing brands too, and its order from one supplier depends on its order from the others. Hotkar and Gilbert (Management Science, 2021) study what changes when the reseller is non-exclusive. Their headline finding, Proposition 5, is that both conclusions of the exclusive model can reverse.

Setting

Two suppliers, $i\in\{1,2\}$ , sell partially substitutable products through one reseller. Supplier 1 can also sell directly. The reseller orders $q_1$ and $q_2$ ; supplier 1 sells $y$ units directly. The substitutability between the two suppliers' products is $\theta_{12}\in(0,1)$ , written $\theta$ below. Supplier 1's direct product is a perfect substitute for her product at the reseller. Prices clear the market linearly:

p_1=1-q_1-\theta q_2-y,\qquad p_2=1-q_2-\theta q_1-\theta y,\qquad p_d=1-y-q_1-\theta q_2 .

Production and reselling cost nothing. A direct sale costs supplier 1 an extra $c$ per unit, and $c$ may be negative: the direct channel can be more efficient than the reseller. With wholesale prices $w_1,w_2\ge0$ , the reseller earns $q_1(p_1-w_1)+q_2(p_2-w_2)$ , supplier 1 earns $y(p_d-c)+q_1w_1$ , and supplier 2 earns $q_2w_2$ .

The game has three stages:

the suppliers set $w_1$ and $w_2$ simultaneously, and neither observes the other's price;
the reseller, who sees both prices, orders $q_1$ and $q_2$ ;
supplier 1 observes $q_1$ , but not $q_2$ or $w_2$ , and chooses $y$ .

Supplier 1 holds a belief $w_2'$ about supplier 2's price. In stage III her quantity $y$ and her conjecture $q_2'$ of the reseller's order from supplier 2 are mutual best responses computed with $w_2'$ (Lemma 1). In an equilibrium (the paper's (4.7)–(4.16)), beliefs equal the actual prices. The reseller best-responds at every price pair, anticipating supplier 1's reaction. Neither supplier gains from a unilateral price change. After a deviation by supplier 2, supplier 1's belief stays where it was. This is not a subgame-perfect equilibrium, because supplier 1 cannot observe $w_2$ .

The paper restricts the direct cost to $c_0(\theta)<c<c_3(\theta)$ (p. 9). It identifies thresholds $c_0\le c_1\le c_2\le c_3$ (Table 2) that separate three regimes:

Direct Only ( $c\le c_1$ ) and Direct Only Boundary ( $c_1\le c\le c_2$ ), in which the reseller orders nothing from supplier 1;
Reseller & Direct ( $c>c_2$ ), in which supplier 1 uses both channels.

The sign of $c_2$ is that of

\mathrm{Num1}(\theta)=32-\theta\Big(80+\theta\big(32+\theta(14+\theta(8-(4-\theta)\theta))\big)\Big),

which has a unique root $\hat\theta\approx0.3443$ in $(0,1)$ .

Formalization targets

Goal: Proposition 5 (p. 22)

\exists\,\hat\theta\in(0,1),\ \mathrm{Num1}(\hat\theta)=0,\ \text{such that}

for $0<\theta<\hat\theta$ : $c_2(\theta)>0$ , and for every $c\in(0,c_2(\theta)]$ an equilibrium exists and every equilibrium has $q_1^*=0<y^*$ . Supplier 1 sells only directly, although her direct channel is less efficient;
for $\hat\theta<\theta<1$ : $c_2(\theta)<0$ . For $\hat\theta<\theta\le 9/10$ and every $c\in(c_2(\theta),0)$ there is an equilibrium with $q_1^*>0$ and $y^*>0$ . Supplier 1 sells through both channels, although her direct channel is more efficient.

Milestones

Lemma 1: the stage-III pair $(y^{III},q_2')$ , which is unique.
Lemma 2: the reseller's conditionally optimal $q_2^{III}$ .
Corollary 1: $q_2^{III}=q_2'$ when $w_2=w_2'$ .
Lemma 4: the threshold order $c_0\le c_1\le c_2\le c_3$ .
Lemma 4: for $c\le c_2$ , the Direct Only and Direct Only Boundary prices are equilibria, and every equilibrium has $q_1^*=0<y^*$ .
Lemma 4: the Reseller & Direct equilibrium for $c_2<c<0$ (stated for $\theta\le 9/10$ ).
The sign facts about $\mathrm{Num1}$ used in the proof of Proposition 5.

Significance

With an exclusive reseller, efficiency alone decides channel use: a costlier direct channel is used alongside the reseller, and a cheaper one replaces it. Proposition 5 shows that this rule fails once the reseller also carries a competitor.

When the products are weakly substitutable, supplier 1 may abandon the reseller although it is the cheaper channel. Supplier 2 then prices just low enough to keep her out.
When they are strongly substitutable, supplier 1 keeps selling through the reseller although her own channel is cheaper. The reseller's order shields her from supplier 2.

The result explains why observed channel structures need not reflect relative channel costs. It also shows which assumption of the exclusive model drives its conclusions.

As far as the mission's searches found, no part of this model has been machine-checked. The mission formalizes a game with unobservable prices and belief-based stage-III conjectures. Such games occur throughout the supply-chain contracting literature, and the equilibrium predicate here can be reused for them. The paper's proofs are algebraic, but they verify deviation incentives across a piecewise-defined reseller response, with polynomials of degree eight in $\theta$ . A formal proof has to check every branch.

Difficulty

The reseller's best response is piecewise in $q_1$ : supplier 1 sells directly only while $q_1$ is below a threshold, and her conjecture about $q_2$ can hit zero. The paper analyzes the reseller's choice under a restriction (Lemmas 1–3) that rules out the conjecture $q_2'=0$ for small $q_1$ , and argues that the excluded region cannot occur in equilibrium. Deviation prices, however, can push the reseller into that region. There the reseller's objective is not concave in $q_1$ , and supplier 1 may find a price cut that triggers a jump in the reseller's order. A proof of Lemma 4 cannot simply cite first-order conditions inside the restricted region: it has to rule out such jumps for every deviation price. Numerically this succeeds for $\theta\le 9/10$ , but it fails for $\theta$ close to $1$ .

The uniqueness claim in part (a) is a statement about every strategy profile, including the reseller's off-path rules. It cannot be obtained by exhibiting one profile. The equilibrium prices themselves are not unique for $c\le c_2$ , so this claim concerns the channel use $q_1^*=0<y^*$ only.

Formalization scope

Everything is real-valued and lives in NonExclEncroach.Channels. The conventions are:

the paper's case $\theta_{1d}=1$ (§4), hence $\theta_{2d}=\theta$ ; §5 ( $\theta_{1d}=0.8$ ) is out of scope;
the standing range $0<\theta<1$ and $c_0<c<c_3$ (p. 9), with $c$ allowed to be negative;
prices and quantities in $[0,\infty)$ ;
best responses as argmaxes over $[0,\infty)$ , with no tie-breaking rule;
a strategy profile made of the two prices, supplier 1's direct-quantity and conjecture rules as functions of the observed $q_1$ , and the reseller's order rule at every price pair. Supplier 1's belief is the equilibrium price of supplier 2 and does not move after supplier 2 deviates.

The goal quantifies over this equilibrium predicate. Stating Proposition 5 with the quantities read off Table 1, or as the sign of $c_2$ alone, would reduce it to the sign of $\mathrm{Num1}$ , and is ruled out.

Three statements depart from the page, and each departure is disclosed in its Formalization Note:

Part (b) of the goal and the Direct Only/Boundary part of Lemma 4 are stated for $\theta\le 9/10$ . The Reseller & Direct part of Lemma 4 is stated for $\theta\le 9/10$ and $c_2<c<0$ . A numerical solution of the game shows that the paper's equilibrium prices fail outside these ranges: for $\theta$ near $1$ , for $\theta\ge 0.85$ with $c>0.3$ , and just below $c_3$ (where supplier 2 gains by raising her price until the reseller shuts down the direct channel). The paper also announces that the Direct Only and Direct Only Boundary prices are the unique equilibrium prices for $c\le c_2$ . That is false: a lower $w_2$ , with $w_1$ at the reseller's threshold, can also be an equilibrium. Those prices are therefore stated as existence.
"There exist positive (negative) values of $c$ " is strengthened to every $c$ in $(0,c_2]$ (in $(c_2,0)$ ).
Lemma 2 assumes that the upper branch of (4.19) is non-negative.

Not formalized: Lemma 3, whose threshold $2c-1$ is correct only when $w_2=w_2'$ ; the appendix lemma eliminating equilibria with $q_2'=0$ ; and Propositions 1–4 and 6–8.

Contributions welcome: proofs of the milestones, a general existence theorem for the reseller's order rule, and an analysis of the game for $\theta$ near $1$ .

Selected references

P. Hotkar and S. M. Gilbert, Supplier Encroachment in a Non-Exclusive Reselling Channel, Management Science, 2021; SSRN working paper 3238502. https://ssrn.com/abstract=3238502 , https://doi.org/10.1287/mnsc.2020.3786
A. Arya, B. Mittendorf and D. E. M. Sappington, The Bright Side of Supplier Encroachment, Marketing Science 26(5), 2007. https://doi.org/10.1287/mksc.1070.0280
D. G. Pearce, Rationalizable Strategic Behavior and the Problem of Perfection, Econometrica 52(4), 1984. https://doi.org/10.2307/1911197
B. D. Bernheim, Rationalizable Strategic Behavior, Econometrica 52(4), 1984. https://doi.org/10.2307/1911196

9 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Optimal Short-Termism: The No-Underinvestment and No-Overhang Problems Have the Same Solutions, so Committing to Unlevered Long-Term Effort Rules Out Excessive Short-TermismResearch Paper

Motivation

Managers are often accused of short-termism: boosting current cash flow at the expense of long-run firm value. Hackbarth, Rivera and Wong (Management Science, 2022; working paper SSRN 3060869) study short-termism inside a dynamic-agency model of a levered firm. A risk-averse manager exerts two unobservable efforts: long-term effort $a$ , which raises the growth rate of firm size, and short-term effort $e$ , which raises current profitability. The firm issues perpetual debt with coupon $C$ , and shareholders choose the manager's incentive contract and the default time.

Debt distorts incentives through debt overhang (Myers, 1977): shareholders bear the cost of effort but share its benefits with bondholders, so they underinvest. The paper's question is whether debt also distorts the mix between short- and long-term effort, and whether that distortion is a separate agency cost or a consequence of underinvestment. Proposition 5 answers the second question: if shareholders commit to the long-term effort an unlevered firm would choose, they voluntarily choose the unlevered short-term effort too. Excessive short-termism is then an indirect cost of debt, transmitted only through long-term effort.

Setting

Firm size $\delta$ evolves as $d\delta_t=(\phi+a_t)\delta_t\,dt+\sigma_\delta\delta_t\,dZ^P_t$ and is absorbed at a lower boundary $\underline\delta>0$ . Profitability evolves as $dA_t=(\psi+e_t)\,dt+\sigma_A\,dZ^T_t$ , and the two shocks have correlation $\rho\in[-1,1]$ . Efforts lie in the effort box $a\in[0,\bar a]$ , $e\in[0,\bar e]$ . Effort costs $\tfrac12(\theta_aa^2+2\theta_{ae}ae+\theta_ee^2)\delta$ , where $\theta_{ae}$ may have either sign (complements or substitutes). Everyone discounts at $r>0$ , the manager has CARA coefficient $\gamma>0$ , and the corporate tax rate is $\tau\in(0,1)$ .

The paper reduces the shareholders' problem to an ODE for the equity value $f(\delta)$ . Write

H_C(\delta,a,e,f',f'')=\delta(\psi+e)-(1-\tau)C-\tfrac12(\theta_aa^2+2\theta_{ae}ae+\theta_ee^2)\delta+(\phi+a)\delta f'+\tfrac12\sigma_\delta^2\delta^2f''-\frac{\gamma r\delta^2}{2}\Sigma(a,e),

where $\Sigma(a,e)=(\theta_aa+\theta_{ae}e)^2\sigma_\delta^2+(\theta_ee+\theta_{ae}a)^2\sigma_A^2+2\rho(\theta_aa+\theta_{ae}e)(\theta_ee+\theta_{ae}a)\sigma_\delta\sigma_A$ is the manager's incentive-risk term. The levered HJB (18) is $rf(\delta)=\max_{(a,e)}H_C(\delta,a,e,f'(\delta),f''(\delta))$ . With $C=0$ it is the unlevered HJB (25). The unlevered value $f_u$ solves (25), has $f_u(0)=0$ , is twice continuously differentiable on $(0,\infty)$ , and has linear growth, as in Proposition 3. Its maximizers $(a_u(\delta),e_u(\delta))$ form the unlevered effort policy.

Two constrained problems compare commitment regimes. Both impose, at a default threshold $\delta_B$ , value matching $f(\delta_B)=0$ , smooth pasting $f'(\delta_B)=0$ , and transversality $f'(\delta)\to\psi/(r-\phi)$ as $\delta\to\infty$ .

No overhang (NO), (A.27): both efforts are fixed at the unlevered policy, $rf(\delta)=H_C(\delta,a_u(\delta),e_u(\delta),f'(\delta),f''(\delta))$ for $\delta>\delta_B$ .
No underinvestment (NU), (A.29): only long-term effort is fixed, and short-term effort is reoptimized: $rf(\delta)=\max_{e\in[0,\bar e]}H_C(\delta,a_u(\delta),e,f'(\delta),f''(\delta))$ for $\delta>\delta_B$ .

Formalization targets

Goal: Proposition 5

For every coupon $C$ , every unlevered value $f_u$ solving (25), every associated effort policy $(a_u,e_u)$ , every function $f$ and every threshold $\delta_B$ ,

(f,\delta_B)\text{ solves (NU)}\iff(f,\delta_B)\text{ solves (NO)}.

The unlevered value and its policy are hypotheses, matching the objects used in the paper's statement and proof.

Milestones

Condensed Hamiltonian (A.2.1). The identity

H_C=\delta\big(af'+e-\tfrac12a^2\hat A-\tfrac12e^2\hat D-ae\hat B\big)+\delta\psi-(1-\tau)C+\phi\delta f'+\tfrac12\sigma_\delta^2\delta^2f''

with the paper's $\hat A,\hat B,\hat D$ . 2. Section of the joint maximizer (A.4.2). For every slope $f_1$ , $e_u(\delta)$ maximizes $e\mapsto a_u(\delta)f_1+e-\tfrac12a_u(\delta)^2\hat A-\tfrac12e^2\hat D-a_u(\delta)e\hat B$ over $[0,\bar e]$ . 3. (A.26). For every $C$ and $f$ , the maximum over $e\in[0,\bar e]$ of $H_C(\delta,a_u(\delta),e,f'(\delta),f''(\delta))$ is attained at $e_u(\delta)$ , so the right-hand sides of (A.29) and (A.27) agree.

Significance

The result. Proposition 5, together with Proposition 4 (with independent effort costs, debt does not affect short-term effort), shows that debt affects the two efforts asymmetrically. Debt distorts long-term effort directly through underinvestment, and short-term effort only through its interaction with long-term effort in the cost and risk terms. A contract or covenant that pins down long-term effort therefore removes the short-termism distortion as well. The converse fails: committing to $e_u$ does not recover $a_u$ . The paper's calibration (§5) quantifies the value of these commitment regimes. Proposition 5 guarantees that two of them coincide, so the no-underinvestment numbers are also the no-overhang numbers.

Formalizing it. The result is proved in the paper, and no part of the model is formalized anywhere to our knowledge. This mission produces a machine-checked statement of the levered-firm HJB, the unlevered effort policy as a constrained maximizer, and the two commitment problems. It also gives a corrected version of the appendix display (A.26), which as printed omits a factor $\delta$ , the factor $e$ in one cross term, and contains a stray sign. These objects can be reused for later statements of the paper, such as Proposition 4 and the comparative statics of §4.4.

Difficulty

The proof has no analytic depth. The work is in the encoding, where the obvious readings fail in specific ways:

The appendix writes the unlevered maximizer as an unconstrained $\arg\max_{a,e}$ . Read literally, $e_u(\delta)$ could exceed $\bar e$ , and then the NU problem, which maximizes over $[0,\bar e]$ , would differ from NO. The box constraint of Definition 1 is what makes the statement true.
The unlevered policy is defined at the unlevered slope $f_u'(\delta)$ , but it is used at the levered slope $f'(\delta)$ . The step needs the observation that the slope enters the objective only through a term independent of $e$ . A statement of the section property at $f_u'$ only would not prove the goal.
The closed forms (26) and (A.23) for $(a_u,e_u)$ are valid only in the interior case and under a concavity assumption the paper leaves implicit. They must not serve as the definition of the policy.

Formalization scope

All quantities are real numbers. The parameters form a structure, and the standing assumptions of §2 ( $r>0$ , $\sigma_\delta,\sigma_A>0$ , $\rho\in[-1,1]$ , $\gamma>0$ , $\tau\in(0,1)$ , $\bar a,\bar e>0$ , $\underline\delta>0$ ) are one predicate. Its single added clause is $\phi<r$ , which the transversality limit $\psi/(r-\phi)$ presupposes. No concavity assumption and none of the paper's Conditions 1–2 are imposed.

Conventions committed to:

$f'$ and $f''$ are deriv f and deriv (deriv f), and $f$ is required to be $C^2$ on the open set $(\delta_B,\infty)$ .
The ODE is imposed for $\delta>\delta_B$ , with $\underline\delta\le\delta_B$ .
Smooth pasting is the right derivative at $\delta_B$ .
The threshold $\delta_B$ is a parameter shared by both problems.
Every "max" is IsGreatest of the image, so attainment is part of the statement.
The unlevered value solves (25) with the boundary, regularity and growth conditions of Proposition 3. Its policy is a pair of functions that, for $\delta\ge\underline\delta$ , lies in the effort box and maximizes the $C=0$ integrand over the box.

The trivializing encodings are ruled out: NU maximizes over $e\in[0,\bar e]$ , NO fixes $e=e_u(\delta)$ , and $(a_u,e_u)$ comes only from the unlevered maximization at $f_u'$ , never from a hypothesis about the levered integrand.

Not in scope: the continuous-time contracting results (Proposition 1, which needs martingale representation), the verification theorems (Propositions 2, 3, 6, 7, which rest on Strulovici–Szydlowski 2015), Proposition 4, Lemmas 1–2 and the calibration. Contributions are welcome on all three milestones and the goal. The model file is self-contained and depends only on Mathlib.

Selected references

D. Hackbarth, A. Rivera, T.-Y. Wong, Optimal Short-Termism, Management Science, 2022. https://doi.org/10.1287/mnsc.2021.4139 ; working paper ECGI Finance 546/2018, June 2021 version, https://ssrn.com/abstract=3060869 (the version cited by this mission).
S. C. Myers, Determinants of corporate borrowing, Journal of Financial Economics 5(2), 147–175, 1977. https://doi.org/10.1016/0304-405X(77)90015-0
H. E. Leland, Corporate debt value, bond covenants, and optimal capital structure, Journal of Finance 49(4), 1213–1252, 1994.
B. Strulovici, M. Szydlowski, On the smoothness of value functions and the existence of optimal strategies in diffusion models, Journal of Economic Theory 159, 1016–1055, 2015.

5 thms2 active usersReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

Contracting, Pricing, and Data Collection Under the AI Flywheel Effect: Under Moral Hazard the Firm Collects More (Less) Data Than First Best When the Data Impact Increases (Decreases)Research Paper

Motivation

Companies often sell a machine-learning product before its model has reached its final quality. Use of the product then yields data that can improve later versions. This feedback is the AI flywheel studied by Gurkan and de Véricourt. A firm may hire a specialist to develop the model, but the specialist's effort is costly and hidden. More customer data can then change both the product's future quality and the cost of inducing effort. The authors ask how that interaction changes the firm's price and data collection relative to a firm that develops the model itself. Their working paper reports that the direction depends on how the effect of effort varies with dataset size Gurkan and de Véricourt, 2021/2022.

The setting connects a pricing decision to an incentive decision. A lower price attracts more buyers and supplies more data for the next period, yet it also gives up current revenue. When a provider trains the model, the value of additional data depends on how data alter the provider's chance of producing a high-quality result under effort and under shirking. The theorem isolates that change through one ratio rather than requiring a particular parametric learning curve.

Setting

There are two periods and a unit mass of potential buyers in each. A buyer's sensitivity to algorithm accuracy is uniformly distributed on $[0,1]$ . The algorithm's accuracy is either $\alpha_h$ or $\alpha_\ell$ , where $0<\alpha_\ell<\alpha_h$ . Given a dataset of size $d$ , a provider who exerts effort produces high accuracy with probability $\pi_w(d)$ and pays cost $\kappa>0$ ; a provider who shirks produces it with the lower probability $\pi_s(d)$ and pays no effort cost. The firm observes accuracy and can condition payments on it, while effort itself is unobservable.

If the firm collects $\delta$ data at capacity $\nu>0$ , the buyer model gives period revenue

R_\nu(\delta,\alpha) =\alpha\frac{\delta}{\nu}\left(1-\frac{\delta}{\nu}\right), \qquad 0\le\delta\le\nu.

First-period sales add data to the initial dataset $d_0$ . When the first algorithm has low accuracy, the provider retrains it on $d_0+\delta_{1\ell}$ ; when accuracy is already high, no retraining is needed. The data impact

\rho(d)=\frac{\pi_w(d)-\pi_s(d)}{\pi_w(d)}

measures the relative effect of effort on the high-accuracy probability. The paper assumes $1/\rho$ is convex on the relevant data interval Gurkan and de Véricourt, §3.2.

The firm's contract selects four nonnegative payments, one for each accuracy outcome in each period, and two first-period data quantities, $\delta_{1h}$ and $\delta_{1\ell}$ . Its expected profit and two incentive constraints are Problem (6)–(9) in the working paper. The first-best benchmark fixes each payment at $\kappa$ and removes the incentive constraints. Write $\delta^*$ for the low-accuracy data quantity of an optimal contract and $\delta^{FB}$ for that of an optimal first-best plan.

Formalization targets

The main target is Theorem 1 of the working paper. For interior optimal prices, it compares the two global optima:

\begin{aligned} \rho\text{ constant} &\Longrightarrow \delta^*=\delta^{FB},\\ \rho\text{ strictly increasing} &\Longrightarrow \delta^*>\delta^{FB},\\ \rho\text{ strictly decreasing} &\Longrightarrow \delta^*<\delta^{FB}. \end{aligned}

Since price and purchased quantity move in opposite directions in this buyer model, collecting more data corresponds to charging less than the first-best price. The three cases cover equality, underpricing, and overpricing without fixing a learning-curve formula Gurkan and de Véricourt, Theorem 1.

The milestones follow the paper's stated results. Lemma 1 characterizes the last-period myopic quantity and revenue. Lemma 2 identifies the optimal accuracy-contingent payments when first-period data choices are fixed. Proposition 1 characterizes the unique optimal contract and its reduced data-choice objective; Proposition 2 gives the unique first-best plan and places its low-accuracy data quantity above the myopic quantity. Two claims in the proof of Theorem 1 record the weak comparison and the distinctness of interior optima under strict monotonicity.

Significance

The theorem specifies the direction of a distortion in a firm's choice of data collection. Its conclusion depends on the relative change in two learning curves, not merely on the fact that more data improve model accuracy. In the increasing-impact regime, the contracting firm collects more data than the first-best firm; in the decreasing-impact regime, it collects less. The result gives a qualitative comparison for pricing and data acquisition when algorithm development is outsourced Gurkan and de Véricourt, §4.2.

The result is proved in the source paper; the task here is to give its two-period model, contract constraints, and comparison a Lean proof. The definitions also provide a reusable small model of two-outcome, two-period moral hazard with limited liability. A complete development would let later statements about welfare, capacity, or alternative contracts reuse the same precise optimization problems. No existing platform definition matches this paper's model, and the draft theorem statements currently have compilation placeholders rather than machine-checked proofs.

Difficulty

The first obstacle is the contract itself. Payments in the second period affect the provider's expected continuation payoff and thereby the first-period incentive constraint, so choosing each period's payments independently does not describe Problem (6). The data choice changes the probability of later accuracy and the incentive cost at the same time. A direct comparison of the two full objective values does not determine whether $\delta^*$ lies above or below $\delta^{FB}$ ; the paper's comparison depends on how the data impact changes with $d$ . Strict inequalities also need interior optimal choices. At a boundary, two distinct objective functions can select the same endpoint even when $\rho$ is strictly monotone.

Formalization scope

The Lean development uses real-valued data sizes, payments, probabilities, and revenues. It represents the learning curves $\pi_w$ and $\pi_s$ as functions on $\mathbb R$ , with hypotheses restricted to $[d_{\min},d_{\max}]$ . Feasible data choices lie in $[0,\nu]$ , and $d_0+\nu\le d_{\max}$ keeps every evaluated learning-curve value inside the stated domain. The standard-uniform quantile is the identity on its support. The second-period value is the supremum of revenue over $[0,\nu]$ ; Lemma 1 supplies its attained maximum. Both contract and first-best optimality are global over their respective feasible sets.

The standing assumptions include positive effort cost and low accuracy, $0\le\pi_s(d)<\pi_w(d)<1$ , strictly increasing concave learning curves $\pi_w$ and $\pi_s$ , differentiability of both curves, and convexity of $1/\rho$ . Positive $\alpha_\ell$ and strict $\pi_w<1$ make the paper's uniqueness conclusions well posed. Differentiability is weaker than the twice-continuous differentiability mentioned in the source's later proofs. The paper's condition favoring effort in both periods motivates the chosen contracting problem; effort is already imposed by its two incentive constraints. Interiority of the optimal low-accuracy quantities is an explicit hypothesis of the comparison theorem, reflecting the paper's assumption that optimal prices neither cover nor exclude the entire market Gurkan and de Véricourt, §3.4 and EC.1.

The goal concerns optimal solutions of the full six-variable contract problem and the full first-best problem. Defining $\delta^*$ and $\delta^{FB}$ only as maximizers of the reduced one-variable objectives would omit the contract's incentive constraints. A complete proof needs real optimization on compact intervals, concavity and differentiability facts, and a precise account of the payment constraints. Contributions to those components and to the stated milestones fit this mission.

Selected references

Huseyin Gurkan and Francis de Véricourt, Contracting, Pricing and Data Collection under the AI Flywheel Effect, ESMT Working Paper 20-01 (R3), August 17, 2021; subsequently published in Management Science, 2022. DOI: 10.1287/mnsc.2022.4333. The theorem numbers and printed pages in this mission follow the working-paper PDF.

8 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Optimal Team Composition: Diversity to Foster Implicit Team Incentives: The Specialized–Diverse Wage Gap Falls Until Collusion Binds, Then Rises, and Diverse Teams Are Optimal Below S*(δ)Research Paper

Motivation

Firms decide not only how to pay workers but whom to put together. A long empirical and theoretical literature on teams asks whether homogeneous ("specialized") or heterogeneous ("diverse") teams perform better. Most arguments for diversity are informational: diverse teams bring different knowledge or perspectives. Glover and Kim (SSRN 3344922, published in Management Science 2021, doi:10.1287/mnsc.2020.3762) give an argument based on incentives instead. In a repeated relationship, teammates who can watch each other can enforce effort by threatening to punish a shirker (mutual monitoring). The same ability lets them coordinate against the principal (tacit collusion). Whether production efforts are complements or substitutes determines how strong each force is. The paper shows that diverse teams, whose efforts are complements, can be cheaper to motivate even when specialized teams are more productive. This mission formalizes the paper's main comparative-statics result about this trade-off.

The model belongs to the literature on implicit incentives in repeated teams, which studies relational contracting and mutual monitoring among agents (Arya, Fellingham and Glover 1997; Che and Yoo 2001). Its new element is that the team's technology depends on its composition.

Setting

A principal hires four agents for two tasks each period. Each task is done by a team of two agents. Each agent chooses effort $e \in \{0,1\}$ (shirk or work) at cost $ce$ , with $c > 0$ , and all parties share a discount factor $\delta \in [0,1]$ . A team of kind $k \in \{s, d\}$ (specialized or diverse) produces $S > 0$ with probability $f_k(n)$ when $n$ of its two members work, and $0$ otherwise. The agent receives a wage $w_k \ge 0$ on success and nothing on failure.

The standing assumptions are:

$0 < f_k(0) < f_k(1) < f_k(2) < 1$ for both technologies;
specialization is more productive: $f_s(2) > f_d(2)$ ;
A.1 $\frac{f_s(2)-f_s(0)}{f_s(2)-f_s(1)} > 2 > \frac{f_d(2)-f_d(0)}{f_d(2)-f_d(1)}$ : efforts are substitutes in specialized teams and complements in diverse teams;
A.2 $\frac{f_s(1)-f_s(0)}{f_s(2)-f_s(1)} < 2$ : the substitutability is weak;
A.3 $\frac{f_s(1)}{f_s(2)} > \frac{f_d(1)}{f_d(2)}$ .

The normalized punishment is $x_k = \frac{f_k(2)-f_k(0)}{f_k(2)-f_k(1)}$ . Two thresholds matter:

\delta^m = \frac{2f_s(1)-f_s(2)-f_s(0)}{f_s(1)-f_s(0)}, \qquad \delta^C = \sqrt{\frac{f_s(2)-f_s(1)}{f_s(1)-f_s(0)}}.

The principal's programs (Appendix A) minimize the wage subject to constraints:

A diverse wage must satisfy (IR) $f_d(2)w_d - c \ge 0$ and (M-IC) $f_d(2)w_d - c \ge (1-\delta)f_d(1)w_d + \delta f_d(0)w_d$ .
A specialized wage must satisfy (IR), and an (M-IC) constraint whose punishment is (shirk, shirk) for $\delta \ge \delta^m$ and (work, shirk) for $\delta < \delta^m$ .
To deter collusion it must also satisfy (No-cycling) $f_s(2)w_s - c \ge \frac{f_s(1)w_s - c}{1+\delta} + \delta\frac{f_s(1)w_s}{1+\delta}$ .

The least feasible wages are $w_d^*$ (diverse), $w_s^*$ (specialized, mutual monitoring only) and $w_s^{**}$ (specialized, collusion-proof). Expected wages are $E[w_k] = f_k(2)w_k$ . The principal's per-period payoffs are $V_s = 2f_s(2)S - 4E[w_s^{**}]$ and $V_d = 2f_d(2)S - 4E[w_d^*]$ . With $\Delta = f_s(2)-f_d(2)$ , the output threshold is

S^*(\delta) = \frac{2}{\Delta}\big(E[w_s^{**}] - E[w_d^*]\big).

Formalization targets

Goal: Proposition 2

Assume $\frac{f_s(0)}{f_s(2)} > \frac{f_d(0)}{f_d(2)}$ , and write $G(\delta) = E[w_s^{**}] - E[w_d^*]$ . Then

G \text{ is strictly decreasing on } [0,\delta^C], \qquad G \text{ is strictly increasing on } (\delta^C, 1],

V_d > V_s \text{ for } S < S^*(\delta), \qquad V_s \ge V_d \text{ for } S \ge S^*(\delta), \qquad \frac{\partial S^*(\delta)}{\partial\delta} > 0 \text{ for } \delta \in (\delta^C,1).

Milestones

In attack order:

Lemma 1, the closed forms of $w_d^*$ and $w_s^*$ , with $\delta^m \in (0,1)$ .
The stage-game punishment switch at $\delta^m$ (proof of Lemma 1).
The bounds $\delta^m < \tfrac12 < \tfrac{1}{\sqrt 2} < \delta^C < 1$ .
Lemma 3, $w_s^{**} = \frac{c}{f_s(2)-f_s(1)}\max\{1-\delta, \frac{1}{1+\delta(x_s-1)}, \frac{\delta}{1+\delta}\}$ .
The shapes of $E[w_d^*]$ and $E[w_s^{**}]$ in $\delta$ .
Proposition 1: absent collusion, the gap $E[w_s^*] - E[w_d^*]$ is positive and strictly decreasing.
Lemma 4, first sentence: $G > 0$ on $[0,1]$ .
The derivative $\partial E[w_s^{**}]/\partial\delta = \frac{f_s(2)c}{(1+\delta)^2(f_s(2)-f_s(1))}$ for $\delta > \delta^C$ .
Equation (2): $V_d > V_s \iff \Delta S < 2(E[w_s^{**}] - E[w_d^*])$ .

Significance

Proposition 2 says that patience affects the two compositions in opposite directions once collusion matters. As long as only mutual monitoring binds, more patience helps specialized teams more, because their larger normalized punishment $x_s$ is multiplied by $\delta$ . Beyond $\delta^C$ the specialized team must be paid to prevent its members from taking turns shirking, and this cost grows with $\delta$ . The threshold $S^*(\delta)$ below which diversity is optimal therefore rises with patience past $\delta^C$ . So the model predicts that long-lived teams with valuable but not too valuable output should be diverse, for incentive reasons alone.

The proofs in the paper are short calculations, and the proof of Proposition 1 compares the gap only at $\delta = 0$ , $\delta^m$ and $1$ . A machine-checked development certifies the closed forms of the three programs, the strict monotonicity on whole intervals (not only at sample points), and the derivative claim. To our knowledge none of these results has been formalized.

Difficulty

Each wage is a minimum over a feasible set defined by inequalities. The specialized (M-IC) constraint changes form at $\delta^m$ , and the (No-cycling) constraint takes over at $\delta^C$ . A solver must first identify the binding constraint on each region and show that the least element exists, which is Lemmas 1 and 3, before any monotonicity argument starts. The obvious approach, comparing the two closed forms termwise, fails on $[\delta^m, \delta^C]$ : there both expected wages decrease, and the claim is that the specialized one decreases faster. That requires the ratio condition $f_s(0)/f_s(2) > f_d(0)/f_d(2)$ together with A.1 and A.3, not just the sign of each derivative. Strictness at the kinks $\delta^m$ and $\delta^C$ , where the piecewise wage is not differentiable, also needs care.

Formalization scope

All quantities are real numbers. A technology is a structure Tech with fields f0 f1 f2. Assumptions A.1–A.3 are kept in the paper's ratio form inside Standing. The optimal wages are not defined by closed formulas. Every theorem about them takes arbitrary functions ws wd : ℝ → ℝ with the hypothesis that, for each $\delta \in [0,1]$ , ws δ and wd δ are the least elements (IsLeast) of the Appendix A feasible sets. Defining the wages by their closed forms would make Lemmas 1 and 3 hold by definition, and that trivializing formalization is ruled out. The specialized (M-IC) constraint is piecewise at $\delta^m$ , exactly as printed.

Conventions:

The failure payment is $0$ .
"Increasing in effort" is strict.
"Monotone" is read as strict (StrictAntiOn, StrictMonoOn).
The derivative clause uses deriv on the open interval $(\delta^C, 1)$ , so it also asserts differentiability.
At $S = S^*(\delta)$ the two compositions tie, and "specialized teams are optimal otherwise" is read weakly.
The hypothesis of Proposition 2, "the conditions ensuring $E[w_s^{**}] - E[w_d^*] > 0$ (characterized in Lemma 4)", is pinned down as Lemma 4's explicit condition $f_s(0)/f_s(2) > f_d(0)/f_d(2)$ .

Not formalized:

the crossing cases of Lemmas 2 and 4;
the second sentence of Lemma 3;
the argument that (No-cycling) is the only way to deter collusion (the programs are taken as given);
the extensions of §4 and Appendices C–D.

The development needs only real inequalities, maxima of finitely many functions, and one-variable calculus from Mathlib. Contributions are welcome at every milestone. Lemmas 1 and 3 are reusable by anyone working on further results of the paper.

Selected references

J. Glover and E. Kim, Optimal Team Composition: Diversity to Foster Implicit Team Incentives, SSRN working paper 3344922 (June 2020 version). https://ssrn.com/abstract=3344922 ; published in Management Science, 2021. https://doi.org/10.1287/mnsc.2020.3762
A. Arya, J. Fellingham and J. Glover, Teams, repeated tasks, and implicit incentives, Journal of Accounting and Economics 23(1), 7–30, 1997.
Y.-K. Che and S.-W. Yoo, Optimal Incentives for Teams, American Economic Review 91(3), 525–541, 2001. https://doi.org/10.1257/aer.91.3.525

12 thms2 active usersReviewed

Completed

Economics Machine Learning Operations Research·Captain: mikedeng1

“Un”Fair Machine Learning Algorithms: With Endogenous Learning Effort, Equal Treatment Accepts a Larger Share of the Protected Group's Good Candidates than Equal Opportunity in a Risky MarketResearch Paper

Motivation

Lenders, employers and insurers increasingly screen applicants with learned scores, and regulators and the fair machine learning literature ask that such screening be fair across demographic groups. Two notions are standard. Equal treatment (ET) asks that the same decision rule be applied to everyone, regardless of group; the paper notes that it is what the law currently requires. Equal opportunity (EO), proposed by Hardt, Price and Srebro (2016), asks instead that qualified applicants be accepted at the same rate in every group. EO is often presented as the notion that protects a disadvantaged group better, because it corrects for differences in how well the screening technology separates good from bad applicants in each group.

Most analyses of these notions take the classifier as given. Fu, Aseri, Singh and Srinivasan point out that a profit-maximizing firm also chooses how much to invest in learning, and that a fairness constraint changes that choice. Their Theorem 2 identifies a regime in which, once the firm's learning response is taken into account, EO accepts no larger a share of the protected group's qualified applicants than ET does. The result is a short, fully explicit comparative-statics statement about a parametric model, which makes it a natural target for formal verification.

Setting

A bank screens loan candidates from two groups of equal (unit) size: a protected group $p$ and a regular group $r$ . A good candidate repays and earns the bank $\alpha>0$ ; a bad candidate defaults and costs it $\beta>0$ . The proportions of bad candidates are $d_p$ and $d_r$ , with $0<d_r<d_p<1$ , and the expected profit and loss per group are

\alpha_p=\alpha(1-d_p),\quad \beta_p=\beta d_p,\quad \alpha_r=\alpha(1-d_r),\quad \beta_r=\beta d_r,

with the paper's assumption $\beta_r\ge\alpha_r$ (hence $\beta_p>\alpha_p$ ).

The bank chooses a learning effort $s\in[0,1/(2\gamma_r)]$ . In group $A\in\{p,r\}$ , scores of bad candidates are uniform on $[0,1-\gamma_A s]$ and scores of good candidates uniform on $[\gamma_A s,1]$ , where the learning rates satisfy $0<\gamma_p<\gamma_r$ : learning separates the regular group faster. The bank accepts a candidate of group $A$ whose score exceeds a threshold $c_A\in[0,1]$ , and pays the learning cost $\tau(s)=ks/(1-\gamma_r s)$ . Its profit $\pi(c_p,c_r,s)$ is equation (1) of the paper: expected profit from accepted good candidates minus expected loss from accepted bad candidates, summed over the two groups, minus $\tau(s)$ .

The coverage rate of group $A$ is the fraction of its good candidates that are accepted,

\phi_A=\min\Big\{\frac{1-c_A}{1-\gamma_A s},1\Big\}.

Under ET the bank must use $c_p=c_r$ ; under EO it must equalize the coverage rates, $\frac{1-c_r}{1-\gamma_r s}=\frac{1-c_p}{1-\gamma_p s}$ (equation (6)). Writing $(c^{C},s^{C})$ for the bank's optimal decision under constraint $C\in\{ET,EO\}$ , the quantity of interest is $\phi^{C}_p$ , the protected coverage rate at that optimum.

The paper focuses on the low-loss case $\beta_p\le\alpha_p+\alpha_r$ (case (1), p. 17) and on learning costs in a middle range: with

A=\alpha_p\gamma_r-\beta_p\gamma_r+\beta_p\gamma_p,\qquad \rho=\frac{1}{2-\gamma_p/\gamma_r},

it assumes $k=\alpha_r\gamma_r+\sigma^2A$ with $\sigma\in[\rho,1)$ , so that learning is neither so cheap that it separates perfectly nor so expensive that the market fails.

Formalization targets

Goal: Theorem 2 (p. 23)

Under the standing assumptions, the low-loss case and the cost range above, if

\frac{\alpha_p}{\beta_p}\le 1-\frac{1-(2-\sigma)^2\sigma^2}{(1-\sigma^2)(2-\sigma)^2}\cdot\frac{\gamma_p}{\gamma_r},

then for every optimal ET decision and every optimal EO decision

\phi^{ET}_p\ \ge\ \phi^{EO}_p .

Milestones

Threshold reductions (eqs. (4), (10), case (1), pp. 15–17). For each effort $s$ , the optimal ET threshold is $1-\gamma_r s$ and the optimal EO thresholds are $c_p=1-\gamma_r s(1-\gamma_p s)/(1-\gamma_r s)$ , $c_r=1-\gamma_r s$ ; the resulting profits are explicit functions $\pi_{ET}(s)$ and $\pi_{EO}(s)$ .
Unimodality (proof of Theorem 1, p. 43) of $\pi_{ET}$ and $\pi_{EO}$ on $[0,1/(2\gamma_r)]$ , and an interior optimum (p. 23): the optimal efforts exist, are positive, and $s^{EO}<1/(2\gamma_r)$ .
Closed forms (eqs. (51), (52), p. 44):

\phi^{ET}_p=\frac{\gamma_r}{\gamma_r-\gamma_p}\Big[1-\Big(\frac{k-\alpha_r\gamma_r}{A}\Big)^{1/2}\Big],\qquad \phi^{EO}_p=\frac{\gamma_r}{\gamma_r-\gamma_p}\Big[\Big(\frac{\beta_p\gamma_p}{k-\alpha_r\gamma_r+\beta_p\gamma_r-\alpha_p\gamma_r}\Big)^{1/2}-1\Big].

The difference in $\sigma$ (eqs. (53)–(54)) and the sufficient condition (eqs. (55)–(59), p. 45): under the hypothesis of Theorem 2, $\big(\beta_p\gamma_p/(\sigma^2\beta_p\gamma_p+(1-\sigma^2)(\beta_p\gamma_r-\alpha_p\gamma_r))\big)^{1/2}\le 2-\sigma$ .

Significance

Theorem 2 is the paper's main statement about the protected group. It says that a constraint designed to raise the protected group's acceptance of qualified applicants can fail to do so once the firm re-optimizes its investment in learning: when lending to the protected group is risky enough relative to its return, the EO-constrained firm learns less, and the protected group's coverage rate is no higher than under ET. The paper uses it, together with its Theorem 3 on success rates, to argue that the choice between fairness notions should account for endogenous learning, and it explains the condition's dependence on the learning-efficiency gap $\gamma_r-\gamma_p$ and the expected loss $\beta_p-\alpha_p$ .

The result is proved in the paper by first-order conditions and algebra. It has not been formalized. The formalization adds a machine-checked passage from the bank's joint optimization over thresholds and effort, with the piecewise-linear profit (1), to the closed-form comparison: the threshold reductions and the existence and location of the optimal efforts are asserted in the paper with little or no argument, and the mission makes each of them an explicit, checked statement.

Difficulty

The algebra of (53)–(59) is short. The work lies upstream of it. The profit (1) is a sum of min and max terms, and its maximization over thresholds must be carried out case by case on the positions of $c$ relative to the four breakpoints $\gamma_p s<\gamma_r s\le 1-\gamma_r s<1-\gamma_p s$ ; under EO the thresholds are further tied by constraint (6). The first-order conditions (47)–(48) identify the optimal efforts only once unimodality and interiority are established, and these hold only in the stated cost range: at its endpoint $\sigma=\rho$ the ET optimum sits exactly at the boundary $1/(2\gamma_r)$ . Substituting the closed forms (51)–(52) directly into the conclusion skips all of this and is not the theorem.

Formalization scope

Everything is real-valued and lives in the namespace UnfairML.Coverage. One definitions file holds the parameters (Params: $\alpha,\beta,d_p,d_r,\gamma_p,\gamma_r$ ), the derived quantities, the standing assumptions (Standing), the low-loss case (LowLoss), the cost $\tau$ , profit (1), the coverage rate, the EO constraint (6), the optimality predicates IsOptET and IsOptEO, the reduced profits $\pi_{ET},\pi_{EO}$ of case (1), and the cost range CostRange.

Conventions committed to:

effort ranges over the closed interval $[0,1/(2\gamma_r)]$ of Appendix A, not the half-open interval of §3.1 (on the half-open interval the ET problem has no optimum at $\sigma=\rho$ );
thresholds range over $[0,1]$ , and every optimality quantifier is restricted to these boxes, where all denominators $1-\gamma s$ are at least $1/2$ ;
$\alpha>0$ and $\beta>0$ are added to the paper's standing assumptions;
the goal quantifies over all optimal decisions of the joint problem, with the coverage rate read off the optimal threshold and effort;
two misprints are corrected and labelled: the unmatched parenthesis in Theorem 2's bound is read as $1-(2-\sigma)^2\sigma^2$ , as in (56), and the prefactor of (54) is $\gamma_r/(\gamma_r-\gamma_p)$ , as in (53).

A goal stated about maximizers of $\pi_{ET},\pi_{EO}$ , or with (51)–(52) substituted, would be a different and much weaker statement and is ruled out. The cost range is satisfiable only when $A>0$ ; a sorry-free check that all hypotheses of the goal hold together for an explicit rational instance accompanies the development.

No Mathlib extension is needed beyond real analysis on intervals (monotonicity from derivatives, IsMaxOn). Contributions are welcome at every milestone; the threshold reductions are self-contained piecewise-linear arguments and a natural starting point.

Selected references

R. Fu, M. Aseri, P. V. Singh, K. Srinivasan, “Un”Fair Machine Learning Algorithms, SSRN working paper 3408275 (version of 25 Mar 2021); published in Management Science. https://ssrn.com/abstract=3408275 , https://doi.org/10.1287/mnsc.2021.4065
M. Hardt, E. Price, N. Srebro, Equality of Opportunity in Supervised Learning, NeurIPS 2016. https://arxiv.org/abs/1610.02413

10 thms2 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

Prepositioning and Local Purchasing for Emergency Operations Under Budget, Demand, and Supply Uncertainty: Above a Budget Threshold, Optimal Prepo Stock Is the Newsvendor Fractile of Net DemandResearch Paper

Motivation

Humanitarian organizations (HOs) such as the Red Cross or UNICEF keep prepositioned stock ("prepo") of relief items in distribution centres, so that they can fly supplies to a disaster area in the first days after a rapid-onset event. A second source is local purchasing in or near the affected region after the disaster strikes: it is cheaper per unit and supports the local economy, but local supply is uncertain (a severe event can destroy it), and buying it requires cash that the HO may not have at the right moment. Budgets of HOs are tight and partly random: a fixed budget at the start of a cycle, a steady inflow of donations, and an emergency fund raised once a disaster is in the news.

Eftekhar, Song and Webster (SSRN 3210309; published in Manufacturing & Service Operations Management, 2021, doi:10.1287/msom.2020.0956) model the HO's choice of a prepo level under budget, demand and local-supply uncertainty. Their single-cycle result answers a practical question: when is the classical newsvendor rule (stock the critical fractile of demand) the right prepositioning policy, once local supply and budget constraints are taken into account?

Setting

A prepo cost cycle starts when the HO chooses a prepo level $x$ and ends after the relief period of the next disaster. The unit cost of prepo is normalized to $c=1$ . The parameters are a holding cost $i\ge0$ per dollar-period; a local supply cost multiple $0<\alpha<1$ ; a unit shortage cost $v>1$ ; an initial budget $b\ge0$ , with $x\le b$ ; and a funds inflow rate $\gamma\ge0$ .

On a probability space, the random time to the disaster $T$ , the relief demand $D$ , the local supply $Q$ and the emergency fund $R$ are nonnegative and integrable, and $T$ is independent of $(D,Q,R)$ ; $\mu_D=\mathbb E[D]$ , $\mu_T=\mathbb E[T]$ . When the disaster strikes, the money available for local spend is

\hat b(x,R,T)=b+\gamma T+R-x .

The HO buys locally first, $\min\{D,Q,\hat b/\alpha\}$ units, leaving the local shortage $S(x)=(D-\min\{Q,\hat b/\alpha\})^+$ ; prepo covers $\min\{x,S(x)\}$ and $(S(x)-x)^+$ is unmet. The expected cycle cost is

C(x)=\mathbb E\bigl[iTx+\alpha\min\{D,Q,\hat b/\alpha\}+\min\{x,S(x)\}+v(S(x)-x)^+\bigr],

and the HO solves $\Pi:\ \min_{0\le x\le b}C(x)$ . The auxiliary model relaxes the local budget constraint, replacing $\min\{Q,\hat b/\alpha\}$ by $Q$ :

C_a(x)=\alpha\mu_D+i\mu_Tx+(1-\alpha)\mathbb E[(D-Q)^+]+(v-1)\mathbb E[(D-Q-x)^+].

With $\beta^*=i\mu_T/(v-1)$ , the number $x_+=\bar F^{-1}_{D-Q}(\beta^*)$ is a $(1-\beta^*)$ -fractile of the net demand $D-Q$ , and the threshold budget is

\bar b=\max\{\alpha\min\{d,q\}-r:(d,q,r)\in\Omega\}-\gamma\underline T+(x_+)^+,

with $\Omega$ the support of $(D,Q,R)$ and $\underline T$ the lower end of the support of $T$ .

Formalization targets

Goal: Proposition 2(b), corrected reading

If $b\ge\bar b$ , then

\bar x^*=\min\{(x_+)^+,b\}\ \text{ minimizes } C \text{ and } C_a \text{ on } [0,b], \qquad\text{and}\qquad \bar x^*=(x_+)^+ \ \text{ when } \max\{\alpha\min\{d,q\}-r\}-\gamma\underline T\ge0 .

The paper prints " $x^*=\bar x^*=(\bar F^{-1}_{D-Q}(\beta^*))^+$ ". The last equality is false in a corner: if $\gamma=0$ and $R=\alpha D+1$ almost surely, then $\bar b=(x_+)^+-1$ , and any $b$ with $\bar b\le b<(x_+)^+$ makes $(x_+)^+$ infeasible. The goal states the printed equality under the extra condition, and the optimality of $\bar x^*$ under $b\ge\bar b$ alone.

Milestones

The cost identity of p. 7: $C(x)=\alpha\mu_D+i\mu_Tx+(1-\alpha)\mathbb E[S(x)]+(v-1)\mathbb E[(S(x)-x)^+]$ .
The relaxation of p. 9: $C_a(x)\le C(x)$ .
Eq. (4): $\bar x^*=\min\{(x_+)^+,b\}$ minimizes $C_a$ on $[0,b]$ .
The claim at (5): if $b\ge\bar b$ , then for $0\le x\le(x_+)^+$ , $x \le b$ , almost surely $\min\{D,Q\}\le\hat b/\alpha$ , hence $S(x)=(D-Q)^+$ .
The reduction of p. 10: if $b\ge\bar b$ , then $C=C_a$ on $[0,\min\{(x_+)^+,b\}]$ .
Proposition 1, first clause: $C$ is convex.

Significance

Proposition 2(b) says that a well-funded HO can plan prepositioning with a newsvendor rule on net demand $D-Q$ : the optimal shortage probability is $\beta^*=i\mu_T/(v-1)$ , set by holding cost, disaster frequency and shortage premium, and the budget matters only through the cap $b$ . Below the threshold, the same rule gives an upper bound on optimal prepo (Proposition 2(a)), so $\bar b$ separates the regime where the heuristic is exact from the one where it overstocks. The comparative statics of §4.2 and the dynamic policy of §5 build on this single-cycle analysis.

The paper's proofs are in an online supplement. This mission produces a machine-checked version of the threshold result without density assumptions, and with a corrected statement. No part of this model is formalized elsewhere: the platform's newsvendor results concern models without local supply, random budgets or a budget cap.

Difficulty

The cost $C$ couples three nonsmooth effects: the cap $\hat b/\alpha$ on local purchases, which depends on $x$ through the budget, the split of the shortage between prepo and unmet demand, and the expectation over a joint law with no density. The obvious argument, "above $\bar b$ the cap never binds, so $C=C_a$ and eq. (4) applies", proves only that $C$ and $C_a$ agree on $[0,\bar x^*]$ . For $x>(x_+)^+$ the cap can bind, so $C$ could in principle dip below $C(\bar x^*)$ to the right of $\bar x^*$ . Ruling this out needs the global inequality $C_a\le C$ . Eq. (4) itself is a newsvendor argument at a generalized fractile: $C_a$ is convex but not differentiable at atoms of $D-Q$ , and the case $\beta^*\ge1$ , where the inverse is $-\infty$ , must be handled.

Formalization scope

All quantities are real; expectations are Bochner integrals over a probability measure $\mu$ . The standing assumptions, bundled in Params.Standing and Env.Standing, are: $0<\alpha<1$ , $i\ge0$ , $v>1$ , $b\ge0$ , $\gamma\ge0$ ; $D,Q,R,T$ measurable, integrable and almost surely nonnegative; $T$ independent of $(D,Q,R)$ (stated on p. 6, unused by the statements). The conventions are:

$c=1$ (the paper's normalization), so the model has no $c$ .
The feasible set is $[0,b]$ : prepo is a quantity, and every solution formula of the paper carries $(\cdot)^+$ .
" $x^*=\bar x^*$ " is read as " $\bar x^*$ is a minimizer" (IsMinOn), since $C$ is convex but not strictly.
$x_+$ is the least number satisfying the fractile inequalities $\mathbb P(D-Q>x_+)\le\beta^*<\mathbb P(D-Q>y)$ for $y<x_+$ , or a surrogate $x_+\le0$ when $\beta^*\ge1$ ; it is not a closed-form infimum. When $\beta^*=0$ and $D-Q$ is unbounded above, the paper's $x_+$ is $+\infty$ and no real witness exists, so the statements are silent in that corner.
$b\ge\bar b$ is encoded as the existence of numbers $M$ , $T_{lo}$ with $\alpha\min\{D,Q\}-R\le M$ and $T\ge T_{lo}$ almost surely and $M-\gamma T_{lo}+(x_+)^+\le b$ . This is equivalent to $b\ge\bar b$ (take $M$ the maximum over the support and $T_{lo}=\underline T$ ; conversely $\bar b\le M-\gamma T_{lo}+(x_+)^+$ because $\gamma\ge0$ ), and it involves no supremum.
The densities $f_{DQR}$ , $f_T$ of the paper are dropped: every statement holds for arbitrary integrable nonnegative primitives, which is a generalization.

$C$ is defined as the expectation of the operational cost (the first line of the display on p. 7), and $C_a$ as the separate closed expression of p. 9; a formalization defining $C$ by its closed form, or $C$ as $C_a$ above the threshold, would make the milestones trivial and is excluded.

Not formalized: the second clause of Proposition 1 (it needs the densities and derivatives (2)–(3)), Proposition 2(a), (c)–(e), the comparative statics of §4.2 and the dynamic model of §5. The development needs only Mathlib's integration and independence API; the newsvendor lemma at a generalized fractile (milestone 3) is reusable for other newsvendor models. Proofs of any milestone are welcome, as are a proof of Proposition 2(a) from the same definitions.

Selected references

M. Eftekhar, J.-S. Song, S. Webster, Pre-Positioning and Local-Purchasing for Emergency Operations Under Budget and Supply Uncertainty, SSRN 3210309, revision of Aug. 13, 2020. https://ssrn.com/abstract=3210309
M. Eftekhar, J.-S. Song, S. Webster, Prepositioning and Local Purchasing for Emergency Operations Under Budget, Demand, and Supply Uncertainty, Manufacturing & Service Operations Management, 2021. https://doi.org/10.1287/msom.2020.0956
J.-S. Song, The Effect of Leadtime Uncertainty in a Simple Stochastic Inventory Model, Management Science 40, 603–613, 1994 (the newsvendor monotonicity the paper invokes on p. 9).

8 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Cover-Up of Vehicle Defects: The Role of Regulator Investigation Announcements: Harm and Signal-Reliability Thresholds Determine When the Manufacturer Covers Up Under the U.S. PolicyResearch Paper

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.

9 thms2 active usersReviewed

Completed

Operations Research Probability Statistics·Captain: mikedeng1

Evaluating Stochastic Seeding Strategies in Networks: The Hájek Estimator of the Difference Between Two Seeding Strategies Is Consistent and Asymptotically NormalResearch Paper

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.

7 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Asymmetric Reporting Timeliness and Informational Feedback: Timely Loss Recognition Raises the Speculator's Gains from Selling on Bad News and Widens the Trading RegionResearch Paper

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.

10 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Operational Strategies for Distributing Durable Goods in the Base of the Pyramid: At Low Ability to Pay and High Risk Aversion the Profit-Maximizing Allocation Yields the Lowest Consumer SurplusResearch Paper

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:

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

11 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Bundling for Flexibility and Variety: An Economic Model for Multiproducer Value Aggregation: The Producers' Output Game Has a Unique Equilibrium, Solved in Closed FormResearch Paper

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

(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}$ .
(4a)–(4c): a positive output is a best response if and only if it solves the first-order condition (4c).
(4e): (4c) yields a nonnegative output if and only if $c_i \le \gamma S(Q)/Q$ .
§3.3: in equilibrium, a producer is active if and only if $c_i < \gamma S(Q)/Q$ .
Proof step (i): the active producers form an initial segment of the cost order.
(5a)–(5c): summing (4c) over the first $k$ producers pins down the aggregate output in closed form.
Downward closedness: if $k \ge 2$ satisfies the condition of (2a), so does $k - 1$ , and $k = 1$ always does.
(6): at the aggregate (5c), the participation bound of the $k$ -th producer is condition (2a).
(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.

Each producer's profit, viewed as a function of its own output, must be shown concave, so that (4c) describes the best response exactly.
The all-zero profile must be ruled out separately, because there the revenue share is $0/0$ .
The active set of an arbitrary equilibrium must be shown to be an initial segment of the cost order.
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

12 thms2 active usersReviewed

Algorithmic Game Theory Control Theory Operations Research+2·Captain: mikedeng1

Nonzero-Sum Stochastic Games and Mean-Field Games with Impulse Controls: A Regular Solution of the N-Player Quasi-Variational Inequalities Gives a Nash EquilibriumResearch Paper

Why this game matters

An impulse control changes a system's state at a chosen instant, rather than continuously adjusting its drift. When several decision makers can intervene in the same state process, an intervention changes both the acting player's future cost and every opponent's. This makes the equilibrium question different from separate single-player control problems. Basei, Cao and Guo formulate a multidimensional, $N$ -player stochastic impulse game and give a verification theorem for Nash equilibria in their preprint. This mission formalizes that theorem, Theorem 2.12, and the path and QVI statements on which its proof depends. It is the cost-minimizing, $N$ -player generalization of the two-player impulse game of Aïd et al., posed independently because the conventions and equilibrium inequalities differ; that two-player verification theorem is itself an open target on the platform.

Game and costs

There are $N\ge1$ players and a state $X$ in a nonempty open domain $S\subseteq\mathbb R^d$ . Between interventions the state follows an Itô diffusion with drift $b$ , volatility $\sigma$ , and an $M$ -dimensional Brownian driver. Player $i$ chooses a strategy $(A_i,\xi_i)$ : a closed action region $A_i$ and a continuous impulse rule $\xi_i:S\to Z_i$ . When the state enters $A_i$ , that player shifts it from $y$ to $\Gamma^i(y,\xi_i(y))$ . The process stops at its exit time $\tau_S$ from $S$ . The action regions of an admissible profile are pairwise disjoint, although consecutive interventions at one instant can still occur when an impulse lands in another player's region. These rules are given in Definitions 2.1, 2.2 and 2.7 of the source.

Every player minimizes cost. Player $i$ pays a discounted running cost $f_i$ , an own-intervention cost $\phi_i$ , a cross cost $\psi_{i,j}$ when player $j\ne i$ intervenes, and terminal cost $h_i$ if the game exits. With $\tau_{i,k}$ and $\xi_{i,k}$ denoting player $i$ 's intervention times and impulses, the expected cost is

J^i(x;\varphi)=\mathbb E_x\!\left[\int_0^{\tau_S}e^{-\rho_i s}f_i(X_s)\,ds+\sum_{\tau_{i,k}<\tau_S}e^{-\rho_i\tau_{i,k}}\phi_i(X_{(\tau_{i,k})-},\xi_{i,k})+\sum_{j\ne i}\sum_{\tau_{j,k}<\tau_S}e^{-\rho_i\tau_{j,k}}\psi_{i,j}(X_{(\tau_{j,k})-},\xi_{j,k})+\mathbf1_{\{\tau_S<\infty\}}e^{-\rho_i\tau_S}h_i(X_{\tau_S})\right].

An admissible profile satisfies the source's integrability, moment and nonaccumulation conditions. A Nash equilibrium is an admissible profile for which no player can lower their own cost through an admissible unilateral change Definitions 2.6–2.8.

Formalization targets

For candidate values $V_i$ and minimizing impulses $\xi_i$ , define the own intervention operator $\mathcal M_iV_i(y)=V_i(\Gamma^i(y,\xi_i(y)))+\phi_i(y,\xi_i(y))$ and the cross intervention operator $\mathcal H_{i,j}V_i(y)=V_i(\Gamma^j(y,\xi_j(y)))+\psi_{i,j}(y,\xi_j(y))$ . Put $D_i=\{y\in S:\mathcal M_iV_i(y)-V_i(y)>0\}$ , $A_i^*=\{y\in S:\mathcal M_iV_i(y)-V_i(y)=0\}$ , and $W_i=S\cap\bigcap_{j\ne i}D_j$ . The QVI system requires a boundary limit $V_i\to h_i$ , nonnegative own intervention gaps, zero cross gaps when an opponent acts, and the diffusion condition

\min\{\mathcal LV_i(y)-\rho_iV_i(y)+f_i(y),\ \mathcal M_iV_i(y)-V_i(y)\}=0 \qquad(y\in W_i\setminus\partial D_i).

Here $\mathcal L$ is the generator of the diffusion with the same $b$ and $\sigma$ equations (2.10)–(2.13).

The goal, Theorem 2.12, says that if every $\xi_i$ uniquely minimizes the own intervention expression, the $V_i$ solve the full QVI system and have the stated smoothness and boundary regularity, and $\varphi^*=((A_i^*,\xi_i))_i$ is admissible at $x$ , then (with one added hypothesis, explained under Formalization scope)

\varphi^*\text{ is a Nash equilibrium},\qquad V_i(x)=J^i(x;\varphi^*)\quad\text{for every }i.

The milestone list follows the proof's path: the controlled-process representation and jumps in Lemma 2.3; the candidate opponents' waiting and intervention properties in (2.15); the smooth approximations $V_{i,m}$ of (a)–(c), which the paper takes from Øksendal, proof of Thm. 10.4.1 and App. D; the three pointwise comparisons (2.19)–(2.21), a thin bridge from the QVI to the proof; the deviation bound in Step 1; and the value identity in Step 2. The localized Itô identity (2.18) is not a separate milestone: as printed, its expectation is not shown to be finite near the boundary of $W_i$ , and with simultaneous interventions its jump terms must be read stage by stage, so a faithful statement needs choices the page does not make. It remains the natural intermediate target between (a)–(c) and Step 1.

What the result provides

The theorem turns a regular solution of a coupled, nonlocal QVI system into a certificate for an equilibrium and its expected costs. It supplies the bridge from analytic candidate value functions to the original stochastic game. The result is proved in the preprint; the Lean declarations here are open statements, so the remaining work is a machine-checked development of the path construction, Itô formula across interventions, approximation near action boundaries and limiting arguments. The stochastic basis and diffusion generator reused here are published definitions from the two-player development, while the $N$ -player game and its minimizing QVI are new reusable interfaces.

Main obstacles

Applying a smooth Itô formula directly to $V_i(X_t)$ fails because $X$ jumps at interventions and $V_i$ is only $C^1$ across $\partial D_i$ . The source therefore uses smooth approximations and localizes before taking limits Theorem 2.12, proof. The analytic challenge is to control the generator of the approximants near a Lipschitz surface; the probabilistic challenge is to justify the expectation and the limits from the exact admissibility conditions. Treating the QVI as an inequality everywhere in $S$ would impose a generator value where the second derivative need not exist.

Formalization scope

Lean represents the state as a Euclidean space, players as Fin N with $N\ge1$ , costs and values as real numbers, and times as $[0,\infty]$ . The published SolvesFrom predicate encodes the restarted SDE through a Brownian Itô integral; the filtration satisfies the usual conditions and supports an $\mathcal F$ -Brownian motion. The source names the Brownian natural filtration, so this is a disclosed generalization. An admissible realization is a family of diffusion pieces solving that same SDE. Membership in $\Phi_x$ asks for at least one realization, while cost identities and Nash comparisons cover every admissible realization. The expected cost includes an integrability requirement, and admissibility asks that the running-cost integrand be integrable in time along almost every path, which is how "provided that the right-hand side exists and is finite" (Definition 2.6) is read. This prevents Lean's integral default on a nonintegrable payoff from making the theorem empty.

$S$ is open: the page calls it "a non-empty subset", but p. 9 says that $V_i$ "is not defined in $\partial S$ ", which is openness, and the $C^2$ condition (ii) and the generator in (2.13d) need an open domain. One hypothesis is added to Theorem 2.12, Step 1 and Step 2: along every admissible deviation, the time the state spends on $\partial D_i$ has Lebesgue measure zero almost surely. This is the occupation-time hypothesis of Øksendal's Theorem 10.4.1, the result whose proof the paper cites for (a)–(c); the passage from (2.17) to (2.18) uses it, because (c) controls $\mathcal LV_{i,m}$ only off $\partial D_i$ . The page omits it, and the theorem fails without it when $\sigma$ is degenerate: a path can run along $\partial D_i$ , where (2.13d) imposes nothing on $f_i$ . For a nondegenerate diffusion the hypothesis holds automatically. In (a)–(c), $W_i$ is assumed open, as the page's $C^2(\cap_{j\ne i}\mathcal D_j)$ presupposes; in the proof it is open because $S$ is open and the $A_j^*$ are closed.

The path construction uses entry into closed action regions, choosing the least index when multiple entry times agree; exit from $S$ uses the next stage's exit time. Discount at infinite time is zero. The path norm in the moment condition is taken through $\tau_S$ , because a process continued beyond game exit could have an infinite global supremum and make $\Phi_x$ empty. Cross costs use player $j$ 's intervention time. Boundary data in (2.13a) are limits from within $S$ ; the generator equation and derivative bounds are required where the derivatives exist, off $\partial D_i$ . The common waiting region includes $S$ , so it remains $S$ for one player. Action regions are built from $V_i$ and $\xi_i$ , not free variables. The source's printed formulas also call scalar costs vector valued and state some jump identities without accounting for consecutive interventions; the definitions and Lemma 2.3 follow the operational readings described in the item notes. In Lemma 2.3 the avoidance of the action regions is stated at positive times, since the initial state may lie in an action region without an intervention at time $0$ . A statement that drops the QVI clauses, fixes one realization for the conclusion, restricts the deviations, or reads (2.8) as a supremum over all times (which makes $\Phi_x$ empty for bounded $S$ ) would trivialize the goal and is ruled out by the definitions.

The definitions of the N-player path, admissibility, cost and QVI are intended for reuse. Contributions that establish the localized Itô identity, smooth approximation and dominated-convergence steps are especially useful. Every proposed proof must preserve the full QVI system, all admissible unilateral deviations, and the source's standing assumptions.

Selected references

M. Basei, H. Cao and X. Guo, Nonzero-sum stochastic games and mean-field games with impulse controls, arXiv:1901.08085v4, 2020. https://arxiv.org/abs/1901.08085v4
B. Øksendal, Stochastic Differential Equations, 6th ed., Springer, 2003 (Theorem 10.4.1 and Appendix D). https://doi.org/10.1007/978-3-642-14394-6
R. Aïd et al., Nonzero-Sum Stochastic Differential Games with Impulse Controls: A Verification Theorem with Applications, Mathematics of Operations Research 45(1), 2020. https://doi.org/10.1287/moor.2019.0982

11 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Risk, Ambiguity, and the Value of Diversification: Increasing or Constant Absolute Ambiguity Aversion Lowers the Smooth-Model Value of Diversification Below Its Ambiguity-Neutral LevelResearch Paper

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

The closed form $VD_{risk}=p(1-p)\big[2u(W_0-\tfrac L2)-u(W_0-L)-u(W_0)\big]$ , (A.1).
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.
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).
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$ .
If $p_1=1-p_2$ then $\Delta(1)=\Delta(2)$ .
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$ .
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

9 thms2 active usersReviewed

Economics Operations Research Probability·Captain: mikedeng1

A General Analysis of Sequential Social Learning: Asymptotic Learning Holds for Every Utility Function if and only if Private Signals Are Totally UnboundedResearch Paper

Motivation

In sequential social learning, agents act one after another. Each agent observes the actions of its predecessors and a private signal about an unknown state of the world. The model explains herd behaviour, information cascades and the adoption of products, technologies and opinions when people imitate one another. The basic question is whether the population eventually acts as if it knew the state, or whether public information can lock agents into a wrong action.

The answer depends on the setting:

Bikhchandani, Hirshleifer and Welch (1992) and Banerjee (1992) showed that with finitely many signals agents eventually ignore their private information and may herd on a wrong action.
Smith and Sorensen (2000) characterized learning for binary states and actions: asymptotic learning holds if and only if private beliefs are unbounded, meaning a single signal can make an agent arbitrarily sure of either state.
Arieli and Mueller-Frank (preprint SSRN 2466903, 2019; Mathematics of Operations Research, 2021) treat general state spaces, compact action spaces and all bounded utilities that are continuous in the action. They characterize when learning holds for every such utility.

Setting

A social learning model $(\Omega,\mu,A,S,F)$ consists of the following:

a separable complete metric state space $\Omega$ with a prior $\mu$ ;
a compact metric action space $A$ with at least two actions;
a standard Borel signal space $S$ ;
a Markov kernel $F:\Omega\to\Delta(S)$ , $\omega\mapsto F_\omega$ . Any two $F_\omega, F_{\omega'}$ are mutually absolutely continuous, and distinct states have distinct signal laws.

A state $\omega\sim\mu$ is drawn once. Agents $t=0,1,2,\dots$ act in sequence. Agent $t$ observes the history $h_t=(a_0,\dots,a_{t-1})$ and a private signal $s_t\sim F_\omega$ , drawn conditionally i.i.d. given $\omega$ . It then chooses an action by a mixed strategy $\sigma_t(h_t,s_t)\in\Delta(A)$ . All agents share a utility $u$ from the class $U$ of bounded measurable functions $A\times\Omega\to\mathbb R$ that are continuous in the action. The profile $\sigma$ , the prior and the kernel determine the play measure $P_\sigma$ on states, signals and actions.

A profile is a perfect Bayesian equilibrium (PBE) if no agent can raise its expected utility $E_\sigma[u(a_t,\omega)]$ by changing its own strategy. Write $O(\omega)=\max_a u(a,\omega)$ and $y_t=u(a_t,\omega)$ .

Asymptotic learning holds for $u$ if $y_t\to O(\omega)$ $P_\sigma$ -almost surely in every PBE.
Adequate learning holds if asymptotic learning holds for every $u\in U$ .

Let $\mu F(E\mid s)$ be the posterior probability of an event $E\subseteq\Omega$ after one signal $s$ . The information structure has totally unbounded signals if the support of the law of $\mu F(E\mid s)$ contains both $0$ and $1$ for every event $E$ with $0<\mu(E)<1$ .

Formalization targets

Goal: Theorem 1

\text{adequate learning holds}\iff (F,\mu)\text{ features totally unbounded signals.}

The statement is an equivalence between two properties of the model. It has no constants.

Milestones

The milestones are the results the paper's proof uses, in attack order:

Lemma 3. A utility in $U$ is jointly uniformly continuous on a compact set of measure at least $1-\varepsilon$ .
Lemma 4. A single agent observing two signals has an $\varepsilon$ -optimal strategy that takes finitely many actions and is constant on the cells of a finite product partition.
Lemma 1. The vanishing value of private information: $d_t=E_\sigma[y_t-\hat y_t\mid h_t]\to0$ almost surely in every PBE, where $\hat y_t=\max_a E_\sigma[u(a,\omega)\mid h_t]$ .
Lemma 2. The belief at infinity $\mu_\infty(\cdot\mid h)$ is almost surely a degenerate prior: one more signal has zero value against it.
Lemma 5 (first part). Total unboundedness passes from $\mu$ to every $\nu\ll\mu$ with $d\nu/d\mu\le C$ .
Lemma 7. Conditioning $\mathbf P\in\Delta(\Delta(\Omega))$ on a set $K$ gives a barycenter whose density with respect to $\tilde{\mathbf P}$ is at most $1/\mathbf P(K)$ .
Lemma 8. If learning fails with probability above $r'$ , there is a set $B$ with $\mu(B)>0$ on which the failure persists, and every belief concentrated near $B$ acts almost optimally on $B$ .
Necessity. Without totally unbounded signals, some $u\in U$ has no asymptotic learning.

Significance

Theorem 1 separates two questions. Whether learning succeeds for a particular utility depends on the utility, and for finite actions the paper gives weaker sufficient conditions (its Theorems 2 and 3). Whether learning succeeds for every utility depends on the information structure alone, and total unboundedness is exactly the condition. The theorem extends Smith and Sorensen's binary characterization to arbitrary separable complete metric state spaces. It also shows that their convex-hull condition does not carry over to more states. Lemma 1, the vanishing value of private information, holds in every sequential social learning game and is a reusable tool beyond this paper.

The results are proved on paper. To our knowledge none of them has a machine-checked proof. Formalizing them requires:

the equilibrium play measure, built by the Ionescu-Tulcea theorem;
martingale convergence of public beliefs;
a regular-conditional-probability treatment of beliefs over general Polish state spaces.

The paper's proofs pass over some of this measure theory, for example the measurability of best replies and of the maximal posterior payoff. A formal proof has to supply it.

Difficulty

Necessity is a direct construction. The difficulty is sufficiency. The natural first idea is to copy the binary argument: the public belief is a martingale, so it converges, and at a limit belief in the interior of the simplex unbounded signals would give private information positive value. With a general state space and a general utility this breaks in two places:

the limit belief $\mu_\infty$ is a random measure on $\Omega$ , not a number in $(0,1)$ ;
"positive value of a signal" has to hold uniformly over agents who face different histories.

The paper handles this with three ingredients:

Lemma 2, whose proof needs an imitation argument through Lemma 4's finite discretization;
Lemma 8, which localizes the failure of learning to a small set $B$ ;
Lemmas 5 and 7, which transfer total unboundedness from the prior to an averaged limit belief.

Each step uses facts about conditional distributions that hold only almost everywhere.

Formalization scope

Everything is in the namespace SeqSocialLearning.Adequate on top of Mathlib. The conventions are:

Agents are indexed from $0$ : Lean's agent $t$ is the paper's agent $t+1$ and sees Fin t → A.
Strategies are Markov kernels Kernel ((Fin t → A) × S) A, so they are mixed, as on p. 4. Restricting to pure strategies would change the equilibrium set.
The play measure $P_\sigma$ is constructed with Kernel.trajMeasure on trajectories of triples $(\omega,s_t,a_t)$ . The state is copied into every coordinate.
PBE is the paper's ex-ante definition: no profitable unilateral measurable deviation. No off-path optimality is imposed.
Posteriors use Mathlib's posterior and condDistrib. "The support contains $0$ and $1$ " is stated in the equivalent $\varepsilon$ -form.
Degeneracy of a prior is the equality of the one-signal decision value with the no-signal value.
Lemma 8's $\min_{\omega'\in B}$ is an infimum.
Lemma 4's product partition is a grid given by two finite measurable maps.
Nonempty Ω appears as a hypothesis; it follows from $\mu$ being a probability measure.

Two formalizations would make the goal trivial, and both are excluded:

quantifying total unboundedness over all events, including those of prior probability $0$ or $1$ , would make it always false;
positing the play measure by a predicate instead of constructing it would let it be arbitrary.

Contributions are welcome on two kinds of work:

reusable infrastructure: measurable selection of best replies on compact action spaces, martingale convergence of condDistrib along a filtration, and the identification of the play measure's marginals;
the proofs of the eight milestones and of the goal.

Theorems 2 and 3 (finite actions), Lemma 6, the second part of Lemma 5 and Example 1 are not part of this mission.

Selected references

I. Arieli and M. Mueller-Frank, A General Analysis of Sequential Social Learning, SSRN 2466903 (version of February 21, 2019); Mathematics of Operations Research, 2021. https://doi.org/10.1287/moor.2020.1093 — https://ssrn.com/abstract=2466903
L. Smith and P. Sørensen, Pathological Outcomes of Observational Learning, Econometrica 68(2), 2000. https://doi.org/10.1111/1468-0262.00113
S. Bikhchandani, D. Hirshleifer and I. Welch, A Theory of Fads, Fashion, Custom, and Cultural Change as Informational Cascades, Journal of Political Economy 100(5), 1992. https://doi.org/10.1086/261849
A. V. Banerjee, A Simple Model of Herd Behavior, Quarterly Journal of Economics 107(3), 1992. https://doi.org/10.2307/2118364
D. Rosenberg, E. Solan and N. Vieille, Informational Externalities and Emergence of Consensus, Games and Economic Behavior 66(2), 2009. https://doi.org/10.1016/j.geb.2008.07.007

13 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Service Design for a Holistic Customer Experience: A Process Framework: Step Types and the Inverse Correlation Matrix Decide Whether Optimal Step Efforts Are Complementary or SubstitutableResearch Paper

Motivation

A medical visit, a hotel stay or a bank onboarding is not one transaction but a service process: a sequence of steps (check-in, waiting, examination, payment), each delivered by the provider and each experienced by the customer. Practitioners design such processes with descriptive tools such as customer-journey maps and service blueprints, which list the steps and their touchpoints but do not say how much effort each step deserves. Two features make this allocation non-obvious. First, customers judge the experience as a whole, and the experiences at different steps are correlated: a long wait colours the examination that follows. Second, effort changes not only the average quality of a step but also its variability, and the direction depends on the step: at a routine step (check-in) more effort makes the outcome more predictable, while at a non-routine step (a diagnostic procedure) it may make it less so.

Bellos and Kavadias (Management Science, 2020) give a model in which the optimal effort per step has a closed form, and characterise when the efforts at two steps move together (are complementary) or in opposite directions (are substitutable) in response to a change in one step's characteristics. The answer depends on the two step types and on one entry of the inverse of the correlation matrix, not on the correlation itself. This mission formalizes that characterisation.

Setting

There are $n$ steps $i \in \mathcal J = \{1,\dots,n\}$ . The provider chooses an effort $\delta_i \in [0,1]$ at every step and one price $\pi$ .

Functional value. Step $i$ delivers $V_i = \delta_i V^H_i + (1-\delta_i)V^L_i$ with $V^H_i > V^L_i \ge 0$ . Steps reinforce each other through technical couplings $\beta_{j,i} \in [0,1)$ ( $j \ne i$ ), $\beta_{i,i} = 1$ , $\sum_{i\ne j}\beta_{j,i} < 1$ , and the functional value at step $i$ is $\mathcal V_i = \sum_j \beta_{j,i}V_j$ .
Variability. The experiential value at step $i$ has standard deviation $\sigma_i = \delta_i\sigma^H_i + (1-\delta_i)\sigma^L_i$ with $\sigma^H_i, \sigma^L_i \ge 0$ . The step is routine if $\sigma^H_i < \sigma^L_i$ and non-routine if $\sigma^H_i > \sigma^L_i$ .
Correlation. The experiences at steps $i$ and $j$ have correlation $\rho_{i,j} \in (-1,1)$ , collected in a symmetric positive definite correlation matrix $\mathbf P$ with unit diagonal.
Utility. Customers with risk aversion $r > 0$ obtain the mean-variance net utility

\mathcal U(\delta,\pi) = \sum_{i=1}^n \mathcal V_i - \frac r2\Big(\sum_{i=1}^n\sigma_i^2 + 2\sum\sum_{i<j}\rho_{i,j}\sigma_i\sigma_j\Big) - \pi.

Design problem. With unit costs $c_i \in (\sum_{j\ne i}\beta_{j,i}, 1)$ and a reservation profit $\pi_0 \ge 0$ , the provider maximizes $\mathcal U(\delta,\pi)$ subject to $\pi - \sum_i V_ic_i \ge \pi_0$ and $0 \le \delta_i \le 1$ . An optimal effort $\delta^*$ is the effort of an optimal design.

The paper's analysis assumes that each $V^H_i - V^L_i$ lies in an explicit interval $(\underline{\Delta V}_i, \overline{\Delta V}_i)$ built from the other parameters, the cofactors of $\mathbf P$ and $|\mathbf P|$ (the interior condition), and for its comparative statics it sets the technical couplings between distinct steps to zero.

Formalization targets

Goal: Proposition 3

Fix a step $i$ . Under the interior condition and without technical coupling, the effort at step $i$ satisfies

\frac{\partial\delta^*_i}{\partial c_i} < 0,\qquad \frac{\partial\delta^*_i}{\partial V^H_i} > 0,\qquad \operatorname{sgn}\frac{\partial\delta^*_i}{\partial\sigma^H_i} = -\operatorname{sgn}(\sigma^H_i - \sigma^L_i),

and for every $j \ne i$ the effort at step $j$ responds to $c_i$ , $V^H_i$ and $\sigma^H_i$ in the same directions if and only if

\Big(\operatorname{sgn}[\sigma^H_i-\sigma^L_i] = \operatorname{sgn}[\sigma^H_j-\sigma^L_j] \text{ and } [\mathbf P^{-1}]_{i,j} > 0\Big) \text{ or } \Big(\operatorname{sgn}[\sigma^H_i-\sigma^L_i] \ne \operatorname{sgn}[\sigma^H_j-\sigma^L_j] \text{ and } [\mathbf P^{-1}]_{i,j} < 0\Big),

and in the opposite directions otherwise (when $[\mathbf P^{-1}]_{i,j} \ne 0$ ). The derivatives are of the optimizer of the design problem, in one parameter at a time.

Milestones

For a given effort the optimal price is $\tilde\pi(\delta) = \pi_0 + \sum_i V_ic_i$ , so the problem reduces to maximizing $\tilde{\mathcal U}(\delta) = \mathcal U(\delta,\tilde\pi(\delta))$ over $[0,1]^n$ .
The Hessian of $\tilde{\mathcal U}$ has entries $-r(\sigma^H_i-\sigma^L_i)(\sigma^H_j-\sigma^L_j)\rho_{i,j}$ and leading minors $|\boldsymbol H_k| = (-1)^kr^k\prod_{j\le k}(\sigma^H_j-\sigma^L_j)^2|\mathbf P[1:k;1:k]|$ ; $\tilde{\mathcal U}$ is strictly concave.
The gradient of $\tilde{\mathcal U}$ , and the unique solution $\hat\delta$ of the first-order conditions.
The slope $\partial\hat\delta_i/\partial(V^H_i-V^L_i) > 0$ and the thresholds: $\hat\delta_i \le 0$ iff $V^H_i - V^L_i \le \underline{\Delta V}_i$ , $\hat\delta_i \ge 1$ iff $V^H_i - V^L_i \ge \overline{\Delta V}_i$ .
Proposition 1: under the interior condition the optimal effort is unique and equals

\delta^*_i = \hat\delta_i = \sum_{j=1}^n\frac{\big(1-(c_j-\sum_{m\ne j}\beta_{j,m})\big)(V^H_j-V^L_j)}{r(\sigma^H_i-\sigma^L_i)(\sigma^H_j-\sigma^L_j)}[\mathbf P^{-1}]_{i,j} - \frac{\sigma^L_i}{\sigma^H_i-\sigma^L_i}.

The explicit partial derivatives of $\delta^*$ in $c_j$ , $V^H_j$ , $\sigma^H_j$ , own-step and cross-step, and the own-step half of Proposition 3.

Significance

The result. Proposition 3 says that a change at one step propagates to every other step through the inverse correlation matrix. An entry $[\mathbf P^{-1}]_{i,j}$ is, up to a negative factor, the partial correlation of steps $i$ and $j$ given all other steps. So two steps whose experiences are positively correlated can still have substitutable efforts once the rest of the process is accounted for, and two uncorrelated steps can have coupled efforts. Pairing a routine with a non-routine step reverses the direction. The paper's later results, on antedependent and autoregressive correlation structures and on the first versus the last step, use this characterisation as their starting point.

Formalizing it. The result is proved on paper. As far as is known, it has no machine-checked proof. Formalizing it means: a verified closed form for the maximizer of a box-constrained concave quadratic with a correlation-matrix Hessian; the identification of the optimizer with that closed form near the base point, so that the optimizer is differentiable there; and the sign analysis. Along the way the formalization corrects two printed slips: the auxiliary quantities $A$ and $B$ in the proof of Proposition 3 (as printed, the displayed identity for $\delta^*_i$ fails), and the printed "Otherwise", which is false when $[\mathbf P^{-1}]_{i,j} = 0$ .

Difficulty

The sign algebra at the end is short. The work lies in the step before it: Proposition 3 differentiates the optimizer of a constrained problem, not a formula. To differentiate it one has to show that under the interior condition the optimizer exists, is unique, and coincides with $\hat\delta$ on a neighbourhood of the parameters in each direction of perturbation. This needs strict concavity from positive definiteness of $\mathbf P$ , the identification of the interior condition (stated through cofactors of $\mathbf P$ ) with $\hat\delta \in (0,1)^n$ , and the openness of that condition in the parameters. Differentiating $\hat\delta$ directly and reading off signs proves a statement about the closed form, not Proposition 3.

Formalization scope

Steps are Fin n, 0-based. All quantities are real. The utility $\mathcal U$ is defined by its mean-variance expression; no random variables appear. $\mathbf P$ is assumed symmetric, positive definite, with unit diagonal and off-diagonal entries in $(-1,1)$ . The cofactor $(-1)^{i+j}|\mathbf P[-j;-i]|$ is Matrix.adjugate P i j. Two hypotheses are added to the page and disclosed: $r > 0$ (the model allows $r \ge 0$ , but Proposition 1 divides by $r$ ) and $\sigma^H_i \ne \sigma^L_i$ (every step is routine or non-routine). Proposition 3 assumes $\beta_{j,i} = 0$ for $j \ne i$ , the paper's own simplification for §4. A partial derivative is Lean's deriv of the optimal effort along one parameter, the others fixed ( $V^L_i$ fixed when $V^H_i$ moves, $\sigma^L_i$ fixed when $\sigma^H_i$ moves). The optimal effort is a choice of maximizer of the §3.3 problem, with junk value $0$ when none exists.

Stating Proposition 3 for the closed form $\hat\delta$ instead of the optimizer of the design problem would trivialize it, and that formalization is ruled out. Likewise the interior condition is the page's interval on $V^H_i - V^L_i$ , not the assumption $\hat\delta \in (0,1)^n$ .

The development needs Mathlib's positive definite matrices, adjugates and determinants, strict concavity, and one-variable derivatives. Reusable by-products: strict concavity and the unique maximizer of a concave quadratic with Hessian $-rD\mathbf PD$ ; positivity of principal cofactors of a positive definite matrix. Contributions are welcome on any milestone, and alternative proofs of Proposition 1 by convex duality or KKT are welcome too.

Selected references

I. Bellos and S. Kavadias, Service design for a holistic customer experience: a process framework, Management Science, 2020 (authors' manuscript). https://doi.org/10.1287/mnsc.2020.3609
U. Karmarkar and R. Pitbladdo, Quality, class, and competition, Management Science 43(1), 27–39, 1997. https://doi.org/10.1287/mnsc.43.1.27
A. Raveh, On the use of the inverse of the correlation matrix in multivariate data analysis, The American Statistician 39(1), 39–42, 1985. https://doi.org/10.2307/2683904

13 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Bitcoin: A Natural Oligopoly: Under Economies of Scale Every Participating Miner's Equilibrium Market Share Is at Least 1 − (1/α)(c_i/c_j)Research Paper

Why mining shares matter

Proof-of-work mining allocates a fixed reward among miners whose investments determine their chances of receiving it. The resulting distribution of mining power matters for decentralization: if a few miners control most of the investment, the economic mechanism does not support a diffuse set of participants. Arnosti and Weinberg study this question in a contest model where miners have different unit costs and rewards may rise more than proportionally with investment. Their proportional model has an explicit equilibrium; the economies-of-scale model asks what can still be said about market shares when that explicit characterization is unavailable.

The authors' result is a bound for each miner who invests, measured against the cost of any other miner who invests. It applies even when unit costs are asymmetric. The claim is conditional on a pure equilibrium: for sufficiently strong economies of scale, such an equilibrium need not exist, as the paper observes. The mission concerns the quantitative restriction on every equilibrium that does exist, not an assertion that all parameter choices have one.

Contest and equilibrium

There are $n\ge2$ miners and a prize worth one. Miner $i$ chooses a nonnegative investment $q_i$ and pays $c_iq_i$ , where the unit cost $c_i$ is strictly positive. A parameter $\alpha\ge1$ determines how investment affects rewards. At an investment profile $q=(q_1,\ldots,q_n)$ , the market share of miner $i$ is

x_i(q)=\frac{q_i^\alpha}{\sum_{j=1}^n q_j^\alpha}

when some miner invests. When every investment is zero, the model assigns every miner share zero. The utility of miner $i$ is $U_i(q)=x_i(q)-c_iq_i$ . The prize value is fixed at one throughout; there is no extra reward parameter.

A pure Nash equilibrium is a nonnegative profile $q$ at which no miner can increase its own utility by replacing $q_i$ with another nonnegative investment while all other investments remain fixed. This global comparison matters because, with economies of scale, a local first-order condition alone does not characterize a best response. The paper's phrase “equilibrium in the EoS model” has this pure-strategy meaning. A miner participates when $q_i>0$ ; at the equilibrium profiles of interest this is equivalent to having positive market share.

The paper states the cost vector in increasing order without loss of generality in its earlier proportional-model section. The share bound is invariant under relabelling, so its formal statement permits any assignment of positive costs to the $n$ miners. No pair of miners has to be distinct.

Formalization targets

The goal is Theorem 2 of the arXiv preprint. For every pure equilibrium $q$ and every pair of participants $i,j$ , including $i=j$ , it states

x_i(q)\ge 1-\frac1\alpha\frac{c_i}{c_j}.

The bound depends on both the scale exponent and the relative costs. Setting $i=j$ gives the symmetric threshold $1-1/\alpha$ for each participant. The target therefore retains the exact cost ratio and the paper's quantifier over all participating pairs. It does not require a selected or unique equilibrium.

The milestone list follows the authors' named results and one explicit analytic statement in their proof. Lemma 3 gives the equilibrium identity $c_iq_i=\alpha x_i(q)(1-x_i(q))$ and a separate inequality that still applies to a nonparticipant. Corollary 4 gives $x_i(q)\ge1-1/\alpha$ when $x_i(q)>0$ . In the proof of Proposition 1, the function $f_\alpha(x)=x^{1-1/\alpha}(1-x)$ is decreasing on the open interval $(1-1/\alpha,1)$ ; the milestone states strict decrease, matching the negative derivative shown there. Proposition 1 then says that if $q_i\ge q_j>0$ , then $c_i\le c_j$ , with equality exactly when $q_i=q_j$ . These are the source's results that support Theorem 2, rather than substitutes with weaker conclusions.

What the bound gives

The theorem turns a claim about scale effects into a checkable limit on equilibrium concentration. When costs are equal, every participant has share at least $1-1/\alpha$ . Thus, as the paper notes, sufficiently strong scale effects limit the number of participants in any pure equilibrium. With unequal costs, the same result gives a pairwise share guarantee that accounts for each miner's cost relative to another participant's. A bound only in terms of $\alpha$ would lose that comparison.

The mathematical result is proved in the cited paper. This mission asks for machine-checked Lean proofs of the statement and its source milestones. The definitions and theorem statements here are local drafts; compilation of a statement confirms that Lean can parse it, not that a proof exists. The reusable global pure Nash predicate is imported from an existing formalization. The paper-specific layer consists of the contest success function, utility, equilibrium specialization, and share-shape function. Together they make it possible to compare formal proofs of the same economic claim without silently changing the game.

Main difficulty

For $\alpha>1$ , the utility from a unilateral investment change can have a shape that is not captured by a single local optimum test. An argument based solely on setting a derivative to zero can miss a better distant deviation or the boundary action $q_i=0$ . The first-order relations of Lemma 3 are consequences of global equilibrium, not its definition. The main share bound also compares two miners at once: knowing only a participant's own first-order identity gives an expression involving its own share and investment, while Theorem 2 asks for an exact ratio of two different costs. Proposition 1 supplies the ordering information needed by the authors' argument. At $\alpha=1$ , the model meets the proportional case, so formulas involving $q_i^{\alpha-1}$ must still make sense at zero investment.

Formalization scope

Lean indexes miners by Fin n; its zero-based labels correspond to the paper's miners $1,\ldots,n$ without changing any statement. The model uses real-valued investments and costs, with the strategy constraint $q_i\ge0$ , and real exponentiation for $q_i^\alpha$ . Standing assumptions are $n\ge2$ , $\alpha\ge1$ , and $c_i>0$ for every miner. The model explicitly assigns zero share at the all-zero profile, rather than relying on a convention for division by zero. The imported feasible-strategy Nash predicate is specialized to the set of nonnegative real numbers and therefore quantifies over every nonnegative unilateral deviation. No theorem adds positivity of the aggregate investment as a premise: that property must follow from equilibrium where it is needed.

These choices rule out a trivializing formalization in which equilibrium is defined by Lemma 3's first-order equations or the goal is weakened to the equal-cost case. The exact exponent, the unit prize, and the ratio $c_i/c_j$ are part of the target. The real-power convention gives $0^0=1$ at $\alpha=1$ in Lemma 3's inequality; the theorem's denominator is positive at equilibrium. Formal proofs will need finite-sum and real-power facts, unilateral-deviation reasoning, real analysis for the shape function, and inequalities linking investment, share, and costs. Proofs of the four milestones, alternative proofs of the goal, and reusable game-theoretic lemmas are within scope. The paper's separate proportional-equilibrium characterization and countably infinite-miner model are outside this mission.

Selected references

Nick Arnosti and S. Matthew Weinberg, Bitcoin: A Natural Oligopoly, arXiv:1811.08572v1, 2018; later published in Management Science, 2022. Pinned preprint.

7 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Capacity Expansions with Bundled Supplies of Attributes: An Application to Server Procurement in Cloud Computing: A Unique Fixed-Cost Threshold Decides Simultaneous Versus Sequential ReplenishmentResearch Paper

Motivation

A cloud provider buys servers in preset configurations, while its demand for processing and memory grows at different rates. Each server configuration supplies both resources, so adding capacity for one resource also changes the unused capacity of the other. Purchases incur a charge for the servers, a charge for making an expansion, and an ongoing cost for unused capacity. The choice between buying configurations together and staggering their purchases is therefore a cost decision even when demand is known. Arbabian, Chen, and Moinzadeh study this decision for two resources and two server configurations over a finite planning horizon. Their Proposition 1 identifies a threshold in the fixed cost of a joint expansion.

The result was stated in the authors' April 14, 2019 manuscript and published in Manufacturing & Service Operations Management in 2020. This mission uses the manuscript's theorem numbers and pages. The result is a known mathematical claim; the remaining work is to give its definitions and proof in Lean, with the source's policy classes and cost accounting represented explicitly.

Setting

There are two capacity attributes, indexed by $i\in\{1,2\}$ , and two cluster types, indexed by $j\in\{1,2\}$ . A unit of cluster $j$ supplies $a_{ij}>0$ units of attribute $i$ . Demand for attribute $i$ increases at a nonnegative rate $d_i(t)$ over $[0,T]$ , and $D_i(s,t)=\int_s^t d_i(u)\,du$ is its growth between $s$ and $t$ . The provider starts with both attributes at their minimum desired excess capacity, normalized to zero. It must meet demand at every time and return both excess capacities to zero at the end of the horizon. Replenishment takes effect immediately. These are the base-model conventions in §3 of the manuscript.

A capacity expansion cycle begins and ends when both attributes are leveled. In a sequential cycle, one cluster type leads: it is bought one or more times, followed by one purchase of the other type. Each expansion costs $A>0$ . In a simultaneous cycle, both types are bought at each expansion, whose fixed cost is $\beta A$ for $\beta\in[1,2]$ . Cluster $j$ has unit purchase cost $c_j$ , and unused attribute $i$ has holding rate $h_i>0$ . If $E_i(t)$ is the excess capacity after the expansions at time $t$ , total holding cost is $\sum_i h_i\int_0^T E_i(t)\,dt$ . Total cost also includes all fixed and purchase costs. Sequential policies may have any positive number of cycles, any positive number of leading expansions within each cycle, and either leading type. For joint policies, the intervals between consecutive joint expansions form a partition of $[0,T]$ .

Formalization targets

The main target is the unique fixed-cost threshold of Proposition 1. Write $V_{\mathrm{seq}}$ for the infimum of costs of all feasible sequential policies and $V_{\mathrm{sim}}(\beta)$ for the corresponding simultaneous infimum. The threshold $\bar\beta\in(1,2)$ satisfies, for every $\beta\in[1,2]$ ,

V_{\mathrm{sim}}(\beta)\le V_{\mathrm{seq}}\iff\beta\le\bar\beta, \qquad V_{\mathrm{sim}}(\beta)<V_{\mathrm{seq}}\iff\beta<\bar\beta.

This makes equality at $\bar\beta$ explicit, in line with the paragraph following Proposition 1. The milestone list records the source's sequential and simultaneous cost identities, the fixed-time holding comparison, the split comparison from the appendix, the two endpoint inequalities, and monotonicity in $\beta$ . Equation (8), which fixes the final sequential expansion time inside a cycle, is another milestone because the authors use its uniqueness in their analysis.

Significance

The threshold gives a precise decision rule for the model: a lower relative joint expansion charge favors buying both types together; a higher charge favors staggered purchases. It compares optimized policies, whose cycle boundaries and expansion times may differ, rather than only two schedules held at the same times. The result therefore captures the interaction of the fixed charge and the time spent holding unused capacity. The paper also analyzes specialized one-cycle schedules under exponential demand; those results are separate from this mission's general comparison.

A completed Lean development would make the policy definitions, cost identities, and threshold claim machine checked. It would also provide reusable definitions for finite-horizon bundled capacity expansion, including a time-dependent excess-capacity trajectory and its integral holding cost. The manuscript supplies a mathematical proof, but this proposal's theorem files currently contain open sorry proofs. The mission invites proofs of its listed statements and the analytic facts needed to connect them, including existence of optimal schedules.

Difficulty

The straightforward comparison uses identical expansion times. That comparison identifies a holding-cost difference, but it does not compare the two optimized classes: the least-cost sequential schedule and the least-cost joint schedule may choose different times and different numbers of expansions. The paper's endpoint arguments also rely on strict inequalities for optimal costs. A strict inequality for every fixed schedule does not automatically become strict after taking an infimum. Showing that the relevant optima are attained, or supplying an equivalent uniform argument, is part of the formalization burden. The fixed expansion charge bounds how many expansions a near-optimal policy can afford, but the interval lengths remain continuous variables.

Formalization scope

Lean represents the attributes and cluster types by Fin 2, with index 0 corresponding to the paper's 1 and index 1 to its 2. The matrix entry a i j is capacity of attribute $i$ per unit of cluster $j$ . Times, demand, quantities, and costs are real. Replenishment times are strictly increasing, and a purchase at time $t$ contributes to the right-continuous excess capacity at $t$ . Policy validity requires no shortage and balance at cycle endpoints. The positive determinant $\alpha=a_{11}a_{22}-a_{12}a_{21}$ records the nondegenerate, attribute-intensive cluster configurations needed by the paper's division formulas. The optimal costs are real infima over full policy classes, with no attainment built into their definitions. Holding cost is computed from the integral of actual excess capacity; defining it by the displayed closed forms would erase the content of Lemmas 1 and 2.

The theorem assumes continuous demand rates and the strict demand-ratio guard $a_{12}d_2(t)<a_{22}d_1(t)$ and $a_{21}d_1(t)<a_{11}d_2(t)$ throughout $[0,T]$ . The manuscript states Assumption 1 only for chosen leading intervals. Its Proposition 1 needs more: without the guard, taking $a=((2,1),(1,2))$ , $A=100$ , $c_j=0$ , $h_i=1$ , $d_2=1$ , and $d_1=90$ on $[0,0.01)$ then $10/99$ permits one joint expansion at $\beta=2$ for at most 202 while every feasible sequential policy costs at least 300. Demand continuity supports the cost integrals; the strict guard makes every subinterval satisfy Assumption 1 strictly and keeps the appendix's sequential split feasible. Neither regularity nor this guard is claimed as a printed hypothesis of Proposition 1.

The appendix prints an extra $h_1$ outside the sum in its Case 2 holding-cost difference; the Lean milestone uses $\sum_i h_i(y-s)a_{i2}Q_2$ , consistent with the preceding integrals. The paper also prints $[0,1]$ in its last monotonicity sentence, while its fixed-cost parameter is defined on $[1,2]$ ; the milestone uses the model's interval. Useful contributions include formal integration identities for these finite replenishment schedules, existence and finiteness of the policy optima, and the comparison claims in the milestones.

Selected references

M. E. Arbabian, S. Chen, and K. Moinzadeh, Capacity Expansions with Bundled Supplies of Attributes: An Application to Server Procurement in Cloud Computing, Manufacturing & Service Operations Management, 2020. SSRN manuscript, April 14, 2019; published DOI.

10 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research·Captain: mikedeng1

Asset Selling Under Debt Obligations: Under a Single Debt Payment Due Before the Horizon Ends, the Optimal First Sale Follows a Control Band of Two Critical PricesResearch Paper

Selling an asset bought with debt

Firms that hold a large, divisible asset (a commodity inventory, a block of shares, a stock of natural gas) often financed it with debt and must sell it over time to repay that debt. Without debt, the timing problem is classical: Karlin (1962) showed that a non-divisible asset facing independent prices should be sold the first time the price exceeds a reservation price. Debt changes the incentives in two opposite directions. Limited liability caps the shareholders' loss at zero, which rewards gambling on high future prices and delays selling. Bankruptcy also destroys the value of the unsold asset, an indirect bankruptcy cost, which rewards selling early to secure the debt payment. Ahn, Wang and Wu (SSRN 3472345, published in Operations Research 69(4), 2021, doi:10.1287/opre.2019.1961) solve the resulting dynamic program with Markov prices. This mission formalizes their central structural result: the optimal first sale under a single debt payment due before the end of the horizon.

Setting

A seller holds an amount $x_t \in [0,1]$ of a divisible asset at the beginning of period $t = 1, \dots, T$ , with $x_1 = 1$ . The selling price $P_t$ follows a Markov process: the law of $P_{t+1}$ given $P_t = p$ is a probability kernel $\kappa_t(p)$ , with finite conditional mean. Write $E_t$ for the expectation given the current price. The discount factor is $\rho \in (0,1)$ , the per-period selling capacity is $\ell \in (0,1]$ , and unsold asset is worthless after period $T$ .

The debt-free value $U_t(x,p)$ solves, with $U_{T+1} \equiv 0$ ,

U_t(x,p) = \max_{0 \le q \le \min(x,\ell)} \; p\,q + \rho\,E_t\,U_{t+1}(x-q, P_{t+1}).

The debt-free critical price is $R^o_t = \rho\,E[U_{t+1}(1,P_{t+1}) \mid P_t]$ .

Debt. A schedule $d = (d_t)_{t \le m}$ , $d_t \ge 0$ , is due at the end of periods $t = 1, \dots, m$ , with maturity $1 \le m \le T$ . The seller's working capital $w_t$ starts at $w_1 = 0$ and grows at rate $1/\rho$ . In period $t \le m$ , a quantity $q$ is feasible if $0 \le q \le \min(x_t,\ell)$ and $w_t + p_t q \ge d_t$ . If no quantity is feasible, the seller is bankrupt and the equity value $V_t(x,w,p;d)$ is $0$ . Otherwise

V_m(x,w,p;d) = \max_{q \text{ feasible}} \; p\,q + w - d_m + \rho\,E_m\,U_{m+1}(x-q,P_{m+1}),

V_t(x,w,p;d) = \max_{q \text{ feasible}} \; \rho\,E_t\,V_{t+1}\big(x-q,\ \rho^{-1}(w + p\,q - d_t),\ P_{t+1}; d\big), \quad t < m.

For a single payment $d_m = D$ (and $d_t = 0$ otherwise), write $\delta_t = \rho^{m-t}D$ and $C_t = \rho\,E_t V_{t+1}(1,0,P_{t+1};d)$ , with $V_{m+1} := 0$ . The net effect of debt is

\Delta_t = V_t(1,0,P_t;d) - \big(U_t(1,P_t) - \rho^{m-t}D\big).

It is the value of limited liability net of the bankruptcy cost. The two critical prices are

R^{(1)}_t = \min\Big\{\frac{\delta_t R^o_t}{R^o_t - C_t},\ C_t + \delta_t\Big\}, \qquad R^{(2)}_t = \max\{R^o_t,\ C_t + \delta_t\}.

Formalization targets

Goal: Proposition 4 (p. 14)

Assume $\ell = 1$ , a single payment $D > 0$ at $m < T$ , a period $t \le m$ before any sale ( $x = 1$ , $w = 0$ ), and a price $p > 0$ . Then $R^{(1)}_t \le R^{(2)}_t$ , and:

p < R^{(1)}_t \Rightarrow \text{sell nothing } (t<m) \text{ or bankruptcy } (t=m), \qquad R^{(1)}_t \le p < R^{(2)}_t \Rightarrow q = \delta_t/p \text{ is optimal}, \qquad p \ge R^{(2)}_t \Rightarrow q = 1 \text{ is optimal}.

After the debt-securing sale, the optimal quantities coincide with the debt-free ones. Moreover:

E_t\Delta_{t+1} < 0 \Rightarrow R^{(1)}_t < R^{(2)}_t = R^o_t, \qquad E_t\Delta_{t+1} \ge 0 \Rightarrow R^{(1)}_t = R^{(2)}_t \ge R^o_t.

When $E_t\Delta_{t+1} = 0$ , all three prices coincide.

Milestones

In attack order:

Lemma 1(i)–(ii) (p. 8). Enough working capital makes $V_t = U_t + w - \sum_{i\ge t}\rho^{i-t}d_i$ . With no asset left, $V_t = (w - \sum_{i \ge t}\rho^{i-t}d_i)^+$ .
Proposition 1 (p. 9) with (A.1). The debt-free rule is to sell everything once $P_t \ge R^o_t$ ; moreover $U_t(x,p) = \max\{p, R^o_t\}x$ and $R^o_t = \rho E_t\max\{P_{t+1}, R^o_{t+1}\}$ .
(A.6). The closed form of $V_m$ .
Lemma 3 (p. 13). Convexity, linearity and continuity of $V_t$ in $(x, w, d_m)$ .
(A.8). $V_t$ is a three-term maximum.
(A.9). Its specialization at $x = 1$ , $w = 0$ .
Footnote 4. $0 \le C_t < R^o_t$ .

Significance

Proposition 4 is the paper's headline. Under debt, the first sale follows a control band. Below $R^{(1)}_t$ the seller waits. Between the two critical prices, the seller sells exactly the quantity whose revenue covers the discounted debt; in that band a higher price means a smaller sale. Above $R^{(2)}_t$ the seller sells everything. Part (ii) separates the two economic forces by the sign of one number, $E_t\Delta_{t+1}$ . When the bankruptcy cost dominates, part of the asset is sold earlier than without debt. When limited liability dominates, selling is delayed and done all at once. The same structure underlies the paper's later results on threshold debt levels and general installment schedules.

The result is proved on paper but has not been formalized; the platform has no asset-selling, reservation-price or debt-constrained selling model. The mission contributes three things. The first is a finite-horizon Markov-price dynamic program with an explicit bankruptcy branch and limited liability, built on Mathlib's probability kernels. The second is Karlin-type debt-free stopping results for a divisible asset. The third is the full convexity argument behind the control band.

Difficulty

Part (ii) is signed algebra once footnote 4 is known; the work is in part (i). Because of the bankruptcy branch, $V_t$ is neither convex nor concave in general (Lemma 1(iii)). So the first-order reasoning that settles the debt-free problem, a linear objective in $q$ , does not carry over. Two facts reduce the optimum to three candidate quantities. The first is convexity of $V_t$ in $(x, w, d_m)$ below the debt-covering region, proved by backward induction together with the debt level. The second is linearity above that region. The induction must carry the debt level as a variable.

Every value function is integrated against a kernel. Before any identity between expectations can be used, $p' \mapsto U_{t+1}(x,p')$ and $p' \mapsto V_{t+1}(x,w,p')$ must be shown measurable and integrable, and both are suprema over a continuum of quantities. The strict inequality of footnote 4 is a separate induction: $V_{t+1}(1,0,\cdot) < U_{t+1}(1,\cdot)$ at every positive price.

Formalization scope

Everything lives in the namespace AssetDebt.ControlBand.

Representation.

Periods are natural numbers and values are real numbers.
κ t p is the law of $P_{t+1}$ given $P_t = p$ , a Mathlib Kernel ℝ ℝ.
$U$ and $V$ are defined by well-founded recursion as suprema of the objective over the feasible set. For $V$ , the bankruptcy test comes first, so the supremum is only taken over a nonempty interval.
$V_t := 0$ for $t > m$ , which is the paper's convention $V_{m+1} := 0$ .
Feasibility is written $0 \le q \le \min(x,\ell)$ , $d_t \le w + pq$ . This avoids dividing by $p$ .
"Optimal" means feasible and attaining the maximum; uniqueness is not claimed.
The critical prices $R^{(1)}_t, R^{(2)}_t$ are the explicit thresholds (A.10) from the paper's proof, not a free existential.
$E_t\Delta_{t+1}$ is the integral of $\Delta_{t+1}$ as defined in (5).

Added hypotheses.

Prices are almost surely strictly positive. The paper writes $P_t \ge 0$ but divides by $p_t$ .
The multi-step conditional means $E[P_s \mid p_t]$ , $t < s \le T$ , are finite. The paper treats $R^o_t$ as a real number, and the one-step assumption alone does not guarantee that.
Section 3's standing assumption $\ell = 1$ is a hypothesis of every statement except Lemma 1.

Excluded trivializations. $V$ is never defined by its closed forms (A.6), (A.8) or (A.9), which would make the goal an unfolding exercise. The critical prices are not existentially quantified: a price-dependent existential could be witnessed by thresholds read off the optimal action itself.

Infrastructure. A complete development needs measurability of suprema of kernel integrals, sup-shift lemmas for bounded intervals, and the backward-induction convexity argument. The debt-free results (Proposition 1) and the sup and measurability lemmas apply to other finite-horizon selling and stopping models. Contributions are welcome on any milestone, in particular on the measurability layer.

Selected references

H.-S. Ahn, D. D. Wang, O. Q. Wu, Asset Selling Under Debt Obligations, SSRN 3472345, version of May 7, 2019. https://ssrn.com/abstract=3472345 ; published in Operations Research 69(4), 2021. https://doi.org/10.1287/opre.2019.1961
S. Karlin, Stochastic models and optimal policy for selling an asset, in K. J. Arrow, S. Karlin, H. Scarf (eds.), Studies in Applied Probability and Management Science, Stanford University Press, 1962, pp. 148–158 (cited as in the paper’s reference list).
O. Besbes, D. A. Iancu, N. Trichakis, Dynamic pricing under debt: spiraling distortions and efficiency losses, Management Science 64(10), 2018, pp. 4572–4589 (cited as in the paper's reference list).

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

Quality Disclosure Under Consumer Loss Aversion: In a Duopoly with Costly Disclosure, Stronger Loss Aversion Lowers the Disclosure Threshold and Raises Each Firm's Ex Ante ProfitResearch Paper

Motivation

A seller can disclose privately known product quality, but credible disclosure costs money. In a market with competing sellers, disclosure changes both what consumers believe about a silent seller and how aggressively the sellers can price. Zhang and Li study this interaction when consumers are loss averse about quality: learning that a product falls below an expected standard hurts more than learning that it exceeds the standard helps. Their duopoly result says that stronger consumer loss aversion makes firms disclose more often and raises each firm's profit before quality is known, even though disclosure itself remains costly. The model and result appear in the SSRN preprint, §§3.1–3.3 and Proposition 2.

The paper first gives a monopoly benchmark and then analyzes two firms facing the same consumers. The duopoly question is distinct because a firm's disclosure affects the gap between its own product's perceived value and its rival's. The paper's Proposition 2 is a comparative statement about the equilibrium of this disclosure game, not a claim about a distribution chosen for a numerical example. The formalization targets the general quality distribution used in the paper.

Setting

Two symmetric firms, A and B, each have one product and a privately known quality $q_a,q_b\in[0,1]$ . Their qualities are independent draws from a common cumulative distribution $F$ with a continuous, strictly positive density $f$ and $F(1)=1$ . A firm may pay a common disclosure cost $c>0$ to reveal its quality truthfully. Otherwise, consumers infer quality from nondisclosure. With a common disclosure threshold $\hat q$ , firms reveal quality above $\hat q$ and remain silent at or below it. The inferred quality of a silent firm is the conditional mean $\bar q=E[q\mid q\le\hat q]$ .

When a product's quality is disclosed, a consumer values it at $q-p$ , where $p$ is its price. When quality is hidden, the consumer experiences a gain or loss relative to $\bar q$ . With gain sensitivity $g>0$ and loss sensitivity $l>0$ , equation (1) gives utility

u=q-p+g\max\{q-\bar q,0\}-l\max\{\bar q-q,0\}.

The degree of consumer loss aversion is $k=l-g$ . The paper assumes $k>0$ and also discusses the loss neutral benchmark $k=0$ . It uses two functions of the quality distribution,

G(x)=\frac{\int_0^x F(q)\,dq}{F(x)},\qquad H(x)=\frac{\int_0^{x-G(x)}F(q)\,dq}{F(x)},\qquad 0<x\le1.

They express the belief as $\bar q=\hat q-G(\hat q)$ and the expected gross utility of a silent product as $\bar q-kH(\hat q)$ , by equation (2). After disclosure decisions, firms set prices against homogeneous consumers. Under the paper's participation condition, the Bertrand outcome awards the firm with the higher gross consumer value the difference between the two values as revenue; the lower valued firm earns zero. Disclosure cost is then subtracted from the revealing firm's revenue. A symmetric equilibrium threshold means that both firms use the same $\hat q$ and each firm's disclosure choice is a best response at every quality.

Formalization targets

Proposition 2: threshold and profit

Fix $F,f,c,g$ and compare $l_1<l_2$ at fixed $g$ , with $0\le k_1=l_1-g<k_2=l_2-g$ . For the corresponding symmetric best response thresholds $\hat q_1,\hat q_2$ , Proposition 2 asks for both strict comparisons:

\hat q_2<\hat q_1,\qquad E(\pi^d_1)<E(\pi^d_2).

Here $E(\pi^d_i)$ is either firm's ex ante profit, averaged over its own quality before the draw. The result does not prescribe a numerical disclosure threshold or profit. The preprint's Proposition 2, p. 18, states the two directional claims; its proof on p. A7 gives strict signs.

The milestones preserve the paper's intermediate statements: the nondisclosure belief and expected utility, growth of $H$ , the two disclosure profits, the equilibrium equation (6) and its unique root in Claim 3, the ex ante profit identity (7), and the derivative of the integral $L$ . In particular, the game defined above determines the threshold and profit; equations (6) and (7) are claims to establish about those objects.

Significance

The result identifies a setting in which a consumer preference that lowers the perceived value of undisclosed goods can benefit competing firms. A stronger aversion to disappointed quality expectations changes firms' disclosure decisions and, through those decisions, the price differences available in competition. Proposition 2 gives a statement about each firm's expected profit, while the paper separately discusses cases in which an individual firm's realized profit can rise or fall. These distinctions are explicit in the preprint's §3.3, pp. 15–18.

The economic result is established in the paper; this mission seeks a machine checked Lean proof of its symmetric equilibrium claim and the paper's supporting identities. The statements here compile as open targets, and no proof is asserted to have been formalized. The work also develops reusable interval integral facts for conditional means and costed disclosure games with a general continuous quality density.

Difficulty

The central difficulty is the link between the original disclosure game and the integral expressions used in the paper's comparative statics. The profit of disclosing depends on the rival's random quality and its disclosure decision. The profit of silence depends on a belief formed from the same threshold that firms choose. A formula about a root of equation (6) alone does not establish that the root is a best response threshold in this game. Likewise, the compact profit expression (7) must agree with the profit obtained by integrating the game's conditional Bertrand margins and paying disclosure cost.

The general density also matters. A calculation for the uniform distribution in the paper's numerical footnote does not cover the paper's proposition. Establishing strictness requires keeping the positive density, the monotonicity assumption on $G$ , and the consumer participation domain visible throughout the development.

Formalization scope

Lean represents $F$ and $f$ as real valued functions relevant on $[0,1]$ , together with a proposition asserting that $f$ is continuous and positive there, that $F(x)=\int_0^x f(q)\,dq$ on the interval, and that $F(1)=1$ . Every expectation against $dF(q)$ is an interval integral against $f(q)\,dq$ . The firms' independent, identical draws are encoded by using that same density separately for own and rival quality; no probability space is introduced. The standing assumption that $G$ is increasing is expressed as strict monotonicity on $(0,1]$ . The threshold lies in that interval, so division by $F(0)=0$ cannot create a boundary statement about an undefined conditional mean.

Lean's utility function is gross of price. Its pricing layer represents the paper's homogeneous consumer Bertrand outcome by $\max\{u-v,0\}$ . The symmetric equilibrium predicate requires the silent product's gross utility to be nonnegative, and the strategic payoff identities carry the same condition. This is the bound in footnote 3 of §3.3, p. 15. The comparison fixes $g$ and increases $l$ ; it includes $k_1=0$ to cover the paper's loss neutral benchmark. The model's positive $g$ and $l$ assumptions are explicit in the economic statements. The milestone for $H$ exposes positivity on the full positive interval, beyond the page's explicit $H(1)>0$ .

The symmetric equilibrium is defined by best responses in disclosure and the participation condition, with consumers using the conditional belief and firms receiving Bertrand revenue less disclosure cost. Neither the equilibrium threshold nor ex ante profit is defined by the simplified equation it is supposed to satisfy. Claim 3 gives a unique root of the threshold equation; an admissible root must also satisfy participation to represent an equilibrium. The paper's Claim 2 about the absence of asymmetric equilibria is outside this mission: Proposition 2 is framed for the symmetric equilibrium, and the printed argument for Claim 2 has an unresolved monotonicity step. Contributions to the model identities, equilibrium characterization, integral calculus, and goal proof are all within scope.

Selected references

J. Zhang and K. J. Li, Quality Disclosure under Consumer Loss Aversion, SSRN preprint 3544738, version of 2020-01-20, §§3.1–3.3 and Appendix, 2020. SSRN.
J. Zhang and K. J. Li, Quality Disclosure under Consumer Loss Aversion, Management Science 67, 2021. DOI: 10.1287/mnsc.2020.3745. The mission's page and equation citations refer to the pinned preprint above.

10 thms2 active usersReviewed

Completed

Economics Operations Research·Captain: mikedeng1

Trade Credit Insurance: Operational Value and Contract Choice: With an Attractive Outside Option, the Cancelable Contract δ = 0, p = f = c/θ₁ + β₁r Is Optimal and Recovers the Full Value of TCIResearch Paper

Motivation

Suppliers often let buyers pay after delivery. If the buyer defaults, the supplier loses the credit sale revenue and may also face a financing cost from the resulting cash shortfall. Trade credit insurance transfers part of this loss to an insurer, but the insurer may possess information about the buyer that the supplier cannot observe. The insurer can use that information by canceling coverage before shipment. Yang, Bakshi, and Chen study how this option changes both the insurer's incentive to gather information and the supplier's decision to ship. Their Proposition 3 identifies a regime in which a simple cancelable contract recovers the entire value available to a centralized decision maker. Yang, Bakshi, and Chen (2021)

The question matters for contract design because a policy's deductible and refund affect different decisions. A deductible changes the supplier's loss if the buyer defaults. A refund changes the insurer's cost of canceling coverage. With a sufficiently attractive alternative sales channel, these terms can induce the insurer to reveal adverse credit information through cancelation while leaving the supplier fully covered when she ships. This mission states that claim precisely for the three-signal model in the authors' accepted manuscript. Accepted manuscript, §§3 and 6

Setting

A supplier receives an order for one unit at credit price $r$ . She may ship on credit or sell through an outside channel for $r_0<r$ . When the buyer defaults, the supplier receives no payment from the buyer. Her financing cost depends on end-of-period net cash flow $x$ :

L(x)=l(T-x)^+=l\max\{T-x,0\}.

Here $T$ is a cash flow threshold and $l$ is the marginal cost of falling short. At the time of contracting, the buyer's default probability is $\bar\beta$ . An insurer can pay cost $c$ to monitor the buyer and observe one of three signals $i=1,2,3$ . Signal $i$ occurs with probability $\theta_i$ and has conditional default probability $\beta_i$ , where $\beta_1<\beta_2<\beta_3$ and $\bar\beta=\sum_i\theta_i\beta_i$ . The paper assumes the outside channel is initially less attractive than the credit sale: $r_0<(1-\bar\beta)r$ . Accepted manuscript, §3 and Table 1

A cancelable contract is $\kappa=(p,\delta,f)$ . The supplier pays premium $p$ ; if she ships while covered and the buyer defaults, the insurer pays the credit price minus deductible $\delta$ . Before shipment, the insurer can instead cancel coverage and refund $f$ . After this decision, the supplier chooses whether to ship. The contract must satisfy $0\le\delta\le r$ and $0\le f\le p$ . The insurer's monitoring decision compares its expected total cost with three alternatives: keep coverage without monitoring, cancel without monitoring, and decline the contract. The supplier's payoff includes her premium, any refund, default losses, and financing costs. Accepted manuscript, §§3 and 6, and Lemma B.1

The first-best payoff is the maximum available to a financially unconstrained planner who controls monitoring and, if monitoring occurs, can choose whether to ship at each signal. The paper's Proposition 1 identifies it as

\Pi^{FB}=(1-\bar\beta)r+(\phi-c)^+,\qquad \phi=\sum_{i=1}^{3}\theta_i[r_0-(1-\beta_i)r]^+.

The quantity $\phi$ is the value of using the signal to avoid credit shipments for which the outside sale is better. The supplier receives the full value of TCI when her payoff under a contract equals $\Pi^{FB}$ . Accepted manuscript, Proposition 1 and its proof

Formalization targets

Potential value and first-best

Proposition 1 gives the difference between the first-best and the no-insurance payoff:

\Pi^{FB}-\Pi^{NI} =\min\{\bar\beta L(0),(1-\bar\beta)r-r_0\}+(\phi-c)^+.

This benchmark makes the phrase “full value” testable against a separate maximization over planner policies, rather than against a formula chosen to fit the contract. Accepted manuscript, Proposition 1, p. 11

Cancelable contract with an attractive outside option

The goal is Proposition 3. Under Assumptions 1 and 2, the paper's efficient-monitoring regime $c\le\phi$ , and $r_0\ge(1-\beta_2)r$ , it identifies

\delta=0,\qquad p=f=\frac{c}{\theta_1}+\beta_1r.

The insurer monitors and cancels at signals 2 and 3; the supplier ships only at signal 1. Her payoff equals $\Pi^{FB}$ , and no other admissible cancelable contract gives her more. Milestones establish the monitoring conditions, the first-best formula, feasibility and resulting decisions, attainment of the payoff, and the upper bound over other contracts. Accepted manuscript, Proposition 3, p. 18, and proof, pp. xi–xii

Significance

Proposition 3 identifies a regime where cancelation transmits the insurer's private credit information into the supplier's shipment choice. It gives exact contract terms, the induced actions at each signal, and a payoff that meets the centralized benchmark. The result thus pins down when the option to cancel coverage eliminates the loss from the two parties controlling different decisions. Yang, Bakshi, and Chen (2021), §6.2

The result is proved in the paper. The remaining formalization work is to prove the Lean statements, beginning with the finite three-signal model and ending with the optimality inequality over every admissible cancelable contract. A local prior-art search found no published declaration with this model and these conclusions. The finite contract and policy definitions can also support formal statements about the paper's other regimes, provided their distinct assumptions and timing rules are introduced explicitly.

Difficulty

The contract sits on several decision boundaries. In particular, the insurer's cost of monitoring can equal the refund, so replacing a weak incentive comparison by a strict one would discard the proposed contract. The supplier can be indifferent about shipping at signal 2 after coverage is canceled when $r_0=(1-\beta_2)r$ . The paper's displayed threshold rule and its Proposition 3 proof make different tie choices there. The formal goal follows the proof's choice and records it in the model.

A second difficulty is showing global optimality. Computing the proposed contract's payoff alone does not compare it with contracts that generate different cancelation or shipping patterns. The upper-bound milestone covers all admissible cancelable contracts, while the first-best is defined from the planner's actual choices. The threshold $\mathbb B=(r-r_0)/[\delta+L(r-\delta-p)]$ cannot define shipping at the proposed contract, because its denominator is zero there. Accepted manuscript, equations (1), (6)–(9), and proof of Proposition 3

Formalization scope

Lean uses real-valued prices, costs, probabilities, and payoffs, and a finite signal type with three members. Lean indices $0,1,2$ correspond to the paper's signals $1,2,3$ . The prior $\bar\beta$ is defined by Table 1's weighted average $\sum_i\theta_i\beta_i$ . Standing hypotheses state nonnegative signal probabilities summing to one, ordered default probabilities in $[0,1]$ , $r_0<r$ , $r_0<(1-\bar\beta)r$ , and positive monitoring cost. The explicit additions $l\ge0$ and $\theta_1>0$ make financing cost nonnegative and $c/\theta_1$ meaningful. Assumption 1, Assumption 2, and $c\le\phi$ remain separate hypotheses.

Decisions are defined by payoff comparisons. Shipping under coverage uses the weak inequality in (1); cancelation and shipping after cancelation use the strict tie choices in the proof of Proposition 3, equations (64)–(66). The first-best is a maximum over no-monitoring choices and all shipping policies after monitoring. Optimality compares the supplier's payoff with every valid cancelable contract that induces monitoring and actual cancelation at some signal. Defining the first-best as the desired formula, restricting competitors to contracts with the proposed policy, or using division by a zero threshold denominator would empty the intended claim.

The development needs finite sums, real inequalities, maxima, and a representation of sequential contract decisions. Contributions proving the monitoring characterization, planner value, feasibility, payoff identity, and global upper bound are within scope. The model's finite signal and contract interfaces may be reused in further results of the paper.

Selected references

S. A. Yang, N. Bakshi, and C. J. Chen, Trade Credit Insurance: Operational Value and Contract Choice, Management Science 67(2), 2021. DOI.
S. A. Yang, N. Bakshi, and C. J. Chen, Trade Credit Insurance: Operational Value and Contract Choice, authors' accepted manuscript, LBS Research Online eprint 1343, current version December 2019. Repository record.

7 thms2 active usersReviewed

All missions

Approximate Parametric Computation of Minimum-Cost Flows with Convex Costs: Linear Splines of the Marginal Costs with Bounded Step Sizes Give an (α, β)-Approximate Minimum-Cost Flow FunctionResearch Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Skill Acquisition and Data Sales: Under Uncertain Skill Acquisition and Accurate Data, Higher Skill-Acquisition Costs Raise Data Clarity, Data Price and Price InformativenessResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 5

Milestones

Significance

Difficulty

Formalization scope

Selected references

Managing Social Responsibility in Multitier Supply Chains: The Buyer's Optimal Strategy Is Control, Delegation or No Effort, Decided by Thresholds in the Loss-Adjusted Effort CostsResearch Paper

Why responsibility effort matters across tiers

Three firms, effort, and risk

Formalization targets

What the result gives

Where the classification is difficult

Formalization scope

Selected references

Optimal Management of Evolving Hierarchies: Full Transfers to Immediate Predecessors Form the Unique Decentralized Socially Optimal Allocation SchemeResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Managing Self-Replicating Innovative Goods: Characterization of the Optimal Production and Sales Policies under Strong ReplicabilityResearch Paper

Why self-replicating goods

The model

Formalization targets

Goal: Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Supplier Encroachment in a Non-Exclusive Reselling Channel: The Encroaching Supplier May Sell Only Directly at a Positive Direct Cost, or Through Both Channels at a Negative OneResearch Paper

Why encroachment through a shared reseller matters

Setting

Formalization targets

Goal: Proposition 5 (p. 22)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal Short-Termism: The No-Underinvestment and No-Overhang Problems Have the Same Solutions, so Committing to Unlevered Long-Term Effort Rules Out Excessive Short-TermismResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 5

Milestones

Significance

Difficulty

Formalization scope

Selected references

Contracting, Pricing, and Data Collection Under the AI Flywheel Effect: Under Moral Hazard the Firm Collects More (Less) Data Than First Best When the Data Impact Increases (Decreases)Research Paper

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Optimal Team Composition: Diversity to Foster Implicit Team Incentives: The Specialized–Diverse Wage Gap Falls Until Collusion Binds, Then Rises, and Diverse Teams Are Optimal Below S*(δ)Research Paper

Motivation

Setting

Formalization targets

Goal: Proposition 2