Algorithmic Game Theory

Motivation

A service platform makes decisions on two sides of a market. It charges consumers a price and pays independent providers a wage, then earns a margin only when it can match a consumer with a provider. Capacity is another decision available to the platform: it can limit how many matches it will carry, for example by limiting the active provider pool. Hu and Liu ask whether committing to this limit before setting price and wage changes the competitive outcome. Their submitted manuscript models this question for two competing platforms and states a two-sided counterpart of the quantity-precommitment result associated with Kreps and Scheinkman. The point matters for platform operations because a capacity decision can determine the price, wage, volume, and profit that emerge after both platforms react. Hu and Liu, submitted manuscript, §3.5.

Setting

There are two platforms, indexed by $i\in\{1,2\}$; $j$ denotes the other platform. The potential market size is $\Omega>0$. Each platform posts a consumer price $p_i\in\mathbb R$ and a provider wage $w_i\in\mathbb R$. Demand and supply are the positive parts

$$d_i(p)=[\Omega-p_i+\gamma p_j]^+, \qquad s_i(w)=[w_i-\beta w_j]^+,$$

where $[x]^+=\max\{x,0\}$. The demand substitution factor $\gamma$ and the supply substitution factor $\beta$ both lie in $[0,1)$. Higher rival prices raise a platform's demand; higher rival wages reduce its supply. A platform can serve only the smaller of its demand and supply. Its profit without a capacity limit is the margin $p_i-w_i$ times that number of matches. These are the manuscript's displays (1)–(3). Hu and Liu, submitted manuscript, pp. 8–9.

The first game is quantity competition. Each platform chooses a nonnegative matching quantity $z_i$. The prices and wages that clear demand and supply at those quantities are

$$p_i(z)=\frac{(1+\gamma)\Omega-z_i-\gamma z_j}{1-\gamma^2}, \qquad w_i(z)=\frac{z_i+\beta z_j}{1-\beta^2}.$$

A platform earns $(p_i(z)-w_i(z))z_i$. A quantity Nash equilibrium is a nonnegative vector $z$ at which neither platform can gain by choosing any other nonnegative quantity while the rival quantity stays fixed. The inverse price and wage appear in the proof of Lemma 6, where the profit function is written as (F.3). Hu and Liu, submitted manuscript, p. 14 and Online Appendix p. 32.

The second game is capacity precommitment. In stage one, each platform chooses a nonnegative capacity $q_i$, the most matches it can make. In stage two, both platforms simultaneously choose prices and wages. Platform $i$ then serves $m_i=\min\{d_i(p),s_i(w),q_i\}$ matches and earns $(p_i-w_i)m_i$. A second-stage Nash equilibrium lets a platform change its price and wage together. A subgame-perfect equilibrium specifies stage-two play after every admissible capacity vector and requires that no platform benefit from changing its stage-one capacity and then following the continuation for the changed vector. Hu and Liu, submitted manuscript, pp. 14–15 and Online Appendix §A.

Formalization targets

The goal is Proposition 1: capacity precommitment and quantity competition have the same equilibrium price, wage, matching quantity, and profit for each platform. Writing $q,\sigma$ for a capacity profile and its continuation plan, and $z$ for a quantity equilibrium, the target is

$$\forall i\in\{1,2\},\qquad \bigl(p_i(\sigma(q)),w_i(\sigma(q)),m_i(q,\sigma(q)),\pi_i(q,\sigma(q))\bigr) = \bigl(p_i(z),w_i(z),z_i,(p_i(z)-w_i(z))z_i\bigr).$$

The goal also asserts that an equilibrium of each game exists, so this comparison has actual outcomes to compare. Lemma 6 gives the unique quantity equilibrium and its closed forms. The subgame analysis in Online Appendix §A.1 gives a platform's best response to fixed rival price and wage. Lemma 7 states that demand and supply both equal committed capacity in the two-stage equilibrium. These three statements are the mission's milestones. Hu and Liu, submitted manuscript, pp. 14–15 and Online Appendix p. 1.

Significance

Proposition 1 supplies an operational interpretation of quantity competition in a market where each platform controls both consumer price and provider wage. A quantity outcome can arise through an earlier capacity choice followed by ordinary spot-market price and wage decisions. The conclusion covers four separate outcomes for each firm, so it supports comparisons of capacity policies in terms of what consumers pay, what providers receive, how many matches occur, and platform profit. The result is proved in the manuscript; its proofs are in Online Appendix §F of the same cited artifact. Hu and Liu, submitted manuscript, p. 15 and Online Appendix p. 33.

The formalization asks for machine-checked proofs of these known statements under explicit equilibrium conventions. It also creates reusable definitions for a two-sided market with positive-part demand and supply, a quantity game, and a two-stage capacity game. The paper's displayed formulas become auditable statements about every equilibrium of those games rather than numbers inserted into the definition of an outcome. No machine-checked proof of this specific proposition is asserted here.

Difficulty

The central issue is the full two-stage game. A stage-two platform changes price and wage jointly, and a stage-one capacity deviation leads to a new stage-two equilibrium. Checking a price deviation while holding wages fixed, or checking only capacities near a proposed equilibrium, does not establish the proposition. The positive parts in demand and supply also create zero-profit price-and-wage equilibria. Such equilibria can be used as off-path continuations and can change the set of stage-one equilibria. The formal target therefore selects positive profit for each platform whenever a subgame equilibrium permits it. The manuscript's Appendix §A distinguishes several regions of capacity profiles; this regime structure is part of the difficulty of proving a statement about all deviations. Hu and Liu, submitted manuscript, Online Appendix §§A.1–A.2.

Formalization scope

Lean uses Fin 2 for platforms and a named rival map. Prices and wages are real-valued. Capacities and chosen quantities are nonnegative reals. The standing parameters are $\Omega>0$ and $0\le\beta,\gamma<1$; these ranges keep the market-clearing denominators $1-\beta^2$ and $1-\gamma^2$ nonzero. Demand and supply retain the manuscript's positive-part operation even when it is inactive at a positive equilibrium.

A continuation plan maps every capacity profile to a pair of price and wage profiles. At every nonnegative capacity profile it must choose a second-stage Nash equilibrium. For each platform, if that subgame has an equilibrium in which it earns positive profit, the chosen equilibrium must give it positive profit. This includes a subgame in which its rival committed zero capacity. This selection is an explicit addition to the printed equilibrium language, needed because the unqualified statement admits zero-profit off-path punishments. The stage-one Nash condition evaluates a capacity deviation using the continuation plan at the deviated capacity. The manuscript does not specify strategy sets; the stated real and nonnegative domains make them explicit. The goal ranges over equilibria rather than defining outcomes from Lemma 6's closed forms, and it asserts existence to prevent a vacuous comparison.

Contributions can establish the market-clearing identities, the quantity equilibrium and its uniqueness, joint price-and-wage best responses, the capacity-binding result, and the existence and outcome claims of Proposition 1. The generic two-player Nash predicate and the positive-part market model are reusable beyond this mission.

Selected references

• Ming Hu and Yan Liu, Precommitments in Two-Sided Market Competition, submitted manuscript (SSRN 3734828; TSpace), published in Manufacturing & Service Operations Management 25(2), 2023, DOI 10.1287/msom.2022.1173. Mission statements follow the submitted manuscript and its Online Appendix, not the journal pagination.

Motivation

A Fisher market allocates a common supply of items among buyers with separate budgets. When the items form a continuum, such as positions in a measurable interval, a buyer's valuation and the market price are functions rather than finite lists. This is a useful model for divisible resources and for settings in which an allocation can be described as a measurable subset of a continuous item space. Gao and Kroer develop equilibrium and convex-programming results for this setting in Infinite-Dimensional Fisher Markets and Tractable Fair Division. Their Section 6 extends the analysis from linear utility to quasilinear utility, where the buyer subtracts the cost of the allocated bundle from its value.

Quasilinear utility changes the role of money. A buyer can retain an unspent part of the budget and value it outside the market. Consequently, normalizing each buyer's valuation independently, which is harmless for linear demand, changes quasilinear demand. The extension therefore needs its own equilibrium definition and its own pair of optimization programs. This mission concerns the existence and exact equilibrium characterization stated in Theorem 10 of the cited preprint, rather than the numerical algorithms discussed elsewhere in that paper.

