Analysis

Motivation

Digital platforms (marketplaces, payment networks, sharing services) need large up-front investments in capacity before any revenue arrives, and their founders typically finance them by selling equity to venture capitalists. Since 2017 an alternative has been available: issuing a platform-specific cryptocurrency (a utility token) in an initial coin offering (ICO), and running the platform on a blockchain whose fee rules are fixed in a smart contract. Whether this is merely a new funding channel or a better business model is a question for operations management, corporate finance and platform economics alike.

J. Chod, N. Trichakis and S. A. Yang (Platform Tokenization: Financing, Governance, and Moral Hazard, Management Science, 2022) answer it in a model in which the entrepreneur's effort is not contractible. They show that the answer depends on the cost of building capacity: when capacity is expensive, equity wins (their Proposition 1), and when it is cheap, tokens win (their Proposition 2). This mission formalizes the second result.

Setting

An entrepreneur builds a platform of capacity $Q$ at cost $C(Q)=KQ^k$ and exerts effort $e$ at private cost $\gamma e$. Buyers' inverse demand is $d(e,q)=e^aq^{-b}$ and sellers' supply curve is $s(q)=mq^n$, with $0<a<b<1$, $m,n\ge0$ and $k>(1-b)/(1-a)$. Sellers pay a one-time cost $c$ to join, cash flows are discounted by $\delta\in(0,1)$, and each token is used $v\ge1$ times per period. The per-period surplus is

$$\mathcal F(e,q)=q\bigl(d(e,q)-s(q)\bigr),$$

with partial derivatives $\mathcal F_e$, $d_e$ in $e$. The entrepreneur's objective in both models is the net present value

$$\frac{\mathcal F(e,Q)}{1-\delta}-cQ-C(Q)-\gamma e .$$

In the traditional model the entrepreneur sells an equity share $\alpha$ to a venture capitalist and can raise the fee once sellers have sunk their joining cost (holdup), which forces a first-period subsidy. Its equilibrium payoff \Pi^\$$ is the maximum of the objective subject to (1-\alpha)\mathcal F_e/(1-\delta)=\gamma$, where$\alpha$is the VC's break-even share, (17)–(20). In the **blockchain-based model** she sells a fraction$\alpha$of the tokens and commits to the fee; the payoff$\Pi^B$is the maximum subject to$\mathcal F_e/(1-\delta)-\alpha\frac1v d_eQ=\gamma$and$\alpha,d(e,Q)Q=vC(Q)$with$\alpha\le1$, (33)–(36). Corollary 1 rewrites both as one program with effort factors$\beta^$$,$\beta^B$, the blockchain one carrying the extra cap$d(e,Q)Q\ge vC(Q)$.

Formalization targets

Goal: Proposition 2

With all other parameters fixed and $c>0$ or $m>0$, there is $\varepsilon>0$ such that for every $K\in(0,\varepsilon]$ both suprema are finite and $\Pi^B>\Pi^\$\qquad\text{unless}\qquad\Pi^B=\Pi^\$=0 .$ No value of $\varepsilon$ is fixed: the goal asserts only the existence of a cheap-capacity regime.

Milestones

1. Corollary 1 for $i=B$ and $i=$$: Lemmas 2–3's programs equal (37)–(40).
2. (B.19)–(B.20): for small $K$ the token cap (39) does not bind.
3. Claim (i): $h(e,Q)>g(e,Q)$, i.e. \beta^B>\beta^\$$ wherever d>s$.
4. (B.29): e^\(Q)<e^B(Q)<e^*(Q)$, in root form.
5. Claim (ii): the objective is strictly concave in $e$ with unique maximizer $e^*(Q)$.

Significance

Proposition 2 is the paper's headline. It isolates two advantages of tokenization that hold even without any cost or technology difference: token investors are exposed to platform revenue rather than profit, which is less sensitive to effort, so the entrepreneur internalizes more of the marginal value of her effort; and a fee committed on a blockchain removes the holdup problem and with it the subsidy the traditional platform must finance. Together with Proposition 1 it delineates when a platform should tokenize.

The result is proved in the paper (Appendix B, pp. 19–20). It has not been machine-checked. The proof is short but leaves two steps informal: the relaxation of the cap (39) "by continuity", and the existence of optimal solutions behind the printed "max". A formal proof settles both, and fixes the exact hypotheses under which the claim holds (see the scope section).

Difficulty

The algebra of Corollary 1 and of Claim (i) is routine. The difficulty is analytic. The naive argument compares the two programs pointwise in $Q$ at their largest effort roots, but the payoffs are suprema over non-compact feasible sets, and the comparison only transfers to the suprema if the traditional supremum is attained, or approached at capacities bounded away from $0$ and $\infty$. The relaxation of (39) requires a bound, uniform in small $K$, showing that points violating the cap cannot approach the relaxed supremum; this is where $c>0$ or $m>0$ enters, since with $c=m=0$ the objective near such points is not controlled as $K\to0$.

Formalization scope

Parameters are a structure Params with real fields $a,b,m,n,K,k,c,\gamma,\delta,v$; Params.Standing collects the printed assumptions ($0<a<b<1$, $m,n\ge0$, $k>(1-b)/(1-a)$, $v\ge1$) and four the paper uses without stating ($0<\delta<1$, $c\ge0$, $\gamma>0$, $K\ge0$). Powers are Real.rpow, with Lean's $0^y=0$ for $y\ne0$; the partials $\mathcal F_e=ae^{a-1}Q^{1-b}$, $d_e=ae^{a-1}Q^{-b}$ are closed forms, certified by two HasDerivAt helper theorems, and $e^*(Q)$ is a closed form certified as the argmax by Claim (ii).

\Pi^\$$ and \Pi^B$are *defined* by the programs of Lemmas 2 and 3; the underlying dynamic game is not modelled. Each payoff is$\max{0,\sup(\text{objective over the feasible set})}$: the supremum replaces the printed max, never shown attained, and$0$ is the outside option of not starting the venture, invoked in the last paragraph of the paper's proof.

Departures from the printed statement, all disclosed in the items:

• $K\in(0,\varepsilon]$ instead of $[0,\varepsilon]$: at $K=0$ the Corollary 1 payoff programs coincide on the branch $c\le d-s$ (e.g. $c=0$, $m=1$), contradicting the printed strict claim. Lemma 2's literal $0<\alpha$ constraint omits that zero-investment boundary, so this mission states the common positive-$K$ regime.
• The added hypothesis $c>0$ or $m>0$: with $c=m=0$, \beta^\=\beta^B$and the blockchain program is the traditional one plus a cap, so$\Pi^B\le\Pi^$$for every$K>0$.
• Corollary 1 for i=\$$ is posed for K>0$and as an equality of payoffs: at$K=0$, (19) gives$\alpha=0$, which (20) excludes.

The goal cannot be met vacuously: it asserts that both objective images are bounded above, so the suprema are not Lean's junk value $0$, and the helper piTrad_pos_example states \Pi^\>0$at the Figure 1 parameters ($k=1$,$K=0.01$), ruling out an empty traditional program.

A complete development needs real-power calculus, the intermediate value theorem, strict concavity of $e\mapsto e^a$, and a compactness or coercivity argument for the suprema. The coercivity bounds for programs of the form "maximize a concave revenue minus a power cost subject to a first-order condition" are reusable for other effort-and-capacity models. Proofs of any milestone are welcome, as are proofs of the helpers.

Selected references

