Completed

Functional Analysis Harmonic Analysis·Captain: Elsie66

Bochner's Theorem: Positive-Definite FunctionsTextbook

Motivation

Positive-definite functions sit at a crossroads of harmonic analysis, probability, and machine learning. A function $f:\mathbb R\to\mathbb C$ is positive-definite if, for every finite family of points $x_1,\dots,x_n$ and complex coefficients $c_1,\dots,c_n$ , the Hermitian quadratic form $\sum_{i,j}\overline{c_i}c_j f(x_i-x_j)$ is real and nonnegative. This single algebraic condition is exactly what makes $f$ realizable as: the covariance kernel of a stationary stochastic process; the characteristic function of a random variable (up to normalization); a valid Mercer/RBF kernel in machine learning; or a valid random-features/spectral density in random-feature kernel approximation methods.

Bochner's theorem (1932) is the structural reason all of these examples work: it says positive-definiteness is not merely a necessary condition for such a representation, but exactly characterizes it. A continuous, normalized ( $f(0)=1$ ) function is positive-definite if and only if it is the Fourier–Stieltjes transform of some probability measure $\nu$ on $\mathbb R$ — i.e. $f$ is the characteristic function of a random variable. This mission asks for a machine-checked proof of that theorem, together with its most useful corollary: the case where $f$ is additionally Lebesgue-integrable, so that $\nu$ has an explicit continuous density given directly by the ordinary Fourier transform of $f$ .

Setting

Fix IsPositiveDefinite f as above, for $f:\mathbb R\to\mathbb C$ (not restricted to real-valued kernels — the standard, fully general statement). A positive-definite function is automatically Hermitian-symmetric, $f(-x)=\overline{f(x)}$ (IsPositiveDefinite.conj_neg), which is exactly what makes a representation by a genuine (positive) probability measure possible, rather than a signed or complex one. The theorem works with f continuous and normalized. No further hypothesis (in particular, no integrability of f) is assumed for the general representation theorem: the representing measure $\nu$ need not be absolutely continuous (e.g. for a periodic $f$ , $\nu$ is a discrete measure supported on the harmonics of the period — this is Herglotz's 1911 theorem, the periodic special case). Under the extra hypothesis that f is Lebesgue-integrable, the representing measure becomes absolutely continuous with a continuous density: this density is fourierTransform f, the (real part of the) Fourier transform of f — automatically real-valued, again by Hermitian symmetry — and Fourier inversion recovers f from it.

Formalization targets

Goal — Bochner's theorem, general case

f \text{ continuous, positive-definite, } f(0)=1 \;\Longrightarrow\; \exists\, \nu \text{ a probability measure on } \mathbb R,\; \forall x,\; f(x) = \int_{\mathbb R} e^{i2\pi\xi x}\,d\nu(\xi).

The central representation theorem: no integrability hypothesis on $f$ , so $\nu$ may be any probability measure, not necessarily a density.

Milestone — Bochner's theorem, `L¹` (density) case

f \text{ continuous, integrable, positive-definite, } f(0)=1 \;\Longrightarrow\; \tau:=\text{fourierTransform } f \text{ is continuous}, \;\tau \ge 0,\; \int \tau = 1, \text{ and } f(x) = \int e^{i2\pi\xi x}\tau(\xi)\,d\xi.

The special case where the representing measure of the goal theorem is absolutely continuous with an explicit density — the form most directly usable in applications. Provable independently of the general goal theorem via classical Fourier-inversion machinery, so it is a natural, self-contained first target.

Significance

Bochner's theorem is one of the load-bearing structural results of 20th-century harmonic analysis: it underlies Bochner–Minlos-type theorems for random fields, the entire theory of stationary Gaussian processes, kernel methods in statistics and machine learning, and (via its periodic specialization, Herglotz's theorem) the spectral theory of stationary time series. Formalizing it gives the platform a reusable, general-purpose characterization of positive-definite functions that any future mission on kernel methods, random features, or characteristic functions can build on directly.

Difficulty

The general representation theorem is the harder target: the standard proof (see the Wikipedia article linked below) constructs, from f, a strongly continuous unitary representation of $\mathbb R$ on a Hilbert space via a GNS-type construction, then invokes Stone's theorem and the spectral theorem to extract the representing measure — a substantial functional-analytic argument, since f need not be integrable and $\nu$ need not have a density. The L¹ milestone is comparatively more tractable: it can be attacked directly via Mathlib's existing Fourier-transform and Fourier-inversion machinery for integrable functions, plus the elementary fact (already available for reuse: IsPositiveDefinite.conj_neg) that a positive-definite function is Hermitian-symmetric.

Formalization scope

IsPositiveDefinite is formalized exactly as the finite Hermitian-form condition above, over Fin n → ℝ point families and Fin n → ℂ coefficients, matching the standard convention in the literature, with f : ℝ → ℂ — the fully general, complex-valued statement, not restricted to real-valued kernels. fourierTransform f ξ is defined as the real part of ∫ Complex.exp(-i2πξ x) * f(x) dx; this is provably the exact (not merely real-part-of) Fourier transform once f is positive-definite, since Hermitian symmetry forces the integral to be real already.

Selected references

Bochner's theorem, Wikipedia — states the general locally-compact-abelian-group form and sketches the unitary-representation proof; a good map of the territory before diving into either target.
Salomon Bochner, Vorlesungen über Fouriersche Integrale, Akademische Verlagsgesellschaft, 1932.
Gustav Herglotz, Über Potenzreihen mit positivem, reellem Teil im Einheitskreis, Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, 1911.
Walter Rudin, Fourier Analysis on Groups, Interscience, 1962, Chapter 1.

8 thms2 active usersReviewed

Completed

Combinatorics Theoretical Computer Science·Captain: sr

Erdős (1947): The Probabilistic Ramsey Lower BoundResearch Paper

Motivation

Ramsey theory asks for the smallest number $R(k)$ such that every graph on $R(k)$ vertices contains either a clique of size $k$ or an independent set of size $k$ . Beyond being one of the oldest problems in extremal combinatorics, Ramsey numbers sit at the junction of combinatorics, probability, and computer science: the two-coloring of edges they quantify is exactly the distinction between a graph and its complement, and their growth controls constructions used in derandomization and in the theory of Boolean functions.

This mission formalizes the paper that started the probabilistic method as a systematic tool: Erdős's 1947 proof that $R(k) > 2^{k/2}$ . It is also the natural companion to the platform's Sipser–Gács–Lautemann mission: the union-bound argument formalized here is the same counting technique that drives the Lautemann lemma used to place $\mathsf{BPP}$ in $\Sigma_2^p$ .

Timeline. Ramsey proved in 1928 that $R(k)$ is finite; Erdős and Szekeres gave the first upper bounds in 1935; Erdős's 1947 paper supplied the exponential lower bound $R(k) > 2^{k/2}$ by a one-page counting argument, introducing the probabilistic method. Better constants for specific regimes followed (Lovász local lemma 1975, Spencer 1977), but no general lower bound beyond $2^{(1+o(1))k/2}$ is known today.

Setting

Fix an integer $k \ge 3$ and put $N = 2^{\lfloor k/2 \rfloor}$ . A graph is a pair $(V,E)$ with $E$ an irreflexive symmetric relation on $V$ ; here vertices are labeled $0, \dots, N-1$ . A subset $s \subseteq V$ of size $k$ is a clique if every two distinct vertices of $s$ are adjacent, and an independent set if every two distinct vertices of $s$ are non-adjacent. A $k$ -set that is either a clique or an independent set is monochromatic: it is monochromatic in the two-coloring of the complete graph on $V$ in which an edge is colored by the graph (present) or its complement (absent).

The ambient probability space is the uniform distribution over all graphs on $N$ labeled vertices — equivalently, each of the $\binom{N}{2}$ possible edges is present independently with probability $1/2$ . This space has exactly $2^{\binom{N}{2}}$ elements.

A graph with no monochromatic $k$ -set is a graph with neither a $k$ -clique nor an independent $k$ -set. The mission's goal, "the Ramsey number satisfies $R(k) > 2^{k/2}$ ", is formalized as the bare existence of such a graph on $N = 2^{\lfloor k/2 \rfloor}$ vertices, without defining the Ramsey number itself.

Formalization targets

Goal: the probabilistic lower bound

R(k) > 2^{k/2}, \qquad k \ge 3

i.e. there exists a graph on $N = 2^{\lfloor k/2 \rfloor}$ labeled vertices that contains no monochromatic $k$ -set.

Stronger: the three steps of the proof, as separate targets

Count estimate. For $k \ge 3$ and $N = 2^{\lfloor k/2 \rfloor}$ ,

\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1, \qquad \text{equivalently} \quad \binom{N}{k} \cdot 2 < 2^{\binom{k}{2}}.

Union-bound principle. In any finite outcome space, if the total number of outcomes ruled out by all bad events together is less than the number of outcomes, some outcome avoids every bad event:

\sum_i \left| \{\omega : \mathrm{bad}\ i\ \omega\} \right| < |\Omega| \implies \exists\, \omega, \ \forall i,\ \neg \mathrm{bad}\ i\ \omega.

Pair-count bound. Over all graphs on $N$ vertices, the total number of pairs $(G, s)$ with $s$ a monochromatic $k$ -set in $G$ is at most

\binom{N}{k} \cdot 2^{1+\binom{N}{2}-\binom{k}{2}}.

The goal follows by combining the three steps: the pair count is the sum over bad events in the union-bound principle, and the count estimate makes that sum smaller than the $2^{\binom{N}{2}}$ graphs.

Significance

The result. The lower bound $R(k) > 2^{k/2}$ is exponential, matching (up to the constant in the exponent) the best known upper bound $R(k) < 4^k$ from Erdős–Szekeres. It shows that the Ramsey function, despite being finite, grows genuinely fast — and the proof's method became more influential than the bound: the probabilistic method now permeates combinatorics, graph theory, and theoretical computer science (random graphs, discrepancy, property testing, derandomization).

Formalizing it. Mathlib currently contains no Ramsey theory at all: no definition of a Ramsey number and no lower bound. This mission closes that gap with the foundational result, in a way that is deliberately elementary — no measure theory, no randomness: the "probabilistic" argument is re-expressed as exact counting, which is why the statements are fully formalizable in Mathlib today. The union-bound principle (target 2) is a reusable lemma for future probabilistic-method formalizations, and the monochromatic-set infrastructure (targets 1 and 3) is the natural base layer for a future definition of the Ramsey number $R(k)$ .

Difficulty

The central difficulty is that the bad events — "the $k$ -set $s$ is monochromatic" — overlap heavily: a typical graph contains many monochromatic $k$ -sets, so the union bound must be crude enough to survive the overlap. Concretely, the estimate $\binom{N}{k} \cdot 2^{1-\binom{k}{2}} < 1$ holds for $N = 2^{\lfloor k/2 \rfloor}$ but fails for $N = 2^{\lfloor k/2 \rfloor+1}$ ; the naive "take one vertex more" step is where the argument breaks. A solver who tries to strengthen the bound will find the exponent is tight.

A second difficulty is purely formal: the uniform distribution over graphs has to be eliminated. The mission's statements do this by counting graphs with a fixed monochromatic $k$ -set ( $2^{1+\binom{N}{2}-\binom{k}{2}}$ of them) and applying the union-bound principle, so no probability theory enters the formalization.

Formalization scope

Representation. Graphs are SimpleGraph (Fin N): a relation on $N$ labeled vertices. A candidate set is a Finset (Fin N) of cardinality $k$ ; "monochromatic" is IsClique ∨ IsIndepSet on the graph; "no monochromatic $k$ -set" is the predicate NoMonoK. All counting is cardinality of finite sets; monoCount N k G is the number of monochromatic $k$ -sets of $G$ .

Conventions. $N = 2^{\lfloor k/2 \rfloor}$ uses natural-number division, so for odd $k$ the graph lives on $2^{(k-1)/2}$ vertices — the standard reading of $R(k) > 2^{k/2}$ . The hypothesis $k \ge 3$ is explicit. The theorem quantifies existence over all graphs; it does not define the Ramsey number $R(k)$ (a definition item for it, with the re-stated bound $R(k) > 2^{k/2}$ , is a natural follow-up contribution).

Reusability. The union-bound principle, the monochromatic- $k$ -set machinery, and the pair-count bound are all reusable beyond this mission. Welcome contributions: defining ramseyNumber and restating the bound as $R(k) > 2^{\lfloor k/2 \rfloor}$ ; the Erdős–Szekeres upper bound $R(k) \le 4^k$ as a companion mission; applications of the same principle elsewhere.

Selected references

Paul Erdős, Some remarks on the theory of graphs, Bulletin of the American Mathematical Society 53(4), 1947, pp. 292–294. https://doi.org/10.1090/S0002-9904-1947-08785-X — the source paper: main construction proving $R(k) > 2^{k/2}$ .
Noga Alon, Joel H. Spencer, The Probabilistic Method, 4th ed., Wiley, 2016 — Chapter 1 (the Erdős lower bound) and Chapter 3 (Lovász local lemma); standard exposition of the technique.
Stanisław Radziszowski, Small Ramsey Numbers, Electronic Journal of Combinatorics, Dynamic Survey DS1 — survey of Ramsey number bounds and history.

Context: where this sits in the formalization landscape

This mission is not a duplicate of existing platform content, and the choice of target is deliberate:

Mathlib gap. The pinned environment (mathlib 0df444a) contains no Ramsey-number theory at all — nothing in Combinatorics/SimpleGraph, no ramseyNumber-style definition. This mission seeds that subfield with reusable infrastructure: the monochromatic-set model, the finite union-bound (probabilistic-method) principle, and the double-counting bound are all general-purpose lemmas, not one-off steps.
Existing Ramsey content is a different quantity. The platform's fully-proved Erdos183 mission concerns multicolour triangle Ramsey numbers $R(3,\dots,3)$ and is driven by recursive palette constructions — a different Ramsey parameter and a different technique. The classical 2-colour diagonal bound formalized here appears nowhere on the platform as a proved statement.
Directly load-bearing for a live open problem. The public open problem diagonal_ramsey_asymptotics (same environment 0df444a) asks, eventually in $k$ , for $2^{\lfloor k/2 \rfloor} \le R(k,k) \le 4^k$ ; its upper half is already proved as ramsey_theory_upper_bound. The lower half is exactly what this mission's goal supplies: once ramsey_lower_bound is proved, closing that open problem reduces to a translation between the graph formulation used here (SimpleGraph / NoMonoK) and the edge-colouring formulation (ramseyDiag) used there, plus the eventual-quantifier wrapper.
Formalization convention. The bound is stated on $N = 2^{\lfloor k/2 \rfloor}$ vertices (natural-number division), matching the exponent convention of the existing platform open problem above. For even $k$ this is exactly Erdős's $2^{k/2}$ ; for odd $k$ it is the standard floor form, equivalent to the classical asymptotic reading $R(k)^{1/k} \ge \sqrt{2}$ .

5 thms2 active usersReviewed

Completed

Operations Research Optimization·Captain: Shuze Chen

Dynamic Programming and Optimal Control I: The DP AlgorithmTextbook

Motivation

Dynamic programming is the backbone of stochastic optimal control, operations research, and reinforcement learning. Its cornerstone — that the backward recursion of Bellman computes the optimal cost of a finite-horizon stochastic control problem — is stated as Proposition 1.3.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., Athena Scientific, 2005), the standard graduate text on the subject. Every convergence result for value iteration, every performance bound for approximate DP, and every correctness proof for a planning algorithm ultimately leans on this proposition. A machine-checked version of it — over a clean, reusable model of the basic problem — is the natural foundation stone for formalized control theory and RL theory alike.

Setting

The basic problem (§1.2 of the book): a discrete-time system

x_{k+1} = f_k(x_k, u_k, w_k), \qquad k = 0, 1, \dots, N-1,

with state $x_k \in S$ , control $u_k$ constrained to a finite nonempty set $U_k(x_k) \subseteq C$ , and disturbance $w_k$ drawn from a finite space $W$ with conditional probabilities $p_k(w \mid x_k, u_k)$ . A policy is a sequence $\pi = \{\mu_0, \mu_1, \dots\}$ of feedback maps $\mu_k : S \to C$ ; it is admissible if $\mu_k(x) \in U_k(x)$ everywhere. Its expected cost from $x_0$ is

J_\pi(x_0) = \mathbb{E}\Big[ g_N(x_N) + \sum_{k=0}^{N-1} g_k(x_k, \mu_k(x_k), w_k) \Big].

In the Lean development these are BertsekasDPModel, BertsekasDPPolicyCost (backward recursion on remaining stages), and the DP recursion BertsekasDPValue:

J_N = g_N, \qquad J_k(x) = \min_{u \in U_k(x)} \mathbb{E}_w\big[ g_k(x,u,w) + J_{k+1}(f_k(x,u,w)) \big].

Section 1.6 of the book develops the minimax variant, where the disturbance is chosen antagonistically from a finite membership set $W_k(x,u)$ ; the mission mirrors it with BertsekasMinimaxDPModel, BertsekasMinimaxPolicyCost, BertsekasMinimaxValue.

Target

J_0(x_0) \;=\; \min_{\pi \text{ admissible}} J_\pi(x_0), \qquad \text{with the minimum attained,}

formalized as BertsekasDP.dp_algorithm_optimality: the DP value at the horizon is an IsLeast of the set of admissible policy costs. Milestones: the min–max interchange Lemma 1.6.1 (minimax_selection_interchange) and the minimax DP validity (minimax_dp_algorithm).

Significance

The proposition itself is the license to compute optimal policies stage by stage; downstream, Missions VI and VII of this series (lookahead bounds, infinite-horizon theory) consume exactly this model and recursion. Formalizing it produces the reusable model of the basic problem — the shared vocabulary for the whole series. The result is classical and proved in the book; the contribution here is a machine-checked proof over a model faithful to the book's, with the measurable-selection subtleties deliberately avoided by finiteness (see scope).

Difficulty

The proof is a backward induction, but the standard informal argument ("interchange expectation and minimization") must be carried out honestly: the induction hypothesis is about all states simultaneously, the minimizing control must be selected as a function of the state (choice over a finite set), and the policy-cost recursion must be related to the value recursion stage by stage. The minimax milestone needs the interchange lemma with its $> -\infty$ proviso — the classic trap is losing that hypothesis and asserting a false unconditioned interchange.

Formalization scope

Finite disturbance space (Fintype W), finite nonempty control-constraint sets (Finset, inf'), arbitrary (possibly infinite) state space; expectations are finite weighted sums, probabilities are required to be distributions only at admissible controls. Stage data are total functions on $\mathbb{N}$ ; only stages $0,\dots,N-1$ matter. Policies are deterministic Markov feedback maps — for this class the book's result is exactly recovered. The trivializing risks (empty constraint sets, junk beyond horizon) are ruled out by the nonemptiness field and by evaluating at exactly $N$ remaining stages. Lemma 1.6.1 is stated in the extended reals over arbitrary types with the book's finiteness-of-infimum proviso.

Selected references

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. ISBN 1-886529-26-4. (Prop. 1.3.1, §1.2–1.3, §1.6.) http://www.athenasc.com/dpbook.html
R. Bellman, Dynamic Programming, Princeton University Press, 1957.

5 thms2 active usersReviewed

Completed

Markov Chain Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times XIII: Coupling from the PastTextbook

Motivation

Every sampling guarantee in this series so far is approximate: run the chain for $t_{\mathrm{mix}}(\varepsilon)$ steps and the output is within $\varepsilon$ of stationarity. In 1996 Propp and Wilson showed that, astonishingly, one can often sample exactly from the stationary distribution of a chain — with no error at all and no knowledge of the mixing time — by running the chain not forward from the present but from the past. Their algorithm, coupling from the past (CFTP), drives all states simultaneously with the same sequence of random update maps drawn from times $-1,-2,-3,\dots$ ; as soon as the composed map from some time $-t$ collapses the entire state space to a single value, that value is an exact sample from $\pi$ . Chapter 22 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009; the chapter is by Propp and Wilson themselves) presents the algorithm, the monotone shortcut that makes it practical for huge state spaces, and the proof of exactness. This mission — the final one of the series — formalizes that correctness proof.

Setting

Throughout, $P$ is a chain on a finite state space $V$ with stationary distribution $\pi$ . A random mapping representation of $P$ is a probability distribution $\nu$ on update functions $f:V\to V$ that reproduces the transition probabilities in one step:

\nu\{f: f(x)=y\}\;=\;P(x,y)\qquad\text{for all }x,y.

Sampling $f\sim\nu$ and applying it to the current state is exactly one $P$ -step — simultaneously from every possible current state.

CFTP draws i.i.d. maps $f_{-1},f_{-2},\dots\sim\nu$ indexed by past times and composes them forward from the past up to time zero:

F^0_{-t}\;=\;f_{-1}\circ f_{-2}\circ\cdots\circ f_{-t}.

Note the order: extending the horizon deeper into the past prepends new randomness inside the composition, while the maps near time $0$ stay fixed — this is the crucial asymmetry between running from the past and running into the future. The composition has coalesced when $F^0_{-t}$ is a constant map — all starting states have been funneled to one common value — and the algorithm outputs that value. In the monotone variant, $V$ carries a partial order with a bottom state $\hat0$ and a top state $\hat1$ and every update map is monotone; then it suffices to track the two extreme trajectories.

Formalization targets

Goal

Correctness of coupling from the past (Propp–Wilson; §22.2–22.3), the capstone of the series: if $\nu$ is a random mapping representation of $P$ , $\pi$ is stationary for $P$ , and coalescence is almost sure, then for every state $y$ the probability that the CFTP composition has coalesced to the value $y$ within $t$ steps from the past tends, as $t\to\infty$ , to exactly $\pi(y)$ — the output of the algorithm is an exact sample from the stationary distribution, with no mixing-time error term.

Milestones

Proposition 1.5 / §22.3 — every finite Markov chain has a random mapping representation: a suitable $\nu$ always exists.
Coalescence (§22.3) — if some finite composition of update maps collapses the state space with positive probability, then coalescence is almost sure: the probability that $F^0_{-t}$ is not yet constant tends to $0$ as $t\to\infty$ .
Monotone CFTP (§22.2) — if the state space has a bottom $\hat0$ and a top $\hat1$ and every update map is monotone, then the composition is constant as soon as it merely identifies $\hat0$ and $\hat1$ : checking two trajectories certifies coalescence of all of them.