Setting

There are $n$ buyers and an item space $\Theta$, a compact subset of $\mathbb R^d$, with restricted Lebesgue measure $\mu$. Buyer $i$ has an integrable, nonnegative valuation density $v_i$ with $\int_\Theta v_i\,d\mu>0$, and a strictly positive budget $B_i$. A bundle is an essentially bounded, nonnegative measurable function $x_i$ on $\Theta$. An allocation $x=(x_i)$ is feasible when $\sum_i x_i\le1$ almost everywhere. A pure allocation assigns almost disjoint measurable sets $\Theta_i$ to buyers, so $x_i=\mathbf1_{\Theta_i}$ almost everywhere; some items may remain unallocated.

A price density $p$ is nonnegative and integrable. The pairing $\langle f,g\rangle=\int_\Theta f(\theta)g(\theta)\,d\mu(\theta)$ gives the value of a bundle and its cost. At price $p$, buyer $i$ chooses an affordable bundle maximizing $\langle v_i-p,x_i\rangle$, with affordability $\langle p,x_i\rangle\le B_i$. A quasilinear market equilibrium (QLME) is a feasible allocation and price at which every buyer makes such a choice and unsold items have zero total price: $\langle p,1-\sum_i x_i\rangle=0$.

The quasilinear Eisenberg–Gale primal program uses a nonnegative variable $\delta_i$ for each buyer and maximizes $\sum_i(B_i\log u_i-\delta_i)$, where $u_i\le\langle v_i,x_i\rangle+\delta_i$. Its dual program minimizes $\langle p,1\rangle-\sum_i B_i\log\beta_i$ subject to $p\ge\beta_i v_i$ and $0\le\beta_i\le1$. The primal is represented by $(x,\delta)$ with $u_i=\langle v_i,x_i\rangle+\delta_i$ at an optimum. This saturated form has the same optimum as the displayed program and makes the optimality conditions unambiguous.

Formalization targets

Theorem 10: attainment and equilibrium

The goal is the full four-part statement. The primal attains its maximum at a pure allocation. The dual attains its minimum with a unique vector $\beta^*$ and price density $p^*=\max_i\beta_i^*v_i$ almost everywhere. For feasible primal and dual points, simultaneous optimality is equivalent to market clearance and

$$\beta_i(\langle v_i,x_i\rangle+\delta_i)=B_i,\qquad \delta_i(1-\beta_i)=0,\qquad \langle p-\beta_i v_i,x_i\rangle=0 \quad\text{for every }i.$$

Finally, $(x,p)$ is a QLME exactly when there are $\delta$ and $\beta$ for which $(x,\delta)$ and $(p,\beta)$ are optimal in the two programs. The same given $p$ must appear on both sides of this equivalence.

Milestone results

The milestones follow the statements in the proof of Theorem 10: attainment of the utility-space program (A.14), uniqueness of the minimizer in the reduced dual program, weak duality (A.15) with its additive constant $\sum_iB_i(\log B_i-1)$, the KKT characterization, and each direction of the QLME equivalence. The earlier paper's Lemma 1 identifies the feasible utility set with utilities of pure allocations and supplies the compactness used here. It belongs to the first mission of this series and is not duplicated as a target in this one.

Significance

The theorem establishes that the two infinite-dimensional programs describe the quasilinear market exactly. Attainment guarantees actual optimal allocation and price objects rather than only approximating sequences. Pure attainment gives a measurable partition-type allocation. The unique $\beta^*$ pins down each buyer's utility price, while $p^*=\max_i\beta_i^*v_i$ identifies the price density almost everywhere. The KKT equations give precise tests for a candidate optimal pair, and the final equivalence translates between optimization solutions and buyer-level equilibrium behavior. These are the claims made by Theorem 10 and its appendix proof.

The result is proved in the paper; the work here is to formalize its statement and, in later solver contributions, its proof in Lean. A complete development will also provide reusable infrastructure for integrating valuation densities against essentially bounded bundles, representing continuum-item allocations, and relating a finite buyer-indexed vector to pointwise price maxima. No machine-checked proof of this mission's goal is supplied with this draft.

Difficulty

The optimization variables include functions in $L^\infty$ and $L^1$, and the positive cone of $L^1$ has no useful interior for a direct appeal to standard infinite-dimensional convex-duality theorems. The finite-dimensional utility vector is easier to optimize over, but recovering a pure allocation from it requires the measurable-allocation result established earlier in the paper. The dual price is a pointwise maximum of integrable densities, and equality of prices is meaningful almost everywhere. Equilibrium demand compares a buyer's assigned bundle with every affordable essentially bounded bundle, so an optimality statement about program variables must account for that full comparison.

Formalization scope

Lean represents densities and bundles as functions on the ambient Euclidean space, with the measure restricted to $\Theta$; values outside $\Theta$ do not matter. The standing hypotheses are compactness of $\Theta$, integrability and almost-everywhere nonnegativity of every $v_i$, strictly positive total valuation, and strictly positive budgets. There is no assumption that total budgets or total item measure equal one. The buyer type Fin n is zero-based; the paper numbers buyers from one. The empty-buyer case is allowed and has the expected trivial finite-vector interpretation.

The equilibrium predicate includes supply feasibility. The printed QLME definition on page 29 omits it, although the linear-market definition includes it and Theorem 10(d) requires it. Without it, a buyer can receive more than unit supply on part of the item space while buyer optimality and market clearance still hold. The primal uses the saturated value $u_i=\langle v_i,x_i\rangle+\delta_i$; leaving $u$ free below that value makes the printed KKT converse false. These two choices are disclosed in the item descriptions and moderation notes, with concrete counterexamples there.

The paper treats $\log0$ as a limiting infinite cost. Lean's real logarithm is total, so optimality compares only points whose logarithm arguments are positive. The utility KKT equation is multiplied by $\beta_i$ to avoid division by zero. Valuation and price densities are integrable, and bundles are essentially bounded, so pairings are genuine finite integrals. The pointwise maximum over buyers is an indexed supremum; feasibility and uniqueness use almost-everywhere equality for price functions and exact equality for the finite vector $\beta$. These conventions prevent degenerate total-function values from deciding the theorem.

Contributions can address the measurable utility-set and pure-allocation infrastructure, finite-dimensional attainment, weak duality, the equality conditions, or the demand comparison. The intermediate milestones are stated at the strength used in the paper; the goal contains the entire four-part result.

Selected references

• Yuan Gao and Christian Kroer, Infinite-Dimensional Fisher Markets and Tractable Fair Division, preprint arXiv:2010.03025v5, 2021; published in Operations Research, 2023. arXiv preprint.

Motivation

In reward-based crowdfunding, a seller asks customers to pay before the product's quality is known to them. A high-quality seller can try to communicate private quality through the prices he posts. That signal is costly because a price that deters imitation may also reduce the seller's own expected revenue. Bolandifar, Chen, Kouvelis and Zhou study this tradeoff when a campaign must meet a financing target and a successful campaign leads to a later retail period (SSRN manuscript, §§3–5). Their model asks whether a high-quality seller can separate himself from a low-quality seller by committing in advance to both the crowdfunding price and the later retail price.

The manuscript treats price commitment separately from the case in which the seller chooses the retail price after the campaign. This mission concerns the commitment case, specifically Proposition 2 and the lemmas that support it. The theorem describes a separating equilibrium after applying the intuitive criterion: the high-quality seller chooses a lower crowdfunding price and a higher retail price than he would under full information. The cited artifact is the authors' SSRN manuscript dated 2022-05-30; its proofs are in Appendix A (manuscript, pp. 38–43).

Setting

There are two privately known product qualities, $0<q_L<q_H$. A seller commits to a price pair $x=(P_1,P_2)$, where $P_1$ is paid by crowdfunding backers and $P_2$ is charged in the regular selling period. The project needs a financing target $T>0$, so a feasible pair satisfies $P_1\ge T$ and $P_2>0$. Both period market sizes are normalized to one; production and salvage costs are zero, and future revenue is not discounted (manuscript, pp. 9–13).