• J. Chod, N. Trichakis, S. A. Yang, Platform Tokenization: Financing, Governance, and Moral Hazard, Management Science, Articles in Advance, 2022. https://doi.org/10.1287/mnsc.2021.4225
• M. C. Jensen, W. H. Meckling, Theory of the Firm: Managerial Behavior, Agency Costs and Ownership Structure, Journal of Financial Economics 3(4), 1976. https://doi.org/10.1016/0304-405X(76)90026-X

Why congestion in matching markets matters

Online matching platforms (labor platforms such as Upwork or TaskRabbit, dating sites, short-term rental platforms) make it cheap to contact potential partners, but not cheap to find one who is still available. A worker who has already accepted a job, or a listing that is already booked, keeps receiving applications and keeps being screened. Arnosti, Johari and Kanoria, Managing Congestion in Matching Markets (M&SOM 23(3):620–636, 2021), build a stochastic game-theoretic model of this effect, in which applicants pay to apply and employers pay to screen, and employers cannot see which applicants have already matched. They prove that the model has a unique equilibrium, compute both sides' welfare in it in closed form, and use the formulas to evaluate platform interventions (application limits, application fees, a market-wide wage).

This mission formalizes the equilibrium characterization: the closed-form equilibrium welfare of Theorem 2, together with the existence and uniqueness results (Proposition 2, Theorem 1) and the identities from the paper's endnotes that connect them.

The stationary mean-field model

A market has four parameters: $r>0$, the number of applicants per employer; $\beta\in(0,1]$, the probability that an applicant is qualified for a given employer; $c_a$, the cost of one application; and $c_s$, the cost of screening one applicant. Throughout, Assumption 1 holds: $\max(c_a,c_s)<\beta$. Write $c'_s = c_s/\beta$.

Applicants choose an application intensity $m\ge0$: an applicant sends a Poisson($m$) number of applications, each of which becomes an offer independently with probability $p$, the acceptance probability. The applicant takes the first offer, so the expected payoff is

$$W_a(m,p) = 1-e^{-mp}-c_a m, \tag{2}$$

maximized by the applicant best response

$$\mathcal M(p) = 0 \ \text{ if } p\le c_a, \qquad \mathcal M(p)=\tfrac1p\log\bigl(\tfrac p{c_a}\bigr)\ \text{ if } p>c_a. \tag{3}$$

Employers receive a Poisson($rm$) number of applications. Each applicant is qualified with probability $\beta$ and still available with probability $q$. An employer either screens sequentially until it hires (screening probability $\alpha$) or exits. The employer best-response correspondence is

$$\mathcal A(q) = \{0\}\ \text{if } q<c'_s,\qquad [0,1]\ \text{if } q=c'_s,\qquad \{1\}\ \text{if } q>c'_s, \tag{4}$$