Significance

The results. CFTP is one of the most striking algorithmic ideas probability has produced: a Las Vegas algorithm whose output distribution is exactly $\pi$ , side-stepping every mixing-time estimate of the previous twelve missions. The monotone shortcut is what made it explode in practice — for the Ising model of Mission IX the $2^n$ trajectories collapse to two, and Propp–Wilson famously drew exact Ising samples on large grids at the critical temperature. CFTP remains the foundation of exact-simulation methods across statistical physics, spatial statistics, and randomized algorithms.

Formalizing it. The correctness argument is short but famously slippery — the standard pitfall (running the coupling into the future yields a biased sample) is precisely a statement about the order of composition, which a formal proof pins down mercilessly. Nothing about exact sampling exists in any proof-assistant library. Formalized CFTP correctness is a fitting keystone: it consumes the random-map representation (Chapter 1), stationarity (Mission I), and the almost-sure-coalescence analysis, and certifies the algorithm practitioners actually run.

Difficulty

The whole content lies in managing the composition order and the limiting argument without measure theory. The probability space at horizon $t$ is the finite product of $t$ copies of $\nu$ (tuples of update maps, weighted by products); the key observation — for fixed $t$ , the law of $F^0_{-t}$ applied to any fixed start equals the law of $t$ forward steps — is a finite re-indexing argument. Exactness then follows from a sandwich: on the event of coalescence by time $t$ , the output equals $F^0_{-t}(x)$ for every $x$ ; choosing the start according to $\pi$ shows the output law differs from $\pi$ by at most the non-coalescence probability, and the hypothesis drives that to zero. Formalizing this needs care at exactly the point where informal proofs wave: the event "coalesced by $-t$ " is increasing in $t$ because the maps near zero are shared between horizons — the tuple encoding must make this monotonicity provable. The coalescence milestone is a geometric-trials argument (independent blocks each collapse with probability bounded below), and the monotone milestone is an induction showing monotonicity of compositions plus the squeeze between the extreme trajectories. All randomness is finite products of a finite distribution; limits are limits of explicit real sequences.

Formalization scope

Update-map distributions are functions $(V\to V)\to\mathbb R$ with the distribution predicate of Mission I; the random-map representation condition is a finite-sum identity. The composition $F^0_{-t}$ is encoded by a tuple $F:\mathrm{Fin}\,t\to(V\to V)$ with $F(i)$ the map used at time $-(i{+}1)$ , folded so that the last entry applies first — the from-the-past order. Coalescence probabilities and output probabilities are finite sums over tuples of products of $\nu$ -weights; "coalescence is almost sure" is the statement that the non-coalescence probability tends to $0$ , and the goal's conclusion is a limit of real sequences (Filter.Tendsto), not a measure-theoretic almost-sure statement. The monotone milestone is stated abstractly for any finite partial order with OrderBot and OrderTop and any tuple of monotone maps — reusable beyond CFTP. No measure theory, filtrations, or i.i.d. infrastructure is required anywhere.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009 (Chapter 22, by J. G. Propp and D. B. Wilson). https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
J. G. Propp, D. B. Wilson, Exact sampling with coupled Markov chains and applications to statistical mechanics, Random Structures Algorithms 9 (1996). https://doi.org/10.1002/(SICI)1098-2418(199608/09)9:1/2<223::AID-RSA14>3.0.CO;2-O
D. B. Wilson, How to couple from the past using a read-once source of randomness, Random Structures Algorithms 16 (2000). https://doi.org/10.1002/(SICI)1098-2418(200003)16:2<85::AID-RSA1>3.0.CO;2-H

5 thms2 active usersReviewed

Completed

Markov Chain Stochastic Systems·Captain: Shuze Chen

Markov Chains and Mixing Times II: The Convergence TheoremTextbook

Motivation

The first mission of this series established that an irreducible finite Markov chain has a unique stationary distribution $\pi$ . The present mission, covering Chapters 3–4 of Levin–Peres–Wilmer, Markov Chains and Mixing Times (AMS, 2009), answers the two questions that make that fact useful. First, the inverse problem of sampling: given a target distribution $\pi$ — uniform over proper colorings, a Gibbs measure, a posterior — how does one build a chain whose stationary distribution is $\pi$ ? The Metropolis and Glauber constructions of Chapter 3 are the universal answers, and they are the engine of Markov chain Monte Carlo across statistical physics, Bayesian statistics, and approximate counting. Second, the convergence question: in what sense, and how fast, does an irreducible aperiodic chain approach $\pi$ ? Chapter 4 introduces the total variation distance, proves the Convergence Theorem — geometric convergence to stationarity — and defines the mixing time, the parameter the entire remainder of the book estimates.

Setting

All chains live on a finite state space $V$ and are presented by row-stochastic matrices, with the definitions of Mission I. The total variation distance between distributions $\mu$ and $\nu$ is

\|\mu-\nu\|_{\mathrm{TV}} = \max_{A\subseteq V}\,|\mu(A)-\nu(A)|,

the maximal discrepancy over events. A coupling of $\mu$ and $\nu$ is a distribution on $V\times V$ whose marginals are $\mu$ and $\nu$ . For a chain $P$ with stationary $\pi$ one sets

d(t)=\max_x \|P^t(x,\cdot)-\pi\|_{\mathrm{TV}},\qquad \bar d(t)=\max_{x,y}\|P^t(x,\cdot)-P^t(y,\cdot)\|_{\mathrm{TV}},

and the mixing time is $t_{\mathrm{mix}}(\varepsilon)=\min\{t : d(t)\le\varepsilon\}$ , with $t_{\mathrm{mix}}=t_{\mathrm{mix}}(1/4)$ .

The Metropolis chain for a target $\pi$ and a symmetric proposal chain $\Psi$ accepts a proposed move $x\to y$ with probability $1\wedge \pi(y)/\pi(x)$ ; a general (not necessarily symmetric) base chain is handled by the ratio $\bigl(\pi(y)\Psi(y,x)\bigr)/\bigl(\pi(x)\Psi(x,y)\bigr)\wedge 1$ . The Glauber dynamics for a distribution $\pi$ on configurations $V^{\text{sites}}$ picks a uniform site and re-samples its value from $\pi$ conditioned on the rest.

Formalization targets

Goal

$\text{$P$ irreducible and aperiodic}\;\Longrightarrow\;\exists\,\alpha\in(0,1),\ C>0:\quad d(t)\le C\alpha^{t}.$

This is Theorem 4.9, the Convergence Theorem. It asserts only the geometric shape of convergence, leaving all quantitative rates to later missions, which is why it is the goal.

Milestones

The milestones are the chapter's working parts: stationarity and reversibility of the Metropolis chain for symmetric and general base chains (§3.2, Exercise 3.1), stationarity and reversibility of the Glauber dynamics (§3.3, Exercise 3.2); the three characterizations of total variation distance — the half- $\ell^1$ formula (Proposition 4.2 with Remark 4.3), the supremum over $[-1,1]$ -bounded test functions (Proposition 4.5), and the coupling characterization with an optimal coupling attaining it (Proposition 4.7 with Remark 4.8); the comparison $d\le\bar d\le 2d$ (Lemma 4.11) and submultiplicativity $\bar d(s+t)\le\bar d(s)\bar d(t)$ (Lemma 4.12); the standard mixing-time consequences $d(\ell\, t_{\mathrm{mix}}(\varepsilon))\le(2\varepsilon)^\ell$ and $t_{\mathrm{mix}}(\varepsilon)\le\lceil\log_2\varepsilon^{-1}\rceil\, t_{\mathrm{mix}}$ (§4.5); and the equality of distance to stationarity for a group walk and its inverse walk (Lemma 4.13 and Corollary 4.14).

Significance

The results. The Convergence Theorem is the qualitative foundation on which quantitative mixing theory stands: it guarantees that $t_{\mathrm{mix}}(\varepsilon)$ is finite, so every bound in Missions III–XIII is a bound on a well-defined quantity. The TV characterizations are used constantly — the coupling characterization is the engine of Mission III, the half- $\ell^1$ formula of every explicit computation. The Metropolis and Glauber stationarity results justify the chains analyzed in Missions III (colorings, hardcore), VIII (path coupling) and IX (Ising). Submultiplicativity of $\bar d$ is what makes $t_{\mathrm{mix}}$ a meaningful single number.

Formalizing them. None of this exists in Mathlib: there is no total variation distance for finitely supported distributions, no coupling theory, no mixing time, no MCMC correctness statement. The definition layer published here (TV distance, $d$ , $\bar d$ , $t_{\mathrm{mix}}$ , couplings, Metropolis, Glauber) is imported by every subsequent mission of the series.

Difficulty

The tempting proof of Theorem 4.9 via spectral decomposition fails twice: it needs reversibility, which the theorem does not assume, and spectral machinery that arrives only in Mission VII. The book's proof is the Doeblin decomposition: by Proposition 1.7 some power satisfies $P^r(x,y)\ge\delta\pi(y)$ , so $P^r=(1-\theta)\Pi+\theta Q$ with $\Pi$ the rank-one matrix of rows $\pi$ , and induction gives $P^{rk}=(1-\theta^k)\Pi+\theta^kQ^k$ . The formal work is matrix algebra with careful bookkeeping of the remainder chain $Q$ , plus the monotonicity of $d$ needed to interpolate between multiples of $r$ . For Proposition 4.7 the delicate half is constructing the optimal coupling: mass $\mu\wedge\nu$ on the diagonal and the normalized product of the positive parts off it, with the degenerate case $\mu=\nu$ handled separately. The Glauber stationarity statement must be phrased with care because configurations outside the support of $\pi$ have junk rows; the formalization asserts stochasticity only at supported configurations, and detailed balance globally.

Formalization scope

Total variation distance is defined as the supremum over events, $\bigsqcup_{A}\,|\mu(A)-\nu(A)|$ over Finset V, exactly as in (4.1); the half- $\ell^1$ formula is a milestone, not the definition. The mixing time is sInf of the set $\{t : d(t)\le\varepsilon\}$ in $\mathbb N$ (junk value $0$ if empty — impossible under the goal theorem). Couplings are distributions on the product with prescribed marginals; no probability-space machinery is used. The mixing-time inequalities are stated with the integer-rounding slack made explicit (e.g. $\lceil\log_2\varepsilon^{-1}\rceil$ via Nat.ceil of a real logarithm) so that no statement is true only "up to rounding". The Metropolis definitions use total real division, so the hypotheses require $\pi>0$ pointwise; this matches the book, which divides by $\pi(x)$ throughout.

Welcome contributions beyond the milestones: simp lemmas for tvDist, monotonicity of $d$ and $\bar d$ in $t$ , and triangle-inequality infrastructure — all reused by Missions III–XIII.

Selected references

D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009. https://documents.epfl.ch/groups/i/ip/ipg/www/2013-2014/Random_Walks/markovmixing.pdf
N. Metropolis, A. Rosenbluth, M. Rosenbluth, A. Teller, E. Teller, Equation of state calculations by fast computing machines, J. Chem. Phys. 21 (1953). https://doi.org/10.1063/1.1699114
W. Doeblin, Exposé de la théorie des chaînes simples constantes de Markov à un nombre fini d'états, Rev. Math. Union Interbalkan. 2 (1938).

14 thms2 active usersReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Optimal Patrol of a Perimeter: Optimal Randomized Patrol Schedule and Value of the Patrol Game Against an Observing AttackerResearch Paper

Motivation

Patrolling protects a border or facility perimeter against an intruder who needs uninterrupted time to complete an attack. The defender controls when patrollers pass; the attacker controls when to strike. In a patrol game, the question is how to time patrols when the attacker can observe them (Lin, Optimal Patrol of a Perimeter).

An observing attacker can wait until a patroller has passed before starting. Lin's result shows that a randomised schedule still gives the defender the same optimal detection probability as against a blind attacker, in closed form.

Setting

Fix three parameters: a dispatch rate $\lambda > 0$ , an attack duration $t > 0$ and a detection probability $p \in (0, 1]$ .

Defender. A pure strategy is a nondecreasing sequence of times $s_1 \le s_2 \le \cdots$ in $[0, \infty)$ at which patrollers pass a fixed location. With $N(T) = \#\{n : s_n \le T\}$ the number of patrollers dispatched by time $T$ , the sequence is feasible if it satisfies condition (1) of the paper,

\lim_{T \to \infty} \frac{N(T)}{T} = \lambda .

A mixed strategy is a probability measure $\mu$ on sequences under which almost every sequence is feasible.

Attacker. The attacker chooses an operating window $[y, z]$ with $0 < y < z$ , watches the patrollers go by, and at a time $\tau$ of his choosing starts an attack that occupies $(\tau, \tau + t]$ and must end by $z$ . The choice of $\tau$ may depend on everything observed up to and including time $\tau$ : it is a stopping time of the arrival process.

Payoff. Each patroller passing during the attack detects it independently with probability $p$ . If the attack meets $N$ patrollers it escapes with probability $(1 - p)^N$ , so the detection probability of $\tau$ against $\mu$ is

P_{\mathrm{det}}(\mu, \tau) = E_\mu\bigl[1 - (1 - p)^{N(\tau, \tau + t]}\bigr].

The defender moves first and maximises; the attacker responds and minimises. This Stackelberg game is $\Gamma(\lambda, t, p)$ . Its value is (2):

V(\lambda, t, p) = 1 - (\lambda t - \lfloor \lambda t \rfloor)(1 - p)^{\lceil \lambda t \rceil} - (1 - \lambda t + \lfloor \lambda t \rfloor)(1 - p)^{\lfloor \lambda t \rfloor}.

The claimed optimal schedule $\mu^*$ puts blue patrollers deterministically at $jt + k\Delta$ , with $\Delta = t / \lceil \lambda t \rceil$ , $j = 0, 1, 2, \dots$ and $k = 1, \dots, \lfloor \lambda t \rfloor$ . It puts a red patroller at each $jt$ independently with probability $\lambda t - \lfloor \lambda t \rfloor$ . When $\lambda t$ is an integer there are no red patrollers, and the blue ones pass at fixed intervals of $1/\lambda$ .

Formalization targets

Goal: Theorem 2

For all $\lambda > 0$ , $t > 0$ , $p \in (0, 1]$ :

$\mu^*$ is a feasible mixed strategy;
$\displaystyle \inf_{\tau} P_{\mathrm{det}}(\mu^*, \tau) \ge V(\lambda, t, p)$ over all attacks $\tau$ ;
for every feasible mixed strategy $\mu$ and $\varepsilon > 0$ there is an attack $\tau$ with $P_{\mathrm{det}}(\mu, \tau) < V(\lambda, t, p) + \varepsilon$ ;
$V$ is nondecreasing in $\lambda$ , in $t$ and in $p$ .

Items 2 and 3 state $\sup_\mu \inf_\tau P_{\mathrm{det}}(\mu, \tau) = V(\lambda, t, p)$ , attained at $\mu^*$ .

Milestones

Lemma 1 (p. 5). Among laws on $\{0, 1, 2, \dots\}$ with mean $c > 0$ , the detection probability $1 - E[(1 - p)^N]$ is at most $V$ with $\lambda t$ replaced by $c$ , and the least-variance law on $\{\lfloor c \rfloor, \lceil c \rceil\}$ attains it.
Window counting (p. 7). Every window $(a, a + t]$ with $a \ge 0$ contains exactly $\lfloor \lambda t \rfloor$ blue time points and exactly one red slot.
Feasibility (p. 7, with (1)). $\mu^*$ is a feasible mixed strategy.
Guarantee (p. 7). $P_{\mathrm{det}}(\mu^*, \tau) = V(\lambda, t, p)$ for every attack $\tau$ .
Converse (pp. 7–8). For every feasible $\mu$ and $\varepsilon > 0$ some deterministic start time $y > 0$ has $P_{\mathrm{det}}(\mu, y) < V(\lambda, t, p) + \varepsilon$ .
Monotonicity (p. 8). $V$ is nondecreasing in each argument.

Significance

The result. Watching the patrollers gives the attacker no improvement in the game value. The value interpolates $n \mapsto 1 - (1 - p)^n$ at $n = \lambda t$ , giving a closed-form trade-off between patrol rate, attack duration and detection reliability. The same schedule supports the paper's Theorem 3 (invisible patrollers) and Theorem 4 (a whole perimeter).

Formalizing it. The paper proves the result; this mission seeks a machine-checked proof. The development must specify the attacker's information, almost-sure feasibility of the random schedule, and the converse. It also supplies a reusable model of continuous-time patrol games with adaptive attackers.

Difficulty

For a fixed window, the blue count is fixed and its red slot is independent. An observing attacker instead chooses a stopping time from past arrivals. The proof must account for which red slots he has seen. The half-open window matters: with $[\tau, \tau + t)$ , an attacker starting at an empty red slot meets only $\lfloor \lambda t \rfloor$ patrollers.

The converse is harder because a feasible mixed strategy may have infinite expected count in every window even when each path has rate $\lambda$ . An argument based only on the expected count therefore fails.

Formalization scope

Lean namespace PerimeterPatrol.Visible. Schedules are maps $s : \mathbb N \to \mathbb R$ (patroller $n + 1$ passes at $s(n)$ ) with the product $\sigma$ -algebra. Feasibility requires Monotone s, $0 \le s(0)$ , and the limit (1) along atTop, with counts given by Nat.card. A mixed strategy is an IsProbabilityMeasure that is almost surely feasible. The attacker's information up to time $u$ is the $\sigma$ -algebra generated by the counts $N(v)$ , $v \le u$ . An attack is a start-time rule $\tau$ with a fixed window $[y, z]$ , $0 < y$ , such that $\{\tau \le u\}$ is measurable for that $\sigma$ -algebra for every $u$ . The detection probability is a Bochner integral of a $[0,1]$ -valued function. $\mu^*$ is the pushforward of i.i.d. uniform draws on $[0, 1]$ , with the red patroller at $jt$ present iff the $j$ -th draw is below $\lambda t - \lfloor \lambda t \rfloor$ .

Conventions committed to:

the attack window is $(\tau, \tau + t]$ , with information up to and including $\tau$ ;
the attacker may observe from time $0$ rather than from $y$ , which enlarges the attacker class, so the guarantee is at least as strong as the paper's;
"increasing" sequences may have ties;
floors and ceilings are Nat.floor and Nat.ceil, exact for positive arguments;
"increases" in (2) means nondecreasing, because $V \equiv 1$ when $p = 1$ and $\lambda t \ge 1$ ;
Lemma 1's least-variance law is claimed to be a maximiser, not the unique one (uniqueness fails at $p = 1$ ).

The attacker class includes measurable adaptive stopping times; the optimal schedule must be a probability measure; and the value is characterized through the two game inequalities rather than an unrestricted real supremum or infimum.

Needed infrastructure: counting functions of nondecreasing sequences, the stopping-time and independence argument for the red slots, the strong law of large numbers (Mathlib's ProbabilityTheory.strong_law_ae) for the long-run rate of $\mu^*$ , and an averaging argument over start times for the converse. The counting and stopping-time lemmas for point processes on $[0, \infty)$ are reusable beyond this mission. Proofs of any milestone, and alternative routes to the converse, are welcome.

Not formalized here: Theorem 3 (p. 9) as a separate item, Theorem 4 (the perimeter game, p. 10), Theorem 5 (the finite-horizon simultaneous game, p. 11) and the remarks of §2.1 and §5.

Selected references

K. Y. Lin, Optimal Patrol of a Perimeter, Operations Research, 2022, Technical Note; preprint arXiv:1905.03600v3, 2020. https://arxiv.org/abs/1905.03600v3 , https://doi.org/10.1287/opre.2021.2117

9 thms1 active userReviewed

Machine Learning Statistics·Captain: mikedeng1

Assessing Algorithmic Fairness with Unobserved Protected Class Using Data Combination: The Partial Identification Set of Demographic Disparity Is the Closed Interval with Fréchet–Hoeffding EndpointsResearch Paper

Why the disparity is uncertain

An auditor may need to measure whether a decision rule approves members of one protected group more often than members of another. The decision, the relevant outcome, and useful proxy variables may be observed in a primary dataset, while protected class and the same proxies are observed in a separate auxiliary dataset. There is no record linking the two datasets person by person. Consequently, the two observed distributions do not determine a unique joint distribution, even if they are known without sampling error. Kallus, Mao, and Zhou study what can still be said about such fairness measures from the two marginals alone (arXiv:1906.00285v2, §§2, 4–5).

The issue is relevant whenever protected labels cannot be joined to individual decisions. Proxy methods can estimate group membership, but their errors do not disappear merely because the marginal distributions are known. A set of compatible disparity values makes the uncertainty visible. This mission treats the population result in Proposition 7 of the cited preprint; estimation from finite samples and the paper's empirical case studies are separate topics.

Observed information and compatible joints

Let decision $\hat Y\in\{0,1\}$ and true outcome $Y\in\{0,1\}$ . The protected class $A\in\{a,b\}$ has two groups, with $a$ conventionally advantaged and $b$ disadvantaged. The proxy $Z$ takes values in a measurable space $\mathcal Z$ ; it may be categorical, continuous, or mixed. The primary marginal is $P(\hat Y,Y,Z)$ , and the auxiliary marginal is $P(A,Z)$ . Both share one proxy distribution $P(Z)$ , as required when they arise from a common population joint law.

For each proxy value $z$ , write $\eta_{\mathrm{aux}}(\alpha,z)=P(A=\alpha\mid Z=z)$ and $\eta_{\mathrm{priT}}(\hat y,y,z)=P(\hat Y=\hat y,Y=y\mid Z=z)$ . Their decision marginal is $\eta_{\mathrm{pri}}(\hat y,z)=\sum_y\eta_{\mathrm{priT}}(\hat y,y,z)$ . A coupling of two discrete probability vectors is a nonnegative array whose row and column sums equal those vectors. The paper's set $\mathcal P_D$ contains all measurable conditional joint arrays $\pi(\alpha,\hat y,y\mid z)$ that couple $\eta_{\mathrm{priT}}(\cdot,\cdot,z)$ and $\eta_{\mathrm{aux}}(\cdot,z)$ at each $z$ , together with the fixed $P(Z)$ . It imposes no additional assumptions on the unknown association of class and outcomes.

The demographic disparity of a compatible joint $P'$ is $\delta_{DD}(a,b;P')=P'(\hat Y=1\mid A=a)-P'(\hat Y=1\mid A=b)$ . Its partial identification set is