All funding customers have the same taste $\theta_c$, uniformly distributed on $[0,1]$ and unknown to the seller. They believe quality is $q_j$ and back the campaign when $\theta_c q_j\ge P_1$. Thus success has probability $\max\{0,1-P_1/q_j\}$. After a successful campaign, true quality $q_i$ becomes known. A fraction $\alpha\in(0,1)$ of regular customers have the same taste as the funding customers; success updates their conditional taste distribution. The remaining fraction has independent uniform tastes. A customer in the regular period buys if taste times $q_i$ is at least $P_2$ (manuscript, pp. 10–11).

Write $\Pi^{ij}(P_1,P_2)$ for the seller's expected total profit when true quality is $q_i$ and customers believe $q_j$. The expressions $V^{ij}$ and $W^{ij}$ distinguish the regions in which returning customers buy for sure or with a conditional probability. Write $\Pi^{ij*}$ for the maximum of $\Pi^{ij}$ over feasible pairs. In particular, $\Pi^{L*}=\Pi^{LL*}$ is the low type's full-information payoff. These are outcomes of optimization, not inserted formulas (manuscript, pp. 22–24, (7)–(11)).

In a separating equilibrium, the two seller types choose different feasible pairs $x_H$ and $x_L$. Funding customers believe the product is high quality exactly at $x_H$ and low quality at every other pair, including off-path pairs. Neither seller type can gain by deviating under those beliefs. The intuitive criterion then checks whether an off-path pair would be profitable to the high type if believed high while being unattractive to the low type (manuscript, pp. 13, 19).

Formalization targets

Lemma 4 identifies an attained full-information optimum for any choice of true and believed quality in $\{q_L,q_H\}$. Its crowdfunding price is

$$P_1^{ij*}=\max\left\{\frac{4q_j-(1-\alpha)q_i}{8},T\right\},$$

and its retail price follows the three cases of equation (11), depending on whether $T$ lies below $q_j/2$, between that threshold and $q_j/[2(1-\alpha)]$, or above the second threshold (manuscript, p. 23, Lemma 4).

The goal is Proposition 2 in the small-quality-gap regime $q_L<q_H\le(\alpha^2+6\alpha+25)q_L/16$. Define $(\dot P_1,\dot P_2)$ by its equations, requiring $\dot P_2>q_H/2$:

$$4\dot P_1+(1-\alpha)\dot P_2=2q_H,\qquad W^{LH}(\dot P_1,\dot P_2)=\Pi^{L*}.$$

When $T\le\dot P_1$, the goal states that the unique separating equilibrium surviving the intuitive criterion has $x_H=(\dot P_1,\dot P_2)$ and the low type at his full-information optimum. Relative to every full-information optimum $(P^H_{1f},P^H_{2f})$ of the high type, it also states

$$\dot P_1<P^H_{1f},\qquad \dot P_2>P^H_{2f}.$$

The mission separately targets uniqueness of the dotted pair, the first claim of Lemma 6 concerning profitable imitation of the high type's full-information pair, and the constrained optimum in equations (A.13)–(A.14) (manuscript, pp. 26–27, 41).

Significance

The result identifies how a commitment to the later price changes the signal available during crowdfunding. The high type's retail price is raised while his crowdfunding price is lowered, so the signal is encoded in the pair, rather than in a single crowdfunding price. The theorem also determines which separating outcome survives a refinement intended to remove equilibria supported only by arbitrary off-path beliefs (manuscript, pp. 26–27).

The mathematical result is already proved in the manuscript. The remaining formalization work is to give the economic model an exact Lean meaning, prove the optimization and equilibrium assertions, and make the boundary conventions explicit. The five open Lean theorems in this proposal are statements to be proved; their sorry bodies are not machine-checked proofs.

Difficulty

The seller's payoff changes expression when the regular price crosses a threshold determined by the funding price and the two qualities. The low type can mimic a pair whose regular price exceeds $q_L$, in which case regular sales vanish but the crowdfunding payoff can still rise. This makes a direct comparison of the printed $W^{LH}$ expression with the actual mimicking payoff invalid outside its demand region. The intuitive criterion adds a second layer: it tests deviations under a different belief from the default off-path belief. These regime changes and belief-dependent deviations are the central obstacles to a concise, faithful Lean statement (manuscript, pp. 23, 26–27, 41–43).

Formalization scope

Lean represents qualities, prices, probabilities and payoffs as real numbers. Its parameter structure contains $q_L,q_H,\alpha,T$, with $0<q_L<q_H$, $0<\alpha<1$ and $T>0$. The prior high-quality belief is omitted because the separating statements use beliefs fixed by the observed pair. Market sizes, zero costs, salvage value and discount rate are incorporated into the payoff. The funding success probability and purchase probabilities are clipped at zero outside their printed domains. The printed $V^{ij}$ and $W^{ij}$ remain available for the page 41 equations; $W^{ij}$ is only used away from its zero denominator. Suprema range over all feasible pairs $P_1\ge T$, $P_2>0$, and “optimal” means the displayed pair attains that supremum.

The manuscript's Proposition 2 needs the additional bound $T\le(3+\alpha)q_L/8$. Without it, the low type's constrained full-information payoff can be too small and he can profitably mimic a dotted pair with $\dot P_2>q_L$; a numerical counterexample and the discrepancy are recorded in the local moderation notes. This proposal states that bound openly rather than treating the printed proposition as valid for all $T\le\dot P_1$. Lemma 4 also records its displayed domain $T\le q_j$. The goal does not define the optimum by a formula, the equilibrium by the paper's necessary conditions (13)–(14), or the dotted pair by an arbitrary choice.

The foundational setting is a reusable two-type, two-price payoff and equilibrium model. A complete development must establish the payoff's agreement with the manuscript's regions, attainment and comparison of the full-information optima, uniqueness of the dotted pair, optimization on the relevant iso-profit curve, and the no-deviation and intuitive-criterion conclusions. Contributions proving these targets or reusable real optimization lemmas are within scope.

Selected references

• E. Bolandifar, Z. Chen, P. Kouvelis and W. Zhou, Quality Signaling through Crowdfunding Pricing, SSRN manuscript 3689946, 2022-05-30, SSRN. Published as Manufacturing & Service Operations Management, doi:10.1287/msom.2022.1177.

Motivation

After a sudden-onset disaster, humanitarian organizations (HOs) raise most of their response budget from private donors within days. Donors increasingly earmark their gifts, restricting them to a region, a program or a type of expense. Earmarking makes an appeal more attractive to a donor but lowers the share of each dollar that the HO can deploy immediately. Aflaki and Pedraza-Martinez (SSRN 3705595, published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1202) model how HOs set earmarking and fundraising effort under three institutional arrangements: competition, full collaboration (a coalition that fundraises and decides as one), and partial collaboration, in which HOs pool the cost of reaching donors on a common platform while each donor still chooses which HO to give to. Joint appeals such as the UK's Disasters Emergency Committee are of the last kind.

This mission formalizes the paper's equilibrium result for partial collaboration (Proposition 4): equilibria exist, equilibrium earmarking is determined by first-order conditions that do not involve the efforts, and only the HOs with the largest required funding relative to their unit performance pay for the platform, while the others free-ride.

Setting

There are $n \ge 1$ HOs $i \in I = \{1, \dots, n\}$. HO $i$ chooses a base utility $s_i \in [a_i, b_i]$, the attractiveness to donors that its earmarking level induces, and an effort $x_i \in [0, 1]$, the fraction of donors it pays to contact, at cost $C_i(x_i)$. Its unit performance $\delta_i(s_i) \in (0, 1]$ is the fraction of each donated dollar usable now, and $B_i > 0$ is its required funding. The mean donation is normalized to $1$.

Pooled effort reaches $\bar x = \min\left(\sum_{i \in I} x_i, 1\right)$ donors. A contacted donor gives to HO $i$ with the multinomial-logit probability

$$\theta^p_i(s) = \frac{e^{s_i}}{1 + \sum_{j \in I} e^{s_j}},$$