and the employer payoff is $W_e(\alpha,m,q) = \alpha(1-e^{-rm\beta q})(1-c'_s/q)$ (5).

With $E(x) = (1-e^{-x})/x$ ($E(0)=1$), the consistency conditions are

$$q = E(mp), \qquad p = \alpha\beta\,E(rm\beta q). \tag{6–7}$$

A solution $(p,q)$ is a mean-field steady state of the strategies $(m,\alpha)$. A mean-field equilibrium (MFE) is a pair $(m^*,\alpha^*)$ with a steady state $(p^*,q^*)$ such that $m^* = \mathcal M(p^*)$ and $\alpha^*\in\mathcal A(q^*)$ (Definition 1). Equilibrium welfare is $\Pi^*_a = W_a(m^*,p^*)$ and $\Pi^*_e = W_e(\alpha^*,m^*,q^*)$.

Formalization targets

Goal: Theorem 2 (p. 628)

There are unique $\hat p,\bar p>c_a$ with

$$r\Bigl(1-\frac{c_a}{\hat p}\Bigr) = 1-e^{-\frac{r\beta}{\hat p}\left(1-\frac{c_a}{\hat p}\right)}, \qquad 1-\frac{c_a}{\bar p}+\frac{c_s}{\beta}\log\Bigl(\frac{c_a}{\bar p}\Bigr)=0, \tag{13–14}$$

the MFE is unique, and in it

$$p^*=\min(\hat p,\bar p),\qquad \Pi^*_a = 1-\frac{c_a}{p^*}+\frac{c_a}{p^*}\log\frac{c_a}{p^*},\qquad \Pi^*_e = r\Bigl(1-\frac{c_a}{p^*}+\frac{c_s}{\beta}\log\frac{c_a}{p^*}\Bigr). \tag{15–16}$$

The theorem is exact; it has no constants to improve.

Milestones

1. Proposition 2 (p. 626): for fixed $m\ge0$, $\alpha\in[0,1]$, $r$, $\beta$, the system (6)–(7) has a unique solution.
2. Theorem 2, (13) and Theorem 2, (14) (p. 628): the two root equations each have a unique root above $c_a$.
3. Endnote 13 (p. 635): at the applicant best response, consistency (7) with every employer screening ($\alpha=1$) is equation (13).
4. §5.1 (p. 628): at the applicant best response, employers are exactly indifferent ($q=c'_s$) iff (14) holds.
5. Theorem 1 (p. 627): the MFE exists and is unique.
6. Endnote 12 (p. 635): the welfare identities (15) and (16) at the best response and a steady state.

Significance

Theorem 2 reduces equilibrium welfare on both sides to one scalar, $p^*=\min(\hat p,\bar p)$, and splits markets into two regimes (Definition 2): application-limited ($\bar p>\hat p$; all employers screen; applicants compete in a "tragedy of the commons") and screening-limited ($\bar p<\hat p$; employers are indifferent and their welfare is zero, by (14) and (16)). All of the paper's later results, including the welfare bounds of Theorem 3, the effect of application limits (Theorems 4–5), application costs (Theorem 6) and wages (Theorem 7), are computed from these formulas.

Proposition 2, Theorem 1 and Theorem 2 are stated in the article but their proofs are in a technical report (Arnosti, Johari, Kanoria 2019, SSRN), not reproduced in the article and not used here. To our knowledge none of these results has a machine-checked proof. A formal development would give a self-contained, checked proof of the equilibrium characterization from the article's definitions alone.

Where the difficulty lies

The welfare identities (15)–(16) are algebra once $m^*=\mathcal M(p^*)$ and $p^*>c_a$ are known. The root statements are one-variable analysis. The hard part is the equilibrium itself. Proposition 2 is a fixed-point problem: substituting (7) into (6) gives an increasing map $q\mapsto E(m\alpha\beta E(rm\beta q))$, and an increasing map can have several fixed points, so a monotonicity argument alone does not give uniqueness. Theorem 1 then has to handle the correspondence $\mathcal A$: an equilibrium may sit at the kink $q^*=c'_s$ with an interior $\alpha^*$, and the case analysis has to show that exactly one of the regimes $\alpha^*=1$, $\alpha^*<1$ applies and that it pins down $(m^*,\alpha^*)$.

Formalization scope

All objects live in the namespace MatchCongestion.Welfare, over ℝ. The conventions are:

• Positivity. Params.Standing is Assumption 1 together with $0<r$, $0<\beta\le1$, $0<c_a$, $0<c_s$, which the paper uses without listing them ("costs", $\beta$ a probability). Without $c_s>0$, (14) has no root above $c_a$.
• The ratio at zero. The page leaves (6)–(7) undefined at $mp=0$ and $rm\beta q=0$. They are written through $E$ with $E(0)=1$, the continuous extension.
• Definition 1. It composes $\mathcal M$ and $\mathcal A$ with the steady-state maps $\mathcal P,\mathcal Q$. IsMFE instead asks for some steady state $(p,q)$; by Proposition 2 the two readings agree.
• The correspondence. $\mathcal A(q)$ is a Set ℝ.
• Roots and welfare. $\hat p,\bar p$ are quantified (any roots above $c_a$), not chosen. $\Pi^*_a,\Pi^*_e$ are $W_a,W_e$ at the MFE's own steady state. $\log$ is Real.log.

Several formalizations would make the goal trivial or false, and none is used:

• a raw division (1 - exp (-x)) / x in (6)–(7) would make $(m,\alpha,p,q)=(0,0,0,0)$ a spurious second equilibrium;
• an "every MFE satisfies …" goal without the existence-and-uniqueness conjunct would be vacuous;
• choosing $\hat p,\bar p$ by Classical.choose, or $\mathcal P,\mathcal Q$ in Definition 1, would leave junk values unconstrained;
• $\mathcal A$ as a function would erase the screening-limited equilibrium, which has an interior $\alpha^*$;
• $\mathcal M$ without the case split $p\le c_a$ would make the best response negative.

Proposition 1 (the employer's sequential screening problem, specified only in an online appendix), the application-limit model (8)–(9) with Proposition 3, Theorems 3–7 and the finite-system limit theorems 8–10 are out of scope. Contributions of independent interest are a general lemma on unique roots of strictly convex or concave one-variable functions on an interval, and analytic facts about $E$ (positivity, strict monotonicity, $E\le1$ on $[0,\infty)$).

Selected references

• N. Arnosti, R. Johari, Y. Kanoria, Managing Congestion in Matching Markets, Manufacturing & Service Operations Management 23(3):620–636, 2021. https://doi.org/10.1287/msom.2020.0927
• N. Arnosti, R. Johari, Y. Kanoria, Managing Congestion in Matching Markets (full technical report), preprint, 2019. http://dx.doi.org/10.2139/ssrn.2427960

Motivation

A polynomial threshold function makes a Boolean decision by evaluating a real polynomial and keeping only its sign. Its average sensitivity measures how often that decision changes after one uniformly chosen input coordinate is reversed, summed over all coordinate choices. This is a basic quantitative question in the analysis of Boolean functions: how much can a low-degree decision rule vary across the edges of the Boolean cube?

The result collected here is a uniform bound with an explicit coefficient. The OpenAI weighted-grading development supplies a complete coefficient-eight construction. Lagdive, Aglave and Damre sharpen its probability estimate and obtain the sufficient coefficient 3.83. The present fixed-source development formalizes the refined estimate, extracts the coefficient 3.762, and connects it to the full polynomial-threshold statement.

This mission organizes that completed result and its reusable supporting theorems. Its goal and both milestones already have accepted Lean proofs. It does not present the coefficient as optimal, and it makes no claim of exhaustive historical priority.

Setting

Let $n,d$ be positive integers, and let $p$ be a real polynomial in $n$ variables with total degree at most $d$. Choose an input $x$ uniformly from the sign cube $\{-1,1\}^n$. For a coordinate $i$, write $x^{\oplus i}$ for the same input with coordinate $i$ negated. The threshold convention is

$$f(x)=\begin{cases}1,&p(x)\ge0,\\-1,&p(x)<0.\end{cases}$$

In particular, a zero of the polynomial is assigned the positive sign. The average sensitivity is

$$\operatorname{AS}(f)=\sum_{i=1}^{n}\Pr\{f(x)\ne f(x^{\oplus i})\}.$$

For the scalar supporting statements, let $B_n$ have the symmetric binomial distribution with parameters $n$ and $1/2$. Its mean absolute deviation is

$$b_n=\mathbb E|B_n-n/2|=2^{-n-1}\sum_{j=0}^{n}\binom nj|2j-n|.$$

The accompanying definition module fixes this finite sum and the normalized central coefficient $c_k=4^{-k}\binom{2k}{k}$. These definitions contain no estimates or unproved hypotheses.

Formalization targets

Goal — the coefficient 3.762 for arbitrary real polynomials

For every $n,d\ge1$ and every real polynomial of total degree at most $d$, prove

$$\operatorname{AS}(\operatorname{sign}p)\le\frac{1881}{500}\,d\sqrt n.$$

The goal is the published theorem AverageSensitivity.polynomial_bound_3762_general. It has no multilinearity hypothesis and no requirement that $d\le n$. The narrower range $1\le d\le n$ used by the Big O board is therefore included. The goal's fixed coefficient records this particular verified result; a future sharper coefficient would be a separate statement.

Milestone 1 — the refined finite one-sided coupling estimate

Let a finite set carry nonnegative probability weights $w$, and let real functions $U,V$ have identical weighted distributions. Let $m$ be any real centre and let $a\ge0$. If $V-U\le a$ on the support of the weights, prove

$$\mathbb E(U-V)^2\le4a\mathbb E|U-m|+a^2.$$

This is the finite form of the first estimate in Lemma 2 of Lagdive, Aglave and Damre. The centre is arbitrary; independence, exchangeability and a two-sided displacement bound are not hypotheses. Its published formalization is already proved.

Milestone 2 — exact extraction of the universal coefficient

For positive integers $n,d$ and a real number $A$, prove the scalar implication

$$A\le n,\qquad A\le8db_n+2d^2\quad\Longrightarrow\quad A\le\frac{1881}{500}d\sqrt n.$$

This is AverageSensitivity.extract_constant. Its statement is independent of the polynomial and matrix constructions. It records the coefficient extraction proved in this development, rather than attributing 3.762 to the earlier paper.

Significance and current status

The result gives one coefficient that works simultaneously for every positive dimension and degree. Such uniformity distinguishes it from estimates that hold only for a fixed degree or only as the dimension tends to infinity. It also preserves the stated convention at polynomial zeros, so the class of threshold functions is unchanged at the boundary.

The formal contribution is a complete connection from the polynomial and the actual finite cube to the numerical bound. The final theorem does not assume the existence of a grading, an energy bound, a coupling estimate or a small-dimension certificate. Those mathematical components are discharged inside the proof chain. The two supporting milestones are independently importable results, and the live dependency graph records both as actual prerequisites of the goal's accepted reduction.

All three theorem nodes are currently Proved. The closed repository proof was rebuilt with Lean 4.33.1 and the platform's Mathlib revision, and an independent Linux build also passed. The final theorem's axiom dependencies are exactly propext, Classical.choice and Quot.sound. These checks establish the formal result under the displayed definitions; they do not establish optimality of the coefficient or independent human peer review.

Difficulty

A one-sided bound on the difference of two variables does not by itself bound the difference in the opposite direction. The equal-distribution condition is therefore essential to the coupling milestone. Omitting it would change the problem into a false assertion. In the polynomial application, the relevant distributions also have to come from the actual block masses of the constructed grading; treating those masses or the grading properties as free assumptions would omit the central analytic work.

The constant extraction must cover all admissible dimension-degree pairs. A calculation for finitely many dimensions cannot establish the universal statement, while an asymptotic first-moment estimate can leave uncontrolled small dimensions or degree-dependent errors. The formal target includes both the infinite range and every exceptional finite case. Numerical optimization and floating-point experiments are not premises of the accepted result.

Formalization scope

Cube vertices are functions Fin n → Bool, interpreted coordinatewise as signs. A coordinate flip is an explicit function update, and each probability is a finite cardinality divided by $2^n$. The polynomial is a Mathlib MvPolynomial (Fin n) ℝ; the degree bound refers to its total degree. General polynomial inputs are included through a proved value-preserving, degree-nonincreasing multilinearization. Positive dimensions ensure the normalizing denominator is nonzero. Degree zero and dimension zero are outside the displayed goal's quantifiers.

The two definition references provide the original cube/threshold interface and the exact scalar moment interface. The coupling milestone uses finite weighted sums, so equality of distributions is stated for every real test function without additional measurability assumptions. The scalar milestone quantifies over an arbitrary real $A$ satisfying its two explicit upper bounds. The main goal has no analogous auxiliary assumptions.

This is a Research Paper mission for a completed fixed-source development, with the main theorem and both milestones linked by their existing identities. It creates no duplicate theorem statements. Alternative proofs and subsequent sharper bounds can reuse these interfaces, but they are not claimed as completed by this mission. The construction and earlier probability refinement remain attributed to their original sources. Proof development and source preparation used OpenAI Codex.

Selected references

• OpenAI, Average sensitivity of polynomial threshold functions, preprint and Lean source, 2026. Fixed Lean development.
• Prathmesh Lagdive, Vaibhav Aglave and Suraj Damre, An elementary improvement of the average sensitivity bound for polynomial threshold functions, 2026, Lemma 2 and the dimension-degree estimate. Fixed manuscript source.
• Anchen0823, Average sensitivity: a Lean proof with coefficient 3.762, source development, 2026. Verified source revision. Prove2Me accepted main submission: 0f539328-c783-4509-a78e-a86ac777468c.

Motivation

Service systems such as public fast-charging stations for electric vehicles let each customer choose how long to be served. Lin, Shang and Sun (SSRN 3709573, 2020; later in Management Science, doi:10.1287/mnsc.2022.4474) study a firm that announces to every arriving customer the current wait time $w$ (the work already in the queue) and a price rate $p$ per unit of service time. The customer then decides whether to join and, if so, how long a service to buy. Queue pricing usually conditions on the queue length with random service times (Low 1974; Paschalidis and Tsitsiklis 2000; Kim and Randhawa 2018). Here the state is the wait time, and it moves deterministically between arrivals.

The firm maximizes long-run average revenue or social welfare. The optimality condition the paper derives is not an ordinary differential equation but a delay differential equation (DDE) that looks ahead: the value at $w$ depends on the value at $w + \mathtt t(p) > w$. This mission formalizes the paper's existence theorem for that equation.

Setting

A model has a usage utility $U$, a waiting cost $c$, a Poisson arrival rate $\lambda > 0$ and a maximum service time $C > 0$, under Assumption 1 (p. 7):

1. $U(t) \ge 0$, $U(0) = 0$, $0 \le U'(t) \le U'(0)$ and $U''(t) < 0$ on $[0, C]$;
2. $\frac{d^2}{dt^2}[U'(t)t] < 0$ on $[0, C]$;
3. $c(0) = 0$, $c'(w) > 0$ and $c''(w) \ge 0$ for $w \ge 0$.

At price $p \in [0, U'(0)]$ a joining customer chooses the service time $\mathtt t(p) = \min\{(U')^{-1}(p), C\}$ (5). They join when $U(\mathtt t(p)) - p\,\mathtt t(p) - c(w) \ge 0$. Three thresholds follow:

• $\bar w$ solves $U(C) = c(\bar w)$; above it nobody joins.
• $\Gamma(w)$, for $w \in [0, \bar w]$, is the highest price at which a customer still joins (Proposition 2).
• $\hat w$ and $L(w)$ (Proposition 1) describe when the marginal price $U'(t)$ still attracts a customer.

The per-customer value is $\mathbf v(p) - \alpha c(w)$, with $\mathbf v(p) = p\,\mathtt t(p)$, $\alpha = 0$ for revenue and $\mathbf v(p) = U(\mathtt t(p))$, $\alpha = 1$ for welfare (Lemma 1).

The optimality equations (12)–(15) ask for a constant $\mathsf g$ (the average rate) and a relative value function $V$ with

$$\mathsf g = -V'(w) + \lambda \max\Big\{\max_{p \in [0, \Gamma(w)]} \big[\mathbf v(p) - \alpha c(w) + V(w + \mathtt t(p)) - V(w)\big],\ 0\Big\}, \quad w \in (0, \bar w],$$ $$\mathsf g = \lambda \max\Big\{\max_{p \in [0, \Gamma(0)]} \big[\mathbf v(p) + V(\mathtt t(p)) - V(0)\big],\ 0\Big\}, \qquad \mathsf g = -V'(w) \ (w > \bar w), \qquad V(\bar w) = 0.$$

Algorithm 1 (p. 14) is a backward explicit-Euler shooting scheme. For a guess $g \ge 0$ and $N$ grid cells on $[0, \bar w]$, it starts from $V^g_N(w) = -(w - \bar w)g$ for $w \ge \bar w$. It then builds a piecewise-linear $V^g_N$ cell by cell from right to left. On the cell ending at $x$ the slope is $-g + K^g_N(x)$, where the slope adjustment $K^g_N(x)$ is $\lambda$ times the positive part of the inner maximum at $x$. The shooting value is $g_N = \min\{g \ge 0 : g \ge K^g_N(0)\}$ (23). Finally $\bar g = \lim_j g_{2^j}$ (24) and $V^{\bar g}(w) = \lim_j V^{\bar g}_{2^j}(w)$ (Proposition 6).

Formalization targets

Goal: Theorem 1 (p. 17)

$$\bar g = \lim_{j\to\infty} g_{2^j} \ \text{exists},\quad V^{\bar g}_{2^j}(w) \to V^{\bar g}(w)\ (w \ge 0),\quad (\bar g, V^{\bar g}) \text{ solves (12)–(15)},\quad V^{\bar g} \text{ is nonincreasing and concave on } [0, \bar w + C].$$

Milestones

The milestones follow the paper's proof in order:

• Thresholds and the value function (Propositions 1–3, pp. 8–11): uniqueness of $\hat w$ and $\bar w$, the characterization (8) of $\Gamma$, $\Gamma(0) = U'(0)$ with $\Gamma$ decreasing, and the bounds (V1)–(V2) on $\mathbf v$.
• The finite-$N$ scheme (Proposition 4, Lemmas 2, 3, 5): $V^g_N$ is concave and $K^g_N$ is nonincreasing; $K$ increases when the grid is refined and decreases in $g$; and $K^{U'(0)}_N \equiv 0$.
• The limits (Proposition 5, Lemma 6, Proposition 6): $g_{2^j}$ increases to $\bar g \le U'(0)$, the $V^{\bar g}_{2^j}$ are uniformly $\bar g$-Lipschitz, and they converge uniformly to a concave, nonincreasing, Lipschitz $V^{\bar g}$.
• The equations in the limit (Lemma 7, Propositions 7–8): $K^{\bar g}_{2^j}(0) \to \bar g$; the boundary condition (13); differentiability of $V^{\bar g}$ on $[0, \bar w]$ and the DDE (12).

Significance

Theorem 1 is the existence half of the paper's verification argument. Its Theorem 2 then shows that the constructed $\bar g$ equals the optimal long-run average rate over all predictable price processes. Its Theorem 3 reads the structure of the optimal price and service-time policies off $V^{\bar g}$. Without a solution of (12)–(15) neither result has an object to talk about. The construction also gives a convergent numerical method (Algorithm 1) for a class of look-ahead DDEs that standard ODE theory does not cover.

The proofs are written out in the paper's Appendix B, except Lemma 12, an internal step of Proposition 8 whose proof the authors leave out. None of it is machine-checked. A complete formalization would check every step of the shooting argument and supply the omitted lemma. It would also yield a reusable framework: Euler-type schemes for delay equations whose delay points forward, monotone in the grid and in a scalar parameter.

Difficulty

The obvious approach, Cauchy–Lipschitz, fails: (12) is not an initial-value problem. $V'(w)$ depends on $V$ on $[w, w + C]$, so the equation must be integrated backwards from $\bar w$, and then the value $\mathsf g$ is unknown. The shooting scheme fixes $g$, integrates backwards, and tunes $g$ so that the boundary condition (13) at $w = 0$ holds in the limit. For fixed $g$ the approximations need not converge as $N \to \infty$ (the slope at $0$ can diverge), so $g$ and $N$ must be coupled through $g_N$.

The hard step is Proposition 8. Each $V^{\bar g}_{2^j}$ has kinks at every grid point, yet the limit has to be differentiable. One has to show that the left and right derivatives of the concave limit coincide and equal the right-hand side of (12), which requires passing a maximum over a $w$-dependent price set to the limit.

Formalization scope

All declarations live in the namespace WaitTimePricing.Existence, and only Mathlib is imported. Conventions:

• $U, c : \mathbb R \to \mathbb R$ are $C^3$ and $C^2$ on $\mathbb R$, a disclosed strengthening of "three/two times differentiable". Assumption 1's inequalities are imposed exactly on $[0, C]$ and $[0, \infty)$. $\lambda > 0$ and $C > 0$ are added; the paper uses them without stating them.
• $\mathtt t(p) = \sup\{t \in [0, C] : p \le U'(t)\}$, meaningful for $p \in [0, U'(0)]$. $\hat w$, $L(w)$, $\bar w$ and $\Gamma(w)$ are defined by their characterizing sets, not by closed forms. Propositions 1–2 are theorems about these sets.
• The objective is one of Lemma 1's two cases. The paper's remark that any $\mathbf v$ satisfying (V1)–(V2) would do is not formalized, because it silently needs continuity of $\mathbf v$.
• Every "max" in (12), (13), (19) and (22) is a real supremum over $[0, \Gamma(w)]$. For the continuous $V$ used here this set is nonempty and bounded, and the supremum is attained.
• $V'$ is never a default-valued derivative. (12) and (14) assert that $V$ has the prescribed derivative, two-sided for $w \in (0, \bar w]$ and $w > \bar w$; Proposition 8 states the case $w = 0$ with a right derivative.
• Algorithm 1 is a recursion over the passes of its loop, with $N \ge 1$. The initialization (16) is extended from $[\bar w, \bar w + C]$ to $[\bar w, \infty)$ so that (14) can hold as printed on $(\bar w, \infty)$. Only values on $[0, \bar w + C]$ enter the loop, so the construction is unchanged.
• $\bar g$ and $V^{\bar g}$ are defined as limits that take a default value when the limit does not exist. Propositions 5–6 and the goal assert the convergence.
• "Decreasing" is nonincreasing everywhere (including $\Gamma$, Proposition 2(iii)), the reading the proofs establish.

Trivializations ruled out. The goal names the paper's $\bar g$ and $V^{\bar g}$ together with their convergence, not an arbitrary solution and not default values of undefined limits. It cannot be met at a kink through a default-valued derivative. Its inner maxima cannot vanish through an empty or unbounded set. $\Gamma$ and $\mathtt t$ are not closed forms that would make (8) true by definition. The weaker statement "some $(\mathsf g, V)$ solves (12)–(15)" is not the goal.

Contributions are welcome at every milestone. Reusable pieces include monotonicity of a max-operator under backward induction, Dini-type uniform convergence of monotone sequences of equi-Lipschitz concave functions, and the differentiability of a concave limit of piecewise-linear functions. Theorem 2 (optimality over predictable controls) and Theorem 3 (policy structure) are outside this mission. Theorem 3 appears to fail as printed when $\bar g > U'(C)$.

Selected references

• C.-A. Lin, K. Shang, P. Sun, Wait Time Based Pricing for Queues with Customer-Chosen Service Times, SSRN 3709573, version of October 12, 2020. https://ssrn.com/abstract=3709573 (journal version: Management Science, https://doi.org/10.1287/mnsc.2022.4474)
• D. W. Low, Optimal dynamic pricing policies for an M/M/s queue, Operations Research 22(3), 1974. https://doi.org/10.1287/opre.22.3.545
• I. C. Paschalidis, J. N. Tsitsiklis, Congestion-dependent pricing of network services, IEEE/ACM Transactions on Networking 8(2), 2000. https://doi.org/10.1109/90.842140
• J. Kim, R. S. Randhawa, The value of dynamic pricing in large queueing systems, Operations Research 66(2), 2018. https://doi.org/10.1287/opre.2017.1668
• D. P. Bertsekas, Dynamic Programming and Optimal Control, 2nd ed., Athena Scientific, 2000. http://www.athenasc.com/dpbook.html

Motivation

A delivery company can assign each driver a permanent district instead of allowing every driver to serve the whole city. This makes dispatching simpler, but it raises a service question: if the districts receive almost equal shares of demand and travel workload, how different can their expected delivery times be? Carlsson, Liu, Salari and Yu study this question for a region partitioning policy in which one vehicle serves each district. Their Proposition 3 gives an explicit error bound for a partition whose shares are accurate within a tolerance ε. The proposition complements their exact equitability result, Theorem 6, by quantifying the effect of a partition that can only be computed approximately.

Setting

The service region R is a compact convex subset of the Euclidean plane, with depot x₀ ∈ R. Orders arrive at a rate λ and have locations distributed with density f on R. The density is nonnegative, Lipschitz on R, and normalized by ∫_R f(x) dx = 1. There are m ≥ 1 identical vehicles, each with speed v > 0 and capacity q ≥ 1. An order requires a mean on site service time s̄ ≥ 0. The positive constant β is the geometric constant in the paper's heavy traffic delivery time expression. A partition R₁, …, R_m covers R, with districts disjoint up to area zero; vehicle i serves R_i.

For a measurable district S, let p(S) = ∫_S f(x) dx be its share of demand. Its arrival rate is λ_S = λp(S), and its conditional density is f_S(x) = f(x)/p(S) when p(S) > 0. The paper uses two partition measures:

$$\mu_1(S)=\int_S\sqrt{f(x)}\,dx,\qquad \mu_2(S)=\int_S(\bar s vq+2\lVert x-x_0\rVert)f(x)\,dx.$$

The first controls the leading travel term. The second combines service time and radial travel from the depot. A partition is ε equitable when, for every district i and each j ∈ {1,2}, the difference between μ_j(R_i) and μ_j(R)/m has absolute value at most ε.

For vehicle count k, arrival rate a, region S, and density g, write the workload factor as

$$W(k,a,S,g)=\frac{a\bar s}{k} +\frac{2a}{kvq}\int_S\lVert x-x_0\rVert g(x)\,dx.$$

The heavy traffic expression from the paper's Theorem 3 is

$$L(k,a,S,g)=\frac{\beta^2a(1-1/q)^2 \left[\int_S\sqrt{g(x)}\,dx\right]^2} {2k^2v^2(1-W(k,a,S,g))^2}.$$

The comparison value is L* = L(m,λ,R,f). For district i, the value L_i = L(1,λ_{R_i},R_i,f_{R_i}) uses that district's own arrival rate, density, and workload factor.

Formalization targets

Proposition 3: approximate districts

For λ > 0 with W(m,λ,R,f) < 1, ε ≥ 0, and an ε equitable partition, define the corrected tolerance factor

$$\eta=\frac{\varepsilon}{ \min\left\{\mu_1(R)/m,\; \frac{vq}{\lambda}\left(1-\frac{\lambda\mu_2(R)}{mvq}\right) \right\}}.$$

When η < 1, the target is the two sided estimate

$$\lvert L_i-L^*\rvert\le \frac{4\eta}{(1-\eta)^2}L^* \qquad\text{for every }i.$$

The first milestone rewrites each district's Theorem 3 expression using μ₁(R_i) and μ₂(R_i). The next two milestones give upper and lower comparisons with L*. The final algebraic milestone evaluates the larger of the two relative deviations. These are the displayed steps on the paper's e companion pages ec6 and ec12–ec13.

The printed Proposition 3 uses max in the denominator defining η. Its proof requires min: when the two entries are 1 and 100 and ε = 0.1, a district can have L_i/L* = (1.1/0.999)² ≈ 1.212, while the printed η = 0.001 permits a deviation of only about 0.004. The correction is recorded in the theorem statements and audit notes.

Significance

The bound makes partition accuracy interpretable as a service guarantee. Once both shares are close enough that η < 1, every district's leading delivery time lies in a controlled interval around the flexible policy's benchmark. It states a guarantee for each district, rather than just for a demand weighted average, so it addresses unequal service across the region.

The authors prove the displayed comparison in their accepted manuscript. This mission formalizes the comparison between explicit heavy traffic expressions; it does not claim a new queueing theorem or a machine checked proof of the stochastic model. The reusable output is a precise Lean interface for spatial demand integrals, workload, conditional district densities, and perturbation bounds involving both numerator and denominator errors. The theorem items are proof targets.

Difficulty

The denominator responds to the μ₂ error in the opposite direction from the numerator's response to the μ₁ error. Bounding their ratio requires both the district workload and the lower numerator estimate to stay in their proper sign ranges. Simply squaring the ε share inequalities is invalid until those signs are known. The condition η < 1 supplies the required room; it also rules out a zero probability district under the other hypotheses. The printed choice of max for η fails to control the error in whichever of the two scales is smaller.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin 2), Lebesgue set integrals, and real valued leading terms. The density, region, depot, fleet parameters, and positive β are fixed while λ and ε vary. The source's compactness, convexity, Lipschitz density, normalization, positive vehicle count, speed, and capacity, and nonnegative mean service time are included in a single standing predicate. A partition has null measurable pieces, pairwise disjoint almost everywhere, and exact union R; shared district boundaries have area zero. The goal also states λ > 0, global workload < 1, ε ≥ 0, and η < 1, matching the stable regime and the proof's small ε condition. Capacity q = 1 remains admitted: both leading terms then vanish and the inequality still holds.

The stochastic renewal arrivals, routing policy, and queueing process are outside this development. Theorem 3 supplies the paper's leading expression, applied separately to the full region and each district. Thus L_i and L* here are leading expressions at one fixed λ, not the underlying expected delivery time functions. A fixed positive ε makes η grow near the heavy traffic boundary, so the page's parenthetical “in heavy traffic” is read through the leading expressions used by its proof. The district value is formed from λ_{R_i} and f_{R_i}; it is not defined from the global benchmark or from the right hand side of the first milestone.

A complete proof will need standard facts about set integrals and square roots, the normalization of a conditional density, and inequalities for positive real denominators. The setting definitions can support other region partition comparisons. Contributions establishing these identities and the upper and lower estimates are welcome.

Selected references

• J. G. Carlsson, S. Liu, N. Salari, and H. Yu, Provably Good Region Partitioning for On-Time Last-Mile Delivery, accepted manuscript, SSRN 3915544; published in Operations Research 72(1), 91–109 (2024), DOI: 10.1287/opre.2021.0588. Proposition 3, printed p. 21; proofs on pp. ec6 and ec12–ec13.
• D. J. Bertsimas and G. J. van Ryzin, Stochastic and Dynamic Vehicle Routing with General Demand and Interarrival Time Distributions, Advances in Applied Probability 25(4), 947–978 (1993), DOI: 10.2307/1427801. Source of the heavy traffic expression cited as Theorem 3 in the Carlsson et al. manuscript.

Motivation

A forecaster who issues a probability distribution for a multivariate quantity, such as the joint demand at several locations or the joint returns of several assets, is often judged not on the whole distribution but on a region it implies: the set of outcomes whose cumulative probability, or smoothed density, exceeds a threshold. Such level sets are the multivariate counterpart of quantiles, and they are used as risk regions and as summaries of joint distributions in management science (Abbas, Budescu and Gu 2010) and in density level set estimation (Cadre 2006). To compare competing level set forecasts against realized data, one needs a consistent scoring function: a loss $l(A, y)$ of a candidate set $A$ and an outcome $y$ whose expectation under the true distribution is smallest at the true level set. For univariate quantiles the answer is classical (the quantile or pinball loss, Gneiting 2011); for general multivariate level sets, the paper notes, scores had not been studied beyond density level sets and univariate quantiles.

Meng, Taylor, Ben Taieb and Li (Operations Research, 2025) obtain such scores by decomposing their $L^2$ scoring rule for multivariate distributions into an integral, over the threshold $\alpha$, of scores for the level sets of a smoothed density. This mission formalizes that construction: Theorem 2 of the paper.

Setting

Write $\mathbb R^d$ for $d$-dimensional space with Lebesgue measure $\mathcal L^d$ and the componentwise order ($z \ge y$ means $z_j \ge y_j$ for all $j$). The unknown distribution of the observation $Y$ is a probability measure $P_Y$ on $\mathbb R^d$; the paper writes $f_Y$ for its generalized density. Fix a kernel $w : \mathbb R^d \to \mathbb R$ and a nonnegative integrable weight $h$. The smoothed density is the convolution

$$(f_Y * w)(z) = \int_{\mathbb R^d} w(z - s)\, dP_Y(s).$$

For $w = u = \mathbb 1\{\cdot \ge 0\}$ (the Heaviside function) it is the multivariate CDF $F_Y(z) = P_Y\{s \le z\}$.

The $\alpha$ level set of a function $g$ is (display (9), p. 12)

$$L(g;\alpha) = \{ z \in \mathbb R^d : g(z) \ge \alpha \}.$$

A function $l(A, y)$ of a Borel set $A \subseteq \mathbb R^d$ and a realization $y$ is a consistent scoring function for $L(f_Y * w; \alpha)$ if $\mathbb E_{P_Y}[l(A, \bullet)]$ is minimized at $A = L(f_Y * w;\alpha)$, and strictly consistent if that set is the only minimizer (p. 12). The level set score is (display (11), p. 13)

$$(S')^\Gamma(A, y; w, h, \alpha) = \int_{\mathbb R^d} \bigl(\alpha - w(z - y)\bigr)\, \mathbb 1\{z \in A\}\, h(z)\, dz,$$

and the $L^2$ scoring rule of the paper is (display (3), p. 8)

$$S'(P_X, y; w, h) = \int_{\mathbb R^d} (f_X * w)^2(z)\, h(z)\, dz - 2 \int_{\mathbb R^d} (f_X * w)(z)\, w(z - y)\, h(z)\, dz.$$

In Lean these are smooth, levelSet, scoreΓ, S', cdf and heaviside in the definition item MultivarScores.LevelSet.Setting.

Formalization targets

The paper's Theorem 2 (p. 13) reads:

Let $\mathcal V^d$, $h$, and $w$ satisfy Assumption 1 in the appendix, and $w$ is nonnegative. Let $\alpha > 0$, and let $A \subseteq \mathbb R^d$ be an arbitrary Borel set. Suppose $(S')^\Gamma(A, \bullet; w, h, \alpha)$ is finite $\mathcal L^d$-a.e. and $(S')^\Gamma(A, \bullet; w, h, \alpha) f_Y(\bullet)$ is integrable. Then the following expression defines a consistent scoring function for the $\alpha$ level set $L(f_Y * w; \alpha)$: $(S')^\Gamma(A, y; w, h, \alpha) = \int_{\mathbb R^d} (\alpha - w(z - y))\, \mathbb 1\{z \in A\}\, h(z)\, dz$. (11) If $h$ is nonzero $\mathcal L^d$-a.e. and $L(f_Y * w; \alpha)$ equals the closure of $\{f_Y * w > \alpha\}$, it is strictly consistent. Moreover, with $A = L(f_X * w; \alpha)$, the integral of (11) with respect to $\alpha$ is precisely half of the $L^2$ score in (3), i.e., $\tfrac12 S'(P_X, y; w, h) = \int_0^\infty (S')^\Gamma(L(f_X * w; \alpha), y; w, h, \alpha)\, d\alpha$.

Goal: consistency

For every Borel $A$ and every $\alpha > 0$,

$$\mathbb E_{P_Y}\bigl[(S')^\Gamma(L(f_Y * w;\alpha), \bullet; w, h, \alpha)\bigr] \le \mathbb E_{P_Y}\bigl[(S')^\Gamma(A, \bullet; w, h, \alpha)\bigr].$$

This is the part of Theorem 2 that holds exactly as printed, and it is the goal.

Strict consistency (milestone)

If moreover $h \ne 0$ a.e., $\mathcal L^d\{f_Y * w = \alpha\} = 0$, and $\mathcal L^d(A \,\triangle\, L(f_Y * w;\alpha)) \ne 0$, the inequality is strict. The null-set condition replaces the printed closure condition (see Formalization scope).

Layer-cake decomposition (milestone)

$$\tfrac12 S'(P_X, y; w, h) = \int_0^\infty (S')^\Gamma\bigl(L(f_X * w;\alpha), y; w, h, \alpha\bigr)\, d\alpha.$$

The other milestones are the steps of the paper's proof (pp. 33–34): the per-realization difference $\Delta''$ (p. 33), the expected difference (19) (p. 34), and two companions: the CDF level set score (13) is consistent for $L(F_Y;\alpha)$ (p. 16), and in dimension one it equals the quantile score up to a term depending only on $y$ (Remark 2, p. 17).

Significance

Theorem 2 supplies consistent scoring functions for a whole family of multivariate level sets at once, one for each kernel $w$: CDF level sets (from $w = u$), density level sets (from $w = \delta_0$) and lower-partial-moment level sets. It thereby gives a way to rank and compare multivariate region forecasts, and in one dimension recovers the full class of quantile scores (Remark 2). The layer-cake identity explains the relation between a distribution score and its level set scores, generalizing the classical identity $\mathrm{CRPS} = 2\int_0^1(\text{quantile score})\,d\alpha$ (display (10)); the paper relates its CDF level set score to the Vorob'ev quantile scores of Fissler, Frongillo, Hlavinová and Rudloff (2021).

The result is proved in the paper's appendix (pp. 33–34). It has no machine-checked proof that this mission is aware of. Formalizing it fixes the exact integrability conditions under which the expectations exist (the paper states them loosely in Assumption 1), and it repairs the strict consistency clause, whose printed sufficient condition does not imply what the proof uses.

Difficulty

The core of consistency is a sign argument, but every quantity in it is an integral over $\mathbb R^d$ against $h$ or against $P_Y$, and none of them is a priori finite: $w$ need not be bounded or integrable, and $(S')^\Gamma(A, y)$ must be integrable in $y$ for the true level set as well as for the candidate $A$, although the paper assumes it only for $A$. Exchanging the $y$- and $z$-integrals therefore needs a product-integrability condition, not pointwise finiteness. The layer-cake milestone requires the layer cake formula for two different measures ($h\,dz$ and $w(z-y)h(z)\,dz$), with powers $2$ and $1$, followed by an exchange that keeps the sign of the second term; a nonnegative (lower) integral cannot express the difference. The strict clause needs a measure-theoretic condition on the boundary $\{f_Y * w = \alpha\}$; a topological condition on closures, as printed, is not enough.

Formalization scope

• $\mathbb R^d$ is Fin d → ℝ with volume and the Pi order; $d$ is any natural number. A distribution is a probability measure P : Measure (E d); every integral is a Bochner integral.
• The kernel $w$ is a measurable function. The paper allows a local Borel measure, so that $w = \delta_0$ gives the density level set score (12); that case is not formalized.
• Standing assumptions. $w \ge 0$ and $\alpha > 0$ (Theorem 2), $h \ge 0$ measurable and integrable (Assumption 1(a)), $A$ Borel.
• Integrability. Assumption 1 and Theorem 2's "$(S')^\Gamma(A,\bullet)$ finite a.e. and $(S')^\Gamma(A,\bullet)f_Y$ integrable" are pinned down as the single hypothesis that $(s, z) \mapsto w(z - s)h(z)$ is integrable for $P_Y \otimes \mathcal L^d$. With $w, h \ge 0$ it covers every Borel set at once, including $L(f_Y * w;\alpha)$. The layer-cake milestone uses Assumption 1(b)/(c) for the given $y$ and the almost-everywhere integrability of $w(z - \cdot)$ under $P_X$.
• No class $\mathcal V^d$. The consistency statement is pointwise in $P_Y$; its convexity is never used.
• Strict consistency is stated under $\mathcal L^d\{f_Y * w = \alpha\} = 0$ and $h \ne 0$ a.e., and "only minimizer" is read modulo $\mathcal L^d$-null sets. The printed condition "$L(f_Y * w;\alpha)$ equals the closure of $\{f_Y * w > \alpha\}$" does not imply the null-set property the proof uses: for $d = 1$, $P_Y = \delta_0$, $w = \alpha + \mathrm{dist}(\cdot, C)$ with $C$ a fat Cantor set, the closure condition holds but $\mathbb R \setminus C$ scores as well as $L$.
• Level sets use $\ge$, as in (9). The proof's partition by $\{f_Y * w > \alpha\}$ is a printed slip; the milestones use $A \setminus L$ and $L \setminus A$.
• Ruled out. Because a Bochner integral of a non-integrable function is $0$, dropping the integrability hypotheses, letting $A$ range over non-measurable sets, or fixing particular $w$ or $h$ would trivialize or change the statements; none of these is done.
• Infrastructure: Mathlib's layer cake (MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul and relatives in Mathlib/MeasureTheory/Integral/Layercake.lean) and Fubini–Tonelli (integral_prod). A reusable lemma for $\int\!\!\int g(z) w(z - s) h(z)\,dz\,dP(s) = \int g(z)(f_P * w)(z)h(z)\,dz$ is welcome; it also serves the companion mission on the $L^2$ scoring rules.

Selected references

• X. Meng, J. W. Taylor, S. Ben Taieb, S. Li, Scores for Multivariate Distributions and Level Sets, Operations Research, 2025; preprint arXiv:2002.09578v6, 2023. https://arxiv.org/abs/2002.09578
• T. Gneiting, A. E. Raftery, Strictly Proper Scoring Rules, Prediction, and Estimation, Journal of the American Statistical Association 102(477), 359–378, 2007. https://doi.org/10.1198/016214506000001437
• T. Gneiting, Making and Evaluating Point Forecasts, Journal of the American Statistical Association 106(494), 746–762, 2011. https://doi.org/10.1198/jasa.2011.r10138
• T. Fissler, R. Frongillo, J. Hlavinová, B. Rudloff, Forecast Evaluation of Quantiles, Prediction Intervals, and Other Set-Valued Functionals, Electronic Journal of Statistics 15(1), 1034–1084, 2021. https://doi.org/10.1214/21-EJS1808
• A. E. Abbas, D. V. Budescu, Y. Gu, Assessing Joint Distributions with Isoprobability Contours, Management Science 56(6), 997–1011, 2010. https://doi.org/10.1287/mnsc.1100.1157
• E. H. Lieb, M. Loss, Analysis, 2nd ed., Graduate Studies in Mathematics 14, AMS, 2001. https://doi.org/10.1090/gsm/014

Motivation

A sequence of real numbers $(m_0, m_1, m_2, \dots)$ often arrives as a list of moments: averages $\mathbb E[X^n]$ of powers of a random variable, traces $\langle T^n e, e\rangle$ of powers of a self-adjoint operator, or coefficients of a continued fraction. The Hamburger moment problem, named after Hans Ludwig Hamburger (1920–21), asks when such a list really comes from a measure on the whole real line, and, when it does, whether the measure is determined by its moments. The question sits at the junction of probability (the method of moments, identification of limit laws), spectral theory of symmetric operators and Jacobi matrices, and the theory of orthogonal polynomials; standard monographs include Shohat–Tamarkin (1943) and Schmüdgen (2017).

Timeline (as summarized in the source article and its references):

1. 1894 — Stieltjes treats the analogous problem on $[0,+\infty)$ (the Stieltjes moment problem).
2. 1920–21 — Hamburger extends the theory to the whole real line: solvability is equivalent to positivity of the Hankel kernel $(m_{j+k})$.
3. 1920s — Carleman gives a growth condition on the moments guaranteeing uniqueness (Carleman's condition); the factorial growth bound $|m_n| \le C D^n n!$ is a special case (Reed–Simon 1975, p. 205).
4. Later — the operator-theoretic treatment through self-adjoint extensions of the shift operator and its spectral measure becomes standard (Reed–Simon 1975, p. 145).

Setting

Let $m = (m_n)_{n \ge 0}$ be a sequence of real numbers. A solution of the Hamburger moment problem for $m$ is a positive Borel measure $\mu$ on $\mathbb R$ such that every power $x^n$ is $\mu$-integrable and

$$m_n = \int_{-\infty}^{\infty} x^n \, d\mu(x) \qquad (n = 0, 1, 2, \dots).$$

The sequence $m$ is a moment sequence if at least one solution exists.

The Hankel kernel of $m$ is the infinite matrix $A = (m_{j+k})_{j,k \ge 0}$. It is positive definite (in the sense of the source) if

$$\sum_{j,k \ge 0} m_{j+k}\, c_j \overline{c_k} \;\ge\; 0$$

for every finitary complex sequence $(c_j)_{j \ge 0}$, i.e. $c_j = 0$ for all but finitely many $j$. Its finite sections are the $(n+1)\times(n+1)$ Hankel matrices

$$\Delta_n = (m_{i+j})_{0 \le i,j \le n}.$$

In the Lean development these objects are IsMomentMeasure m μ, IsMomentSequence m, hankelForm m c, HankelPosDef m and hankelMatrix m n, all in the namespace HamburgerMoment.

Formalization targets

Goal — Hamburger's characterization

$$m \text{ is a moment sequence} \iff \sum_{j,k \ge 0} m_{j+k} c_j \overline{c_k} \ge 0 \text{ for every finitary } (c_j) \subset \mathbb C.$$

Milestones

1. The identity $\sum_{j,k} m_{j+k} c_j \overline{c_k} = \int |\sum_j c_j x^j|^2 \, d\mu(x)$ for any solution $\mu$, and the resulting "only if" direction.
2. The "if" direction: a positive definite Hankel kernel is the kernel of a moment sequence.
3. The solution set is convex; hence a solvable problem has either a unique solution or infinitely many.
4. Positivity of $A$ gives $\det \Delta_n \ge 0$ for all $n$; if $\det \Delta_n = 0$ for some $n$, the solution is unique and finitely supported.
5. Uniqueness under the growth bound $|m_n| \le C D^n n!$.
6. Existence of moment sequences with more than one solution.
7. The real-polynomial identity $\int p^2 \, d\mu = \sum_{j,k} a_j a_k m_{j+k} \ge 0$, and the characterization of moment sequences by positive semidefiniteness of all real Hankel matrices $\Delta_n$.

Significance

The result. Hamburger's theorem turns an existence question about measures into a family of finite-dimensional positivity conditions that can be checked on the data. It is the basic tool behind the method of moments in probability (identifying a distribution from its moments, when the problem is determinate), behind the spectral theory of Jacobi matrices, and behind Gauss quadrature and orthogonal polynomials on the line. The uniqueness criteria decide when moments determine a law; the non-uniqueness examples (for instance the log-normal distribution) show that they do not always do so.

Formalizing it. All results here are classical and proved in the literature; to the best of the captain's knowledge none of them is currently available as a formal statement in Mathlib, which has neither moment problems nor Hankel kernels. The mission produces a reusable vocabulary (moment measures, Hankel forms and matrices) and machine-checked versions of the existence theorem, the uniqueness criteria and the non-uniqueness phenomenon.

Difficulty

The "only if" direction is a direct computation. The converse is the substance: from positivity of countably many finite quadratic forms one must produce a countably additive measure on a non-compact space with all moments matching. Compactness arguments on finite sections give measures whose low-order moments match, but mass can escape to infinity and higher moments need not converge; the source's route instead goes through the Hilbert space completion of finitary sequences, self-adjoint extensions of the (generally unbounded) shift operator and the spectral theorem for unbounded self-adjoint operators — machinery that is only partly present in Mathlib. An alternative route via positive linear functionals on polynomials (M. Riesz extension, Riesz–Markov–Kakutani) has to control the same escape of mass. The uniqueness criterion requires quasi-analyticity or Carleman-type estimates.

Formalization scope

1. Sequences are m : ℕ → ℝ; measures are Measure ℝ on the Borel σ-algebra of $\mathbb R$. A solution must have every power $x^n$ integrable, so in particular $\mu$ is finite with total mass $m_0$.
2. Finitary complex sequences are finitely supported functions ℕ →₀ ℂ, and the Hankel form is the finite double sum over the support. "$\ge 0$" is the order on $\mathbb C$ (the value is a nonnegative real number), matching the source.
3. $\Delta_n$ is the real matrix indexed by Fin (n + 1); positive semidefiniteness is Mathlib's Matrix.PosSemidef.
4. Uniqueness statements quantify over all solutions; finite support means the solution vanishes outside a finite set.

Needed infrastructure and welcome contributions: polynomial integrability under finite moments, positive linear functionals on $\mathbb R[x]$, a Riesz–Markov or spectral-measure construction on $\mathbb R$, Vandermonde arguments for finitely supported measures, and Carleman / quasi-analyticity estimates. The definitions of moment measures and Hankel kernels are reusable for the Stieltjes and Hausdorff moment problems.

Selected references

• Wikipedia, Hamburger moment problem, revision oldid=1356180072, https://en.wikipedia.org/w/index.php?title=Hamburger_moment_problem&oldid=1356180072
• H. Hamburger, Über eine Erweiterung des Stieltjesschen Momentenproblems, Math. Ann. 81 (1920), 235–319; 82 (1921), 120–164, 168–187.
• M. Reed, B. Simon, Methods of Modern Mathematical Physics II: Fourier Analysis, Self-Adjointness, Academic Press, 1975, pp. 145, 205.
• T. S. Chihara, An Introduction to Orthogonal Polynomials, Gordon and Breach, 1978, pp. 56, 73.
• K. Schmüdgen, The Moment Problem, Graduate Texts in Mathematics 277, Springer, 2017. https://doi.org/10.1007/978-3-319-64546-9
• J. A. Shohat, J. D. Tamarkin, The Problem of Moments, AMS, 1943.