\Delta_{DD}(\mathcal P_D)=\{\delta_{DD}(a,b;P'):P'\in\mathcal P_D\}.

This set lists every disparity that the two observed marginals permit, rather than selecting a particular way to combine them.

Formalization targets

For a group $\alpha$ , decision $\hat y$ , and proxy value $z$ , define the Fréchet–Hoeffding weight endpoints

w^L_\alpha(\hat y,z)=\max\left\{0,1+\frac{P(A=\alpha\mid Z=z)-1}{P(\hat Y=\hat y\mid Z=z)}\right\},\qquad w^U_\alpha(\hat y,z)=\min\left\{1,\frac{P(A=\alpha\mid Z=z)}{P(\hat Y=\hat y\mid Z=z)}\right\}.

For a class weight function $w$ , let $\mu(\alpha;w)=E[w_\alpha(\hat Y,Z)\hat Y]/P(A=\alpha)$ . The goal, Proposition 7, is the equality

\Delta_{DD}(\mathcal P_D)= \left[\mu(a;w^L)-\mu(b;w^U),\;\mu(a;w^U)-\mu(b;w^L)\right].

Equality makes the interval sharp: every compatible joint produces a value inside it, and every value inside it is produced by a compatible joint. The milestones state the finite coupling bounds, the weighted description of the disparity set, the constraints on admissible weights, the numerical bounds, and attainment of both endpoint values. The source is Proposition 1, Propositions 5–7, and the proof of Proposition 7 on pp. 10 and 14–15 of the preprint (arXiv:1906.00285v2).

What the result gives

The theorem gives an exact range for the difference in group approval rates when class and decision are never observed jointly. An interval that excludes zero has an interpretation that does not depend on choosing one compatible joint law. A wide interval identifies uncertainty due to data combination itself, before finite-sample error enters. A single point signals that the observed marginals identify the demographic disparity under these conventions.

Formalizing the known result adds a reusable definition of finite couplings and a precise model of compatible conditional joints over an arbitrary measurable proxy space. The proposition is proved in the paper; the Lean goal and its milestone statements are open formalization targets. The development also records the null-cell and denominator conventions that ordinary probability notation leaves implicit. It does not claim a machine-checked proof of Proposition 7 yet.

Central difficulty

The observed data fix the class marginal and the joint decision–outcome marginal, but they do not fix their association within a proxy cell. Bounding one cell of a coupling does not by itself prove that an extreme disparity is simultaneously attainable under all marginal constraints. The true outcome $Y$ remains in the compatible-joint model even though demographic disparity uses only $\hat Y$ . When a decision cell has zero probability, a conditional class weight on that cell is undefined, so pointwise weight statements require care. A set inclusion alone would miss the sharpness claim.

Formalization scope

The Lean model uses Fin 2 for each binary outcome and a two-constructor type for protected class. It represents the two observed marginals by one probability measure on $Z$ and measurable, normalized, nonnegative conditional vectors $\eta_{\mathrm{aux}}$ and $\eta_{\mathrm{priT}}$ . The set $\mathcal P_D$ consists of measurable conditional couplings for every $z$ . Conditional probabilities in the candidate joint are ratios of integrals of that joint array. In particular, the denominator of $\delta_{DD}(a,b;P')$ is computed from $P'$ , not inserted from the auxiliary marginal.

The theorem explicitly assumes $P(A=a)>0$ and $P(A=b)>0$ , since conditioning on a group of zero probability is undefined in the paper. The paper's conditional laws are defined almost everywhere; requiring a coupling at every $z$ selects a version and does not change the attainable disparities. On a cell with $P(\hat Y=\hat y\mid Z=z)=0$ , weight identities and bounds are imposed only when that cell has positive probability; all weighted expectations multiply by the cell probability. The integrands arising from compatible joints and admissible weights are measurable and bounded on a probability space, so their real integrals are genuine expectations.

The identification set is built from compatible joint laws and their conditional disparity. Defining it directly as an interval or as the image of a chosen weight set would erase the content of the target. Finite coupling bounds and conditional-joint modeling can be reused outside demographic disparity. Contributions proving the milestone statements, handling measurable selections, and connecting coupling arrays to probability measures are within scope. Estimation, true-positive and true-negative disparities, and additional assumptions on the joint law are outside this mission.

Selected references

Nathan Kallus, Xiaojie Mao, and Angela Zhou, Assessing Algorithmic Fairness with Unobserved Protected Class Using Data Combination, Management Science 68(3), 2022; preprint arXiv:1906.00285v2, 2020. Pinned preprint.

8 thms1 active userReviewed

Economics Graph Theory Operations Research·Captain: mikedeng1

The Value of Price Discrimination in Large Random Networks: The Expected Fractional Regret of Uniform Pricing Vanishes in Erdős–Rényi Networks of Any DensityResearch Paper

Motivation

A seller whose customers influence one another faces a choice between two pricing policies. It can collect information about the social network and charge each customer a personalised price that reflects their position in it, or it can ignore the network and charge everyone one uniform price. Personalised pricing is never worse for the seller, but collecting network data is costly and raises privacy concerns. The question is how much profit the network information is worth.

For a fixed network the answer depends on its fine structure. Candogan, Bimpikis and Ozdaglar (Operations Research 2012) showed that with linear-quadratic utilities the optimal personalised prices are expressed through Bonacich centralities, so the gain from discrimination is a difference of discounted walk counts. Huang, Mani and Wang (SSRN 3368458; published in Management Science, 2021) study this gain, the value of price discrimination, in large random networks. Their main result for random networks, Theorem 5.1, says that in directed Erdős–Rényi networks the seller who prices uniformly loses only a vanishing fraction of the optimal profit, whatever the density of the network. This mission formalizes that theorem and the results its proof rests on.

Setting

There are $n$ consumers. The network is an $n\times n$ matrix $G$ with non-negative entries, where $G_{ij}$ is the influence of consumer $j$ on consumer $i$ . For a square matrix $A$ , $\|A\|$ is its spectral norm (the $\ell^2$ operator norm); $\mathbf 1$ is the all-ones vector, and $\mathbf 1^{\mathsf T}A^k\mathbf 1$ is the total weight of walks of length $k$ in $A$ .

Consumer $i$ facing price $p_i$ chooses a consumption level $x_i$ to maximise

u_i=ax_i-x_i^2+4\rho x_i\sum_{j\ne i}\frac{G_{ij}}{\|G+G^{\mathsf T}\|}x_j-p_ix_i,

with a stand-alone utility $a>0$ and a network coefficient $\rho\in(0,1)$ . The resulting consumption equilibrium is (eq. (1))

x^*(p)=\tfrac12\Big(I-\tfrac{2\rho}{\|G+G^{\mathsf T}\|}G\Big)^{-1}(a\mathbf 1-p).

The seller has marginal cost $c<a$ and profit $\pi(p)=(p-c\mathbf 1)^{\mathsf T}x^*(p)$ . The optimal profit is $\pi^*=\max_{p\in\mathbb R^n}\pi(p)$ ; the optimal uniform price is $p_0=\frac{a+c}{2}\mathbf 1$ . The regret and fractional regret of uniform pricing are

R(p_0)=\pi^*-\pi(p_0),\qquad R_F(p_0)=1-\frac{\pi(p_0)}{\pi^*}.

A directed Erdős–Rényi network $G(n,p)$ is the random $0/1$ matrix whose off-diagonal entries are independent with $\Pr[G_{ij}=1]=p$ , and whose diagonal is zero. $\mathbb E_G$ denotes expectation over it. The constants $a,c,\rho$ are the same for every $n$ .

Formalization targets

Goal: Theorem 5.1

For every sequence of densities $(p(n))_{n\in\mathbb N}$ with values in $[0,1]$ ,

\mathbb E_{G(n,p(n))}[R(p_0)]=o(n)\qquad\text{and}\qquad\mathbb E_{G(n,p(n))}[R_F(p_0)]=o(1).

Both parts are stated. The goal fixes no rate and no density regime; the paper's Theorems 5.2–5.4 give exact rates in three regimes and are not part of this mission.

Milestones

Eq. (3): $\pi^*$ is attained and equals $\frac12(\frac{a-c}{2})^2\,\mathbf 1^{\mathsf T}(I-\frac{\rho}{\|G+G^{\mathsf T}\|}(G+G^{\mathsf T}))^{-1}\mathbf 1$ , with its walk series.
Eq. (4): $p_0$ is the optimal uniform price, and $\pi(p_0)=\frac12(\frac{a-c}{2})^2\,\mathbf 1^{\mathsf T}(I-\frac{2\rho}{\|G+G^{\mathsf T}\|}G)^{-1}\mathbf 1$ .
Lemma 5.3 (for even $t$ ): $\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^k\mathbf 1\le\|G+G^{\mathsf T}\|^{k-t}\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^t\mathbf 1$ for $k\ge t$ .
Eq. (29): $\mathbb E_G[R(p_0)]\le\frac12(\frac{a-c}{2})^2\,\mathbb E_G[\frac{\rho^2}{1-\rho}\|G+G^{\mathsf T}\|^{-2}\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^2\mathbf 1]$ .
Appendix D.1, Case 1, and footnote 6: a non-empty binary network has $\|G+G^{\mathsf T}\|\ge1$ . In the footnote's words, "Therefore a non-empty network (with at lease one link) has spectral norm greater than or equal to 1."
Lemma 5.2: $\mathbb E_G[\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^2\mathbf 1]=2n(n-1)p(1-3p+2np)$ .
Lemma 5.5 (i): $\mathbb E_G[\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^k\mathbf 1]\ge2^k\mathbb E_G[\mathbf 1^{\mathsf T}G^k\mathbf 1]$ for all $k\ge0$ .
Lemma 5.5 (ii): for $1\le k<n$ and $\frac1{n-k+1}\le p<1$ , the gap in (i) is at most $(k-1)2^{k-1}P(n,k)p^{k-1}+(k-1)^k2^kP(n,k-1)p^{k-2}$ , with $P(n,k)=n!/(n-k)!$ .
Eq. (12), Rayleigh step: $\|G+G^{\mathsf T}\|\ge\mathbf 1^{\mathsf T}(G+G^{\mathsf T})\mathbf 1/\mathbf 1^{\mathsf T}\mathbf 1$ .
Eq. (9): for non-empty $G$ and $k>0$ , $0<\mathbf 1^{\mathsf T}\big((G+G^{\mathsf T})/\|G+G^{\mathsf T}\|\big)^k\mathbf 1\le n$ .
Eq. (14): $\frac n2(\frac{a-c}2)^2\le\pi^*\le\frac12(\frac{a-c}2)^2\frac n{1-\rho}$ .

The paper calls the optimal uniform price $p_0$ "under the assumption that $c<a$ , according to [12]" (p. 7); milestone 2 states that optimality as part of eq. (4).

Significance

Theorem 5.1 says that in large random networks the network information has asymptotically no value to a monopolist: the uniform price $p_0$ does not depend on the network, yet earns a fraction of the optimal profit tending to one, for sparse, critical and dense networks alike. This separates the deterministic picture, where some networks have a large value of discrimination (Theorem 4.1 of the paper characterises those with none), from the typical random one. It supplies a benchmark against which network-based pricing, and the cost of collecting network data, can be judged.

The paper proves the theorem by hand. No part of it, and no part of the model, has been machine-checked; the platform has no network pricing model and no walk-count results for directed random graphs. A complete development would make the closed forms (3) and (4), the spectral inequalities and the Erdős–Rényi walk moments reusable. The printed proof of Theorem 5.1 bounds expectations of ratios by almost-sure statements and splits the density sequence into "maximal subsequences"; a formal proof must replace these steps by quantitative ones. The printed proof of Lemma 5.5 (i) relies on a per-walk claim that fails (a closed walk $0\to1\to2\to0\to1$ in $G+G^{\mathsf T}$ can use four arcs of $G$ while it visits three ordered pairs), although the statement itself was checked by exhaustive enumeration for small $n$ ; that lemma needs a new argument.

Difficulty

The regret is a difference of two discounted walk series. Bound (29) controls it by walks of length two and the spectral norm, which suffices when the network is very sparse, but in dense networks, where $\|G+G^{\mathsf T}\|\approx2np$ and $\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^2\mathbf 1\approx4n^3p^2$ , it only gives $O(n)$ . The dense case needs the cancellation between $\mathbf 1^{\mathsf T}(G+G^{\mathsf T})^k\mathbf 1$ and $2^k\mathbf 1^{\mathsf T}G^k\mathbf 1$ for each $k$ up to a slowly growing cutoff (Lemma 5.5), together with a lower bound on the spectral norm that holds with high probability. In the critical regime $np=\Theta(1)$ , neither bound applies directly, and one needs that $\|G+G^{\mathsf T}\|$ grows with $n$ in probability. The goal quantifies over all density sequences, so the argument must be uniform across these regimes; a proof for one regime does not suffice.

Formalization scope

All objects live in the namespace NetPriceDisc.Random and are defined in one file. Networks are Matrix (Fin n) (Fin n) ℝ; the spectral norm is Mathlib's $\ell^2$ operator norm (Matrix.Norms.L2Operator). The consumption equilibrium is formula (1) for every price vector, with no non-negativity constraint on consumption, as in the paper's definition of $\pi(p)$ . $\pi^*$ is defined as the supremum of $\pi$ over $\mathbb R^n$ , and $R$ , $R_F$ from $\pi^*$ and $\pi(p_0)$ ; the closed forms (3) and (4) are theorems, not definitions, so the goal cannot be discharged by unfolding formulas. Lean's convention $x/0=0$ gives the empty network no externality, hence zero regret, which is the paper's own reading of the empty network (p. 12); the empty network keeps its probability $(1-p)^{n(n-1)}$ . The Erdős–Rényi expectation is the finite sum over arc sets $S$ of off-diagonal pairs with weight $p^{|S|}(1-p)^{n(n-1)-|S|}$ ; no measure theory is used. The fractional regret's expectation is the expectation of the ratio. "Any sequence of densities" is a function $\mathbb N\to[0,1]$ , with no further restriction.

Two printed statements are corrected and disclosed: Lemma 5.3 is stated for even $t$ (as printed it fails for odd $t$ ; for the star $K_{1,3}$ with $t=1$ , $k=2$ one gets $12>6\sqrt3$ ), and Lemma 5.5 (ii) for $k\ge1$ (at $k=0$ it involves the undefined $P(n,-1)$ ). Only the deterministic Rayleigh-quotient part of eq. (12) is stated.

Useful infrastructure includes Neumann series and Rayleigh-quotient bounds for symmetric non-negative matrices, walk moments of directed Erdős–Rényi graphs, and maximum-degree or spectral lower bounds in probability. Proofs of any milestone, and alternative routes to the goal that avoid Lemma 5.5, are welcome.

Selected references

J. Huang, A. Mani, Z. Wang, The Value of Price Discrimination in Large Random Networks, SSRN 3368458 (EC '19 submission version); published as The Value of Price Discrimination in Large Social Networks, Management Science, 2021. https://ssrn.com/abstract=3368458, https://doi.org/10.1287/mnsc.2021.4108
O. Candogan, K. Bimpikis, A. Ozdaglar, Optimal Pricing in Networks with Externalities, Operations Research 60(4), 2012. https://doi.org/10.1287/opre.1120.1066
P. Bonacich, Power and Centrality: A Family of Measures, American Journal of Sociology 92(5), 1987. https://doi.org/10.1086/228631
M. Krivelevich, B. Sudakov, The Largest Eigenvalue of Sparse Random Graphs, Combinatorics, Probability and Computing 12(1), 2003. https://doi.org/10.1017/S0963548302005424

13 thms1 active userReviewed

Algorithmic Game Theory Control Theory Stochastic Systems·Captain: mikedeng1

Dynamic Set Values for Nonzero-Sum Games with Multiple Equilibriums: The Set Value of a Continuous-Time Nonzero-Sum Stochastic Differential Game Satisfies the Dynamic Programming PrincipleResearch Paper

Motivation

A nonzero-sum game can have several Nash equilibria with different cost vectors. Selecting one equilibrium before asking how the game behaves over time loses information and may make a proposed dynamic rule depend on that selection. Feinstein, Rudloff and Zhang study the entire set of equilibrium cost vectors and ask whether it can be evaluated consistently after the game is stopped. Their continuous-time result is Theorem 3.9 of the pinned preprint, which the authors identify as the main result of the paper. It follows a discrete-time set-value principle developed earlier in the same work. The question is relevant to stochastic games whose controls use the observed path history and whose players need not share an objective.

Setting

Fix a horizon $T>0$ , a positive state dimension $d$ , and a positive number $N$ of players. The canonical path space is

\Omega=\{\omega\in C([0,T];\mathbb R^d):\omega_0=0\}.

Its coordinate process is $B_t(\omega)=\omega_t$ . The measure $\mathbb P_0$ is Wiener measure, and $\mathcal F_t$ is the filtration generated by the coordinates through time $t$ , augmented by Borel $\mathbb P_0$ -null events. Each player $i$ has a nonempty convex action set $A_i$ . A control profile $\alpha=(\alpha^1,\ldots,\alpha^N)$ consists of progressively measurable, $A_i$ -valued processes. A unilateral deviation may be any such process for that player.

The drift $b$ depends on the entire profile, while player $i$ 's running cost $f_i$ depends on that player's own action. The terminal cost vector is $\xi$ . Assumption 3.1 requires progressive measurability and boundedness of these data. Assumption 3.6 requires uniform continuity in time and path history, and uniform continuity in actions. For a history $(t,\omega)$ , concatenation $\omega\otimes_t\widetilde\omega$ holds the old path through $t$ and continues with the increment path afterward. The paper changes measure from $\mathbb P_0$ with a Girsanov density $M^{t,\omega,\alpha}_{T-t}$ , then defines the cost $J_i(t,\omega,\alpha)$ as the expected shifted terminal cost plus running cost.

An $\varepsilon$ -equilibrium is a profile whose cost for every player is at most $\varepsilon$ above the cost of every unilateral deviation. Let $O_\varepsilon(y)$ be the open Euclidean ball of radius $\varepsilon$ around $y$ . The set value is the intersection of the relaxed value sets

\mathbb V_\varepsilon(t,\omega) =\bigcup_{\alpha\in NE_\varepsilon(t,\omega)} O_\varepsilon(J(t,\omega,\alpha)),\qquad \mathbb V(t,\omega)=\bigcap_{\varepsilon>0}\mathbb V_\varepsilon(t,\omega).

The open lower envelope $\widehat{\mathbb V}_\varepsilon$ is the union of $\mathbb V_{\varepsilon'}$ over $0<\varepsilon'<\varepsilon$ . These objects are defined even if the game has no exact equilibrium.

Formalization targets

The target is Theorem 3.9 in the form (3.12) treated in its proof, at the zero history and initial time. For a stopping time $\tau$ with $\tau(0)>0$ , let $J(\tau,\eta;0,0,\alpha)$ denote the cost of the game stopped at $\tau$ with bounded $\mathcal F_\tau$ -measurable terminal vector $\eta$ . The claim is

\mathbb V(0,0)=\bigcap_{\varepsilon>0} \left\{y:\begin{array}{l} \exists\eta,\alpha\quad \alpha\in NE_\varepsilon(\tau,\eta;0,0),\\ y\in O_\varepsilon(J(\tau,\eta;0,0,\alpha)),\\ \mathbb P_0\!\left(\eta\notin \widehat{\mathbb V}_\varepsilon(\tau,B)\right)\le\varepsilon \end{array}\right\}.

The seven milestones reproduce Proposition 3.4, the density moment bound (3.6), the cost-continuity estimate (3.4), Theorem 3.7(i), Theorem 3.8, and both parts of Lemma 3.10. They cover compactness, regularity and measurability of the set value, as well as approximation of stopping data and controls.

Significance

The equality relates the set of full-horizon equilibrium costs to stopped games whose terminal payoff is approximately compatible with the continuation set value. It gives a dynamic characterization without choosing a particular equilibrium. The relaxation by the same $\varepsilon$ in equilibrium, value ball and exceptional-event probability is part of the result; removing one of those terms changes the game being characterized.

The result is proved in the cited preprint. The mission asks for machine-checked proofs of the stated theorem and its supporting results. The reusable development includes canonical finite-horizon Wiener paths, their augmented filtration, path concatenation, progressive control profiles, a coordinatewise stochastic integral interface, and set-valued equilibrium costs. The published Ethier–Kurtz definition of the Itô-integral relation is reused; it supplies a definition, not a proof of this paper's results.

Difficulty

At a stopping time, the continuation value is a set that depends on the observed path. A pointwise description does not by itself show that membership in this random set is measurable at the stopping time. Equilibrium conditions also compare a profile against every progressively measurable unilateral deviation, so their stability cannot be reduced to a comparison of finitely many actions. The Girsanov density introduces another dependency: its stochastic integral and the resulting costs must be genuine integrable random variables before inequalities between cost vectors have their intended meaning.

Formalization scope

Lean represents $\mathbb R^d$ and $\mathbb R^N$ by Euclidean spaces, with Euclidean norms on costs and the action product. Paths are continuous maps on $[0,T]$ constrained to start at zero. The canonical process is clamped outside the horizon only to make its notation total. The Wiener law is pinned by Brownian finite-dimensional distributions through $T$ and independence of coordinate processes. The filtration adds Borel null sets, so it remains a sub-σ-algebra of the Borel space. Time-indexed controls live on $[0,T]$ ; the stopping times themselves use WithTop ℝ and are constrained to that interval.

Concatenation uses the second increment strictly after $t$ , resolving the overlapping endpoint in the printed indicator formula. Player $i$ 's running cost takes only $a_i$ . The moduli in Assumption 3.6 are common and uniform in the variables specified there. The stopped running cost integrates to $\tau-t$ , with an empty interval contributing zero only outside the theorem's admissible range. The goal uses bounded measurable representatives of $L^\infty$ terminal payoffs; changing a representative on a null set leaves the expected costs and exceptional probability unchanged.

The statement must retain the full Girsanov density, all progressive deviations, the open envelope $\widehat{\mathbb V}_\varepsilon$ , and a nonzero player count. A default-zero integral for a nonintegrable payoff, an arbitrary measure in place of Wiener measure, or a restricted deviation class would trivialize or alter it. Solvers can contribute the integrability and stochastic-integral existence facts needed to establish that the definitions have their intended values, followed by proofs of the listed milestones and goal.

Selected references

Zachary Feinstein, Birgit Rudloff and Jianfeng Zhang, Dynamic Set Values for Nonzero Sum Games with Multiple Equilibriums, arXiv preprint arXiv:2002.00449v2, 2020, §§3.1–3.3. Preprint.
Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, Wiley, 1986, Chapter 5, §2. Publisher record.

14 thms1 active userReviewed

Control Theory Dynamic Programming Stochastic Systems·Captain: mikedeng1

McKean–Vlasov Optimal Control: Limit Theory and Equivalence Between Different Formulations: The N-Player Common-Noise Control Value Converges to the McKean–Vlasov ValueResearch Paper

Why this limit matters

A controller of a large population may choose a separate action for each participant while all participants experience the same random environment. The resulting optimization problem has a growing state space: with $N$ participants, the state records $N$ paths and $N$ controls. A McKean–Vlasov control problem replaces the empirical distribution of those participants by a conditional distribution given the common noise. Djete, Possamaï and Tan prove that this replacement preserves the optimal value asymptotically, even when the participants have different initial laws and the average of those laws does not converge along the full sequence. Their result is Theorem 3.6(iii) of the 2020 preprint, published in 2022.

The distinction between common and individual noise matters for this claim. Conditional on the common noise, particles can still be correlated through a controller that observes the full particle system. The paper's limit theorem concerns the supremum over all admissible predictable particle controls, rather than one prescribed feedback rule. This is the setting in which a finite population optimization problem can approximate its limiting stochastic control problem. The adjacent Proposition 3.7 describes how the limiting value changes with the initial law.

Setting

Fix a time horizon $T>0$ , state dimension $n\ge1$ , individual noise dimension $d\ge1$ , and common noise dimension $\ell\ge0$ . Let $A$ be a nonempty Polish control space with base point $a_0$ . A state or noise path belongs to $C^k=C([0,T],\mathbb R^k)$ , with its uniform norm. The coefficients $b,\sigma,\sigma_0$ determine the drift, individual diffusion and common diffusion; $L$ and $g$ determine running and terminal rewards. The Wasserstein distance $\mathcal W_p$ measures the discrepancy between probability laws with finite $p$ th moments.

For an initial law $\nu$ , the strong problem lives on the canonical space $\Omega=\mathbb R^n\times C^d\times C^\ell$ . Its initial state has law $\nu$ , and $W,B$ are independent Brownian noises relative to the canonical past. An admissible control $\alpha$ is predictable and has finite expected integrated $p$ th power of its distance from $a_0$ . The state $X^\alpha$ solves the controlled equation (2.3). Its coefficients use the conditional law $\bar\mu_t^\alpha$ of the stopped state path and current control given the history of $B$ ; its terminal reward uses the conditional law $\mu_T^\alpha$ of the stopped state path. The strong value $V_S(\nu)$ , equation (2.4), is the supremum of expected reward over those controls and their solutions. These definitions appear in Section 2.1.

For $N\ge1$ , the particle problem has initial laws $\nu^1,\ldots,\nu^N$ , separate Brownian noises $W^i$ , and one shared $B$ . Each particle follows equation (2.16) with the empirical state-control law $\varphi_t^N=N^{-1}\sum_i\delta_{(X^i_{t\wedge\cdot},\alpha_t^i)}$ inside its coefficients. The terminal reward uses the empirical state-path law $\varphi_t^{N,X}$ . Equation (2.17) defines $V_S^N(\nu^1,\ldots,\nu^N)$ as the supremum of the average expected reward. The empirical laws are built from the very particles whose equations use them; they are not outside inputs. See Section 2.4.

Formalization targets

The goal is the value comparison in Theorem 3.6(iii), equation (3.3):

\lim_{N\to\infty}\left|V_S^N(\nu^1,\ldots,\nu^N)-V_S\!\left(\frac1N\sum_{i=1}^N\nu^i\right)\right|=0.

The hypotheses include Assumptions 2.1 and 2.12, an embedding $A\subset\mathbb R^j$ for some $j\ge1$ , continuity of $L$ and $g$ , and a uniform bound on the averages of the initial $p'$ th moments, where $p'>p\ge2$ . The goal does not assume that the averaged initial laws converge. The milestones are the value lower bounds of Propositions 4.15 and 4.16, the subsequence value limit used in equation (4.44), and the initial-law stability statement (3.4) of Proposition 3.7. Each milestone records the particular clause formalized when its printed result contains additional conclusions. Theorem 3.6 and its proof give the source order.

What the result provides

The theorem compares two optimization problems, rather than only the law of a fixed controlled particle system. The comparison permits heterogeneous initial distributions and keeps the common noise in both models. Proposition 3.7 gives a separate stability statement for the limiting value when initial laws converge in $\mathcal W_p$ with uniformly bounded $p'$ th moments. Together these statements identify which finite population values are represented by the limiting control formulation. They are proved in the paper; the open task here is a machine checked derivation from faithful statements.

The formal development fixes the interfaces for conditional laws, predictable controls, path dependent coefficients, Brownian Itô integrals, empirical probability laws and extended real rewards. Those interfaces can support later formalizations of common-noise control and propagation of chaos. The present mission does not state Theorem 3.1(i), the approximation clauses of Theorem 3.1(ii)–(iii), Theorem 3.6(ii), or the “In particular” sentence after Proposition 3.7's equation (3.4). Their different conclusions require further canonical and relaxed-control structures, and the last sentence has a topology ambiguity documented in the paper notes.

Main difficulty

The usual fixed-control convergence question is smaller than the target: particle controls may depend on every observed particle and on the common noise, and the target takes a supremum before comparing values. The conditional law in the limiting equation depends on its own solution, while the empirical law in each particle equation depends on the full coupled particle system. Dropping either dependence changes the optimization problem. Uniform $p'$ th moment control must also coexist with unbounded rewards and the extended real convention for their expectations. The source proof invokes compactness and equivalence between strong, weak and relaxed formulations; formalizing those links is substantial work beyond compiling the goal statement.

Formalization scope

Lean uses EuclideanSpace and continuous maps on $[0,T]$ for the path spaces, and Frobenius norms for diffusion matrices. The control type carries a Polish Borel metric and a base point. $\mathcal P_p$ is a finite-lintegral moment condition, and $\mathcal W_p$ takes values in $\mathbb R_{\ge0}\cup\{\infty\}$ . Values are extended real suprema over admissible controls and actual solutions. Rewards use the paper's convention $\infty-\infty=-\infty$ , rather than a default zero integral. Particle counts are positive; Lean player index zero denotes the paper's player one. The case $\ell=0$ remains included.

Assumption 2.1 includes the displayed Lipschitz, growth and coercive bounds, Borel measurability, nonanticipativity, and lower semicontinuity. Assumption 2.12 factors the coefficients through the state marginal, with $\sigma_0$ independent of the control. The paper leaves the topology behind “continuous” unnamed; the formalization uses sequential $\mathcal W_p$ continuity on finite-moment laws. Its $A\subset\mathbb R^j$ is read as an isometric embedding. Solutions have continuous paths and are adapted to the completed canonical filtration, while conditional laws use the raw common-noise filtration. The goal states finiteness of both values so its real absolute difference is defined. Equation (4.44) is posed in the subsequence form used by its proof. These choices and the source's printed slips are detailed in the moderation notes.

The interface rules out a free conditional-law flow, a free particle empirical measure, and an uncharacterized Brownian law. The weak and relaxed formulations appear only as context for the paper's proof; this proposal contains the strong and particle layers needed by the four selected milestones. Contributions to the omitted equivalence and compactness results are welcome once their canonical-space definitions have been audited.

Selected references

Mao Fabrice Djete, Dylan Possamaï and Xiaolu Tan, McKean–Vlasov optimal control: limit theory and equivalence between different formulations, Mathematics of Operations Research, 2022; arXiv:2001.00925v2. The formal statements use this preprint's pagination and equation numbers.

10 thms1 active userReviewed

Operations Research Reinforcement Learning Statistics·Captain: mikedeng1

Markovian Interference in Experiments: The Differences-In-Q’s Estimator Has Bias Second Order in the Impact of the InterventionResearch Paper

Motivation

An intervention inside a continuing system can change what happens after the moment at which it is assigned. In a search service, for example, an action shown now can alter the system state that later users encounter. A simple randomized experiment therefore mixes two effects: the immediate reward of treatment and the change in the distribution of future states. Farias, Li, Peng and Zheng model this setting as a finite Markov decision process and study how to estimate the long-run effect of always using the intervention from data collected while treatment is randomized Farias et al., 2022.

The paper calls the difference between treatment and control averages the Naive estimator. It can be biased at first order in the intervention's effect on transitions, because both averages use the state distribution generated by the randomized experiment. The differences-in-Q estimator uses state-action values instead of immediate rewards. Theorem 1 asserts that its population bias is at most second order in that transition effect under a geometric mixing assumption Farias et al., 2022, Theorem 1.

Setting

Let $S$ be a finite state space. At each time, the system takes one of two actions: $0$ is control and $1$ is intervention. An action $a$ at state $s$ earns a real reward $r(s,a)$ and moves to the next state according to the row $P_a(s,\cdot)$ of a stochastic matrix $P_a$ . The control policy always selects $0$ ; the intervention policy always selects $1$ . The experiment policy selects each action with probability one half independently at each decision, so its transition matrix and expected reward vector are

P_{1/2}=\tfrac12(P_0+P_1),\qquad r_{1/2}=\tfrac12(r_0+r_1).

Write $\rho_0$ , $\rho_1$ and $\rho_{1/2}$ for stationary probability distributions of these three matrices. The average treatment effect is the difference between the long-run average rewards under always intervening and always controlling:

\mathrm{ATE}=\rho_1^{\top}r_1-\rho_0^{\top}r_0.

For the experiment policy, $Q_{1/2}(s,a)$ is the expected excess reward when action $a$ is taken first at state $s$ and the experiment policy is followed thereafter. Excess means reward relative to the experiment's stationary average reward $\rho_{1/2}^{\top}r_{1/2}$ . The idealized differences-in-Q value is

D=\sum_{s\in S}\rho_{1/2}(s)\bigl(Q_{1/2}(s,1)-Q_{1/2}(s,0)\bigr).

This is the population quantity whose bias Theorem 1 bounds. It is distinct from the finite-sample estimator calculated from a trajectory Farias et al., 2022, §3.1–3.2.

The mixing condition, Assumption 1, says that for every state $s$ and time $k\ge0$ , the total-variation distance between the $k$ -step experiment law and its stationary law is at most $C\lambda^k$ . The intervention impact is measured by a second total-variation bound, $d_{\mathrm{TV}}(P_1(s,\cdot),P_0(s,\cdot))\le\delta$ for every $s$ Farias et al., 2022, Assumption 1 and Theorem 1.

Formalization targets

Second-order population bias

The goal is Theorem 1. With $r_{\max}=\max_{s,a}|r(s,a)|$ , it asks for one polynomial $q$ , valid uniformly over all finite models and all admissible $C$ , $\lambda$ and $\delta$ , such that

|\mathrm{ATE}-D|\le q(\log C)\left(\frac1{1-\lambda}\right)^2r_{\max}\delta^2.

This formalizes the paper's statement that the unspecified constant depends polynomially on $\log C$ . The polynomial is quantified before the state space and the model, so its coefficients cannot be chosen from a particular example.

Source milestones

Five subtargets record the paper's route to this statement: Lemma 1's stationary-distribution perturbation identity; the corrected norm bound of Appendix F, Lemma 2; the corrected average-treatment-effect expansion in Eq. (6); the identification of the experiment's relative value with a group-inverse expression; and the identity that makes $D$ the first-order truncation Farias et al., 2022, pp. 13–15, 41. The goal and these milestones concern the idealized population estimator. Asymptotic normality and finite-sample estimation from Theorem 2 are outside this mission.

Significance

The result quantifies what the DQ adjustment buys in a dynamic experiment. When action-dependent transitions differ by at most $\delta$ in total variation, the population bias scales as $\delta^2$ , with an explicit dependence on the experiment chain's mixing rate and the reward bound. This provides a statement against which variants of the estimator and sharper constants can be compared Farias et al., 2022, Theorem 1.

The theorem is proved in the cited paper; the task here is to give its claim and the supporting identities machine-checkable proofs. The finite-chain definitions, perturbation identity and group-inverse bound can be reused in other average-reward Markov-chain arguments. No machine-checked proof of this theorem or these milestones was found in the local Prove2Me catalog search for this mission.

Difficulty

The immediate-reward difference averages under $\rho_{1/2}$ , whereas the treatment effect compares rewards under $\rho_1$ and $\rho_0$ . Replacing both stationary laws by $\rho_{1/2}$ therefore loses a term of order $\delta$ in general. The relative-value and Q-function expressions account for that term, but their definitions involve infinite excess-reward series. A formal proof must establish their convergence from mixing and reconcile them with the matrix group inverse. It must also control the norm of that inverse with the paper's precise row norm; using a generic matrix norm would change the claim.

Formalization scope

The state type is finite, actions are Fin 2, and reward vectors take real values. The matrices $P_0$ and $P_1$ are row stochastic. Primitivity represents the §2 standing ergodicity convention for the control and intervention policies. A stationary distribution is a nonnegative vector summing to one, so an empty state space cannot satisfy the theorem's hypotheses. Total variation is half the rowwise $\ell_1$ distance. The paper's $\|M\|_{1,\infty}$ is the maximum absolute row sum, and $\mathbf1\rho^{\top}$ is a rank-one matrix. The group inverse is represented by $(I-P+\mathbf1\rho^{\top})^{-1}-\mathbf1\rho^{\top}$ , used under hypotheses making the inverse valid Farias et al., 2022, Appendix A.

The relative value $V_{1/2}$ and action value $Q_{1/2}$ are sums of expected excess rewards, matching the reading of the paper's expectation formulas used in §3.3. They are not defined by the group inverse: the equivalence is a milestone. The idealized DQ value averages their action difference under $\rho_{1/2}$ ; the ATE uses the stationary-distribution form stated on p. 13. The goal assumes $0<\lambda<1$ , as required by the mixing expression and the denominator. Its polynomial constant is uniform over all instances. These choices exclude an instance-dependent constant or a definition that builds the desired equality into $V$ .

The Appendix F version of Lemma 2 is corrected with $C\ge1$ : without it, the one-state case permits a negative stated upper bound. Its premise bounds the maximum row norm. The p. 14 total-variation version omits the factor of two needed to convert to that norm. Accordingly, the remainder inequality and Eq. (6) milestones use the corrected Appendix F premise; their verbatim fields preserve what the paper prints Farias et al., 2022, pp. 14, 41. Contributions that establish these identities and bounds under the stated hypotheses, including reusable finite-chain matrix results and summability facts, are within scope.

Selected references

V. F. Farias, A. A. Li, T. Peng and A. Zheng, Markovian Interference in Experiments, arXiv preprint arXiv:2206.02371v2, 2022. Preprint.

8 thms1 active userReviewed

Operations Research·Captain: mikedeng1

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

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

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

Formalization targets

Goal: Proposition 2(b), corrected reading

If $b\ge\bar b$ , then

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

8 thms1 active userReviewed

Algorithmic Game Theory Combinatorics Operations Research·Captain: mikedeng1

Prophet Inequalities for Independent and Identically Distributed Random Variables from an Unknown Distribution: Without Samples, No Stopping Rule Guarantees More Than 1/e of the Expected MaximumResearch Paper

Motivation

A prophet inequality compares the value obtained by an online decision maker with the largest value in a sequence that could be chosen by someone who sees the entire sequence. The online decision maker observes values one at a time and must decide whether to accept the current value before seeing future values. When the common distribution of the values is known, that distribution can inform the stopping rule. This mission concerns the case in which the distribution is unknown and the rule receives no advance samples. The restriction is operational: the same rule must work across every possible common distribution of the observations. Correa, Dütting, Fischer and Schewior show that the familiar $1/e$ success scale of the classical secretary problem is the sharp asymptotic limit for this setting.

The result matters to online selection when historical observations are unavailable. It says that the loss from not knowing the distribution cannot be removed merely by choosing a more elaborate rule based on the values seen so far. It identifies an asymptotic ceiling that applies to every randomized stopping rule, including rules that react to exact numerical values rather than only to their ranks. The paper also studies what changes when samples are supplied; this mission isolates its zero-sample upper bound. The source paper states the result as Theorem 2 on page 6 of arXiv:1811.06114v2.

Setting

Fix a horizon $n\ge1$ . Independent observations $X_1,\ldots,X_n$ have the same unknown law $F$ on the nonnegative real numbers. A $(k,n)$ stopping rule first receives $k$ independent samples from that law and then sees the $n$ observations in order. At time $i$ , the rule returns a number $r_i\in[0,1]$ . This is its conditional probability of stopping on $X_i$ , given the samples, the observed prefix $X_1,\ldots,X_i$ , and the fact that it has not already stopped. A rule with $k=0$ has no preliminary samples. Its behavior may depend on every observed value and may be randomized.

For fixed samples $s$ and observed values $x$ , the conditional probability that the rule stops at $i$ is

\Pr(\tau=i\mid s,x) =\left(\prod_{j<i}(1-r_j(s,x_1,\ldots,x_j))\right) r_i(s,x_1,\ldots,x_i).

If it never stops, its payoff is $X_\infty=0$ . The benchmark is the prophet's maximum $M_n=\max_{1\le i\le n}X_i$ . A rule has approximation guarantee $\alpha$ when $\mathbb E_F[X_\tau]\ge\alpha\mathbb E_F[M_n]$ for every allowed law $F$ . The paper uses this model in §2, page 5, and develops the zero-sample upper bound in §3.2, pages 6–8. Correa et al.

Two restrictions of a rule appear in the supporting results. A rule is order oblivious when rearranging distinct, nonnegative values seen before the current observation does not change its current stopping probability. A rule is $\varepsilon$ value oblivious on a set $V$ when, on histories of distinct values from $V$ whose current value exceeds the earlier values, its stopping probability at time $i$ lies in $[q_i-\varepsilon,q_i+\varepsilon)$ for some $q_i\in[0,1]$ . The $q_i$ depend on the time, while the interval works for every qualifying history in $V$ . These are Definitions 1 and 2 of the paper. Correa et al.

Formalization targets

The central target is the paper's Theorem 2. For every tolerance $\delta>0$ , a single threshold $n_0$ works for all sufficiently long horizons and all zero-sample rules:

\forall\delta>0\ \exists n_0\ \forall n\ge n_0\ \forall r\ \exists F: \quad \mathbb E_F[M_n]>0, \qquad \mathbb E_F[X_\tau]\le (e^{-1}+\delta)\mathbb E_F[M_n].

The adversarial law $F$ is chosen after the rule $r$ ; the threshold $n_0$ depends only on $\delta$ . The positive benchmark makes the ratio meaningful. The law in the formal target has finite support, as does the law constructed in the paper's proof.

The milestones follow the paper's stated results and displayed bounds. Lemma 2 supplies an order-oblivious rule with the same guarantee; Lemma 3 is the infinite Ramsey statement used for an infinite monochromatic set; and Lemma 1 supplies an $\varepsilon$ value-oblivious rule on an infinite set. Equation (1) bounds the expected maximum for the paper's hard distribution. The pointwise display before equation (5) bounds the effect of replacing an approximately value-oblivious rule by a record rule. Equation (4) gives the asymptotic secretary upper bound for that record rule. In the formal statements, the $o(1)$ terms in (1) and (4) have explicit finite-horizon or $\forall\delta\,\exists n_0$ meanings. Correa et al., pp. 6–10

Significance

The theorem establishes a ceiling on the worst-case approximation ratio of any zero-sample rule. Its quantifier order matters: a rule may perform well on particular distributions, yet no single rule can exceed $1/e$ uniformly over all unknown distributions for large $n$ . Together with the paper's $1/e$ lower bound in Theorem 1, it identifies the sharp asymptotic guarantee without samples. It also gives a baseline against which the paper measures the value of additional samples. Correa et al., Theorems 1–2

The mathematical result is proved in the source paper; the work here is to give a machine-checkable statement and a decomposition that can support a Lean proof. The reusable pieces include a finite-law stopping model, exact conditional stopping probabilities, order and value obliviousness, a uniform-permutation success probability, and an infinite Ramsey statement. The theorem statements in this proposal remain open proof goals. Their compilation checks the representation and syntax, not their truth; solvers must still provide proofs.

Difficulty

The stopping rule class is large. Each $r_i$ can use the exact numerical values of all observations seen so far, and those values range over a continuum. The standard secretary bound concerns decisions based on relative ranks, so it does not immediately bound a value-dependent rule. The upper bound must apply to every such rule while allowing the adversarial distribution to depend on it. A finite hard distribution also produces repeated observations with positive probability, whereas the rank comparison that motivates the secretary bound is simplest on distinct observations. The milestones expose both issues as precise statements without building them into the goal as assumptions. Correa et al., §3.2–3.3

Formalization scope

Lean represents values by real numbers and laws by a finite support in $[0,\infty)$ with nonnegative masses summing to one. Expectations are finite sums over independent product weights. This finite-law class strengthens the existential law in Theorem 2 and restricts the distribution-uniform guarantees in Lemmas 1 and 2; the paper's upper-bound construction has finite support. The rules themselves are arbitrary real-valued functions on real sample and observation vectors, with outputs in $[0,1]$ . They are not limited to deterministic, threshold, rank-based, or measurable rules. Indices start at zero in Lean, so Lean index $0$ is the paper's time $1$ . Failure to stop has payoff zero.

The positive-benchmark clause $\mathbb E_F[M_n]>0$ rules out the point mass at zero, which would satisfy the printed existential inequality as $0\le0$ for every rule and make the target empty of content. For the same reason, the formalization uses the actual expectation of the maximum and the actual expectation selected by the rule, rather than stipulating a closed-form success bound. A set $V:\mathrm{Set}\;\mathbb N$ may contain zero in Lean, though the paper denotes positive integers by $\mathbb N$ ; infinitude is unchanged by that one extra point. The paper's Definition 2 prints $r_i$ where its quantified time is $j$ ; the formalization uses $r_j$ . The hard instance and record rule are defined from their parameters, not supplied as unrelated variables. The convention for a zero-length maximum is Lean's real supremum default, but the hard-instance bound explicitly requires $n\ge1$ .

A complete development can use Mathlib's finite sums, finite products, permutations, real exponential, and finite-set machinery. The stochastic model and its obliviousness predicates can be reused for sample-complexity variants; the Ramsey theorem is useful independently. Contributions proving the listed milestones, strengthening the finite-law model to broader distributions, or connecting the record-rule bound to an existing secretary formalization are within scope.

Selected references

José Correa, Paul Dütting, Felix Fischer and Kevin Schewior, Prophet Inequalities for I.I.D. Random Variables from an Unknown Distribution, arXiv:1811.06114v2, 2021; published in Mathematics of Operations Research, 2022. arXiv preprint

9 thms1 active userReviewed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

Correlated Equilibria and Mean Field Games: A Simple Model: Every Limit Point of Symmetric ε_N-Correlated Equilibria in Restricted Strategies Is a Correlated Mean Field Game SolutionResearch Paper

Motivation

A correlated equilibrium (Aumann, 1974) is a profile of strategies chosen by a mediator: the mediator draws a joint recommendation from a known distribution, tells each player only their own component, and no player can lower their expected cost by systematically deviating from what they are told. Correlated equilibria contain the Nash equilibria, are computable by linear programming in finite games, and model situations with a coordinating device such as a traffic authority or a market designer.

Mean field games (Lasry–Lions, Huang–Malhamé–Caines, 2006) describe Nash equilibria of games with a large number of symmetric players who interact only through the empirical distribution of their states. The limit model replaces the $N$ players by one representative player facing a flow of distributions. Campi and Fischer (arXiv:2004.06185) ask what the corresponding limit object is for correlated equilibria. Their answer is the correlated mean field game solution: a joint law of a recommendation and a random flow of measures, which, unlike a Nash mean field equilibrium, need not be deterministic. They prove that this notion is the right one in both directions: limits of $N$ -player correlated equilibria are correlated solutions (Theorem 6.1), and every correlated solution is approximated by $N$ -player approximate correlated equilibria (Theorem 7.1). This mission targets Theorem 6.1.

Setting

Fix a horizon $T\in\mathbb N$ , nonempty finite sets $\mathcal X$ (states) and $\Gamma$ (actions), and the noise space $\mathcal Z=[0,1]$ with the uniform law $\nu$ . $\mathcal P(\mathcal X)$ is the simplex of probability vectors on $\mathcal X$ with $\mathrm{dist}(m,\tilde m)=\frac12\sum_x|m(x)-\tilde m(x)|$ . The model data are a system function $\Psi(t,x,m,a,z)\in\mathcal X$ , a running cost $f(t,x,m,a)$ and a terminal cost $F(x,m)$ , with $\Psi$ measurable and $f,F$ bounded and measurable.

A restricted strategy is a map $\varphi:\{0,\dots,T-1\}\times\mathcal X\to\Gamma$ ; their finite set is $\mathcal R$ . A strategy modification is any map $u:\mathcal R\to\mathcal R$ .

The $N$ -player game. Given an initial law $\mathfrak m^N$ on $\mathcal X^N$ and a correlated profile $\gamma^N\in\mathcal P(\mathcal R^N)$ , the mediator draws $(\Phi_1,\dots,\Phi_N)\sim\gamma^N$ , independently of the initial states and of i.i.d. noises $\xi_j(t)\sim\nu$ . Player $j$ moves by

X_j(t+1)=\Psi\big(t,X_j(t),\mu_j(t),\Phi_j(t,X_j(t)),\xi_j(t+1)\big),\qquad \mu_j(t)=\tfrac1{N-1}\textstyle\sum_{l\neq j}\delta_{X_l(t)},

except that a deviating player $i$ uses $u\circ\Phi_i$ instead of $\Phi_i$ . Its cost $J_i^N(\mathfrak m^N,\gamma^N,u)$ is the expected sum of running costs plus terminal cost. $\gamma^N$ is an $\varepsilon$ -correlated equilibrium if $J_i^N(\mathfrak m^N,\gamma^N,\mathrm{Id})\le J_i^N(\mathfrak m^N,\gamma^N,u)+\varepsilon$ for all $i$ and $u$ , and symmetric if it is invariant under permutations of the players.

The mean field game. A correlated flow is $\rho\in\mathcal P(\mathcal R\times\mathcal P(\mathcal X)^{T+1})$ . The representative player starts from $X(0)\sim\mathfrak m_0$ , receives $\Phi$ jointly with a random flow $\mu=(\mu(0),\dots,\mu(T))$ , $(\Phi,\mu)\sim\rho$ , independent of $X(0)$ and of the noises, and moves by $X(t+1)=\Psi(t,X(t),\mu(t),u\circ\Phi(t,X(t)),\xi(t+1))$ with cost $J(\mathfrak m_0;\rho,u)$ . $\rho$ is a correlated solution with initial distribution $\mathfrak m_0$ (Definition 4.1) if

optimality: $J(\mathfrak m_0;\rho,\mathrm{Id})\le J(\mathfrak m_0;\rho,u)$ for every $u$ ;
consistency: with $u=\mathrm{Id}$ , $\mu(t)(\cdot)=\mathbb P\big(X(t)\in\cdot\mid\mu(0),\dots,\mu(T)\big)$ for every $t$ .

Formalization targets

Goal: Theorem 6.1

Assume (A1) $\nu\{z:\Psi(t,x,m,a,z)\neq\Psi(t,x,\tilde m,a,z)\}\le w(\mathrm{dist}(m,\tilde m))$ for a measurable $w:[0,\infty)\to[0,1]$ with $w(s)\to0$ as $s\to0^+$ , and $\Psi(t,\cdot)$ is $\tau\otimes\nu$ -a.e. continuous for every probability $\tau$ on $\mathcal X\times\mathcal P(\mathcal X)\times\Gamma$ ; (A2) $f,F$ continuous; (A3) $\gamma^N$ is a symmetric $\varepsilon_N$ -correlated equilibrium with initial law $\mathfrak m^N$ ; (A4) $\varepsilon_N\to0$ ; (A5) $\mathfrak m^N=\otimes^N\mathfrak m_{0,N}$ with $\mathfrak m_{0,N}\to\mathfrak m_0$ . Let

\rho^N=\mathbb P\circ\big(\Phi_1,\mu_1(0),\dots,\mu_1(T)\big)^{-1},\qquad N\ge2,

computed with $u=\mathrm{Id}$ . Then

\{\rho^N\}_{N\ge2}\ \text{is relatively compact in }\mathcal P(\mathcal R\times\mathcal P(\mathcal X)^{T+1}),\qquad \rho^{N_k}\to\rho\ \Longrightarrow\ \rho\ \text{is a correlated solution}.

Milestones

The milestones follow the proof: the coupling bound (2.1); the appendix lemmas on weak convergence (A.1, A.2); the coupling estimates (6.3) and (6.2) and the independence of Step Three; optimality of every limit point; the conditional-law lemmas (A.5, A.4); the pre-limit consistency identity of Step Four; Lemma A.3; consistency of every limit point.

Significance

Theorem 6.1 identifies the limit model of large symmetric games played with a mediator. It shows that correlation does not disappear in the limit: the flow of measures recommended by the mediator may remain random, and the limit object must record its joint law with the recommendation. Together with Theorem 7.1 it makes correlated mean field game solutions the exact counterpart of $N$ -player correlated equilibria, as mean field equilibria are of Nash equilibria. The example of Section 5 of the paper exhibits a correlated solution with a non-deterministic flow that is not a mixture of deterministic-flow solutions.

The result is proved in the paper; to our knowledge no part of it, nor any correlated-equilibrium mean field result, has been formalized. The mission produces a machine-checked model of discrete-time finite-state mean field games with a mediator, and general-purpose lemmas absent from Mathlib: a mapping theorem for almost everywhere continuous maps that identifies limits of relations $Y_n=\Psi(Z_n)$ , converging together on varying probability spaces, limits of regular conditional distributions, and the conditional law of an exchangeable coordinate given the empirical measure.

Difficulty

Compactness is immediate because all spaces are compact. The content is in identifying the limit. Two obvious steps fail. First, the system function is discontinuous (as in Remark 6.1), so the dynamics do not pass to the limit by the continuous mapping theorem; only almost-everywhere continuity with respect to measures of the form $\tau\otimes\nu$ is available. Second, a unilateral deviation by player 1 changes the empirical measures seen by all other players, and through them the whole flow, so it is not clear that the limit flow under a deviation is the limit flow without it. Third, conditional laws are not continuous under convergence in distribution, yet consistency, a statement about the conditional law of the state given the whole flow, must survive the limit.

Formalization scope

The Lean development lives in the namespace SimpleCorrMFG.Conv. $\mathcal P(\mathcal X)$ is stdSimplex ℝ X with its subspace topology and Borel σ-algebra; flows are Fin (T+1) → P(X); restricted strategies are Fin T → X → Γ; times of actions and noises are Fin T (the noise $\xi(t+1)$ has index $t$ ); players are Fin N and the paper's player 1 is index 0; $\nu$ is volume on unitInterval. Probability measures on $\mathcal R\times\mathcal P(\mathcal X)^{T+1}$ are Mathlib's ProbabilityMeasure with the topology of weak convergence, and a limit point is the limit of a subsequence with strictly increasing indices.

The paper defines costs and $\rho^N$ through "any realization" and notes that they do not depend on the choice. The formalization uses the canonical realization: the product law of initial states, recommendations (or the correlated flow) and noises, with the states computed by the recursion. The consistency condition is stated as $\mathbb P(X(t)=x,\ \mu\in B)=\mathbb E[\mathbf 1_B(\mu)\,\mu(t)(\{x\})]$ for every $t$ , $x$ and Borel $B$ , which is the definition of a regular conditional distribution given the whole flow. (A3) is required for $N\ge2$ , where the $N$ -player game is defined.

A formalization in which the flow is conditioned only up to time $t$ , in which the costs are integrals of possibly non-integrable functions, or in which "limit point" refers to a topology other than weak convergence would prove a different and weaker statement and is excluded. The standing assumptions that $\Psi$ is measurable and $f,F$ are bounded and measurable are carried explicitly, so that no expected cost or law is a junk value.

Contributions are welcome on each milestone. The appendix lemmas are independent of the game and reusable. The written proof of (6.2) uses $\mathbb E[w(\mathrm{dist})]\to0$ ; since (A1) does not require $w(0)=0$ , this step needs the observation that the indicator in (A1) vanishes when the two measures coincide.

Selected references

L. Campi, M. Fischer, Correlated equilibria and mean field games: a simple model, arXiv:2004.06185v2, 2021; Mathematics of Operations Research, 2022. https://arxiv.org/abs/2004.06185
R. J. Aumann, Subjectivity and correlation in randomized strategies, Journal of Mathematical Economics 1, 67–96, 1974. https://doi.org/10.1016/0304-4068(74)90037-8
S. Hart, D. Schmeidler, Existence of correlated equilibria, Mathematics of Operations Research 14(1), 18–25, 1989. https://doi.org/10.1287/moor.14.1.18
J.-M. Lasry, P.-L. Lions, Mean field games, Japanese Journal of Mathematics 2, 229–260, 2007. https://doi.org/10.1007/s11537-007-0657-8
D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit, Annals of Applied Probability 30(4), 1693–1761, 2020. https://doi.org/10.1214/19-AAP1541
P. Billingsley, Convergence of Probability Measures, Wiley, 1968.
O. Kallenberg, Foundations of Modern Probability, 2nd ed., Springer, 2001 (Lemma 11.11). https://doi.org/10.1007/978-1-4757-4015-8

18 thms1 active userReviewed

Operations Research Optimization·Captain: mikedeng1

The Discrete Moment Problem with Nonconvex Shape Constraints: Optimal Extreme Point Solutions of the Log-Concave Discrete Moment Problem Are Piecewise Geometric with at Most m PiecesResearch Paper

Motivation

A discrete moment problem asks for the largest expected payoff compatible with prescribed moments of an unknown probability distribution. A decision maker may know the first few moments of demand or loss while the full distribution remains uncertain. The optimization then asks which compatible distribution makes a chosen payoff largest. Chen, He, Jiang, Ryan, and Zhang study what happens when the distribution must also obey a shape constraint. Their preprint treats discrete log-concavity and increasing failure rate as two such constraints. This mission concerns the log-concave case.

The moment constraints alone define a convex polytope of probability vectors. Requiring log-concavity changes its geometry: the feasible region is generally nonconvex. This matters because familiar descriptions of extreme points of a moment polytope no longer describe the candidate worst-case distributions. The paper's Theorem 4.1 gives a finite structural description of the optimal extreme points despite that change. Its proof uses a general result about optimization over reverse convex constraints, Theorem 3.6, which is also included as a milestone. Both statements and their setting are taken from arXiv:1708.02079v1, pages 5–15.

Setting

Fix the finite sample space $\Omega=\{1,\ldots,n\}$ . A distribution is a vector $x=(x_1,\ldots,x_n)$ of nonnegative masses. For each integer $i$ from $0$ through $m$ , its prescribed moment is $q_i$ , so $\sum_{j=1}^{n}j^i x_j=q_i$ . The convention $q_0=1$ makes the masses sum to one. Given payoff coefficients $f_j$ , the discrete moment problem maximizes $\sum_{j=1}^{n}f_jx_j$ over the distributions satisfying these equations.

A distribution is discrete log-concave when its positive masses form one consecutive integer interval $[k,\ell]$ and $x_{j-1}x_{j+1}\le x_j^2$ at every interior index $k<j<\ell$ . In the paper's formulation (DMP-LC), the entries on $[k,\ell]$ are strictly positive and the other entries are zero; the feasible region is the union over all such supports. Its alternative formulation (DMP-LC′) replaces the chosen support with nonnegativity and a family of longer-range inequalities. Proposition 2.4 says that the two feasible regions coincide. The extreme points in this mission are those of the entire feasible region, including every possible support.

The paper also considers a general reverse convex program in $\mathbb R^n$ : minimize a function $c(x)$ subject to $Ax=b$ , $x\ge0$ , and $f_p(x)\le0$ for $p=1,\ldots,P$ . Here the reverse convex condition is relative to the nonnegative orthant: the forbidden set $\{x\ge0:f_p(x)>0\}$ is convex. Under the paper's continuity, quasiconcavity, differentiability, rank, and compactness assumptions, Theorem 3.6 counts the inequalities that are tight at an optimal extreme point.

Formalization targets

The goal is the corrected mathematical content of Theorem 4.1. If (DMP-LC) is feasible, an optimal extreme point exists. Every optimal extreme point $x^*$ has support $[k,\ell]$ and can be covered by at most $m$ geometric pieces. In symbols, there are weakly increasing breakpoints $k=b_0\le b_1\le\cdots\le b_m=\ell$ and positive parameters $\alpha_i,r_i$ such that

x_j^*=\alpha_i r_i^{j-b_{i-1}}\quad\text{for }b_{i-1}\le j\le b_i, \qquad x_j^*=0\quad\text{outside }[k,\ell].

The milestone path includes the equivalence of the two feasible formulations, compact-set extreme-point results, convexity of the forbidden power regions, the reverse convex tight-constraint count, and the two structural steps in the proof of Theorem 4.1. Theorem 3.6 asserts, in particular, that at each optimal extreme point of its $m$ -row program,

n-m\le \#\{p:f_p(x^*)=0\}+\#\{j:x_j^*=0\}.

Significance

The conclusion replaces an unrestricted search over feasible probability vectors with a characterization of the candidates that can be optimal extreme points. It also identifies how the number of prescribed nonzero-order moments controls the number of geometric pieces. The count in Theorem 3.6 applies to the larger class of reverse convex programs described above; it is useful independently of this distributional example. These are results proved in the cited preprint, rather than open conjectures.

The formalization target is to give the known statements a machine-checked proof in Lean. The proposed items are statements with proof placeholders; they do not yet assert that a machine-checked proof exists. The finite moment notation, the log-concave feasible region, and the reverse convex feasible region are separate definition files so the general finite-dimensional objects can be reused. Contributions to the milestone theorems, the proof of the goal, and supporting lemmas are all in scope.

Difficulty

The log-concavity inequalities do not make the feasible region convex, so the standard convex-polytope description of optimal extreme points does not directly apply. In addition, the chosen support may move: a vector that is extreme within one fixed-support slice need not be extreme in the full union. Existence of an optimal solution alone gives no bound on the number of geometric pieces. The challenge is to obtain enough tight constraints at every optimal extreme point, then relate those equalities to its coordinates without assuming the desired shape in the definition of feasibility.

Formalization scope

Lean represents $\mathbb R^n$ as Fin n → ℝ; a Fin n index with value $j-1$ represents the paper's position $j$ . The helper ext supplies the paper's one-based coordinates and returns zero outside $[1,n]$ . Moments use the exact weights $w_j=j$ . All feasible sets use real vectors, with nonnegativity or strict positivity stated where the paper requires it. The (DMP-LC) region is the union over supports satisfying (2b)–(2e); the goal uses extreme points of that whole set and a maximization objective. The reverse convex milestones use minimization, full row rank, and convexity of the forbidden sets inside the nonnegative orthant. Compactness and nonemptiness are explicit assumptions where the source invokes them.

Two corrections to the printed Theorem 4.1 are necessary. First, its bound $0<r_i<1$ is false. With $n=3$ , $m=1$ , $q_0=1$ , $q_1=5/2$ , and payoff $f=(1,0,0)$ , the unique maximizing extreme point is approximately $(0.1162,0.2676,0.6162)$ , whose geometric ratio is about $2.30$ . The formal statement requires $r_i>0$ . Second, the printed strict chain of breakpoints fails for short supports: with $n=3$ , $m=2$ , and moments $(q_0,q_1,q_2)=(1,2,4)$ , the only feasible distribution is the point mass at $2$ . Weak breakpoints express the paper's “at most $m$ pieces” conclusion. They allow degenerate pieces; $m=0$ is retained and forces a point mass. The proof's closed-range wording for tight equalities is read on interior indices, and the tight count uses $m+1$ moment rows. These choices and the paper's typographical slips are recorded with the items.

The feasible region does not encode geometric sequences, and extremeness is never taken only within one support or within its convex hull. The development needs Mathlib's finite sums, finite-dimensional topology, convex hulls, extreme points, matrix rank, continuity, quasiconcavity, and differentiation. The finite discrete moment definition and reverse convex feasible-set definition are intended for reuse beyond this paper.

Selected references

X. Chen, S. He, B. Jiang, C. T. Ryan, and T. Zhang, The Discrete Moment Problem with Nonconvex Shape Constraints, preprint arXiv:1708.02079v1, 2017; published in Operations Research, 2021. Pinned preprint.

14 thms1 active userReviewed

Operations Research Statistics·Captain: mikedeng1

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

Motivation

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

Setting

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

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

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

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

Formalization targets

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

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

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

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

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

Selected references

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

7 thms1 active userReviewed

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

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

Why this game matters

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

Game and costs

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

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

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

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

Formalization targets

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

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

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

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

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

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

What the result provides

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

Main obstacles

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

Formalization scope

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

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

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

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

Selected references

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

11 thms1 active userReviewed

Economics Operations Research·Captain: mikedeng1

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

Motivation

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

The answer depends on the setting:

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 1

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

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

Milestones

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

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

Significance

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

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

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

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

Difficulty

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

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

The paper handles this with three ingredients:

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

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

Formalization scope

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

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

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

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

Contributions are welcome on two kinds of work:

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

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

Selected references

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

12 thms1 active userReviewed

Economics Operations Research·Captain: mikedeng1

Optimal Financing and Disclosure: Truthfully Revealing Whether Cash Flows Exceed the Threshold at Which the Financing Constraint Binds Is an Optimal Disclosure PolicyResearch Paper

Motivation

A firm that needs outside money to start a project knows more about the project than its investors do, and it can usually choose how much of that knowledge to reveal before raising funds: which audits to commission, which metrics to report, how informative an analyst's report will be. The security-design literature studies the security side of this problem, meaning what claim to sell given the information the investors have (Innes, 1990; Nachman and Noe, RFS 1994). The Bayesian persuasion literature (Kamenica and Gentzkow, Bayesian Persuasion, AER 2011) studies the information side, meaning what to reveal when a sender can commit to a signal in advance.

M. Szydlowski, Optimal Financing and Disclosure (Management Science 2021; working paper of March 2017), puts the two together. An entrepreneur who cannot finance a project on the prior alone commits to a disclosure policy so as to maximize her expected payoff, subject to the investors' competitive pricing. The main answer is simple and testable: the optimal policy is a pass/fail test, and the passing standard is set exactly where investors break even. This mission formalizes that answer and the chain of lemmas the paper's appendix uses to reach it.

Setting

The project pays $s \in [0,1]$ . The investment cost is $I \in (0,1)$ . The entrepreneur sells a security with payoff $c(s)$ to competitive investors. $c$ is continuous, $0 \le c(s) \le s$ , and both $c(s)$ and the residual $s - c(s)$ are weakly increasing (equity, debt $\min(s,R)$ and options all qualify). The common prior over $s$ has a continuous density $\mu_0$ with support $[0,1]$ .

A posterior is a probability measure $\mu$ on $[0,1]$ . At posterior $\mu$ the security sells for $p(\mu) = \mathbb E_\mu c(s)$ (1), and the project is financed iff $p(\mu) \ge I$ (2). If it is financed, the entrepreneur receives the residual, a private benefit $B > 0$ , and a share $\lambda \in [0,1]$ of the excess cash, so her payoff (3) is

V(\mu) = \mathbb E_\mu[s - c(s) + B] + \lambda\big(\mathbb E_\mu c(s) - I\big) \ \text{ if } \mathbb E_\mu c(s) \ge I, \qquad V(\mu) = 0 \text{ otherwise}.

A disclosure policy induces a distribution $\tau$ over posteriors. By Kamenica and Gentzkow's equivalence, the feasible $\tau$ are exactly the Bayes-plausible ones, those whose mean posterior is the prior, $\mathbb E_\tau \mu = \mu_0$ (5). The entrepreneur's problem (6) is to maximize $\mathbb E_\tau V(\mu)$ over Bayes-plausible $\tau$ . The threshold policy with cutoff $t$ reveals only whether $s \ge t$ . With probability $q = \int_t^1 \mu_0$ it produces the posterior $\mu_h = \mu_0 / q$ on $[t,1]$ , and otherwise the posterior $\mu_l = \mu_0/(1-q)$ on $[0,t)$ ; this is (17).

Throughout, the project cannot be financed without disclosure: $\mathbb E_{\mu_0} c(s) < I$ (§4).

Formalization targets

Goal: Proposition 1 (p. 18)

There is a threshold $\hat s \in (0,1]$ at which the financing constraint (20) binds,

\int_{\hat s}^1 \big(c(s) - I\big)\,\mu_0(s)\,ds = 0,

such that the threshold policy with cutoff $\hat s$ is Bayes plausible and attains the maximum of $\mathbb E_\tau V(\mu)$ over every Bayes-plausible $\tau$ . The hypothesis $\lambda I \le B$ is added, as explained under Formalization scope.

Milestones (proof of Proposition 1, Appendix A)

Lemma 1 (p. 15): every Bayes-plausible $\tau$ can be replaced, at the same value, by one with two posteriors $\mu_h, \mu_l$ with densities and $\mathbb E_{\mu_l} c < \mathbb E_{\mu_0} c < I \le \mathbb E_{\mu_h} c$ .
Lemma 3 (p. 35): at an optimum of the relaxed fixed- $q$ problem (31), the mass constraint and the financing constraint cannot both be slack.
Lemma 4 (p. 36): the states with nonnegative marginal contribution form an interval $\hat S = [\hat s, 1]$ .
Proposition 7 (p. 33): for fixed $q \in (0,1)$ , the threshold density (17) solves problem (30).
Lemma 5 (p. 38, monotonicity part): the fixed- $q$ value $V(q)$ is strictly increasing in $q$ .
Lemma 6 (p. 38): there is a maximal feasible $\bar q \in (0,1)$ , and $\hat s(\bar q)$ makes (20) bind.
Proposition 8 (p. 37, first case): the optimal two-posterior value is $V^* = \int_{\hat s}^1 (s - c(s) + B)\,\mu_0(s)\,ds$ (37), attained by (17) with the binding $\hat s$ .

Significance

Proposition 1 gives disclosure a concrete shape: certify whether cash flows clear a bar, and say nothing more. The bar is the lowest one at which investors still break even, so the entrepreneur maximizes the probability of financing. The paper's later results build on it: the choice of the optimal security (Proposition 4), extensions to general utility (Proposition 5), and comparative statics of the threshold in the security's information sensitivity (Propositions 2–3).

The result is proved on paper but has not been machine-checked. A formalization adds three things. It checks a proof whose central step goes through an infinite-dimensional linear-programming duality (Levinson, 1966). It pins down hypotheses the printed statement omits, notably $\lambda I \le B$ . And it provides a reusable Lean account of Bayesian persuasion over a continuum of states, with distributions over posteriors as measures on the space of measures.

Difficulty

The obvious argument is a bang-bang argument. Fix the probability $q$ of financing, put as much high-posterior mass as possible on the best states, then optimize over $q$ . Each step hides a gap. The reduction to two posteriors (Lemma 1) needs barycentres of a measure on the space of measures. The fixed- $q$ problem is a linear program over densities with a pointwise cap $\mu_h \le \mu_0/q$ , so finite-dimensional LP duality does not apply. The paper uses an infinite-dimensional duality theorem plus a compactness lemma under an extra equicontinuity restriction (32).

Monotonicity of the value in $q$ is where the printed argument fails in general. The marginal contribution $s - c(s) + B + \lambda(c(s) - I)$ can be negative near the cutoff when $\lambda I > B$ . In that case a slack threshold beats the binding one, and the binding threshold is not optimal. A second trap is that the binding root of (20) need not be unique: for debt, every cutoff above the face value can solve (20) with equality. " $\hat s$ solves (20)" therefore cannot by itself be the content of the theorem.

Formalization scope

The state space is $\mathbb R$ , and $c$ and $\mu_0$ are read only on $[0,1]$ . The prior is Lebesgue measure on $[0,1]$ with density $\mu_0$ . Support $[0,1]$ is encoded as positive prior mass on every nondegenerate subinterval. Posteriors are arbitrary measures on $\mathbb R$ , and a distribution over posteriors is a measure on the space of measures with Mathlib's Giry σ-algebra. Bayes plausibility is: $\tau$ is a probability measure, almost every posterior is a probability measure, and $\tau$ 's monadic join is the prior. Posterior expectations are integrals over $[0,1]$ , written through positive and negative parts so that they are measurable in the posterior. As a result $\mathbb E_\tau V(\mu)$ is never a junk value. Ties in the financing rule go to financing ( $\ge$ ). "Increasing" means weakly increasing. The fixed- $q$ problems range over integrable densities with $0 \le \mu_h \le \mu_0/q$ pointwise, which encodes $\mu_l \ge 0$ . The equicontinuity restriction (32) is dropped; it serves only the compactness Lemma 2, which is not formalized.

Two hypotheses are added, each disclosed in the items that carry it:

$\lambda I \le B$ , on the goal and on Lemma 3, Lemma 5 and Proposition 8. Without it the printed results are false. For $\mu_0 = 1$ , $c(s) = s$ , $I = 0.6$ , $B = 0.1$ and $\lambda = 1$ , the binding threshold $\hat s = 0.2$ earns $0.08$ , while revealing whether $s \ge 0.5$ earns $0.125$ . The hypothesis covers $\lambda = 0$ , the case §5 uses.
$I < c(1)$ , on Lemma 6 and Proposition 8, where $\bar q \in (0,1)$ requires that something can be financed.

The goal quantifies over all Bayes-plausible distributions over posteriors, and its threshold is pinned by optimality, not only by solving (20). A version restricted to threshold or two-point policies, or one whose $\hat s$ is any root of (20), would be a different and weaker theorem. Optimality is stated as "an optimal policy", since the optimum is not unique.

Not formalized: Lemma 2 (compactness); the continuity and differentiability parts of Lemma 5; the second case of Proposition 8 ( $\mathbb E_{\mu_0} c \ge I$ ); and the paper's later Propositions 2–6, 9 and 10. The general definitions of Bayes plausibility and of the reveal-a-cell policy are stated for an arbitrary measurable state space and are reusable for other persuasion missions. Contributions are welcome on any milestone. A barycentre construction for measures on the space of measures (Lemma 1) and a bathtub principle for densities under a pointwise cap (Proposition 7) are of independent use.

Selected references

M. Szydlowski, Optimal Financing and Disclosure, working paper, version of March 2017; published in Management Science 67(1), 2021. https://doi.org/10.1287/mnsc.2019.3462
E. Kamenica and M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
N. Levinson, A class of continuous linear programming problems, Journal of Mathematical Analysis and Applications 16(1), 73–83, 1966.
R. D. Innes, Limited liability and incentive contracting with ex-ante action choices, Journal of Economic Theory 52(1), 45–67, 1990.
D. C. Nachman and T. H. Noe, Optimal design of securities under asymmetric information, Review of Financial Studies 7(1), 1–44, 1994. https://doi.org/10.1093/rfs/7.1.1

10 thms1 active userReviewed

Algorithmic Game Theory Economics Operations Research·Captain: mikedeng1

The Role of Participation in Innovation Contests: Multiple Rewards Are Optimal Exactly When Entry Is Costly, the Budget Is Large and a Failed Contest Is CostlyResearch Paper

Why reward design depends on entry

An innovation contest asks people outside a firm to submit solutions and promises payments according to the rank of their submissions. The firm would like a strong best submission, but a potential solver must decide whether entering is worth a fixed cost before knowing who else will enter. Paying only the winner can encourage effort while leaving the contest with no entries. Paying several ranks can make entry more attractive while spreading the reward budget across more people. Stouras, Hutchison-Krupat and Chao study that tradeoff in a model where the firm values the best solution and pays a penalty if the contest receives none (accepted SSRN version, Sections 3–5.1).

The question is operational: given a budget and entry cost, how many ranks should receive a positive reward? The paper's Theorem 2 describes regimes in which a winner-take-all allocation is optimal and regimes in which the optimum pays several ranks. Its supporting results connect the equilibrium entry threshold to the number of entrants and identify allocations that maximize participation (Theorems 1–2, pp. 10–12).

Contest and ability model

There are $n$ potential solvers, with $n\ge2$ . Their abilities $A_i$ are independent draws from a common distribution on $[0,1]$ with CDF $F$ and continuous, strictly positive density $f$ . A solver who exerts effort $e\ge0$ produces performance $x=ae$ when their ability is $a$ . The marginal cost of effort is one. Entry also costs $c_p$ , so performance $x$ costs $x/a+c_p$ for a solver with $a>0$ (model setup, pp. 6–7).

An allocation $r$ lists rank rewards $r_1\ge\cdots\ge r_n\ge0$ with $\sum_{j=1}^n r_j\le B$ , where $B$ is the firm's budget. Rank one is the best submission. A rank beyond the number of entrants receives no payment. The number $m(r)$ of rewards is the count of strictly positive entries in that list, including tied positive payments at different ranks.

Given $r$ , the paper's symmetric equilibrium has an ability threshold $a_{\min}(r,c_p)$ : a solver enters precisely when $a\ge a_{\min}$ . The expected rank reward $R_r(a)$ determines that threshold, and the paper gives an integral expression for the resulting equilibrium performance $x_r^*(a)$ (Proposition 1, p. 8). Both quantities depend on the entire announced allocation. The independent ability profile has the product law of the density on $[0,1]$ . If $N$ is the number entering, the failure probability is $\Pr(N=0)$ .

The firm's objective is equation (6), with failure cost $c_f\ge0$ :

\Pi(r;c_p,c_f)=\mathbb E\!\left[\max_{1\le i\le n}\{x_r^*(A_i)\mathbf 1_{\{A_i\ge a_{\min}(r,c_p)\}}\}\right]-c_f\Pr_r(N=0).

Every allocation comparison recalculates $a_{\min}$ , $x^*$ , and the failure probability. An optimal allocation maximizes this objective over every feasible $r$ , including allocations that spend less than the budget.

Formalization targets

The main target is Theorem 2, including existence of an optimum. For $c_p=0$ , every positive budget and nonnegative failure cost have an optimum, and every optimum pays exactly one rank. For $c_p>0$ , the corrected statement asserts thresholds $\widehat c_p>c_p$ and, for each budget $c_p<B<n c_p$ , a threshold $\widehat c_f>0$ such that every optimum satisfies

B<\widehat c_p\ \text{or}\ c_f<\widehat c_f\quad\Longrightarrow\quad m(r^*)=1,

\widehat c_p<B\ \text{and}\ \widehat c_f<c_f\quad\Longrightarrow\quad 2\le m(r^*)\le m_p^*(B).

Here $m_p^*(B)$ is the largest number of equal awards that maximizes participation. The same two thresholds govern both clauses. Equality at a threshold is left open because allocations can tie there. The bound $B<n c_p$ is the paper's constrained-budget regime, stated in its discussion and used in its threshold proof (Theorem 1 and its discussion, p. 10; proof of Proposition 1, p. 23). At $n=2$ , this regime may have no multi-reward case; the conditional statement retains the paper's population range.

The milestone results include the rank-probability identity (EC.3), the binomial law for the number of entrants (Proposition 2), the equal-award participation optimum (Theorem 1), attainment of the firm's maximum, and the claim that winner take all maximizes the first, performance term of $\Pi$ (Electronic Companion and proofs, pp. ec1, 9–10, 28).

What the result supplies

The theorem separates the firm's two aims in a precise way: a positive entry cost and a sufficiently consequential failure can justify paying more than the top rank, while the participation-maximizing number $m_p^*$ bounds how far the firm should spread rewards. The result is a statement about all optimal feasible allocations, not merely a comparison of a few equal-split choices. It also identifies the number of entrants through a binomial law, so the failure event has an explicit probability (Proposition 2, p. 9).

The paper presents these results and their arguments, but this mission's statements still require Lean proofs. A complete formalization would connect the rank and participation formulas to the objective evaluated on independent ability profiles, and establish existence and the design regimes. The order-statistic definitions and product-measure treatment of the ability population can be reused in other contest models.

Mathematical difficulty

The obvious thought is to maximize performance and participation separately, then compare their best allocations. That does not settle the firm's problem because changing a reward changes the entry threshold and the performance schedule at the same time. In particular, the performance term under partial entry cannot be replaced by its guaranteed-entry counterpart: entrants are selected by ability, and the selection threshold moves with the allocation. The printed proof of Theorem 2 cites a guaranteed-entry result at this point, leaving a substantive partial-entry comparison for the mission (proof of Theorem 2, pp. 27–28; Theorem EC.2, p. ec5).

Formalization scope

Lean uses natural-number ranks $1,\ldots,n$ , real abilities and rewards, and the density-based measure on $[0,1]$ whose finite product gives independent solver abilities. The order-statistic CDF is a binomial sum; its empty-range value is zero. The participation threshold is the least $a\in[0,1]$ for which expected rank reward reaches $c_p$ , with value one when that set is empty. The submission schedule is equation (4), and the firm's objective is the expectation in equation (6), not its later reduced integral form. A finite maximum over the $n$ solvers represents the best submission. Only positive rewards count toward $m(r)$ ; the unused rank-zero coordinate and rewards above rank $n$ are fixed at zero. At ability zero, division by ability is avoided in the submitted definitions.

The source's proof introduces an additional constraint that $\Pi\ge0$ , even though Theorem 2 does not require it and a large failure cost can make it impossible. The mission keeps the original feasible set with $\sum r_j\le B$ and no sign restriction on $\Pi$ . This prevents a formally easy but vacuous optimum claim. The strict performance milestone is labelled as a strengthening of the printed maximization claim. Contributions that establish the equilibrium characterization, measure identities, continuity and attainment, or a rigorous partial-entry performance comparison are within scope.

Selected references

Konstantinos I. Stouras, Jeremy Hutchison-Krupat and Raul O. Chao, The Role of Participation in Innovation Contests, accepted version forthcoming in Management Science, 2021, SSRN 2924224.

8 thms1 active userReviewed

Economics Operations Research·Captain: mikedeng1

Renewable Power and Electricity Prices: The Impact of Forward Markets: With Skewed, Variable Wind Output the Expected Spot Price First Falls and Then Rises in Wind CapacityResearch Paper

Motivation

Wind and solar generation have near-zero marginal cost. In a wholesale electricity market where prices are set by the marginal producer, adding such capacity displaces expensive conventional generation and lowers the spot price: the merit-order effect. Regulators and system planners rely on this effect when projecting the price impact of renewable expansion, and empirical studies of European markets report it.

Most electricity, however, is not traded only in the spot market. Producers and retailers hedge in forward markets before demand and wind output are known, and forward trading changes how producers with market power behave in the spot market (Allaz and Vila, 1993). Peura and Bunn (Management Science, 2021) ask what happens to the merit-order effect once this channel is included. Their answer is that, when wind output is variable and positively skewed, additional wind capacity eventually raises the expected spot price and the forward price. This mission formalizes that statement, Proposition 2 of the paper, together with the equilibrium characterization it rests on.

Setting

There are two conventional producers with constant marginal cost $c$ , a set of price-taking wind producers with total capacity $k_W \ge 0$ and zero cost, $N_R \ge 1$ price-taking retailers who resell at a fixed retail price $p_R$ , and an elastic industrial demand $D_I = a - p_s$ , where $p_s$ is the spot price.

Two random quantities are drawn on a probability space: the total retail demand $\theta$ , bounded, and the wind yield $\xi \in [0, 1]$ , so that available wind output is $\xi k_W$ . They are independent and both have positive variance. Write $\mu_\theta, \sigma_\theta^2, \tau_\theta$ for the mean, variance and third central moment of $\theta$ , and $\mu_\xi, \sigma_\xi^2, \tau_\xi$ for those of $\xi$ . The coefficient of variation of the yield is $CV_\xi = \sigma_\xi/\mu_\xi$ and its normalized skewness is $\tau^N_\xi = \tau_\xi/\sigma_\xi^3$ .

Trading has two stages.

Forward stage. Before $(\theta, \xi)$ is known, each producer sells a forward quantity $f_{Pi}$ and each retailer buys $f_{Ri}$ at a common forward price $p_f$ . The market clears at zero net supply, $f_P = f_R$ . Every participant maximizes the mean-variance utility $U(\pi) = E[\pi] - \frac{\lambda}{2}V(\pi)$ of its profit, with risk aversion $\lambda > 0$ . Retailers take $p_f$ and the spot-price distribution as given. Producers have market power in the forward market: a producer evaluates each alternative forward position at the forward price that would clear the market.
Spot stage. After $(\theta, \xi)$ is revealed, the producers compete à la Cournot on the inverse residual demand $p_s = a + \theta - \xi k_W - q_P$ , each maximizing $p_s(q_{Pi} - f_{Pi}) - c\,q_{Pi}$ .

With $q_0 = a - c + \theta - \xi k_W$ and $p_0 = a + 2c + \theta - \xi k_W$ , the spot equilibrium is $q^*_{Pi} = (q_0 + 2f_{Pi} - f_{Pj})/3$ and $p_s = (p_0 - f_P)/3$ (Lemma 1). The forward-spot equilibrium is $f^*_{Pi} = \omega/\nu$ and $p_f = a_f - 2b_f\omega/\nu$ for explicit expressions $\omega, \nu, a_f, b_f$ in the parameters, the moments, and $k_W$ (Theorem 1).

Formalization targets

Goal: Proposition 2

If

CV_\xi\,\tau^N_\xi \ge \zeta := \frac{27}{4N_R},

then an equilibrium exists at every capacity $k_W \ge 0$ , and there are thresholds $\bar k^s_W > 0$ and $\bar k^f_W \ge 0$ such that along every equilibrium selection

k_W \mapsto E[p_s] \text{ is strictly decreasing on } [0, \bar k^s_W] \text{ and strictly increasing on } [\bar k^s_W, \infty),

k_W \mapsto p_f \text{ is strictly increasing on } [\bar k^f_W, \infty).

The value of $\zeta$ comes from the paper's proof; the proposition itself only asserts that some $\zeta > 0$ works.

Milestones

Lemma 1 (p. 12): the spot Cournot equilibrium given forward positions.
Lemma 2 (p. 13): the retailers' optimal forward positions, a basis term plus a hedging term, and the resulting clearing condition.
Theorem 1 (p. 14): existence, uniqueness and closed form of the forward-spot equilibrium.
Derivative of $E[p_s]$ (proof of Proposition 2, p. 37): $\partial E[p_s]/\partial k_W = s_{p_s}(k_W)/(9N_R^2\nu^2)$ , where $s_{p_s}(k_W) = \alpha_0 + \alpha_1 k_W + \alpha_2 k_W^2 + \alpha_4 k_W^4$ is a quartic with no cubic term and explicit coefficients.
Sign of the quartic (p. 37): under the $\zeta$ condition, $\alpha_4 \ge 0$ , $\alpha_2 > 0$ and $\alpha_0 < 0$ , and $s_{p_s}$ changes sign exactly once on $[0, \infty)$ , from negative to positive.
Forward price (p. 37): the derivative of the closed-form forward price is eventually positive.

Significance

The result. Proposition 2 isolates a mechanism by which two pro-competitive forces, low-cost capacity and forward trading, can combine to raise prices. Variable and skewed wind output increases the risk that a producer is caught with a large forward position when wind is high and the spot price is low. Producers therefore sell less forward, which by Lemma 1 lowers their spot output and raises the spot price. For large enough capacity this forward effect outweighs the merit-order effect. The condition for the reversal involves only $CV_\xi$ and $\tau^N_\xi$ .

Formalizing it. The result is proved in the paper but has no machine-checked proof. In a formal development the equilibrium has to be defined through the participants' optimization problems, not through the closed forms. Theorem 1 then has to show that this optimization-defined equilibrium exists, is unique, and equals the closed form. The polynomial coefficients have to be checked: the printed $\alpha_1$ has a misplaced parenthesis, and the printed $s_{p_s}$ is off by a factor of $3N_R^2$ . Both are corrected and disclosed in the milestone statements. Neither affects the conclusion.

Difficulty

The goal combines three layers. The probabilistic layer computes means, variances and covariances of products of independent bounded random variables. These computations produce the third central moments $\tau_\theta, \tau_\xi$ and justify replacing the utility of each participant by an explicit quadratic in its own position. The game-theoretic layer has to show that each first-order condition gives a global optimum, which needs strict concavity, and that the producers' best responses, each computed against a clearing price that itself depends on the deviation, meet at a unique point. The analytic layer studies the rational function $E[p_0]/3 - 2\omega/(3\nu)$ of $k_W$ , whose derivative's numerator is a quartic with coefficients that are themselves polynomials in eleven quantities.

A tempting shortcut is to define the equilibrium by its closed form, which reduces the goal to a sign argument on a polynomial. That shortcut removes Theorem 1 entirely and is excluded here. A second tempting reading treats the forward price as fixed when a producer deviates. That makes producers price takers in the forward market, which is a different game whose equilibrium is not $\omega/\nu$ .

Formalization scope

The market parameters are a structure with fields a, c, pR, lam ( $\lambda$ , a Lean keyword) and NR : ℕ; the retailers are indexed by Fin NR. The demand $\theta$ and the yield $\xi$ are real functions on a probability space $(\Omega, P)$ , and the capacity $k_W$ is a separate real argument, so the joint law stays fixed as $k_W$ varies. The standing assumptions, a hypothesis of every model theorem, are: $\theta$ and $\xi$ are measurable and independent; $\theta$ is bounded and $0 \le \xi \le 1$ at every sample point; $\lambda > 0$ ; $N_R \ge 1$ ; $V(\theta) > 0$ and $V(\xi) > 0$ . The last two come from the paper's statement that demand and supply are uncertain in the forward market. Third moments are central. The footnoted conditions $N_R > 6$ and $c \le \min\{p_R, a\}$ are not assumed, since the goal holds without them.

The spot inverse demand is the interior branch of the paper's $p_s = \max\{a + \theta - \xi k_W - q_P, 0\}$ , used for all $k_W \ge 0$ and all realizations, with quantities ranging over the reals. This is what Assumption 1 (no blackouts or curtailment) licenses and what the paper's proof differentiates. The statement is therefore about the model with linear inverse demand. At realistic parameter values the turning point $\bar k^s_W$ can lie where Assumption 1 fails for some realizations, so its economic reading inside the no-curtailment region is the paper's interpretation, not part of the theorem.

The forward-spot equilibrium is a predicate built from optimization alone: retailer optimality over all real positions, clearing, and each producer's optimality against every deviation evaluated at that deviation's own clearing price. The closed forms (13)–(16) and the quartic's coefficients live in a separate definition file used only in milestone conclusions. The goal imports only the model. The goal also contains an existence conjunct, so the statement about equilibrium selections is not vacuous.

A complete development needs moment calculus for bounded independent random variables (variance and covariance of products, third central moments), maximization of concave quadratics, and single-crossing arguments for real polynomials. The moment computations and the mean-variance optimization of an affine position are reusable beyond this mission. Contributions are welcome at every milestone, including partial results.

Selected references

H. Peura, D. W. Bunn, Renewable power and electricity prices: The impact of forward markets, Management Science 67(8), 4772–4788, 2021. https://doi.org/10.1287/mnsc.2020.3710 (read as the author-accepted manuscript, LBS Research Online eprint 1432, https://lbsresearch.london.edu/id/eprint/1432/).
B. Allaz, J.-L. Vila, Cournot competition, futures markets and efficiency, Journal of Economic Theory 59(1), 1–16, 1993. https://doi.org/10.1006/jeth.1993.1001
H. Bessembinder, M. L. Lemmon, Equilibrium pricing and optimal hedging in electricity forward markets, Journal of Finance 57(3), 1347–1382, 2002. https://doi.org/10.1111/1540-6261.00463

9 thms1 active userReviewed

Combinatorics Operations Research Theoretical Computer Science·Captain: mikedeng1

Strong Algorithms for the Ordinal Matroid Secretary Problem: Every Algorithm with Forbidden Sets of Size k Is α(k) Probability-CompetitiveResearch Paper

Motivation

The secretary problem asks an online decision maker to pick the best of $n$ candidates who arrive in uniformly random order, deciding irrevocably on each one at arrival. Its matroid generalization, the matroid secretary problem (MSP) of Babaioff, Immorlica and Kleinberg (SODA 2007), asks the algorithm to select an independent set of a matroid whose elements arrive in random order. The MSP models online hiring under combinatorial constraints, posted-price mechanisms for matroid-constrained markets and online bipartite matching, and the conjecture that it admits an $O(1)$ -competitive algorithm for every matroid is still open.

Soto, Turkieltaub and Verdugo (arXiv:1802.01997; Mathematics of Operations Research, 2021) study the ordinal version, in which the algorithm only compares revealed elements and never sees weights, and introduce the strongest of several competitiveness notions, probability-competitiveness: every element of the optimum must be selected with probability at least $1/\alpha$ . Their central tool is the forbidden sets technique, summarized in a single statement, the Key Lemma, which turns a combinatorial property of an algorithm into a constant competitive ratio. Every constant-ratio algorithm of the paper for a specific matroid class (transversal matroids and gammoids, graphic and hypergraphic matroids, $k$ -framed matroids, laminar matroids, semiplanar gammoids) is obtained by verifying the hypothesis of this lemma.

Timeline. Dynkin (1963) and Lindley (1961) solve the classical problem with ratio $e$ . Babaioff et al. (2007) pose the MSP. Korula and Pál (ICALP 2009) and Kesselheim, Radke, Tönnis and Vöcking (ESA 2013) analyze random-order algorithms through the reverse arrival sequence, the device the Key Lemma abstracts. Soto, Turkieltaub and Verdugo (SODA 2018, MOR 2021) state the Key Lemma and use it to improve the best known ratios for almost all studied matroid classes.

Setting

Let $\mathcal M$ be a matroid on a finite ground set $R$ with $|R| = n$ , and let $\succ$ be a total order on $R$ , the value order. The span of $Q \subseteq R$ is the set of elements whose addition does not increase the rank of $Q$ . For $Q \subseteq R$ , the greedy optimum $\mathrm{OPT}(Q)$ is the base of $Q$ obtained by scanning $Q$ in decreasing value order and keeping each element that keeps the set independent; equivalently

\mathrm{OPT}(Q) = \{ r \in Q : r \notin \mathrm{span}(\{q \in Q : q \succ r\}) \}, \qquad \mathrm{OPT} = \mathrm{OPT}(R).

The elements arrive in a uniformly random order $r_1, r_2, \dots, r_n$ , and $R_t = \{r_1, \dots, r_t\}$ . An algorithm draws a sample size $s \sim \mathrm{Bin}(n, p)$ for a fixed sampling probability $p$ , observes the arrivals, and returns a set $\mathrm{ALG}$ . It has forbidden sets of size $k$ (Definition 7) if

its output is always independent;
it never accepts one of the first $s$ arrivals;
there is a rule assigning to every triple $(X, Y, r^*)$ with $r^* \in \mathrm{OPT}(Y)$ and $X \subseteq Y - r^*$ a set $\mathcal F(X, Y, r^*) \subseteq X$ of at most $k$ forbidden elements, such that for every time $t \ge s+1$ : if $r_t \in \mathrm{OPT}(R_t)$ and no $r_j$ with $s + 1 \le j \le t - 1$ lies in $\mathcal F(R_j, R_t, r_t)$ , then $r_t$ is selected.

The algorithm is $\alpha$ probability-competitive if $\Pr(r \in \mathrm{ALG}) \ge 1/\alpha$ for every $r \in \mathrm{OPT}$ , the probability being over $s$ and the arrival order.

Formalization targets

Goal: Lemma 1 (Key Lemma)

With

(p(k), \alpha(k)) = \begin{cases} (1/e,\ e) & k = 1,\\ (k^{-1/(k-1)},\ k^{k/(k-1)}) & k \ge 2,\end{cases}

every algorithm with forbidden sets of size $k \ge 1$ , run with sampling probability $p = p(k)$ , satisfies

\Pr(r^* \in \mathrm{ALG}) \ \ge\ \frac{1}{\alpha(k)} \qquad \text{for every } r^* \in \mathrm{OPT}.

Milestones

Lemma 4: $\mathrm{OPT} \cap Q \subseteq \mathrm{OPT}(Q)$ for every $Q \subseteq R$ .
Per-scenario bound (proof of Lemma 1): conditioned on $s$ , on $r_t = r^*$ and on $R_t = Y$ , the probability that $r^*$ is selected is at least $\prod_{j=s+1}^{t-1} ((j-k)/j)_+$ .
Display (5): $\Pr(r^* \in \mathrm{ALG}) \ge \mathbb E_{s \sim \mathrm{Bin}(n,p)} \frac1n \sum_{t=s+1}^n \prod_{j=s+1}^{t-1} (1 - k/j)_+$ .
Game bound: the right-hand side of (5) is at least $\int_p^1 (p/\tau)^k\, d\tau$ .
Integral: $\int_p^1 (p/\tau)^k\, d\tau$ equals $-p\ln p$ for $k = 1$ and $(p - p^k)/(k-1)$ for $k \ge 2$ .
Optimizing $p$ : these bounds are maximized over $p \in (0,1]$ at $p(k)$ , with value $1/\alpha(k)$ .

Significance

The Key Lemma separates the analysis of a random-order algorithm into a structural part (exhibit forbidden sets of size $k$ ) and a probabilistic part (the lemma itself), so the probabilistic part is done once. Its consequences in the paper include an $e$ probability-competitive algorithm for transversal matroids (the first guarantee in the probability notion for Kesselheim et al.'s matching algorithm), ratio $4$ for graphic matroids, $3\sqrt3$ for laminar matroids and $k^{k/(k-1)}$ for $k$ -framed matroids. Because probability-competitiveness implies the ordinal, utility and intersection notions, each of these also bounds the weighted problem.

The result is proved in the paper; nothing here is open. To our knowledge no part of it is formalized in Lean. A formal Key Lemma makes every forbidden-sets analysis a purely combinatorial obligation (Definition 7 for a concrete algorithm), and it fixes a precise probability model for the random-order MSP that later formalizations of the paper's algorithms, or of the classical secretary rule, can reuse.

Difficulty

The obvious argument, "each earlier arrival is forbidden with probability at most $k/j$ , so multiply", fails as stated: the forbidden set $\mathcal F(R_j, R_t, r_t)$ depends on the random set $R_j$ , so the events " $r_j$ is not forbidden" are not independent in the forward direction. The proof needs the reverse arrival sequence: conditioned on $R_t$ , the arrivals $r_{t-1}, r_{t-2}, \dots$ are revealed backwards, each uniform in the current prefix and independent of what was revealed after it. Making this conditioning precise over a finite uniform permutation space is the main formal work. The second difficulty is analytic: the expectation in (5) over $s \sim \mathrm{Bin}(n,p)$ has no closed form, and the paper bounds it by a continuous-time coupling with uniform arrival times rather than by direct summation.

Formalization scope

All objects live in one definitions file, namespace OrdinalMSP.Forbidden.

The ground set is a Fintype R with DecidableEq R and a LinearOrder R; the value order $r \succ q$ is q < r. The matroid is a Mathlib Matroid R with ground set Set.univ, and the span is Matroid.closure.
$\mathrm{OPT}(Q)$ is defined by the span characterization above (opt M Q), which is the greedy output.
An arrival order is σ : Fin n ≃ R; σ i arrives at time $i+1$ . Times in milestone statements are the paper's 1-based ones.
An algorithm is any map from (arrival order, sample size) to a finite set. Online-ness is not required, which is a generalization the proof allows; randomness beyond the sample size is not modelled.
The forbidden-set rule is fixed before the run, independent of the order and of $s$ , and is constrained exactly on the printed domain.
$\Pr(r \in \mathrm{ALG})$ is the exact finite sum $\sum_{s=0}^n \binom ns p^s (1-p)^{n-s} \cdot \#\{\sigma : r \in \mathrm{ALG}(\sigma,s)\}/n!$ in $\mathbb R$ , not a measure-theoretic probability.
$e$ is Real.exp 1; the powers are Real.rpow; $p(k)$ and $\alpha(k)$ branch on $k = 1$ before dividing by $k - 1$ .

Definition 7 is satisfiable (the rule "accept every element after the sample" in a free matroid satisfies it with empty forbidden sets), so the goal is not vacuous; a formalization that strengthens Definition 7, for instance by requiring the selection condition for times $t \le s$ , or that fixes $s = \lfloor pn \rfloor$ instead of drawing it from $\mathrm{Bin}(n,p)$ , would prove a different statement and is ruled out. The auxiliary game of the paper is a proof device and is not formalized; its milestone is a real-number inequality.

Needed infrastructure: counting over Fin n ≃ R conditioned on a prefix set (the reverse arrival sequence), binomial sums, interval integrals of $\tau^{-k}$ , and calculus on $p \mapsto -p\ln p$ and $p \mapsto (p - p^k)/(k-1)$ . The reverse-arrival counting lemmas are reusable for any random-order secretary analysis. Contributions of alternative proofs of the game bound (for example by direct summation) are welcome.

Selected references

J. A. Soto, A. Turkieltaub, V. Verdugo, Strong Algorithms for the Ordinal Matroid Secretary Problem, Mathematics of Operations Research, 2021; preprint arXiv:1802.01997v1, 2018. https://arxiv.org/abs/1802.01997
M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, Proc. SODA 2007, pp. 434–443.
N. Korula, M. Pál, Algorithms for secretary problems on graphs and hypergraphs, Proc. ICALP 2009, LNCS 5556, pp. 508–520.
T. Kesselheim, K. Radke, A. Tönnis, B. Vöcking, An optimal online algorithm for weighted bipartite matching and extensions to combinatorial auctions, Proc. ESA 2013, LNCS 8125, pp. 589–600.
E. B. Dynkin, The optimum choice of the instant for stopping a Markov process, Soviet Mathematics Doklady 4:627–629, 1963.
D. V. Lindley, Dynamic programming and decision theory, Applied Statistics 10(1):39–51, 1961.

8 thms1 active userReviewed

Machine Learning Reinforcement Learning Statistics·Captain: mikedeng1

Efficiently Breaking the Curse of Horizon in Off-Policy Evaluation with Double Reinforcement Learning: Cross-Fitted DRL Is Asymptotically Linear and Normal at the MDP Efficiency BoundResearch Paper

Motivation

Off-policy evaluation (OPE) asks for the long-run value of a target decision policy, using only data collected under a different policy. It arises wherever running the target policy is expensive or unsafe: a new treatment rule in medicine, a new recommendation or pricing rule, a candidate controller in reinforcement learning. Importance-sampling estimators reweight whole trajectories. Their variance grows exponentially with the horizon, the curse of horizon (Liu et al. 2018, arXiv:1810.12429).

Kallus and Uehara (arXiv:1909.05850, Operations Research 2022) treat infinite-horizon discounted OPE as a semiparametric estimation problem. They derive the efficiency bound under three models: non-Markov, time-varying Markov and time-invariant Markov (MDP). They then propose double reinforcement learning (DRL), an estimator that combines a q-function estimate with an estimate of the ratio between the discounted state visitation of the target policy and the state distribution of the data. In the MDP model it attains the efficiency bound. This mission formalizes the transition-sampling version of that result, Theorem 6.

Timeline:

2016: Jiang and Li (arXiv:1511.03722) and Thomas and Brunskill (arXiv:1604.00923) give doubly robust OPE estimators for finite horizons, built on trajectory-wise importance weights.
2018: Liu, Li, Tang and Zhou (arXiv:1810.12429) replace trajectory weights by stationary state-distribution ratios, removing the exponential dependence on the horizon, but without efficiency guarantees.
2018: Chernozhukov et al. (arXiv:1608.00060) formalize cross-fitting and Neyman orthogonality for estimation with machine-learned nuisances (double machine learning).
2019–2022: Kallus and Uehara derive the MDP efficiency bound (Theorem 3) and prove that cross-fitted DRL attains it (Theorem 6), also under trajectory sampling with mixing (Theorems 10–13).

Setting

States lie in a measurable space $S$ and actions in a measurable space $A$ . A time-invariant MDP is a transition kernel $p(s'\mid s,a)$ and a reward kernel $p(r\mid s,a)$ with rewards in $[0,R_{\max}]$ . A policy $\pi(a\mid s)$ is a kernel from $S$ to $A$ . Fix a discount $\gamma\in[0,1)$ , a known target policy $\pi_e$ with known initial law $p^{(0)}_{\pi_e}$ , and a behavior policy $\pi_b$ .

The estimand is the normalized discounted value

\rho^{\pi_e}=\lim_{T\to\infty}\Big(\sum_{t=0}^T\gamma^t\Big)^{-1}\mathbb E_{p_{\pi_e}}\Big[\sum_{t=0}^T\gamma^tr_t\Big].

The q-function is $q(s,a)=\mathbb E_{p_{\pi_e}}[\sum_k\gamma^kr_k\mid s_0=s,a_0=a]$ , and $v(s)=\int q(s,a)\,\pi_e(da\mid s)$ . The discounted visitation is $p^{(\infty)}_{\pi_e,\gamma}=(1-\gamma)\sum_t\gamma^t p^{(t)}_{\pi_e}$ , where $p^{(t)}_{\pi_e}$ is the law of $s_t$ .

Transition sampling. The data are i.i.d. observations $O_i=(s,a,r,s')$ with law $p_{\pi_b}$ : $s\sim p^{(0)}_{\pi_b}$ , $a\sim\pi_b(\cdot\mid s)$ , and, given $(s,a)$ , independently $r\sim p(\cdot\mid s,a)$ and $s'\sim p(\cdot\mid s,a)$ . The law of $s'$ may differ from that of $s$ .

The density ratios are $\eta(s,a)=\pi_e(a\mid s)/\pi_b(a\mid s)$ and $w(s)=p^{(\infty)}_{\pi_e,\gamma}(s)/p^{(0)}_{\pi_b}(s)$ . For candidate nuisances $w',q'$ , with $v'(s)=\int q'(s,a)\pi_e(da\mid s)$ , the estimating function is

\psi(s,a,r,s';w',q')=(1-\gamma)\,\mathbb E_{p^{(0)}_{\pi_e}}[v'(s_0)]+w'(s)\eta(s,a)\big(r+\gamma v'(s')-q'(s,a)\big).

The cross-fitted estimator $\hat\rho_{\rm DRL}(\mathcal M_3)$ splits the sample into two folds. It fits $\hat w^{[j]},\hat q^{[j]}$ on fold $j$ and averages $\psi$ over all observations, each evaluated at the nuisances of the other fold. The efficient influence function is $\phi_{\rm eff}=w(s)\eta(s,a)(r+\gamma v(s')-q(s,a))$ , and the efficiency bound is $\mathrm{EB}(\mathcal M_3)=\mathbb E[\phi_{\rm eff}^2]$ .

Formalization targets

Goal: Theorem 6

Assume the following:

$w\le C_w$ and $p_{b,S'}\le C_{S'}p_{b,S}$ (6a);
$\eta\le C_\eta$ (added);
$\hat w^{[j]},\hat q^{[j]}$ lie in $[0,C_w]$ and $[0,R_{\max}/(1-\gamma)]$ (6b);
$\|\hat w^{[j]}-w\|_2,\|\hat q^{[j]}-q\|_2=o_p(1)$ (6c);
$\sqrt n\,\|\hat w^{[j]}-w\|_2\|\hat q^{[k]}-q\|_2=o_p(1)$ for all $j,k\in\{0,1\}$ (6d, equivalent to common envelopes for both folds).

Then

\sqrt n\big(\hat\rho_{\rm DRL}(\mathcal M_3)-\rho^{\pi_e}\big)-\frac1{\sqrt n}\sum_{i<n}\phi_{\rm eff}(O_i)\xrightarrow{p}0,\qquad \sqrt n\big(\hat\rho_{\rm DRL}(\mathcal M_3)-\rho^{\pi_e}\big)\xrightarrow{d}N\big(0,\mathrm{EB}(\mathcal M_3)\big).

No rate exponent or learner class is fixed. Only the product rate enters.

Milestones, in proof order

Lemma 1 (forward): $\mathbb E[\gamma w(s)\eta(s,a)f(s')-w(s)f(s)]+(1-\gamma)\mathbb E_{p^{(0)}_{\pi_e}}[f]=0$ for bounded measurable $f$ .
$\rho^{\pi_e}=\mathbb E[w(s)\eta(s,a)r]$ (p. 16).
Eq. (5): $\mathbb E[\psi(w',q)]=(1-\gamma)\mathbb E_{p^{(0)}_{\pi_e}}[v]=\rho^{\pi_e}$ for every bounded $w'$ .
$\psi(w,q)=\rho^{\pi_e}+\phi_{\rm eff}$ pointwise (p. 22).
Eqs. (6)–(8): $\mathbb E[\psi(w,q')]=\rho^{\pi_e}$ for every bounded $q'$ .
Jensen step, corrected: $\|\hat v(s')-v(s')\|_2\le\sqrt{C_{S'}C_\eta}\,\|\hat q-q\|_2$ .
Term (30): $|\mathbb E\psi(\hat w,\hat q)-\rho^{\pi_e}|\le C_\eta(1+\gamma\sqrt{C_{S'}C_\eta})\|\hat w-w\|_2\|\hat q-q\|_2$ .
Term (28), variance: $\operatorname{var}[\psi(\hat w,\hat q)-\psi(w,q)]\le2a^2\|\hat w-w\|_2^2+2b^2\|\hat q-q\|_2^2$ .
Term (28) is $o_p(1)$ : the centred fold empirical process at the opposite fold's nuisances vanishes.

Significance

Theorem 6 shows that, in a Markov model, a $\sqrt n$ -consistent and efficient OPE estimator exists whose variance scales with the number of observed transitions, not trajectories. It requires no complexity (Donsker or entropy) restriction on the nuisance estimators, only a product rate. Any black-box learners with $\|\hat w-w\|_2\|\hat q-q\|_2=o_p(n^{-1/2})$ , which allows two subparametric rates, give asymptotically valid confidence intervals at the efficiency bound. The mixed-bias identities (Eqs. (5)–(8)) and Lemma 1 are the same ingredients used by later minimax and adversarial estimators of $w$ and $q$ .

The result is proved in the paper; nothing here is presented as open. As far as is known, none of it has a machine-checked proof: no off-policy evaluation, density-ratio characterization or cross-fitting asymptotics exists in Mathlib or on the platform. Formalizing it checks the appendix argument, which is short and contains errors (below). It also produces a reusable layer: kernel-based discounted MDPs on general measurable spaces, discounted visitation measures, and the cross-fitting plus Slutsky template that other double-machine-learning results share.

Difficulty

The obvious route is "the estimator equals the oracle average $\mathbb P_n\psi(w,q)$ plus negligible terms, then apply the CLT". Two of its steps are not routine.

First, the negligible terms are random functions evaluated at random data. The empirical-process term (28) is controlled only conditionally on the other fold, through a conditional Chebyshev argument that needs the independence structure of the split. Treating $\hat w,\hat q$ as fixed functions loses exactly this.

Second, the bias term (30) is second order only because of the mixed-bias structure. That structure rests on Lemma 1, a change-of-measure identity between the discounted visitation of $\pi_e$ and the data distribution. The printed constants are wrong. The Jensen step $\|\hat v(s')-v(s')\|_2\le\sqrt{C_{S'}}\|\hat q-q\|_2$ fails when $\eta$ is large: with one state, $\pi_b$ uniform on two actions and $\pi_e$ a point mass, the left side is $1$ and the right side is $1/\sqrt2$ . The bound by $\|\hat w-w\|_2\|\eta\|_2\|\hat q-q\|_2$ is not a valid inequality for a triple product. Both need a bound $\eta\le C_\eta$ , which the mission adds.

Formalization scope

Spaces and kernels. $S$ , $A$ are measurable spaces, the action σ-algebra countably generated (for Mathlib's jointly measurable Kernel.rnDeriv). The MDP, the policies and the observation law are Mathlib kernels and measures. The paper's base measures are not used.
Ratios. $w$ and $\eta$ are toReal of Radon–Nikodym derivatives, not free functions satisfying an identity. Overlap ( $\pi_e(\cdot\mid s)\ll\pi_b(\cdot\mid s)$ , $p^{(\infty)}_{\pi_e,\gamma}\ll p^{(0)}_{\pi_b}$ ) is a standing assumption.
Objects. $q$ is the discounted series, not "a solution of the Bellman equation". $\rho^{\pi_e}$ is the limit of normalized discounted sums, not $(1-\gamma)\mathbb E[v]$ or $\mathbb E[w\eta r]$ ; those identities are milestones. The discounted visitation is the measure $(1-\gamma)\sum_t\gamma^tp^{(t)}_{\pi_e}$ , the limit of the paper's normalized averages.
Cross-fitting. The folds are $\{i<\lfloor n/2\rfloor\}$ and the rest. Each learner is a jointly measurable function of its own fold's observations only. Rates are convergence in probability of the actual random $L^2$ errors.
Conclusion. "RAL and efficient" is posed as asymptotic linearity with influence function $\phi_{\rm eff}$ plus the normal limit. Regularity needs the tangent-space framework of Theorem 3 and is not posed.
Ruled out. The oracle statement with $\hat w=w$ , $\hat q=q$ is an i.i.d. CLT for a fixed function and drops the theorem's content. It is not an acceptable substitute for the goal.
Infrastructure needed. Linearity and Fubini for kernel compositions; summation of discounted occupancies; conditional Chebyshev for cross-fitted empirical processes; Slutsky (TendstoInDistribution with TendstoInMeasure) and Mathlib's i.i.d. CLT tendstoInDistribution_inv_sqrt_mul_sum_sub. The occupancy and Lemma 1 layer and the cross-fitting template are reusable beyond this mission. Proofs of any milestone, and helper lemmas on kernel powers and discounted sums, are welcome.

Selected references

N. Kallus and M. Uehara, Efficiently Breaking the Curse of Horizon in Off-Policy Evaluation with Double Reinforcement Learning, Operations Research 70(6), 2022; arXiv:1909.05850v6 (2023). https://arxiv.org/abs/1909.05850
Q. Liu, L. Li, Z. Tang and D. Zhou, Breaking the Curse of Horizon: Infinite-Horizon Off-Policy Estimation, NeurIPS 2018. https://arxiv.org/abs/1810.12429
V. Chernozhukov, D. Chetverikov, M. Demirer, E. Duflo, C. Hansen, W. Newey and J. Robins, Double/Debiased Machine Learning for Treatment and Structural Parameters, The Econometrics Journal 21(1), 2018. https://arxiv.org/abs/1608.00060
N. Jiang and L. Li, Doubly Robust Off-Policy Value Evaluation for Reinforcement Learning, ICML 2016. https://arxiv.org/abs/1511.03722
P. Thomas and E. Brunskill, Data-Efficient Off-Policy Policy Evaluation for Reinforcement Learning, ICML 2016. https://arxiv.org/abs/1604.00923

13 thms1 active userReviewed

Algorithmic Game Theory Economics Mechanism Design·Captain: mikedeng1

A Rationale for Imperfect Reporting Standards: With a Low Payoff Threshold and a High Prior, a Conservative Report Beats a Perfectly Informative OneResearch Paper

Motivation

Financial reports help investors value a firm, but a firm can also learn and voluntarily disclose information outside the report. A regulator who makes mandatory reports more precise changes the firm's incentive to acquire that other information. Friedman, Hughes and Michaeli's 2020 preprint, Proposition 1, studies whether a reporting rule that is less precise about one component of value can induce enough additional disclosure about another component to improve investors' information overall. The question matters to accounting standard setters because the regulator's choice affects both the information in the required report and the firm's subsequent behavior. The paper gives a sufficient high-prior condition for conservative reporting to be preferred; this mission addresses the second sentence of Proposition 1 and the results in its proof.

Setting

The firm's value is $\omega=\omega_1+\omega_2$ . The reportable component $\omega_1$ is either zero or one, with prior probability $\alpha\in(0,1)$ of one. The independent privately discoverable component $\omega_2$ lies in $[0,1]$ , has law $\mu$ , mean $\beta$ , second moment $m_2=\sigma^2+\beta^2$ , and cumulative distribution $F(t)=\mu(({-}\infty,t])$ . Investors do not observe either component directly. The firm's payoff depends on whether their posterior mean of $\omega$ reaches a threshold $k\in[0,2]$ . These objects and the sequence of decisions are specified in Section 2 of the preprint.

The regulator first chooses a reporting system with posterior probabilities $(\hat\alpha_G,\hat\alpha_B)$ that the reportable component is one after a good or bad report. Feasible pairs obey $0\le\hat\alpha_B\le\alpha\le\hat\alpha_G\le1$ and $\hat\alpha_B<\hat\alpha_G$ . The perfect benchmark is $(1,0)$ . The candidate conservative system is $(1,k)$ , which gives a bad report even in some good states. Bayes' rule sets the probability of a good report from the two posteriors and the prior.

After observing the rule, the firm chooses an information-acquisition probability $q\in[0,1]$ . If it learns $s=\omega_2$ , it discloses $s$ when $s$ exceeds a cutoff $t^\dagger(q)$ ; otherwise investors see no voluntary message and attribute the cutoff value to the hidden component. The cutoff is defined by the Bayes-consistency condition that its value equals the posterior mean under nondisclosure. The firm maximizes the probability of reaching the payoff threshold and, among ties, chooses the greatest $q$ , as stated on p. 10 of the preprint. The regulator anticipates this choice and minimizes $\Psi$ , the expected posterior variance of $\omega$ after both reporting and disclosure.

Formalization targets

Cutoff and firm response

Lemma 1 gives a unique, decreasing cutoff for $q\in[0,1]$ :

(1-q)(\beta-t^\dagger(q))=q\int_0^{t^\dagger(q)}F(x)\,dx.

Corollary 1 inverts it. Lemma 2 (iii) identifies the firm's greatest best response under the perfect system when $0<k<\beta$ : its cutoff is $k$ and its information probability is $q^\dagger(k)<1$ . These are the first three milestones (pp. 15–16).

Regulator's comparison and goal

The proof of Proposition 1 supplies two variance targets. Under $(1,k)$ , the firm gathers with $q=1$ and the expected posterior variance is $k(1-\alpha)$ . Under $(1,0)$ , let $q_0=q^\dagger(k)$ and $P=1-q_0(1-F(k))$ . The expected posterior variance is

\Psi((1,0),q_0)=m_2-q_0\int_{(k,1]}x^2\,d\mu(x)-k^2P.

The goal uses the corrected sufficient threshold

\alpha^\circ=1+kP-\frac{m_2-q_0\int_{(k,1]}x^2\,d\mu(x)}{k}.

For $0<k<\beta$ and $\alpha>\alpha^\circ$ , the candidate $(1,k)$ is feasible and strictly lowers $\Psi$ relative to $(1,0)$ at their induced firm responses. Hence an optimal rule with $\hat\alpha_G=1$ must have $\hat\alpha_B>0$ . The goal is the second sentence of Proposition 1, with the threshold corrected using the expected-variance comparison in its proof on pp. 34–35. The first sentence, that every optimum has $\hat\alpha_G=1$ , is outside the scope of this mission.

Significance

The comparison establishes a concrete mechanism by which a less informative required report can yield more information in total: it raises the firm's chosen probability of acquiring and disclosing the unreportable component. A strict comparison with the perfect benchmark is stronger than an assertion about a particular optimum, since it certifies why the benchmark cannot be selected in the stated regime.

The result is proved informally in the cited paper, subject to the threshold correction explained below. This mission seeks Lean statements and eventually machine-checked proofs for the cutoff, induced firm responses and expected-variance comparison. No theorem in this mission currently has a machine-checked proof. The model definitions may also be reused for variations of mandatory reporting and voluntary disclosure.

Difficulty

The firm's objective depends on a cutoff that itself changes with the firm's information choice. The obvious approach of holding $q$ fixed while comparing report precision misses the behavioral response that drives the result. The p. 34 comparison has a second subtlety: equation (3) uses weights conditional on nondisclosure, whereas the regulator's $\Psi$ averages over all messages. Comparing the candidate's unconditional variance directly with equation (3) changes the sufficient threshold. The general cutoff and best-response statements also need the distributional assumptions treated consistently; the appendix computations on p. 33 use a uniform distribution even though the main text states a general $F$ .

Formalization scope

Lean represents $\omega_2$ by an atomless probability measure $\mu$ concentrated on $[0,1]$ with full support on every interior interval. This replaces the paper's differentiable density in the integrals and makes the cutoff strictly invertible. The binary component is summarized by its prior $\alpha$ ; independence enters the derived second moment. The regulator chooses posterior pairs directly, as on p. 10. Strict separation of the pair excludes an uninformative system whose conditional posterior and Bayes weight are undefined. The firm chooses $q$ , with the greatest-maximizer tie-break; disclosure is for $s>t$ , equivalent almost surely to $s\ge t$ because $\mu$ has no atoms.

The cutoff relation is cross-multiplied, avoiding a zero-probability nondisclosure denominator at $q=1$ . Lemma 1 establishes the existence and uniqueness needed for the cutoff's sInf representation. Its printed open-range claim is adjusted at $q=0$ and $q=1$ , where the cutoffs are respectively $\beta$ and zero. The regulator's $\Psi$ is defined from the law of total variance, using posterior means after disclosure and nondisclosure. The goal includes feasible $(1,k)$ , best-response existence for both candidate systems and a strict comparison, preventing a vacuous conclusion about regulator optima. These conventions and boundary cases are detailed in the source discussion and appendix.

The printed formula for $\alpha^\circ$ is $1+k-[m_2-q_0\int_{(k,1]}x^2d\mu]/(kP)$ . It omits the nondisclosure probability in the comparison. For uniform $\omega_2$ , the printed condition is $\alpha>2/3+k/3$ , while the corrected condition is $\alpha>1-k/3$ . At $k=0.15$ and $\alpha=0.8333$ , the printed bound is met, but $\Psi(1,0)=0.0075<\Psi(1,k)=0.025$ . The formal goal uses the corrected formula. Contributions that establish the cutoff and inverse relation, the two firm responses, or the two variance identities are welcome; measure integration and posterior-moment lemmas are reusable beyond this mission.

Selected references

Friedman, H., Hughes, J., and Michaeli, B., A Rationale for Imperfect Reporting Standards, SSRN preprint 3636995, version of November 24, 2020, pp. 9–18 and 33–35. SSRN.

9 thms1 active userReviewed

Economics Operations Research·Captain: mikedeng1

Information Sharing on Retail Platforms: Under Asymmetric Full Sharing the Platform Optimally Shares All Signals Truthfully with Floor or Ceiling of min(2/b - 1, N) SellersResearch Paper

Why platforms share demand information

Online retail platforms such as Amazon, Alibaba's Tmall and JD.com host thousands of third-party sellers and observe every customer interaction with each of them. From these interactions the platform learns about market demand far better than any single seller can, and it sells or gives away part of that knowledge through analytics tools (Alibaba's Business Advisor is the example in the source paper). The platform earns a commission on every seller's revenue, so it cares about the sellers' total profit, and it has to decide what each seller is told.

The classic literature on information sharing in oligopoly points the other way. Gal-Or (1985) showed that Cournot competitors facing a common demand shock never voluntarily pool their private demand signals: shared information makes their strategies more correlated, and the resulting competition destroys more value than the better forecasts create. Li (2002) and others refined the conditions. Liu, Zhang and Zhang (Manufacturing & Service Operations Management, 2023; SSRN 3258109) change who decides: the signals belong to the platform, which chooses what each seller learns in order to maximize its commission. Their headline result for the unconstrained ("asymmetric full sharing") format is that the platform shares everything it knows, without any added noise, but only with a limited number of sellers, and that number is determined by the substitution between products alone.

The model

There are $N \ge 1$ sellers of substitutable products. Given quantities $q_1, \dots, q_N$ , seller $i$ 's price is

p_i = a - q_i - b\sum_{d \ne i} q_d + u, \qquad 0 < b \le 1,

where $u \sim N(0, \sigma)$ is a common demand shock with prior variance $\sigma > 0$ . The platform observes, for each seller $i$ , a signal $x_i = u + e_i$ with $e_i \sim N(0, t)$ , $t > 0$ , independent of everything else.

A noise matrix $M = (m_{ij})$ with entries in $[0, +\infty]$ is the platform's sharing strategy. Seller $j$ receives the noisy copy $\hat x_{ij} = x_i + \epsilon_{ij}$ , $\epsilon_{ij} \sim N(0, m_{ij})$ independent, for every $i$ with $m_{ij} < +\infty$ ; $m_{ij} = 0$ is truthful sharing and $m_{ij} = +\infty$ means $x_i$ is withheld from seller $j$ . Seller $j$ 's information $y_j(M)$ is the $\sigma$ -algebra generated by what he receives.

Each seller chooses a quantity measurable with respect to his information to maximize his expected profit $\pi_i = E[(1 - \alpha) q_i p_i]$ , where $\alpha \in (0,1)$ is the platform's commission rate. A Bayesian equilibrium under $M$ is a profile of such strategies from which no seller gains by deviating. The platform's expected profit is $\Pi = E[\alpha \sum_i q_i p_i]$ , and it chooses $M$ before the signals are realized.

Under Asymmetric Full Sharing (AFS) each seller $j$ receives all $N$ signals with one common noise level $\eta_j = m_{ij}$ (for all $i$ ), and the levels may differ across sellers. The benchmark is no sharing, $m_{ij} = +\infty$ for all $i, j$ , with platform profit $\Pi_{NS} = \alpha N a^2/[2 + b(N-1)]^2$ .

Formalization targets

Goal: Proposition 2 (optimal asymmetric full sharing)

Let $m = \min\{2/b - 1, N\}$ . Among all AFS noise matrices in $[0,+\infty]^{N \times N}$ and all equilibria, an optimal strategy is to share $\{x_1, \dots, x_N\}$ truthfully with sellers $1, \dots, K^*$ and nothing with the others, where

K^*_{AFS} \in \big\{\lfloor m \rfloor, \lceil m \rceil\big\}, \qquad \Pi^*_{AFS} = \frac{\alpha N a^2}{[2 + b(N-1)]^2} + \frac{\alpha K^*_{AFS}\,\sigma^2}{[2 + b(K^*_{AFS} - 1)]^2\,(\sigma + t/N)}.

The platform and every seller do weakly better than without sharing, and every optimal truthful group has size $\lfloor m \rfloor$ or $\lceil m \rceil$ .

Milestones

Eq. (5): under full sharing with noise $\eta$ , $E[u \mid y_j] = \frac{\sigma}{\sigma + (t + \eta)/N}\cdot\frac1N\sum_i \hat x_{ij}$ .
Eq. (4): a profile is an equilibrium iff $q_i = \frac12\big(a - b\sum_{d\ne i}E[q_d \mid y_i] + E[u \mid y_i]\big)$ for all $i$ .
Lemma 1: the no-sharing equilibrium quantities $a/(2 + b(N-1))$ and profit $\Pi_{NS}$ .
A seller who receives nothing earns exactly his no-sharing profit (p. 13).
Under AFS, an interior noise level for one seller is strictly beaten by $0$ or $+\infty$ (p. 16).
Proposition 1 (AFS half): optimal AFS matrices have $m^*_{ij} \in \{0, +\infty\}$ .
Eq. (8) at every group size $K \le N$ .
The integer maximizers of $K \mapsto K/[2 + b(K-1)]^2$ on $\{0,\dots,N\}$ lie in $\{\lfloor m \rfloor, \lceil m \rceil\}$ (p. 18).
Informed sellers strictly gain and the others earn the benchmark (p. 19).

Significance

The result separates two levers of information design, precision and audience, and shows that in this linear-Gaussian Cournot setting only the audience matters: the platform never degrades a signal, it only chooses how many sellers see it. The optimal audience size $\min\{2/b - 1, N\}$ depends only on the substitution parameter once the market is large, and equals one seller when products are perfect substitutes. This reverses the Gal-Or no-sharing result by changing who decides, and it explains why a commission-earning platform may rationally treat its sellers asymmetrically, which is the tension the paper's later sections on fairness and privacy constraints study.

The paper's proofs are in an online appendix. No part of this model has a machine-checked proof. The mission produces a reusable Lean layer for Bayesian games with designed Gaussian signals: information $\sigma$ -algebras generated by noisy copies of shared signals, Bayesian Nash equilibrium over square-integrable strategies, and its characterization by first-order conditions in conditional expectations. Mathlib has Gaussian measures, conditional expectation and independence, but not the projection formula for jointly Gaussian vectors that eq. (5) needs.

Difficulty

The closed forms are routine once one assumes that equilibria are linear in the received average signal. The difficulty lies in what that assumption skips. First, eq. (5) is a statement about conditional expectation with respect to a $\sigma$ -algebra generated by $N$ correlated Gaussian variables; it needs the Gaussian conditioning (projection) theorem, not a computation with densities. Second, the goal quantifies over all equilibria, so existence and uniqueness of the equilibrium must be proved for every noise matrix, including those with infinite entries; the paper solves the first-order condition and never discusses uniqueness. Third, Proposition 1 is an optimization over $[0,+\infty]^N$ : the platform's profit is not concave in the noise levels, and the endpoint property for one seller (with the others fixed at arbitrary levels) is the step that rules out partial sharing. Restricting attention to truthful groups from the outset assumes away exactly this step.

Formalization scope

All declarations live in the namespace RetailInfoShare.AFS, with one definitions file RetailInfoShare.AFS.Model. Conventions:

$\sigma$ , $t$ and $m_{ij}$ are variances (gaussianReal 0 σ), as eq. (3) of the paper requires.
The primitives $u$ , $e_i$ and standard normals $\xi_{ij}$ are measurable and mutually independent on one probability space; the added noise is $\epsilon_{ij} = \sqrt{m_{ij}}\,\xi_{ij}$ . The paper's "cov = 0" is read as independence, as its text says.
Noise levels are in ℝ≥0∞; a signal with $m_{ij} = \top$ never enters the receiving seller's information $\sigma$ -algebra.
Equilibrium is the ex-ante best-response property over square-integrable strategies measurable for the seller's information; this is equivalent a.e. to the interim maximization of eq. (2).
The platform's profit is the unconditional expectation (the matrix is chosen before the signals).
Added standing hypotheses: $0 < \alpha < 1$ (never stated in the paper), and $\sigma > 0$ , $t > 0$ , $N \ge 1$ made explicit. Sellers are Fin N, so the paper's sellers $1,\dots,K$ are indices $0,\dots,K-1$ .
Profits and equilibria are defined from the model, never by the closed forms (4) or (8); a formalization that defined $\Pi$ by eq. (8) or optimized only over truthful groups would reduce the goal to milestone 8 and is ruled out.

Out of scope: the AIS half of Proposition 1, Proposition 3 and Lemma 2 (privacy-constrained sharing), the symmetric formats of §5, the pricing mechanism of §6, and the appendix extensions. Contributions of general infrastructure are welcome: the Gaussian conditioning theorem in Mathlib form, and existence and uniqueness of equilibria in linear-quadratic Bayesian games with Gaussian information.

Selected references

Z. Liu, D. J. Zhang, F. Zhang, Information Sharing on Retail Platforms, Manufacturing & Service Operations Management, 2023. https://doi.org/10.1287/msom.2020.0915 (preprint: SSRN 3258109, https://ssrn.com/abstract=3258109)
E. Gal-Or, Information Sharing in Oligopoly, Econometrica 53(2), 1985. https://doi.org/10.2307/1911241
L. Li, Information Sharing in a Supply Chain with Horizontal Competition, Management Science 48(9), 2002. https://doi.org/10.1287/mnsc.48.9.1196.177
L. Li, Cournot Oligopoly with Information Sharing, RAND Journal of Economics 16(4), 1985. https://doi.org/10.2307/2555502

11 thms1 active userReviewed

Probability

Missions

Bochner's Theorem: Positive-Definite FunctionsTextbook

Motivation

Setting

Formalization targets

Goal — Bochner's theorem, general case

Milestone — Bochner's theorem, L¹ (density) case

Significance

Difficulty

Formalization scope

Selected references

Erdős (1947): The Probabilistic Ramsey Lower BoundResearch Paper

Motivation

Setting

Formalization targets

Goal: the probabilistic lower bound

Stronger: the three steps of the proof, as separate targets

Significance

Difficulty

Formalization scope

Selected references

Context: where this sits in the formalization landscape

Dynamic Programming and Optimal Control I: The DP AlgorithmTextbook

Motivation

Setting

Target

Significance

Difficulty

Formalization scope

Selected references

Markov Chains and Mixing Times XIII: Coupling from the PastTextbook

Motivation

Setting

Formalization targets

Goal

Milestones

Significance

Difficulty

Formalization scope

Selected references

Markov Chains and Mixing Times II: The Convergence TheoremTextbook

Motivation

Setting

Formalization targets

Goal

Milestones

Significance

Difficulty

Formalization scope

Selected references

Optimal Patrol of a Perimeter: Optimal Randomized Patrol Schedule and Value of the Patrol Game Against an Observing AttackerResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Assessing Algorithmic Fairness with Unobserved Protected Class Using Data Combination: The Partial Identification Set of Demographic Disparity Is the Closed Interval with Fréchet–Hoeffding EndpointsResearch Paper

Why the disparity is uncertain

Observed information and compatible joints

Formalization targets

What the result gives

Central difficulty

Formalization scope

Selected references

The Value of Price Discrimination in Large Random Networks: The Expected Fractional Regret of Uniform Pricing Vanishes in Erdős–Rényi Networks of Any DensityResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Dynamic Set Values for Nonzero-Sum Games with Multiple Equilibriums: The Set Value of a Continuous-Time Nonzero-Sum Stochastic Differential Game Satisfies the Dynamic Programming PrincipleResearch Paper

Milestone — Bochner's theorem, `L¹` (density) case