the $1$ being the option of not donating, so HO $i$ expects donations $\bar x\,\theta^p_i(s)$ and achieves total performance $\delta_i(s_i)\,\bar x\,\theta^p_i(s)$, of which only $\min(\cdot, B_i)$ is useful. HO $i$ is lexicographic (problem (10)): given the other HOs' strategies, it first minimizes its funding gap $\left(B_i - \delta_i(s_i)\bar x\theta^p_i(s)\right)^+$ over $[a_i, b_i] \times [0,1]$; among the gap minimizers it maximizes its utility $\min\left(\delta_i(s_i)\bar x\theta^p_i(s), B_i\right) - C_i(x_i)$; and an HO that is still indifferent picks a strategy maximizing its unconstrained total performance $\delta_i(s_i)\bar x\theta^p_i(s)$. A Nash equilibrium is a profile $(s, x)$ in the product of the boxes at which every HO's strategy is such a best response. Finally,

$$\alpha^p_i(s) = \min\left(\frac{B_i}{\delta_i(s_i)\,\theta^p_i(s)}, 1\right)$$

is the reach HO $i$ needs to close its own gap.

Formalization targets

Goal: Proposition 4

A pure Nash equilibrium exists. For every profile $(s, x)$ in the box, labelled so that $\alpha^p_1(s) \ge \dots \ge \alpha^p_n(s)$, with $\bar k = \#\{i : \alpha^p_i(s) = \alpha^p_1(s)\}$: $(s, x)$ is an equilibrium if and only if (i) for every $i$ there are $\lambda^p_{i1}, \lambda^p_{i2} \ge 0$ with

$$\frac{\delta_i'(s_i)}{\delta_i(s_i)} + \frac{\partial \theta^p_i(s)/\partial s_i}{\theta^p_i(s)} + \lambda^p_{i1} - \lambda^p_{i2} = 0, \quad \lambda^p_{i1}(a_i - s_i) = 0, \quad \lambda^p_{i2}(s_i - b_i) = 0, \tag{11}$$

and (ii) $\sum_{i=1}^{\bar k} x_i = \alpha^p_1(s)$ and $x_{\bar k+1} = \dots = x_n = 0$.

Milestones

1. (S11): $(s, x)$ is an equilibrium iff each $s_i$ maximizes $\sigma \mapsto \delta_i(\sigma)\theta^p_i(\sigma, s_{-i})$ on $[a_i, b_i]$ and $x_i = \left(\alpha^p_i(s) - \sum_{j \ne i} x_j\right)^+$.
2. Log-concavity: $\sigma \mapsto \delta_i(\sigma)\theta^p_i(\sigma, s_{-i})$ is log-concave on $[a_i, b_i]$.
3. Total effort: every solution of $x_i = (\alpha_i - \sum_{j \ne i} x_j)^+$ with $\alpha$ sorted decreasingly has $\sum_i x_i \ge \alpha_1$.
4. Effort system: for $1 \ge \alpha_1 \ge \dots \ge \alpha_n \ge 0$ and $x \in [0,1]^n$, that system holds iff $\sum_{i \le \bar k} x_i = \alpha_1$ and $x_i = 0$ for $i > \bar k$.

Significance

The proposition separates the two decisions. Equilibrium earmarking solves each HO's own first-order condition (11) and does not depend on anyone's effort, because the pooled reach multiplies every HO's donations by the same factor. Equilibrium effort is a pure coordination outcome: the platform is funded exactly up to the largest required reach $\alpha^p_1$, and only the HOs attaining it contribute. The paper uses these facts to compare earmarking and performance across the three arrangements (its Propositions 5 and 7), and the free-riding structure is what drives the comparison of partial collaboration with competition.

The result is proved in the paper's Online Supplement (pp. S13–S14). No machine-checked version exists. The mission asks for a Lean proof of the proposition as stated, with the equilibrium defined from the HOs' lexicographic problem rather than from its characterization; the effort-system milestones are self-contained statements about a piecewise-linear fixed-point system and are reusable for other pooled-contribution games.

Difficulty

The obvious argument, "each HO maximizes $\delta_i\theta^p_i$, and the rest is bookkeeping", skips the case analysis behind (S11). Whether HO $i$'s gap can be closed depends on the others' efforts. When the others' pooled effort already covers HO $i$'s requirement, HO $i$'s gap and utility no longer depend on its base utility. Only the third, tie-breaking level of the best response then pins $s_i$ down, and without it (11) is false. The existence part needs a fixed point of the base-utility best-response map on $\prod_i [a_i, b_i]$; when HO $i$'s best response is not unique, that map is not even a function. In part (ii), the effort system $x_i = (\alpha_i - \sum_{j \ne i} x_j)^+$ is not a contraction, and the paper's proof by successive elimination of indices is informal.

Formalization scope

HOs are Fin n with 0-based indices, so $\alpha^p_1$ is the value at index 0, and [NeZero n] is assumed. Strategies are in base-utility coordinates: $\delta_i : \mathbb R \to \mathbb R$ is a primitive function of $s_i$, as in the paper's problem (10). The earmarking coordinates are not modelled. All definitions live in one Setting structure with a Standing predicate, which every theorem assumes:

• $a_i \le b_i$ and $B_i > 0$;
• $C_i$ is nonnegative and strictly increasing on $[0,1]$;
• on an open interval containing $[a_i, b_i]$, $\delta_i$ is positive, differentiable and concave;
• $\delta_i \le 1$ on $[a_i, b_i]$.

$B_i > 0$ is implicit in the paper; with all $B_i = 0$ every base utility is an equilibrium strategy. Concavity of $\delta_i$ is used by the paper's proof. The HO problem (10) is printed with decision $(s_i, \bar x)$ and cost $C^p(\bar x)$. It is encoded with HO $i$'s own effort $x_i$ and own cost $C_i(x_i)$, the reading used by the paper's proof and by part (ii). The paper's "without loss of generality" ordering is the hypothesis that $\alpha^p(s)$ is antitone in the index, and $\bar k$ is the number of entries tied with the first; this gives $\bar k = n$ when all tie. Partial derivatives are Mathlib deriv of $t \mapsto \theta^p_i(s \text{ with } s_i := t)$. Every function differentiated is differentiable at the point by Standing. The pure-algebra milestones 3–4 use no game objects.

The equilibrium must not be defined by (S11) or (11); that would make the goal a tautology. The Setting defines it as the three-level lexicographic best response over the full strategy box, and (S11) is a milestone to be proved. A sorry-free check that the standing hypotheses hold for the paper's numerical primitives ($\delta_i(s) = 1 - s/4$, $C_i(x) = x/10$, $[a_i, b_i] = [0,1]$, $B = (0.2, 0.3)$) accompanies the draft.

A full development needs: KKT conditions for a differentiable concave function on a compact interval (including the degenerate interval $a_i = b_i$); log-concavity of the logistic share; a continuous-maximum (Berge-type) argument and Brouwer's fixed-point theorem on a product of intervals; and the algebra of the effort system. Contributions of the interval-KKT lemma and of the effort-system lemmas are welcome as separate theorems.

The source is the authors' SSRN version (abstract 3705595, dated December 2022); all proofs are in its Online Supplement, Section S3.

Selected references

• A. Aflaki, A. J. Pedraza-Martinez, Competition and Collaboration on Fundraising for Short-Term Disaster Response: The Impact on Earmarking and Performance, SSRN 3705595, version of December 2022. https://ssrn.com/abstract=3705595
• A. Aflaki, A. J. Pedraza-Martinez, same title, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2023.1202

Fundraising competition after a disaster

In the days after a sudden-onset disaster, several humanitarian organizations (HOs) appeal to the same pool of donors. Donors increasingly want to earmark their gifts (restrict them to a programme, region or item), and HOs can offer more or less of that control. Earmarked money is less useful in the response: renegotiating restrictions costs time and overhead, so each dollar delivers less immediate relief. HOs therefore face a trade-off between attracting donors and using donations well, and they face it while competing with each other for the same donors.

A. Aflaki and A. J. Pedraza-Martinez model this trade-off as a game among HOs whose donors choose by a multinomial logit (MNL) rule, and compare three regimes: competition, full collaboration and partial collaboration (SSRN 3705595, December 2022; published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2023.1202). This mission formalizes the equilibrium result for the competition regime, Proposition 1 of the paper. The source is the SSRN version dated December 2022; its proofs are in the bound-in Online Supplement (§S3).

The competition game

There are $n \ge 1$ HOs $i \in I = \{1, \dots, n\}$. HO $i$ chooses two numbers:

• a base utility $s_i \in [a_i, b_i]$ that it offers donors (in the paper, a monotone reparametrization of its earmarking level, used from problem (6) on);
• a fundraising effort $x_i \in [0,1]$, the fraction of donors it contacts, at cost $C_i(x_i)$ with $C_i : [0,1] \to \mathbb R_+$ strictly increasing.

Each dollar HO $i$ receives produces $\delta_i(s_i)$ dollars of immediate relief, the unit performance. HO $i$ needs $B_i > 0$ dollars of effective funding. Donors have mean budget $z > 0$.

A donor contacted by the set $J$ of HOs gives HO $i \in J$ the MNL share

$$\theta^J_i(s) = \frac{e^{s_i}}{1 + \sum_{j\in J} e^{s_j}}, \tag{4}$$

the $1$ standing for not donating. Contacts are independent, so with $w^a_i = \prod_{j \ne i} x_j^{a_j}(1-x_j)^{1-a_j}$ for $a \in A_i = \{a \in \{0,1\}^n : a_i = 1\}$ and $J_a = \{j : a_j = 1\}$, HO $i$'s expected donations are

$$\mathbb E[D_i(s;x)] = z\, x_i \sum_{a\in A_i} w^a_i\, \theta^{J_a}_i(s). \tag{5}$$

The unit performance per donor contacted is $PPD_i(s;x) = \delta_i(s_i)\, z \sum_{a\in A_i} w^a_i\, \theta^{J_a}_i(s)$; it does not depend on $x_i$.

Each HO is lexicographic (problem (6)): given the others' strategies, it first minimizes its funding gap $(B_i - \delta_i(s_i)\mathbb E[D_i(s;x)])^+$ over $[a_i,b_i]\times[0,1]$, and among the minimizers it maximizes

$$U_i(s_i,x_i) = \min\big(\delta_i(s_i)\mathbb E[D_i(s;x)],\, B_i\big) - C_i(x_i).$$

A Nash equilibrium is a profile $(s;x) \in \prod_i [a_i,b_i]\times[0,1]^n$ in which every HO's strategy solves its problem (6).

Assumption 1 (p. 16) asks that $\log\delta_i$ be sufficiently concave: $\partial^2 \log\delta_i(s_i)/\partial s_i^2 \le -\tfrac14 + e^{s_i}/(1+e^{s_i})^2$ on $[a_i,b_i]$.

Formalization targets

Goal: Proposition 1 (p. 16)

Under the standing hypotheses and Assumption 1, a Nash equilibrium exists, and a profile in the strategy box is an equilibrium if and only if for every $i$

$$x_i = \min\Big(\frac{B_i}{PPD_i(s;x)},1\Big),\qquad \frac{\delta_i'(s_i)}{\delta_i(s_i)} + \frac{\sum_{a\in A_i} w^a_i\,\partial\theta^{J_a}_i(s)/\partial s_i}{\sum_{a\in A_i} w^a_i\,\theta^{J_a}_i(s)} + \lambda_{i1}-\lambda_{i2} = 0,$$

with $\lambda_{i1},\lambda_{i2}\ge 0$, $\lambda_{i1}(a_i-s_i) = 0$ and $\lambda_{i2}(s_i-b_i) = 0$ (system (7)).

Milestones

1. Lemma 2 (p. 15): $\mathbb E[D_i]$ is nondecreasing in $x_i$ and $s_i$ and nonincreasing in $x_j$, $s_j$ for $j\ne i$.
2. Claim (S5) (p. S10): HO $i$'s strategy solves (6) iff $s_i$ maximizes $PPD_i$ over $[a_i,b_i]$ and $x_i = \min(B_i/PPD_i,1)$.
3. (S8) (p. S12): $\partial^2 \log\big[\sum_{a} w^a_i\theta^{J_a}_i(s)\big]/\partial s_i^2 \le \tfrac14 - e^{s_i}/(1+e^{s_i})^2$ for efforts in $[0,1]$.
4. Log-concavity (p. S12): under Assumption 1, $s_i \mapsto PPD_i$ is log-concave on $[a_i,b_i]$.

Significance

Proposition 1 is the foundation of the paper's comparison of fundraising regimes: Propositions 2, 5, 6 and 7 compare equilibria characterized by (7) with the full- and partial-collaboration outcomes, and the numerical study of the Haiti response (§8) computes equilibria by solving (7). The proposition reduces a two-level game with a non-smooth objective to a per-HO KKT system plus a closed-form effort, and it shows that equilibrium earmarking balances the relative loss in unit performance against the relative gain in donor share.

The result is proved on paper, in the Online Supplement; no machine-checked version exists. Formalizing it would check the reduction from the lexicographic problem to (S5), which hinges on $B_i>0$ and strictly increasing costs, and supply a sound proof of the bound (S8), whose printed derivation is loose (see below). The log-mixture-of-logit bound (S8) and the lexicographic best-response reduction are reusable for other MNL competition models.

Difficulty

The central difficulty is (S8). Each single share $\theta^J_i$ is log-concave in $s_i$, but a mixture of log-concave functions is not log-concave in general, so concavity of $\log\sum_a w^a\theta^{J_a}$ fails and only the weaker, $s_i$-dependent bound (S8) holds. The printed argument passes through a quasi-concavity step and a termwise inequality that do not combine as written; a correct argument must control the variance-like term of the mixture uniformly in the weights. Numerical tests on random instances support (S8).

Existence is a fixed-point argument, but Assumption 1 with "$\le$" yields only concavity, so best responses in $s_i$ can be intervals rather than points, and a single-valued map need not exist. The correspondence is convex-valued, which is where the obvious Brouwer argument needs adjustment.

The reduction (S5) requires handling both regimes of the lexicographic problem: the gap can be closed (effort $B_i/PPD_i$, minimal cost) or cannot (full effort).

Formalization scope

HOs are Fin n. The paper's sum over $a\in A_i$ is a sum over finite sets $J$ with $i\in J$; $w^a_i$ is the product of $x_j$ over $J\setminus\{i\}$ and of $1-x_j$ over $j\notin J$. All statements live in base-utility coordinates: $\delta_i:\mathbb R\to\mathbb R$ is a primitive function of $s_i$ (earmarking $e_i$ and the map $s_i(e_i,\delta_i(e_i))$ are not modelled), and expected donations are the formula (5) (Lemma 1's Gumbel derivation is not formalized).

The standing hypotheses, collected in one predicate, are: $n\ge1$; $a_i\le b_i$; $B_i>0$; $z>0$; $C_i\ge0$ and strictly increasing on $[0,1]$; $\delta_i$ twice continuously differentiable on $\mathbb R$ with $0<\delta_i\le1$ on $[a_i,b_i]$. The additions relative to the page are $B_i>0$ (without it every $s_i$ is a best response and the "only if" fails), $z>0$, $\delta_i>0$ (needed for $\log\delta_i$ and $B_i/PPD_i$), and smoothness on all of $\mathbb R$ rather than on $[a_i,b_i]$. Assumption 1 is a separate predicate, assumed only by the goal and the log-concavity milestone. Derivatives are Mathlib's deriv; $\partial\theta^{J}_i/\partial s_i$ is the derivative of $t\mapsto\theta^J_i(s_{-i},t)$.

The equilibrium is defined as the lexicographic best response of problem (6) over the full strategy box, never by (7), (S5) or an argmax of $PPD_i$; with any of those as the definition the goal would be trivial. Multipliers are existential. Uniqueness of the equilibrium is not claimed.

Welcome contributions: proofs of the milestones, a reusable lemma that the KKT conditions characterize maximizers of a concave differentiable function on a closed interval, and Kakutani-type existence for convex-valued best responses.

Selected references

• A. Aflaki, A. J. Pedraza-Martinez, Competition and Collaboration on Fundraising for Short-Term Disaster Response: The Impact on Earmarking and Performance, SSRN 3705595, version of December 2022. https://ssrn.com/abstract=3705595
• A. Aflaki, A. J. Pedraza-Martinez, same title, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2023.1202
• D. McFadden, Conditional logit analysis of qualitative choice behavior, in Frontiers in Econometrics, 1973.

Motivation

Electric-vehicle makers such as NIO sell cars without the battery and lease the battery separately, a business model called Battery as a Service (BaaS). The leased battery can be swapped at a station in minutes, so a customer is not tied to one battery size: a driver who leases a small battery for the daily commute can rent a large one for a long holiday trip, and a driver who leases a large battery can downgrade for a while and pay less. Shi and Hu (M&SOM 2024, doi:10.1287/msom.2022.0587) ask whether such flexible battery leasing is good for all three parties at once: the manufacturer (profit), the customers (total cost) and the environment (total battery capacity that has to be produced). A business-model innovation of this kind is adopted only if it improves profit; it is defensible publicly only if it does not raise customer cost or the number of batteries in circulation. The paper's answer is a "win-win-win" region of parameters, and that result is the goal of this mission.

Setting

A manufacturer serves a unit mass of customers with two batteries. The low-capacity battery has range $r_l=0$, lease rate $p_l=0$ and acquisition cost $c_l=0$ (normalizations). The high-capacity battery has range $r_h$, lease rate $p_h$ and incremental acquisition cost $c_h$. Driving a distance beyond the battery's range costs the customer the shortfall: a need $x$ served by range $r$ costs $(x-r)^+$ plus the lease rate.

Each customer has a regular need $d\sim\mathcal U[0,1]$, known when choosing a primary battery, and a peak need $D\sim\mathcal U[0,a]$ with $a>1$, independent of $d$ and learned later. A fraction $\rho$ of the time is regular usage, $1-\rho$ peak usage. The standing assumptions are $a>1$, $a/(2+a)<\rho<1$, $0<r_h\le a$ and $0\le c_h\le(1-\rho)a$.

Simple leasing. The manufacturer sets $p_h$; each customer leases low capacity iff $\rho d+(1-\rho)\mathbb E[D]\le p_h+\rho(d-r_h)^++(1-\rho)\mathbb E[(D-r_h)^+]$. With $\tau^b$ the low-capacity volume, the profit is $\Pi^b=(1-\tau^b)(p_h-c_h)$, the total customer cost $CT^b$ is the integral over $d$ of the cost each customer bears, and the total battery capacity is $BT^b=(1-\tau^b)r_h$.

Flexible leasing. A two-period game. The manufacturer sets $p_h$; customers choose primary batteries anticipating the peak period; the manufacturer then sets an upgrade rate $\bar p_h$ and a downgrade rate $\bar p_l$; customers learn $D$ and choose whether to swap according to Table 1 of the paper (a low lessee pays $(D-r_h)^++\bar p_h$ after upgrading, a high lessee pays $D+\bar p_l$ after downgrading). Upgrades $U$ in excess of downgrades $V$ must be met by buying $Q_h=[U-V]^+$ extra high-capacity batteries. The peak-period objective is (1): $(1-\tau)p_h+V(\bar p_l-p_h)+U\bar p_h-c_hQ_h/(1-\rho)$, and the total profit is (2): $\Pi^f=\rho(1-\tau)p_h+(1-\rho)\cdot(1)-(1-\tau)c_h$. A flexible equilibrium is a lease rate $p_h$ with optimal peak rates, a lease volume $\tau$ that customers rationally expect, and a profit no other lease rate and continuation can beat. $CT^f$ is the total expected cost of the customers' choices, and $BT^f=(1-\tau+Q_h)r_h$.

Formalization targets

Write $c_0=a(1-\rho)/2$; by Proposition 2 this is the cost at which the manufacturer stops buying extra batteries.

Goal: Proposition 6 (win-win-win)

For $a>1$, $a/(2+a)<\rho<1$:

1. if $\rho<7a/(8+7a)$, there is $\delta>0$ such that for each $c_h\in(c_0-\delta,c_0)$ there is $R<a$ such that for all $r_h\in(R,a]$, a benchmark optimum and a flexible equilibrium exist, and every pair of them satisfies

$$Q^f_h>0,\qquad \Pi^b<\Pi^f,\qquad CT^f<CT^b,\qquad BT^f<BT^b;$$

2. there is $\delta>0$ such that for each $c_h\in(c_0,c_0+\delta)$ there is $R<a$ such that for all $r_h\in(R,a]$, the same holds with $Q^f_h=0$.

Milestones

Lemma 1 and Proposition 1 (the benchmark), Lemma 2 (peak volumes), Lemma 3 (optimal peak rates), Lemma 4 (flexible lease volume), Proposition 2 in its first case (the flexible equilibrium for $c_h<c_0$), Proposition 4 near the corner $(r_h,c_h)=(a,c_0)$ (customer cost), and Proposition 5 in its first bullet (capacity is smaller iff $\rho<7a/(8+7a)$ and $c_h\le T(r_h)$ for an explicit $T$).

Significance

The result identifies conditions under which a pricing innovation helps the firm, its customers and the environment at the same time: a battery cost near $a(1-\rho)/2$ and a high-capacity range close to the largest peak need. Flexible leasing reallocates high-capacity batteries from customers who do not need them in the peak period to customers who do, so fewer batteries have to be produced. But the manufacturer prices the up/downgrade options to extract the efficiency gain and may buy extra batteries, so lower customer cost and lower capacity are not automatic. Proposition 6 states where all three improvements coexist.

The paper proves its results by calculus on closed forms. Nothing here is machine-checked yet. A formalization adds three things. First, it derives the closed forms from the model itself (customer choices from Table 1, volumes as measures of customer sets, equilibria as maximizers), where the paper states them. Second, it settles which reading of "sufficiently close" and "sufficiently large" is true. Third, it records the regimes in which the intermediate lemmas hold, which the printed statements leave implicit.

Difficulty

The closed forms of Lemmas 1–4 are routine integrals of piecewise-linear functions. The difficulty is global optimality and the corner analysis.

• Equilibrium is global. A flexible equilibrium must beat every lease rate together with every rationally expected continuation, including continuations in the regime where the manufacturer buys no extra batteries and at lease rates where customers all lease one type. A first-order condition on one regime does not establish this.
• The $Q^f_h=0$ side is not the printed one. For $c_h$ just above $c_0$ the equilibrium is a kink regime that the paper does not describe. The paper's second-case formulas in Proposition 2 are not the equilibrium there, so the goal's second branch cannot be obtained from them.
• Order of limits. At the corner $(r_h,c_h)=(a,c_0)$ the two capacities coincide. Profit and customer cost are strictly better under flexible leasing there, but capacity is only weakly better. The capacity comparison holds only when $r_h$ approaches $a$ after $c_h$ is fixed.

Formalization scope

The model is the paper's base model of §3–§4: flexible leasing introduced into an existing BaaS program with independent regular and peak needs. The extensions of §5 (correlated needs, range choice, launching with flexible leasing) and the numerical calibration (§4.1, Figures 2–5) are out of scope.

Representation. All parameters are real numbers. Expectations over $D\sim\mathcal U[0,a]$ are interval integrals divided by $a$; volumes of customers are Lebesgue measures of subsets of $[0,1]$. Every volume, expected cost and equilibrium is defined from the model; the paper's closed forms are theorems, never definitions. Customers lease low when indifferent, upgrade on $\le$ and downgrade on $>$, following the proofs. The lease rate ranges over all of $\mathbb R$; the paper's remark "we require $p_h<\min(1,r_h)$" is not imposed, because the benchmark optimum can exceed 1. The peak rates range over the set $\bar p_h\le a$, $p_h-a\le\bar p_l\le p_h$ that the paper requires (p. 13). An equilibrium is optimal against every continuation at every lease rate.

Readings and added hypotheses.

• Proposition 6 is posed as "$c_h$ sufficiently close to $c_0$, then $r_h$ sufficiently large". A single neighbourhood of $(a,c_0)$ in both variables is false on both sides. On the $Q^f_h>0$ side, Proposition 5's threshold $T(r_h)$ equals $c_0$ at $r_h=a$ and is below it for $r_h<a$. The point $c_h=c_0$ is excluded.
• Each branch of the goal asserts existence of a benchmark optimum and a flexible equilibrium, so it is not vacuous. A goal of the form "every equilibrium is win-win-win" without existence would be trivially true where no equilibrium exists, and is ruled out.
• Lemma 2's interior cases hold with $r_h$ in place of $a$ (and $\bar p_h\ge0$). The statement also gives the missing outer cases for rates below zero or beyond $r_h$, covering every real rate.
• Lemma 3 is posed in the regime $\tau>c_h/(a(1-\rho))$, the only one in which its acquisition quantity is nonnegative. Its rates are assumed to lie below $r_h$.
• Lemmas 1, 4 and Propositions 1, 2, 5 carry the proofs' interior conditions as explicit parameter inequalities: the indifferent customer lies below $r_h$, and Proposition 1's range for $c_h$ holds.
• Proposition 5(i) is the $\le$ form, as in its proof. Proposition 4 is posed in its corner-neighbourhood clauses only.
• Proposition 2's second case, Proposition 3 and the remaining clauses of Propositions 4–5 are not posed: the second case of Proposition 2 is false on part of its range, and Proposition 3's threshold is garbled in the manuscript.

What a complete development needs. Lebesgue measure of intervals, interval integrals of piecewise-linear functions, and maximization of concave quadratics with a kink. It also needs the kink-regime equilibrium on the $Q^f_h=0$ side and continuity arguments at the corner. Lemmas 1–4 are reusable for any variant of the model, and proofs of the milestones in any order are welcome.

Selected references

• L. Shi and B. Hu, Battery as a Service: Flexible Electric Vehicle Battery Leasing, Manufacturing & Service Operations Management, Frontiers in Operations, 2024. Read as the authors' manuscript of 13 January 2024. https://doi.org/10.1287/msom.2022.0587

Why continuum Fisher markets matter

A Fisher market divides a supply of goods among buyers with fixed budgets. In a finite market, each good is a separate coordinate. Fair division can instead involve a continuum of items, such as locations along an interval or points in a region, where a buyer's valuation varies measurably from point to point. Finite dimensional existence and duality arguments do not automatically apply: the allocation is now a function, and the feasible set need not be compact in its natural function space. Gao and Kroer formulate a market and two Eisenberg–Gale programs for this setting, then prove that their optima exist and characterize equilibrium Gao and Kroer, §3.

The result also connects market equilibrium to fair division. A pure allocation assigns measurable regions of the item space to buyers, allowing overlap only on null sets. Existence of a pure optimizer means that a market outcome can be represented by such a division, rather than by fractional shares at each item. The same paper derives Pareto optimality, budget weighted envy freeness, and proportionality for equilibrium allocations Gao and Kroer, Theorems 1 and 3.

Market, allocations, and programs

The item space $\Theta$ is a compact subset of $\mathbb R^d$ with restricted Lebesgue measure $\mu$. There are $n$ buyers. Buyer $i$ has a budget $B_i>0$ and a nonnegative integrable valuation density $v_i$ with $\int_\Theta v_i\,d\mu>0$. The utility of a bounded nonnegative bundle $x_i$ is $\langle v_i,x_i\rangle=\int_\Theta v_i x_i\,d\mu$. An allocation $x=(x_i)$ is feasible when $\sum_i x_i\le1$ almost everywhere. It is pure when each $x_i$ equals the indicator of a measurable set $\Theta_i\subseteq\Theta$, up to almost everywhere equality, and these sets are pairwise disjoint up to null sets. Leftover items are allowed.

A nonnegative integrable price density $p$ defines a buyer's affordable bundles by $\langle p,x_i\rangle\le B_i$. A market equilibrium $(x,p)$ is a feasible allocation and price at which every buyer maximizes utility among affordable bundles and $\langle p,1-\sum_i x_i\rangle=0$. Thus unallocated supply may remain only where it has zero price. The paper's primal Eisenberg–Gale program, $\mathcal P_{EG}$, maximizes weighted log utility over feasible allocations. Its dual program, $\mathcal D_{EG}$, minimizes total price minus weighted log multipliers subject to $p\ge\beta_i v_i$ almost everywhere Gao and Kroer, pp. 6–8.

Formalization targets

The goal is the three part Theorem 1. In the notation above, it asserts attainment of the primal objective at a pure allocation, attainment of the dual objective with a unique multiplier vector $\beta^*$ and price $p^*=\max_i\beta_i^*v_i$ almost everywhere, and the equivalence

$$(x,p)\text{ is a market equilibrium} \quad\Longleftrightarrow\quad x\text{ optimizes }\mathcal P_{EG}\ \text{and}\ (p,\beta^*)\text{ optimizes }\mathcal D_{EG}.$$

The milestone list follows the results the paper uses to reach that goal. Lemma A.1 gives a convex, compact range for utility matrices and, under atomlessness, identifies mixed and partition based ranges. Lemma 1 specializes this to the market's feasible utility set $U$, proving that $U$ is compact and convex and equals the pure utility set $U'$. Lemma 2 establishes attainment and uniqueness in the finite dimensional reduction of the dual problem. Lemma 3 gives weak duality with the paper's constant $C=\sum_i B_i-\sum_i B_i\log B_i$ and its three optimality conditions. Theorem 2 expands the equivalence between optimality and equilibrium, including budget exhaustion and the utility formula $\langle v_i,x_i\rangle=B_i/\beta_i$. These are the paper's numbered results on pp. 8–10 and a1 Gao and Kroer, §3 and Appendix A.1.

The proposal also states Theorem 3, Lemma 4, and Corollaries 1–3 as companion results. They record the resulting fairness properties, normalized equilibrium bounds, winning sets, a construction of dual prices from a pure optimum, and a test for a pure equilibrium Gao and Kroer, pp. 10–11.

What the result provides

Theorem 1 shows that the two programs give actual allocations and prices in the continuum market, not merely limiting objective values. The pure optimizer provides measurable regions for buyers. The dual multipliers give a unique utility price for each buyer, while the price density is determined almost everywhere. Theorem 2 makes these program outputs economically interpretable: each buyer exhausts its budget at equilibrium. Theorem 3 then supplies efficiency and fairness guarantees for those allocations Gao and Kroer, Theorems 1–3.

These results are proved in the cited paper. This mission asks for machine checked Lean proofs of those mathematical statements. Its definitions of allocations, demand, equilibrium, the two programs, and feasible utilities could also support formalization of the paper's later geometric and quasilinear results. The draft declarations compile as open statements; compilation does not establish the theorems.

Why the proof is difficult

The feasible allocations are bounded in an infinite dimensional function space, but that does not make the set compact in the topology used for the optimization problem. The paper instead needs compactness of the finite dimensional set of achievable utility vectors. The range result in Lemma A.1 is therefore central, and its atomless conclusion must be strong enough to replace fractional allocations by measurable partitions Gao and Kroer, Lemma 1 and Appendix A.1.

Standard constraint qualification arguments also do not supply the required duality theorem here: the positive cone in $L^1(\Theta)$ has empty interior. The proposal consequently asks for the paper's specific weak duality inequality, attainment, and optimality characterization rather than assuming a general finite dimensional duality theorem applies Gao and Kroer, Remark 1.

Formalization scope

Lean uses real valued measurable functions on the ambient Euclidean space with measure $\mu=\mathrm{volume}|_\Theta$. It identifies prices and allocations up to $\mu$ almost everywhere equality, as the paper identifies $L^1$ and $L^\infty$ equivalence classes. Bundles must belong to $L^\infty(\mu)$ and prices and valuations must be integrable; these conditions prevent a nonintegrable product from receiving Lean's default integral value of zero. The number of buyers may be zero, consistent with the finite index formulation, while the standing positivity hypotheses apply to every buyer present.

The real logarithm in Lean returns zero at zero. The optimization predicates instead require positive utility or positive dual multipliers and compare only with other positive points, matching the paper's $\log 0=-\infty$ objective convention. The maximization over buyers is the finite supremum $\sup_i\beta_i v_i$. Price and allocation uniqueness is stated almost everywhere; multiplier uniqueness is exact. Lemma A.1 uses the paper's divisible measure condition for atomlessness and fixes its unnamed almost everywhere partition convention by requiring $\sum_jx_j=1$ everywhere. Corollary 3 explicitly requires each denominator $v_i(\Theta_i)$ to be positive. Lemma 4 alone assumes the normalizations $v_i(\Theta)=1$ and $\sum_iB_i=1$, which the paper recalls before its statement.

The goal remains the full three part theorem. It does not assume the range theorem, duality equality, or optimality conditions it is meant to establish. Contributions to the measure range theorem, utility set compactness, the dual reduction, and the equilibrium characterization are all within scope.

Selected references

• Yuan Gao and Christian Kroer, Infinite-Dimensional Fisher Markets and Tractable Fair Division, Operations Research, 2023; formalization follows arXiv:2010.03025v5, 2021, §§2–3 and Appendix A.1.

Motivation

In reward based crowdfunding, customers must decide whether to back a product before its quality is known to them. The entrepreneur knows that quality and chooses a funding price. A high quality entrepreneur may therefore use price to convey information, but the same price is available to a low quality entrepreneur. The choice also changes the chance that the campaign meets its financing target. Bolandifar, Chen, Kouvelis, and Zhou study how these effects interact when the entrepreneur chooses a second, regular selling price after the campaign succeeds. The one price mechanism in this mission concerns the case in which only the funding price is posted in advance.

The question matters to the design and interpretation of crowdfunding campaigns. A lower funding price can be a credible quality signal even though it forgoes immediate revenue. Whether that signal is sustainable depends on the later selling opportunity, the financing target, and the different incentives of the two quality types. The paper gives a precise threshold for the financing target below which one separating outcome survives a refinement of the equilibrium concept.

Setting

The entrepreneur's product has privately known quality $q_i$, either low $q_L$ or high $q_H$, with $0<q_L<q_H$. The financing target is $T>0$. The entrepreneur posts a funding price $p_1\ge T$. Funding period customers all share a taste $\theta_c$ uniformly distributed on $[0,1]$ and evaluate the product using believed quality $q_j$. They back it when $\theta_cq_j\ge p_1$. The funding market has size one, so a successful campaign raises at least $T$ and occurs with probability $1-p_1/q_j$ for $T\le p_1\le q_j$. The formal definition extends this probability by zero for larger prices.

After success, true quality is revealed and the entrepreneur sets a regular selling price $p_2\in(0,q_i]$. A fraction $\alpha\in(0,1)$ of regular period customers have the same taste as the funding customers. Their taste distribution is therefore updated after success. The other regular customers have a fresh, independent uniform taste. The regular market also has size one. Production cost, salvage value, and discounting contribute no additional terms. Conditional regular period profit is $\pi^{ij}_2(p_2\mid p_1)$, the two branch function in equation (2) of the manuscript. Its optimal value $\pi^{ij*}_2(p_1)$ is the supremum over feasible $p_2$. The total expected profit $\pi^{ij}(p_1)$ is the success probability times $p_1+\pi^{ij*}_2(p_1)$.

A separating equilibrium assigns different feasible funding prices $p_H$ and $p_L$ to the two entrepreneur types. Customers believe quality is high at $p_H$ and low at every other price, including off path prices. Under those beliefs, neither type benefits from a feasible deviation. The intuitive criterion removes an equilibrium if an off path price would strictly improve the high type's profit while strictly reducing the low type's profit, were customers to interpret that deviation as a high quality signal. This is the paper's stated test, with the strict low type comparison used in its appendix.

Formalization targets

The separating equilibrium

Define the price threshold

$$\bar p_1=\frac{4q_H-(1-\alpha)q_L-\sqrt{(q_H-q_L)\bigl(16q_H-(1-\alpha)^2q_L\bigr)}}{8}.$$

The goal is Proposition 1 of the manuscript. If $T\le\bar p_1$, there is a separating equilibrium surviving the intuitive criterion, and every surviving separating equilibrium has exactly the prices

$$p_H=\bar p_1,\qquad p_L=\frac{3+\alpha}{8}q_L.$$

The formal goal also says that no separating equilibrium exists when $\bar p_1<T<q_L$. Its scope on this side of the threshold follows the manuscript's proof and the nondegenerate funding market; the printed “otherwise” sentence does not hold literally when $T\ge q_L$.

Supporting targets

Lemma 1 identifies the optimal regular price and its attained profit in each of three funding price ranges, split at $q_j/2$ and $\min\{q_j/[2(1-\alpha)],q_j\}$. Lemma 2 identifies the funding profit's single peak and the maximizing price $\max\{[4q_j-(1-\alpha)q_i]/8,T\}$. The three parts of Lemma 3 characterize the low type's mimicking indifference prices, the high type's upper indifference price, and the ordering of these thresholds. These are the milestones leading to Proposition 1.

Significance

The proposition gives both types' prices and shows why the high type's credible signal is a lower funding price than the low type's. It also identifies a financing target above which this separation disappears within the paper's nondegenerate range. The result relates a platform design parameter, the target, to equilibrium information revealed by price.

The result is proved in the cited manuscript, with proofs in Appendix A. The remaining work in this mission is a machine checked proof of the model's price optimization and equilibrium claims. The definition of the two period payoff, the treatment of the later optimal price, and the explicit deviation predicates may be reusable for other crowdfunding signaling mechanisms. The draft statements are open proof targets; the present mission does not claim those proofs are already formalized.

Difficulty

The later optimal price changes form as the funding price crosses two thresholds. That makes total expected profit a piecewise function, even before the two types' incentives are compared. Maximizing either type's full information payoff alone does not determine a separating equilibrium: the low type might imitate the high type, while the high type might deviate to a price customers would interpret as low quality. The intuitive criterion imposes a further comparison at prices outside the equilibrium path. The claim requires all of these comparisons with the same underlying payoff definition.

Formalization scope

Lean uses one tuple of real parameters $q_L,q_H,\alpha,T$ and the standing restrictions $0<q_L<q_H$, $0<\alpha<1$, and $T>0$. The prior probability of high quality does not occur in the separating price statements. The regular profit is the printed equation (2), with a positive regular price at most true quality. Campaign success probability is clipped at zero for funding prices above believed quality. Funding prices range over all reals at least $T$; the maximum profits are defined as suprema over those feasible prices. Milestones assert attainment, so those suprema cannot be replaced by convenient formula values.

The model uses the paper's market size, cost, salvage, and discount normalizations. Lemma 1 excludes $p_1=q_j$: at that endpoint the printed third case can specify an infeasible regular price. Lemma 2 assumes $T<q_j$ and quantifies only over the four true and believed quality combinations. Lemma 3 is stated for $T\le\bar p_1$ to avoid its circular printed preamble, and one threshold comparison is expressed as a strict profit inequality because the lower crossing can lie below $T$. Proposition 1 does not assert pooling existence, which would require the omitted prior; its no separation clause is restricted to $T<q_L$.

Contributions toward the piecewise optimization lemmas, the threshold characterization, and the equilibrium theorem are welcome. The separating equilibrium is defined by incentive comparisons over all feasible deviations, and its refinement is defined by the off path deviation test. The optimal profits are supremum values of the model payoffs. These choices keep the goal from collapsing into a restatement of a closed form or of the paper's derived necessary and sufficient conditions.

Selected references

• E. Bolandifar, Z. Chen, P. Kouvelis, and W. Zhou, Quality Signaling through Crowdfunding Pricing, SSRN manuscript 3689946, revision of 2022-05-30, §§3–4 and Appendix A. SSRN. Published as Manufacturing & Service Operations Management, DOI 10.1287/msom.2022.1177; the cited artifact here is the SSRN manuscript.