All missions

Motivation

Grover's algorithm (Grover 1996) finds a marked item among $N$ with $O(\sqrt N)$ queries, a quadratic speed-up over any classical algorithm. Whether quantum computers can do substantially better on search, and so solve NP-type problems by brute force in polynomial time, was settled in the negative by Bennett, Bernstein, Brassard and Vazirani (arXiv:quant-ph/9701001, SIAM J. Comput. 26(5), 1997): relative to a random oracle, a quantum algorithm needs $\Omega(2^{n/2})$ queries to decide whether a string has a preimage. The bound matches Grover's algorithm up to a constant factor, and its hybrid argument is one of the two standard lower-bound methods of the field, together with the polynomial method (Beals et al. 1998) and the adversary method (Ambainis 2000).

Timeline:

• 1996: Grover's algorithm searches $N$ items with $O(\sqrt N)$ queries.
• 1997: the paper proves $\mathbf{BQTime}(o(2^{n/2})) \not\supseteq \mathbf{NP}$ relative to a random oracle with probability 1 (Theorem 3.5), and the $\Omega(2^{n/3})$ bound for random permutations (Theorem 3.6).
• 1998: Boyer, Brassard, Høyer and Tapp give tight bounds for quantum searching.
• 1999: Zalka shows Grover's algorithm is exactly optimal.

Setting

A $T$-query algorithm acts on vectors $\varphi \in \mathbb{C}^{(X \cup \{\bot\}) \times R \times W}$, where $X$ is the set of query strings, $R$ the set of answers (an additive group) and $W$ a finite workspace. A basis configuration $(x, z, w)$ with $x \in X$ is querying $x$; $(\bot, z, w)$ is not querying. For an oracle $f : X \to R$ the oracle operator is

$$O_f\,|x, z, w\rangle = |x, z + f(x), w\rangle, \qquad O_f\,|\bot, z, w\rangle = |\bot, z, w\rangle .$$

The algorithm consists of a unit vector $\varphi_0$, unitaries $U_0, \dots, U_{T-1}$ that do not depend on the oracle, and a set of accepting configurations. With oracle $A$ its states are $\varphi_{i+1} = U_i O_A \varphi_i$; the acceptance probability is the squared norm of the accepting part of $\varphi_T$. The query magnitude of $y$ in $\varphi$ is $q_y(\varphi) = \sum_{z, w} |\varphi(y, z, w)|^2$ (Definition 3.2). The algorithm decides a property if it accepts with probability at least $2/3$ when the property holds and at most $1/3$ when it fails.

In the main theorem $X = R = \{0,1\}^n$ with bitwise addition, and the oracle is a uniformly random function $A : \{0,1\}^n \to \{0,1\}^n$. The question is whether $1^n$ belongs to $\mathcal{L}_A = \{y : \exists x\ A(x) = y\}$.

Formalization targets

Goal: Theorem 3.5 (finite form)

$$\exists\, c > 0\ \exists N\ \forall n \ge N\ \forall M \text{ with } T \le c\, 2^{n/2} \text{ queries}: \quad \Pr_A\bigl[M^A \text{ fails to decide } \exists x\ A(x) = 1^n\bigr] \ge \tfrac18 .$$

The constant is existential, matching the theorem's hypothesis $T(n) = o(2^{n/2})$; $c$ and $N$ do not depend on the workspace or the algorithm.

Milestones

1. Theorem 3.1: unit vectors at distance $\varepsilon$ have measurement distributions within total variation $4\varepsilon$.
2. Theorem 3.3 (corrected): changing oracle answers on time–string pairs of total query magnitude $\le \varepsilon^2/T$ moves the final state by at most $2\varepsilon$.
3. Corollary 3.4 (corrected): outside a set of at most $4T^2/\varepsilon^2$ strings, changing the oracle at one string moves the final state by at most $\varepsilon$.
4. $\Pr[1^n \text{ has no preimage}] = ((2^n-1)/2^n)^{2^n} \ge 1/4$.
5. $\Pr[1^n \text{ has a unique preimage}] = ((2^n-1)/2^n)^{2^n-1} \ge 1/e$.
6. Final states within $1/13$ for $A$ and $A_y$ force failure on one of them.
7. The double counting: failing oracles with a unique preimage are at least half the successful oracles with none.

Significance

The theorem shows that the quadratic speed-up of Grover's algorithm cannot be improved for unstructured search, and that relative to a random oracle $\mathbf{NP} \not\subseteq \mathbf{BQP}$; any quantum algorithm for NP-complete problems must use the structure of the problem. Theorem 3.3 and Corollary 3.4 isolate the constraint unitary evolution places on "quantum parallelism" and are reused across quantum lower bounds, including the permutation bound of the companion mission (Theorem 3.6).

The results are proved on paper and, to our knowledge, have no machine-checked proof. The mission produces a formal query model with an XOR oracle, a formal hybrid argument, and the lower bound with its constants checked. Two printed bounds are wrong by constant factors (below); the formal statements carry the corrected constants, and a formal proof settles them. Grover's matching upper bound is on the platform as Grover.search_succeeds_bounded, for a phase oracle and one fixed algorithm.

Difficulty

The obvious argument — each query reveals one bit about where the preimage is, so $\Omega(2^n)$ queries are needed — fails for quantum algorithms, which query all strings in superposition at once. The difficulty is to bound how much a superposition of queries can learn, which requires controlling the accumulated effect of small changes across $T$ unitary steps, and then converting a bound on states into a statement about the probability of failure over random oracles, where the set of sensitive strings depends on the oracle.

Formalization scope

The paper's oracle quantum Turing machines are replaced by the query model above, the model its proofs use. Every oracle QTM running $T$ steps is a $T$-query algorithm: oracle answers on lengths other than $n$ are fixed and absorbed into the unitaries, as the proof fixes them, and the input $1^n$ is absorbed into $\varphi_0$. Queries return the full value $A(x) \in \{0,1\}^n$; one Boolean query is two full-value queries, so the goal implies the Boolean-oracle bound with $c$ halved. Strings are Fin n → ZMod 2; states are EuclideanSpace ℂ (Option X × R × W); probabilities over oracles are counting fractions over all $(2^n)^{2^n}$ functions; total variation distance is the paper's $\sum_x |\mathcal D(x) - \mathcal D'(x)|$ without the factor $1/2$.

Corrections: Theorem 3.3 is printed with conclusion $\le \varepsilon$, which fails (one query string, $T = 1$, distance $2$ at $\varepsilon = 1$; machine-checked); the true bound is $2\varepsilon$. Corollary 3.4 is printed with $|S| \le 2T^2/\varepsilon^2$, which fails (16 strings, $T = 1$, $\varepsilon = 0.45$); the true bound is $4T^2/\varepsilon^2$. The printed constant $T(n) \le 2^{n/2}/20$ in the proof of Theorem 3.5 does not support the step $2^n - \mathrm{card}(S) \ge 2^{n-1}$ even with the paper's own count; the goal states an existential constant, and $c = 1/37$ works with the corrected Corollary 3.4. The closing probability-$1$ argument over countably many machines and the class statement about $\mathbf{BQTime}$ are not formalized.

A formalization in which algorithms query at every step on every branch (no $\bot$ sector), only one side of the bounded-error condition is tested, or the probability is taken over a set of oracles that excludes the hard instances, proves a weaker theorem and is ruled out by these definitions.

Needed infrastructure: norms of finite-dimensional complex vectors, unitaries as linear isometry equivalences, finite counting of functions. The query model and the hybrid argument are reusable for any quantum query lower bound.

Selected references

• C. H. Bennett, E. Bernstein, G. Brassard, U. Vazirani, Strengths and weaknesses of quantum computing, SIAM J. Comput. 26(5):1510–1523, 1997. arXiv:quant-ph/9701001
• L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. arXiv:quant-ph/9605043
• M. Boyer, G. Brassard, P. Høyer, A. Tapp, Tight bounds on quantum searching, Fortschr. Phys. 46, 1998. arXiv:quant-ph/9605034
• C. Zalka, Grover's quantum searching algorithm is optimal, Phys. Rev. A 60, 1999. arXiv:quant-ph/9711070
• R. Beals, H. Buhrman, R. Cleve, M. Mosca, R. de Wolf, Quantum lower bounds by polynomials, J. ACM 48, 2001. arXiv:quant-ph/9802049
• A. Ambainis, Quantum lower bounds by quantum arguments, J. Comput. Syst. Sci. 64, 2002. arXiv:quant-ph/0002066

Motivation

School and university timetabling is one of the oldest applications of combinatorial optimization. In his invited review An introduction to timetabling (European Journal of Operational Research, 1985), D. de Werra opens with the class–teacher model: classes meet teachers for a prescribed number of one-period lectures, and the lectures must be placed into periods or days so that no class and no teacher is overloaded. Every richer timetabling model of the review (preassignments, unavailabilities, course scheduling) is built on top of this one, and the review keeps returning to its graph-theoretic reading as an edge-colouring problem in a bipartite multigraph.

The model comes in three levels of demand. The daily problem asks for a clash-free timetable. The weekly problem asks for an assignment of lectures to days within daily load limits. The balanced weekly problem asks, in addition, that the load of every class and every teacher be spread as evenly as possible over the week, and that the lectures of each class–teacher pair be spread evenly too. The last one is the practical requirement that a teacher should not have all four lectures with one class on Monday.

Timeline (as cited in the review).

• 1916. D. König proves that a bipartite multigraph of maximum degree $\Delta$ can be edge-coloured with $\Delta$ colours. The review states it as Proposition 2.1, citing Berge's Graphes [1].
• 1975. D. de Werra, "A few remarks on chromatic scheduling" (reference [37] of the review), gives the balanced version: for every $p$ the edges of a bipartite multigraph can be $p$-coloured so that every node and every bundle of parallel edges is balanced. This is Proposition 2.3.
• 1978. D. de Werra, "Some comments on a note about timetabling" (INFOR, reference [38]), gives the weekly version with daily load limits, Proposition 2.2.
• 1985. The review collects the three results in matrix form as problems CT1, CT2 and CT3 and sketches a network-flow construction for CT3, citing Krarup [19].

Setting

There are $m$ classes $c_1,\dots,c_m$ and $n$ teachers $t_1,\dots,t_n$. The requirement matrix $R=(r_{ij})$ is an $m\times n$ matrix of nonnegative integers: $r_{ij}$ is the number of lectures class $c_i$ must have with teacher $t_j$. Write $r_{i\cdot}=\sum_j r_{ij}$ for the total load of class $c_i$ and $r_{\cdot j}=\sum_i r_{ij}$ for that of teacher $t_j$. For nonnegative integers $s$ and $p\ge1$, $\lfloor s/p\rfloor$ and $\lceil s/p\rceil$ are the floor and ceiling of the rational $s/p$.

A schedule over $p$ periods or days is an array $x=(x_{ijk})$ of nonnegative integers ($i\le m$, $j\le n$, $k\le p$) that places every lecture exactly once:

$$\sum_{k=1}^p x_{ijk}=r_{ij}\quad\text{for all } i,j. \tag{1}$$

• CT1 asks in addition that $x_{ijk}\in\{0,1\}$ and that $\sum_j x_{ijk}\le1$, $\sum_i x_{ijk}\le1$: no class and no teacher has two lectures in one period.
• CT2, given positive integers $a_i$, $b_j$, asks that $\sum_j x_{ijk}\le a_i$ and $\sum_i x_{ijk}\le b_j$ on every day $k$.
• CT3 asks that on every day $k$

$$\Big\lfloor \tfrac{r_{i\cdot}}{p}\Big\rfloor\le\sum_j x_{ijk}\le\Big\lceil \tfrac{r_{i\cdot}}{p}\Big\rceil,\quad \Big\lfloor \tfrac{r_{\cdot j}}{p}\Big\rfloor\le\sum_i x_{ijk}\le\Big\lceil \tfrac{r_{\cdot j}}{p}\Big\rceil,\quad \Big\lfloor \tfrac{r_{ij}}{p}\Big\rfloor\le x_{ijk}\le\Big\lceil \tfrac{r_{ij}}{p}\Big\rceil. \tag{8–10}$$

In the Lean development these are IsCT1 R p x, IsCT2 R p a b x and IsCT3 R p x, with the floor and ceiling written lo s p and hi s p and the totals rowSum R i, colSum R j.

Formalization targets

Goal: Proposition 2.3

$$\forall\,R\in\mathbb N^{m\times n},\ \forall\,p\ge1:\quad \exists\,x,\ \ x \text{ solves CT3 for } R \text{ over } p \text{ days}.$$

The statement fixes no constant: it asserts that perfectly balanced weekly timetables always exist.

Milestones

1. One balanced day (flow sketch, p. 153): for $p\ge1$ there is a matrix $y$ satisfying the bounds (8), (9), (10) at once.
2. The remaining days stay balanced (same sketch): if $p\ge2$ and $\lfloor s/p\rfloor\le y\le\lceil s/p\rceil$, then $\lfloor s/p\rfloor\le\lfloor (s-y)/(p-1)\rfloor$ and $\lceil (s-y)/(p-1)\rceil\le\lceil s/p\rceil$.
3. Proposition 2.1 (König): CT1 is solvable iff $r_{\cdot j}\le p$ and $r_{i\cdot}\le p$ for all $i,j$.
4. Proposition 2.2: CT2 is solvable iff $r_{\cdot j}\le p\,b_j$ and $r_{i\cdot}\le p\,a_i$.
5. Minimum number of days: CT2 is solvable over $p$ days iff $p\ge\max\big(\max_j\lceil r_{\cdot j}/b_j\rceil,\max_i\lceil r_{i\cdot}/a_i\rceil\big)$.
6. Figure 1: the printed timetable for $R=\begin{pmatrix}1&2&4\\3&0&2\end{pmatrix}$, $p=3$, solves CT3.

Significance

The result. Proposition 2.3 says that the balancing requirement costs nothing: whatever the requirement matrix, the week can be organised so that each class and each teacher has an essentially constant daily load and each class–teacher pair is spread evenly. It contains König's edge-colouring theorem (take $p$ at least the maximum degree, so every daily load is at most one) and the weekly Proposition 2.2 as special cases. Combined with Proposition 2.1 applied to each day, it reduces weekly timetabling to independent daily problems, which is the decomposition the review recommends ("one may start by solving the weekly problem … and then solve separately the resulting daily problems", p. 154). In graph language it is the existence of equitable edge colourings of bipartite multigraphs, a standard tool in scheduling and in the theory of edge colourings.

Formalizing it. All results of this mission are classical and proved in the literature; none of them is formalized on the platform. Mathlib contains Hall's marriage theorem but not König's edge-colouring theorem for bipartite multigraphs, and not balanced or equitable colourings. A complete development gives a machine-checked König edge-colouring theorem in matrix form, the matrix-rounding step with simultaneous row, column and entry bounds, and the balanced-colouring theorem itself.

Difficulty

Each family of constraints alone is easy: spreading a single number $r_{ij}$ evenly over $p$ days, or a single row total, is a matter of division with remainder. The difficulty is that one array must satisfy (1), (8), (9) and (10) simultaneously, so that the per-entry roundings must add up to correct roundings of every row total and every column total on every day. Rounding each entry independently breaks the row and column constraints, and greedy day-by-day choices can leave a remainder that no longer fits the bounds. The crux is integrality: the rational average $r_{ij}/p$ satisfies every bound on every day, but the problem asks for integers, and an integral one-day slice must round all entries, all row totals and all column totals consistently.

Formalization scope

Classes, teachers and days are Fin m, Fin n, Fin p; $R$ and $x$ are natural-number valued, which is the paper's "$x_{ijk}\ge0$ integer". Constraint (4) of CT1 is written $x_{ijk}\le1$. Floors and ceilings are Nat.floor and Nat.ceil of the rational quotient. In (8) and (9) they are applied to the row and column totals, never summed entrywise. The minimum number of days uses Finset.sup, whose empty value is $0$, and is stated as an equivalence ("solvable over $p$ days iff $p\ge p_{\min}$") rather than as an infimum.

Disclosed choices:

• The goal and the one-day milestone assume $p\ge1$; the paper's "for any $p$" means any number of days, and for $p=0$ Lean's division returns $0$.
• The remaining-days milestone assumes $p\ge2$ so that $p-1$ days remain.
• Propositions 2.1, 2.2 and the minimum-days statement hold for every $p$, including $p=0$, and assume nothing more than the page: $a_i,b_j$ positive.
• The edge-colouring and network-flow readings of the paper are stated in prose only; the formal statements are in matrix form, which is how the propositions are stated.

The formalization does not admit a trivial reading: CT3 requires all four constraint families at once, (1) is an equality, and the sanity checks show both that the Figure 1 data satisfy CT3 and that CT1 is not satisfiable for $R=(2)$ and $p=1$.

Useful infrastructure, reusable beyond this mission: integral flows with lower bounds, or total unimodularity of bipartite incidence matrices; König's edge-colouring theorem for bipartite multigraphs; floor and ceiling arithmetic for natural-number quotients. Proofs of any milestone, alternative proofs of the goal, and a sorry-free proof of the Figure 1 instance are all welcome.

Selected references

• D. de Werra, An introduction to timetabling, European Journal of Operational Research 19 (1985) 151–162. https://doi.org/10.1016/0377-2217(85)90167-5
• D. König, Über Graphen und ihre Anwendung auf Determinantentheorie und Mengenlehre, Mathematische Annalen 77 (1916) 453–465. https://doi.org/10.1007/BF01456961
• C. Berge, Graphes, Gauthier-Villars, Paris, 1983 (reference [1] of the review).
• D. de Werra, A few remarks on chromatic scheduling, in B. Roy (ed.), Combinatorial Programming: Methods and Applications, Reidel, Dordrecht, 1975, 337–342.
• D. de Werra, Some comments on a note about timetabling, INFOR 16 (1978) 90–92.
• J. Krarup, Chromatic optimisation: Limitations, objectives, uses, references, European Journal of Operational Research 11 (1982) 1–19.

Motivation

A committee that chooses one alternative by voting would like a voting procedure under which no member can gain by misreporting their preferences. Such a procedure is called strategy-proof. Gibbard (Econometrica 41, 1973) and Satterthwaite (J. Econ. Theory 10, 1975) proved independently that, once at least three outcomes are possible, the only strategy-proof procedures are dictatorial. The result is the starting point of the theory of strategy-proof mechanisms: it is why mechanism design restricts preference domains (single-peaked preferences, quasi-linear utilities) or allows randomization.

This mission formalizes Theorem 1 of Satterthwaite's paper, in the version circulated as Northwestern University CMS-EMS Discussion Paper No. 122 (revised December 12, 1974). Its formulation has one feature that the textbook version lacks: the hypothesis is on the range of the procedure, not on the whole alternative set, and the dictatorship is accordingly relative to that range.

Setting

A committee has a finite set $I_n$ of $n\ge 1$ individuals and a finite set $S_m$ of $m$ alternatives. In a strict committee every individual's ballot $B_i$ is a strong order on $S_m$, a ranking without ties; $x\,\bar B_i\,y$ means that $B_i$ ranks $x$ strictly above $y$. The set of strong orders is $\rho_m$, and a ballot set is $B=(B_1,\dots,B_n)\in\rho^n_m$.

A strict voting procedure $v^{nm}$ assigns to each ballot set a single alternative $v^{nm}(B)\in S_m$. Its range $T_p$ is the set of alternatives it selects at some ballot set, and $p=|T_p|$, so $1\le p\le m$.

Individual $i$ can manipulate $v^{nm}$ at $B$ if some ballot $B_i'$ gives

$$v^{nm}(B_1,\dots,B_i',\dots,B_n)\ \bar B_i\ v^{nm}(B_1,\dots,B_i,\dots,B_n),$$

an outcome $i$ strictly prefers by the standard of the original ballot. The procedure is strategy-proof if no individual can manipulate it at any ballot set.

The procedure is dictatorial if some individual $i$ exists such that, at every ballot set $B$, $v^{nm}(B)$ is the element of the range $T_p$ that $B_i$ ranks highest. It is fully dictatorial if in addition $T_p=S_m$ and partially dictatorial if $T_p\subsetneq S_m$.

The proof uses three further notions. Condition U requires that if every $B_i$ ranks the same $x\in T_p$ above all other elements of $T_p$, then $v^{nm}(B)=x$. The procedure is weak alternative-excluding if $T_p\subsetneq S_m$, and strong alternative-excluding if in addition it satisfies Condition U. Finally $\theta_T(B_i)$ is the restriction of $B_i$ to a subset $T$.

Formalization targets

Goal: Theorem 1 (p. 11)

For a strict committee with $n\ge 1$ and $m\ge p\ge 3$,

$$v^{nm}\ \text{is strategy-proof}\iff v^{nm}\ \text{is dictatorial}.$$

Milestones

1. Lemma 1 (p. 13): a strategy-proof strict procedure satisfies Condition U.
2. Lemma 2 (p. 15): with one individual and three alternatives, a strategy-proof procedure is fully dictatorial or strong alternative-excluding.
3. Lemma 3 (pp. 16–17): for $n+1$ individuals and three alternatives, individuals $1,\dots,n$ cannot manipulate $v^{n+1,3}$ if and only if each of the procedures $B\mapsto v^{n+1,3}(B,B_{n+1})$, one for each ballot of individual $n+1$, is strategy-proof.
4. Lemma 4 (p. 22): the induction step from $n$ to $n+1$ individuals for three alternatives.
5. Lemma 5 (p. 25): for $n\ge 1$, $m\ge 3$, a strategy-proof procedure is fully dictatorial or strong alternative-excluding.
6. Lemma 6 (p. 26): for $n\ge 2$, if $\theta_{T}(C_i)=\theta_{T}(D_i)$ for all $i$, with $T=T_p$, then $v^{nm}(C)=v^{nm}(D)$.
7. Proof of Theorem 1, (27)–(28) (p. 27): in the case of a strategy-proof, strong alternative-excluding $v^{nm}$ with $m>p\ge 3$, it induces a strategy-proof procedure $v^{np}$ on the alternatives of its range with $v^{np}[\theta_T(B_1),\dots,\theta_T(B_n)]=v^{nm}(B)$.

Significance

Theorem 1 characterizes the strategy-proof strict voting procedures completely: given $p\ge 3$, they are exactly the procedures that let one individual pick, from a fixed menu $T_p$, their favourite element. The classical statement assumes the procedure can select every alternative; Theorem 1 shows that excluding alternatives from the menu does not help, since a procedure with any menu of at least three alternatives is still governed by one individual. The paper's correspondence theorem with Arrow's social welfare functions (its Theorem 2) and its extension to ballots with indifference (Theorem 1') build on this statement.

The full-range case is on the platform already: AGT.gibbard_satterthwaite (Theorem 9.8 of Nisan–Roughgarden–Tardos–Vazirani, Algorithmic Game Theory) is proved and states that an incentive compatible social choice function onto at least three alternatives has a dictator; it is included here as a reference item and is exactly the case $T_p=S_m$ of Lemma 5. The open item MechanismDesign.SocialChoice.gibbard_satterthwaite (Börgers, Proposition 8.1) poses the full-range equivalence. Theorem 1 contains both as the special case $T_p=S_m$. What this mission adds is the range-restricted statement and the paper's own route to it: the induction on the number of individuals for three alternatives (Lemmas 2–4) and the reduction of a procedure with a proper range to its range (Lemma 6 and (27)–(28)). The paper only sketches Lemma 4 and defers the induction on $m$ to Satterthwaite's dissertation, so the formal development fills these gaps.

Difficulty

The "if" direction is immediate. For the "only if" direction the natural first idea is to apply the full-range theorem to the procedure viewed as a map into $T_p$. This fails as stated: the procedure is still defined on rankings of all $m$ alternatives, and nothing yet says that its choice ignores how individuals rank alternatives outside $T_p$. That is the content of Lemma 6, which needs strategy-proofness and Condition U; only after it does the procedure factor through rankings of $T_p$, and only then is the factor itself strategy-proof. The full-range case itself is the classical theorem, whose known proofs (via Arrow's theorem, or by pivotal-voter arguments) are combinatorial and long.

Formalization scope

• Individuals and alternatives are finite types ι and A; $n$ = Fintype.card ι, $m$ = Fintype.card A, and the $n+1$ individuals of Lemmas 3–4 are Option ι, with none the individual $n+1$.
• Strict ballots and strategy-proofness come from the published definition agt_social (namespace AGT): a ballot is a relation r with IsStrictTotalOrder A r, r x y is the paper's $x\,\bar B_i\,y$, and strategy-proofness is AGT.IncentiveCompatible, which is the paper's definition (1) on $\rho^n_m$.
• The range is taken over strict ballot sets only, and $p$ is its Set.ncard. Theorem 1 assumes $n\ge 1$ and $p\ge 3$; $m\ge p$ holds automatically, so $m\ge 3$ is not a separate hypothesis.
• Dictatorial reads the paper's dictator function $f^i_T$ as "the $B_i$-maximal element of $T_p$", which for strong orders is unique.
• $\theta_T(C_i)=\theta_T(D_i)$ is encoded as agreement of the two strict relations on $T\times T$, and the procedure $v^{np}$ of (28) lives on the subtype of the range.
• Lemmas keep their printed hypotheses ($m\ge 3$, $p\ge 1$, Lemma 6's $n\ge 2$), even where the conclusion would hold without them. The range restriction milestone keeps the proof's case assumptions of strong alternative exclusion and $m>p\ge 3$.

Two encodings would trivialize the goal and are excluded: a range taken over all relation profiles (junk values would make $p\ge 3$ meaningless), and a dictatorship that only constrains ballot sets at which the dictator's overall favourite lies in $T_p$, or that asks for the dictator's favourite in all of $S_m$ (false whenever $T_p\subsetneq S_m$). The bound $p\ge 3$ is needed: a procedure with two possible outcomes, such as majority vote between two fixed alternatives, is strategy-proof and not dictatorial, and an imposed procedure ($p=1$) is dictatorial only vacuously.

Contributions are welcome at every milestone, and the restriction-to-range step (Lemma 6 and (27)–(28)) is reusable for any statement that transfers results from full-range to range-restricted procedures.

Selected references

• M. A. Satterthwaite, Strategy-proofness and Arrow's Conditions: Existence and Correspondence Theorems for Voting Procedures and Social Welfare Functions, Northwestern University CMS-EMS Discussion Paper No. 122, rev. Dec. 12, 1974; published in J. Econ. Theory 10(2) (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
• A. Gibbard, Manipulation of Voting Schemes: A General Result, Econometrica 41(4) (1973) 587–601. https://doi.org/10.2307/1914083
• N. Nisan, Introduction to Mechanism Design (for Computer Scientists), Chapter 9 of N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007. https://doi.org/10.1017/CBO9780511800481
• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Chapter 8. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001

Motivation

Many limit theorems of probability in Banach spaces, among them the strong law of large numbers and the law of the iterated logarithm for vector-valued random variables, reduce to sharp estimates of the tail probability

$$P\Big(\Big\|\sum_{i\le N}X_i\Big\|\ge t\Big)$$

for independent random variables $X_i$ with values in a Banach space $W$. For many years these estimates were obtained with martingale methods, and they were not optimal. Chapter 13 of M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces (Publ. Math. IHÉS 81, 1995), explains how the isoperimetric inequalities of the earlier chapters, in particular control by $q$ points (Theorem 3.1.1), give such estimates with explicit constants.

Timeline. M. Ledoux observed (unpublished note on Gaussian randomization, reference [L] of the paper) that for Gaussian sums $\sum g_iX_i$ one may split $\|\sum g_iX_i\|$ into its conditional mean given $(X_i)$ plus a deviation, and that the conditional mean has a monotonicity property that replaces positivity arguments ([L], Eq. (13.1)–(13.2) of the paper). Ledoux and Talagrand used this to characterize the Banach-valued random variables satisfying the law of the iterated logarithm (1988). The resulting conviction that an isoperimetric principle was at work led to Talagrand's 1989 isoperimetric theorem (Ann. Probab. 17), superseded in the 1995 paper by Theorem 3.1.1. Ledoux–Talagrand, Probability in Banach Spaces (1991), Theorem 6.17, proves a variant of the bound formalized here that also allows truncation of the variables.

Setting

Let $W$ be a real Banach space with dual $W^*$, and let $X_1,\dots,X_N$ be independent (not necessarily identically distributed) $W$-valued random variables. Let $\varepsilon_1,\dots,\varepsilon_N$ be Rademacher signs: independent, independent of $(X_i)$, with $P(\varepsilon_i=1)=P(\varepsilon_i=-1)=1/2$. Following the paper, write

$$\Big\|\sum_{i\le N}\varepsilon_iX_i\Big\|=E_\varepsilon\Big\|\sum_{i\le N}\varepsilon_iX_i\Big\|+\Big(\Big\|\sum_{i\le N}\varepsilon_iX_i\Big\|-E_\varepsilon\Big\|\sum_{i\le N}\varepsilon_iX_i\Big\|\Big),$$

where $E_\varepsilon$ is expectation in the signs only. The conditional mean is $Z=E_\varepsilon\|\sum_i\varepsilon_iX_i\|$. The weak variance of a point $x=(x_i)\in W^N$ is

$$\sigma^2(x)=\sup\Big\{\sum_{i\le N}w^*(x_i)^2:\ w^*\in W^*,\ \|w^*\|\le1\Big\}.$$

The decreasing rearrangement $\|x_i\|^*=\sup\{t:\ \operatorname{card}\{j\le N:\|x_j\|\ge t\}\ge i\}$ is the $i$-th largest norm, and $\sum_{i\le k}\|x_i\|^*$ is the sum of the $k$ largest norms.

For sets $A_1,\dots,A_q\subseteq W^N$, the $q$-point distance of $x$ is

$$f(A_1,\dots,A_q,x)=\inf\big\{\operatorname{card}\{i\le N:\ x_i\notin\{y^1_i,\dots,y^q_i\}\}:\ y^l\in A_l\big\}.$$

For $b>0$ let $B=\{\sigma\le b\}$ and $k(x)=f(B,\dots,B,x)$ with $q$ copies of $B$.

Formalization targets

Goal: Theorem 13.4 (p. 200)

With $a=2E\|\sum_i\varepsilon_iX_i\|$ and $s^2=E\,\sigma^2(X)$, for all integers $q\ge2$, $k\ge0$ and $u,t>0$,

$$P\Big(\Big\|\sum_{i\le N}\varepsilon_iX_i\Big\|\ge 2aq+3t+u\Big)\le\frac{2^{q+1}}{q^{k+1}}+4\exp\Big(-\frac{u^2}{32qs^2}\Big)+2P\Big(\sum_{i\le k}\|X_i\|^*>t\Big).$$

Milestones

1. Proposition 13.1 (p. 197): for $a>0$, $P(Z\ge qa+t)\le q^{-k-1}P(Z\le a)^{-q}+P(\sum_{i\le k}\|X_i\|^*\ge t)$.
2. Proposition 13.3 (p. 199): for fixed $x\in W^N$ and $u>0$,

$$P_\varepsilon\Big(\Big\|\sum_i\varepsilon_ix_i\Big\|\ge2E_\varepsilon\Big\|\sum_i\varepsilon_ix_i\Big\|+u+\sum_{i\le k(x)}\|x_i\|^*\Big)\le4\exp\Big(-\frac{u^2}{16qb^2}\Big).$$

3. Eq. (13.14) (p. 200): the joint bound at level $2v+u+t$ combining the two.

The goal keeps the paper's explicit constants.

Significance

The result. Theorem 13.4 bounds the tail of a Rademacher sum in an arbitrary Banach space using three quantities only: the mean $E\|\sum\varepsilon_iX_i\|$, the weak variance $s^2$, and the law of the $k$ largest summands. No moment assumption on the $X_i$ beyond these is needed, and $q,k$ are free parameters to optimize. By symmetrization, such bounds are the main input for the law of large numbers and the law of the iterated logarithm in Banach spaces, for the integrability of sums, and for comparison of moments.

Formalizing it. The result is proved in the paper (and in a different form in Ledoux–Talagrand 1991). It is not formalized: Mathlib has independence, product measures and the dual of a normed space, but no Rademacher sums in Banach spaces and none of Talagrand's isoperimetric inequalities. The mission yields a machine-checked statement of the vector-valued tail bound with explicit constants, connected to the $q$-point inequality (Theorem 3.1.1, posed in mission IV of this series) and to the concentration of $\|\sum Y_iv_i\|$ for bounded $Y_i$ (Theorem 13.2, posed in mission IX).

Difficulty

The obvious approach controls $\|\sum_i\varepsilon_iX_i\|$ by its mean plus a concentration term. Bounded-difference (martingale) inequalities do not work here: the increments are $\|X_i\|$, which can be unbounded and heavy-tailed, so the resulting bound depends on $\sum\|X_i\|^2$ rather than on the much smaller weak variance $\sigma^2$. Concentration for the signs conditionally on $(X_i)$ (Theorem 13.2) gives the weak variance, but at scale $\sigma(X)$, a random quantity. The difficulty is to make both the conditional mean $Z$ and $\sigma(X)$ uniformly controlled on most of the space, at the cost of discarding only a few large summands; a single-point isoperimetric inequality does not supply this.

Formalization scope

• $W$ is a real normed space with CompleteSpace W, MeasurableSpace W and BorelSpace W; $W^*$ is W →L[ℝ] ℝ with the operator norm. $\sigma^2$ is a real ⨆ over the dual unit ball, which is nonempty and bounded above by $\sum\|x_i\|^2$.
• The $X_i$ are realized canonically on $W^N$ = Fin N → W with $P$ = Measure.pi μ for laws μ i (independent, not identically distributed). Signs are Fin N → Bool under the platform's uniform measure Komlos.spMeasure N (referenced). The joint law is the product of the two. Coordinates are 0-based; the rearrangement index is 1-based as in the paper.
• $E_\varepsilon$ is the finite average over $2^N$ sign patterns. $a$ and $s^2$ are lower Lebesgue integrals (∫⁻) in $[0,\infty]$, so they need no integrability hypothesis, and $a=\infty$ makes the goal hold with an empty event. Probabilities are in $[0,\infty]$, so $P(B)=0$ or $P(Z\le a)=0$ makes the corresponding term $+\infty$.
• The paper ignores measurability (pp. 81–82). Here measurability of $x\mapsto\|\sum\varepsilon_ix_i\|$ (each sign pattern) and of $\sigma^2$ is an explicit hypothesis; it is automatic for separable $W$.
• The paper writes $q\in\mathbf N$; statements take $q\ge2$, the range of Theorem 3.1.1, and all bounds are trivial for $q\le1$.
• The paper calls $\|x_i\|^*$ the "non-decreasing rearrangement", but its formula gives the $i$-th largest norm; the formula is formalized.
• Trivializing formalizations are ruled out: $\sigma^2$ and $E_\varepsilon$ cannot take junk values (bounded nonempty supremum, finite average), the $q$-point distance is ℕ∞-valued, and no Bochner integral of a possibly non-integrable function appears.

Needed infrastructure: Rademacher sums in Banach spaces, order statistics of finitely many reals, the $q$-point inequality on general product spaces, and Theorem 13.2 for Bernoulli variables. The rearrangement and the $q$-point distance can be reused elsewhere. Contributions are welcome on any milestone, and on proving Proposition 13.3 from a stated form of Theorem 13.2.

Selected references

• M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205. https://doi.org/10.1007/BF02699376
• M. Ledoux, M. Talagrand, Characterization of the law of the iterated logarithm in Banach spaces, Ann. Probab. 16 (1988), 1242–1264. https://doi.org/10.1214/aop/1176991688
• M. Ledoux, M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4
• M. Talagrand, Isoperimetry and integrability of the sum of independent Banach-space valued random variables, Ann. Probab. 17 (1989), 1546–1570. https://doi.org/10.1214/aop/1176991174

Motivation

A random walk in a random environment on $\mathbb Z$ moves one step right with probability $\alpha_x$ and one step left with probability $1-\alpha_x$ from site $x$, where the $\alpha_x$ are themselves i.i.d. random variables. In his 1975 paper, F. Solomon (Ann. Probab. 3(1):1–31, DOI 10.1214/aop/1176996444) decided recurrence and transience of this walk and computed its speed. Section 4 of the paper isolates a piece of that analysis: the conditional mean time for the walk to cross one bond, given the environment.

Fix the environment, make $0$ reflecting, and let $\mu_n$ be the mean first-passage time from $n$ to $n+1$. Conditioning on the first step gives $\mu_n=\sigma_n\mu_{n-1}+(\sigma_n+1)$ with $\sigma_n=(1-\alpha_n)/\alpha_n$, and $Z_n=\tfrac12(\mu_n-1)$ satisfies a linear recursion with random coefficients (p. 28). The sum $Z_1+\dots+Z_n$ is, up to an affine change, the expected time to reach level $n$ in that environment. Recursions of the same form, $Z_n=A_nZ_{n-1}+B_n$ with i.i.d. coefficients, are the random difference equations studied by Kesten (Acta Math. 131, 1973) and Vervaat (Adv. Appl. Probab. 11, 1979); they recur in queueing (waiting-time recursions), insurance (discounted cash flows, "perpetuities") and the analysis of stochastic algorithms.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $\sigma_1,\sigma_2,\dots$ independent, identically distributed, nonnegative real random variables. The system of difference equations (4.1) is

$$Z_0=0,\qquad Z_n=\sigma_n\,(1+Z_{n-1}),\quad n\ge1 .$$

In the Lean development Z σ n ω is defined by this recursion (module SolomonRWRE.DiffEq.System), so it is a function of $\sigma_1,\dots,\sigma_n$ and needs no existence hypothesis. Unfolding gives the closed form (4.3), $Z_n=\sum_{j=1}^n\sigma_j\cdots\sigma_n$.

The mean is $\nu=E(\sigma)=\int\sigma_1\,dP\in[0,\infty]$ (nu P σ); $\sigma$ need not be integrable, and $\nu=\infty$ is allowed. The products are $\rho_j=\sigma_1\cdots\sigma_j$ (rho), and the block sums of the proof are

$$Y_k^n=\sum_{j=1}^{n-k+1}\ \prod_{i=j}^{j+k-1}\sigma_i \qquad(\texttt{Y σ k n}),$$

the sums of the products of $k$ consecutive $\sigma$'s inside $\sigma_1,\dots,\sigma_n$. For one step of the proof the sequence is extended to a two-sided i.i.d. family $\{\sigma_j\}_{j\in\mathbb Z}$ (module TwoSided), with $S_n=\sum_{j=-\infty}^n\sigma_j\cdots\sigma_n\in[0,\infty]$.

Formalization targets

Goal: Theorem (4.4)

$$\lim_{n\to\infty}\frac{Z_1+\dots+Z_n}{n}=\begin{cases}\dfrac{\nu}{1-\nu}, & \nu<1,\\[2mm] \infty, & \nu\ge1,\end{cases}\qquad\text{almost surely.}$$

The goal fixes nothing beyond the paper's hypotheses: any law on $[0,\infty)$, integrable or not. Both cases are almost-sure limits.

Milestones, in the order of the proof (pp. 28–29)

1. The closed form (4.3), $Z_n=\sum_{j=1}^n\sigma_j\cdots\sigma_n$.
2. The regrouping $Z_1+\dots+Z_n=Y_1^n+\dots+Y_n^n$.
3. For fixed $k\ge1$, $Y_k^n/n\to\nu^k$ almost surely, in $[0,\infty]$.
4. $\liminf_n (Z_1+\dots+Z_n)/n\ge\sum_{k\ge1}\nu^k$ almost surely, which settles $\nu\ge1$.
5. For a two-sided family, $Z_n\le S_n$ pathwise, and $S_n<\infty$ almost surely when $\nu<1$.
6. For $\nu<1$, $\limsup_n\frac1n\sum_{k=1}^nZ_k\le\nu/(1-\nu)$ almost surely.

Companion: Lemma (4.2)(i)–(ii)

If $\sum_n n^{-1}P(\rho_n>1)<\infty$ then $\sum_j\rho_j<\infty$ a.s. and $Z_n$ converges in law to $\sum_j\rho_j$; if the series diverges, $Z_n\to\infty$ in probability; when $E(\ln\sigma)$ is defined, the two cases are $E(\ln\sigma)<0$ and $E(\ln\sigma)\ge0$.

Significance

The result. Theorem (4.4) gives the almost-sure growth rate of the cumulative mean passage time of a random walk in a random environment: linear with slope $\nu/(1-\nu)$ when $E(\sigma)<1$, superlinear otherwise. This is the averaged counterpart of the speed law of §1 of the paper (Theorem (1.16)), where the limiting speed $(1-E\sigma)/(1+E\sigma)$ is exactly the reciprocal of $1+2\nu/(1-\nu)$. The superlinear case $\nu\ge1$ is the starting point of the paper's §4 limit laws for $f(n)(Z_1+\dots+Z_n)$ (Lemma (4.5) to Theorem (4.9)), which are stated without proof. Lemma (4.2) concerns the single variable $Z_n$, and its dichotomy is a statement about perpetuities $\sum_j\sigma_1\cdots\sigma_j$.

Formalizing it. The theorem has been proved since 1975; what this mission adds is a machine-checked proof. No result about random difference equations, random products, or this paper is on the platform. The proof needs, for a nonnegative stationary ergodic sequence with possibly infinite mean, the almost-sure convergence of averages in $[0,\infty]$. That convergence is not in Mathlib in this form (Mathlib has the i.i.d. strong law for integrable variables, ProbabilityTheory.strong_law_ae), and Birkhoff's pointwise ergodic theorem is posed on the platform as an open item (Birkhoff1931.tendsto_birkhoffAverage_condExp). A completed mission therefore leaves behind a nonnegative, infinite-mean ergodic theorem for block products of i.i.d. sequences, which is reusable well beyond this paper.

Difficulty

The obvious argument fails at independence. $Z_n$ is a sum of products sharing the factor $\sigma_n$, so $Z_1,Z_2,\dots$ are neither independent nor stationary, and no law of large numbers applies to them directly. The regrouping into $Y_k^n$ produces sums of $k$-dependent block products, which are stationary but not independent, so the i.i.d. strong law does not apply either. Moreover there are $n$ such groups at time $n$, so letting $k$ and $n$ grow together needs a uniform argument: Fatou's lemma gives only the lower bound. The upper bound requires a different object, $S_n$, which is stationary because it looks infinitely far into the past, and it exists only because $\nu<1$ makes the backward series converge. A second trap is the infinite-mean case: $\sigma$ may be non-integrable, and every integrability-based ergodic or strong-law statement must be adapted to nonnegative variables with values in $[0,\infty]$.

Formalization scope

• Driving sequence. σ : ℕ → Ω → ℝ; the hypotheses (IsIIDNonneg) are on $\sigma_1,\sigma_2,\dots$ (the shifted family n ↦ σ (n + 1)): measurable, pointwise nonnegative, mutually independent (iIndepFun), and identically distributed with $\sigma_1$ (IdentDistrib). $\sigma_0$ is unused and unconstrained.
• Expectations are lower Lebesgue integrals in $[0,\infty]$ (∫⁻). A Bochner integral would return $0$ for a non-integrable $\sigma$, which would put $\nu=0<1$ and make the goal false; this trivializing reading is excluded by the definition of nu.
• Limits are taken in $[0,\infty]$: the averages are mapped there by ENNReal.ofReal, which loses nothing because $Z_k\ge0$. In the case $\nu<1$, $\nu/(1-\nu)$ is computed in $[0,\infty]$ and is finite.
• Indices. The sums start at $k=1$ (Finset.Icc 1 n); in $Y_k^n$ the upper limit $n+1-k$ uses natural-number subtraction, which gives the empty sum for $k>n$.
• Two-sided family. Milestone 5 is stated for a separate predicate IsIIDNonnegZ on σ : ℤ → Ω → ℝ; $Z_n$ is computed from its restriction to $\mathbb N$. This mirrors the page's "without loss of generality"; the goal keeps the one-sided family.
• Lemma (4.2). One hypothesis is added: $\sigma_1$ is not almost surely $1$. For $\sigma\equiv1$ the series $\sum n^{-1}P(\rho_n>1)$ vanishes while $\sum\rho_j=\infty$, so clause (i) fails as printed; the paper's proof cites its Lemma (1.6), which assumes nondegeneracy. "Converges in law" is Mathlib's TendstoInDistribution; "$p-\lim Z_n=\infty$" is $P(Z_n\le M)\to0$ for every $M$; $E(\ln\sigma)$ is the difference of the $[0,\infty]$-valued expectations of its positive and negative parts, required not to be both infinite, with $\ln0=-\infty$.

Contributions welcome beyond the milestones: an ergodic theorem for nonnegative stationary sequences with values in $[0,\infty]$; the identity $E(S_1)=\nu/(1-\nu)$; and the construction of a two-sided i.i.d. extension of a one-sided sequence, which turns milestone 5 into a statement about the goal's sequence.

Selected references

• F. Solomon, Random walks in a random environment, The Annals of Probability 3(1):1–31, 1975. https://doi.org/10.1214/aop/1176996444
• H. Kesten, Random difference equations and renewal theory for products of random matrices, Acta Mathematica 131:207–248, 1973. https://doi.org/10.1007/BF02392040
• W. Vervaat, On a stochastic difference equation and a representation of non-negative infinitely divisible random variables, Advances in Applied Probability 11(4):750–783, 1979. https://doi.org/10.2307/1426858
• G. D. Birkhoff, Proof of the ergodic theorem, Proceedings of the National Academy of Sciences 17(12):656–660, 1931. https://doi.org/10.1073/pnas.17.12.656

Motivation

A renewal process models the successive replacements of an article that fails and is replaced at once: light bulbs, machine components, the inter-arrival times of a queue. The central quantity is the renewal function $H(t)$, the expected number of replacements up to time $t$. Long-run average costs of maintenance and inventory policies, the throughput of regenerative systems and the rates in renewal–reward arguments are all read off the growth of $H(t)$. W. L. Smith's survey Renewal Theory and Its Ramifications (J. R. Statist. Soc. B, 1958) organized the field around this function and opened with its oldest general limit result, the elementary renewal theorem, proved in full in §1.2 (pp. 245–247).

Timeline.

• 1941 — W. Feller gives the first rigorous proof of the elementary renewal theorem, through a Tauberian theorem for Laplace integrals.
• 1946 — C. Stein proves, for general sequential sampling procedures, that the stopping index has a finite exponential moment; for renewal processes this gives finite moments of all orders of the count $N_t$.
• 1948 — J. L. Doob gives a purely probabilistic proof, through the strong law of large numbers.
• 1958 — Smith presents Doob's proof in modified form: an identity for the residual lifetime gives the lower bound, and a truncation of the lifetimes gives the upper bound, also when the mean lifetime is infinite.

Setting

Let $(\Omega,\mathcal F,P)$ be a probability space and $X_1, X_2, \dots$ real random variables that are mutually independent, identically distributed, non-negative, and not almost surely zero: $P(X_i = 0) < 1$. Lifetimes equal to zero with positive probability are allowed.

• The renewal epochs are $S_0 = 0$ and $S_n = X_1 + \dots + X_n$.
• The counting variable $N_t$ is the number of $n \ge 1$ with $S_n \le t$, the number of renewals in $[0,t]$; for $t \ge 0$ it is the largest $n$ with $S_n \le t$.
• The renewal function is $H(t) = \mathbb E N_t$ and the mean lifetime is $\mu_1 = \mathbb E X_i \in (0,\infty]$.
• The residual lifetime $\zeta_t$ is defined by $S_{N_t+1} = t + \zeta_t$.
• For $\Delta > 0$ the truncated process is $X_i^\dagger = \min(X_i,\Delta)$, with associated $S_n^\dagger$, $N_t^\dagger$, $H^\dagger$, $\mu_1^\dagger$, $\zeta_t^\dagger$.

In Lean these are IsRenewalProcess P X, S X n, N X t, H X P t, mu1 X P, zeta X t and trunc Δ X in the namespace SmithRenewal.Elementary.

Formalization targets

Goal: the elementary renewal theorem (§1.2, p. 246)

$$\frac{H(t)}{t} \longrightarrow \mu_1^{-1} \qquad (t \to \infty),$$

with $\mu_1 \le \infty$ and $\mu_1^{-1} = 0$ when $\mu_1 = \infty$. No moment beyond the first is assumed, and not even the first: the infinite-mean case is part of the goal.

Milestones, in the order of the paper's argument

1. Stein's result (p. 245). There is $\theta_0 > 0$ with $\mathbb E e^{\theta N_t} < \infty$ for every real $\theta \le \theta_0$; hence $N_t$ has finite moments of all orders and $H(t) < \infty$.
2. Equation (1.1) (p. 246). If $\mu_1 < \infty$, then for $t \ge 0$

$$t + \mathbb E\zeta_t = \mu_1\{1 + H(t)\}.$$

3. Lower bound (p. 246). If $\mu_1 < \infty$, $\liminf_{t\to\infty} H(t)/t \ge \mu_1^{-1}$.
4. Truncation (p. 246). $(X_i^\dagger)$ is a renewal process, $S_n^\dagger \le S_n$, $N_t^\dagger \ge N_t$, $H^\dagger(t) \ge H(t)$ and $\zeta_t^\dagger \le \Delta$.
5. Upper bound (p. 246). For every $\Delta > 0$,

$$\limsup_{t\to\infty}\frac{H(t)}{t} \le \limsup_{t\to\infty}\frac{H^\dagger(t)}{t} \le \{\mu_1^\dagger\}^{-1}.$$

6. Letting $\Delta \to \infty$ (p. 247). $\mu_1^\dagger \to \mu_1$ in $[0,\infty]$.

Significance

The result. The elementary renewal theorem is the law of large numbers for the renewal function: in the long run renewals occur at mean rate $1/\mu_1$. It is the basis of the renewal–reward theorem, of long-run average cost formulas for replacement, maintenance and $(s,S)$ inventory policies, and of rate computations for regenerative queues. The sharper results of Smith's survey — Blackwell's theorem (1.2) and the key renewal theorem (1.3) — refine it and reduce to it on averaging.

Formalizing it. The theorem has been proved since 1941; what this mission adds is a machine-checked development of the continuous-time, real-valued renewal process in Lean, which Mathlib does not contain. Mathlib has the strong law of large numbers, independence and identical distribution, but no renewal counting process, no Wald identity and no renewal function. The platform holds a proved discrete Erdős–Feller–Pollard theorem for integer renewal sequences, a different statement about a different object; to the curators' knowledge the elementary renewal theorem for general non-negative lifetimes has not been formalized.

Difficulty

The almost-sure statement $N_t/t \to 1/\mu_1$ is close to the strong law, since $S_{N_t} \le t < S_{N_t+1}$. The obvious next step, taking expectations, fails: almost-sure convergence does not imply convergence of means, and $N_t/t$ has no evident integrable dominating function. The exact relation (1.1) involves a sum with a random number of terms stopped at $N_t + 1$, and by itself it bounds $H(t)/t$ from one side only, because the residual lifetime $\zeta_t$ can have infinite mean. When $\mu_1 = \infty$ the relation is unavailable altogether, yet the theorem still claims a limit. Throughout, $N_t$ is a priori allowed to be infinite on a null set and $H(t)$ to be infinite, so finiteness itself is part of what must be established.

Formalization scope

• Representation. Lifetimes are X : ℕ → Ω → ℝ, with the paper's $X_1, X_2, \dots$ as X 0, X 1, …. IsRenewalProcess P X bundles measurability, mutual independence (iIndepFun), IdentDistrib (X i) (X 0), non-negativity at every sample point, and P {X 0 = 0} < 1. Strict positivity is not assumed.
• Counting. $N_t$ is the cardinality in ℕ∞ of $\{n \ge 1 : S_n \le t\}$; it is $0$ for $t < 0$ and may be $\infty$ on a null set.
• Expectations. $H(t)$, $\mu_1$ and $\mathbb E\zeta_t$ are lower Lebesgue integrals with values in $[0,\infty]$. No finiteness is presupposed; finiteness of $H(t)$ is milestone 1.
• Ratios and limits. $H(t)/t$ is formed in $[0,\infty]$ and limits are taken as $t \to \infty$ along the reals; $\mu_1^{-1}$ is the inverse in $[0,\infty]$, so $\infty^{-1} = 0$ is the paper's convention.
• Residual lifetime. $\zeta_t = S_{N_t+1} - t$, reading $N_t$ through ENat.toNat; on the null event $N_t = \infty$ this is $S_1 - t$, which never affects an expectation.
• Truncation. $H^\dagger$, $\mu_1^\dagger$, $\zeta_t^\dagger$ are the same definitions applied to trunc Δ X, never separate formulas.

Ruled out. A goal restricted to $\mu_1 < \infty$, a renewal function defined through $\sum_r P(S_r \le t)$ or the renewal equation, or a real-valued ratio with $1/\mu_1$ in $\mathbb R$ (where $1/0 = 0$ and an infinite integral becomes $0$) would each be a different, weaker or trivially true statement; none of them is the goal.

Needed infrastructure and welcome contributions. A Wald identity for stopping indices of i.i.d. sums with values in $[0,\infty]$; the comparison of a renewal count with a negative binomial count; uniform-in-$t$ moment bounds for $N_t$; and the lim inf/lim sup squeeze in $[0,\infty]$. The renewal process definitions and the Wald identity are reusable for Blackwell's theorem, the key renewal theorem and renewal–reward arguments. Alternative proofs of the goal (Feller's Tauberian route, a uniform-integrability argument) are welcome as long as they prove the stated goal.

Selected references

• W. L. Smith, Renewal Theory and Its Ramifications, J. R. Statist. Soc. B 20(2):243–283, 1958. https://doi.org/10.1111/j.2517-6161.1958.tb00294.x
• W. Feller, On the integral equation of renewal theory, Ann. Math. Statist. 12(3):243–267, 1941. https://doi.org/10.1214/aoms/1177731708
• C. Stein, A note on cumulative sums, Ann. Math. Statist. 17(4):498–499, 1946. https://doi.org/10.1214/aoms/1177730890
• J. L. Doob, Renewal theory from the point of view of the theory of probability, Trans. Amer. Math. Soc. 63(3):422–438, 1948. https://doi.org/10.1090/S0002-9947-1948-0025098-8

Why private information changes bargaining

An arbitrator choosing an outcome for several people can ask them about their preferences, but the answer to that question may affect the outcome. A person who expects to gain from a false report may give one. Roger Myerson's 1979 paper puts this incentive problem inside a bargaining model: the arbitrator may randomize over collective choices, and an allocation is considered feasible only if some mechanism makes truthful reporting an equilibrium. The paper then applies a weighted Nash bargaining criterion to the resulting set of feasible interim payoffs. The mission formalizes the existence and uniqueness result for that criterion, along with the finite Bayesian model on which it depends.

The issue matters whenever an agreement is selected using information known privately to its participants. If the arbitrator evaluates a payoff vector that can arise only when somebody has a reason to lie, that vector cannot serve as a credible bargaining alternative under the model's own behavior assumption. Myerson's feasible set keeps the behavioral constraint visible when the group compares agreements. This mission addresses the paper's Theorems 1 and 3 and the claims between them that establish the relevant sets and their reference point.

The finite Bayesian choice problem

Let $I$ be a nonempty finite set of players. Player $i$ has a nonempty finite type set $A_i$, and the group has a nonempty finite set $C$ of possible choices. A type profile is $\alpha\in\prod_{i\in I}A_i$. The utility $U_i(c,\alpha)\in\mathbb R$ is player $i$'s payoff when choice $c$ occurs and $\alpha$ is the true profile. A nonnegative function $P$ on type profiles, summing to one, is the common prior. Write $R_i(a_i)$ for the probability that player $i$ has type $a_i$, and $P_i(\alpha\mid a_i)$ for the posterior probability of $\alpha$ conditional on that type. Every $R_i(a_i)$ is positive, so the conditional probabilities are defined.

A choice mechanism $\pi$ asks each player for a response and assigns a probability $\pi(c\mid s)$ to each choice $c$ at each response profile $s$. For the direct mechanisms used here, the response set of player $i$ is $A_i$: a response is a claimed type. The probabilities are nonnegative and sum to one for each response profile. If a player whose true type is $a_i$ instead reports $b_i$, while the others report truthfully, the player's conditional expected utility is $Z_i(\pi,b_i\mid a_i)$. The posterior $P_i(\alpha\mid a_i)$ weights true profiles; the mechanism sees the profile with only coordinate $i$ replaced by $b_i$; and utility is evaluated at the true profile $\alpha$.

The mechanism is Bayesian incentive-compatible when $Z_i(\pi,a_i\mid a_i)\ge Z_i(\pi,b_i\mid a_i)$ for every player and pair of types. Its interim payoff vector $V(\pi)$ has one coordinate $V_{i,a_i}(\pi)=Z_i(\pi,a_i\mid a_i)$ for every player-type pair. The set $F$ contains the vectors attained by all direct choice mechanisms; $F^*$ contains those attained by Bayesian incentive-compatible direct choice mechanisms. Theorem 1 says $F^*$ is nonempty, convex, compact, and contained in $F$. The nonemptiness claim includes the mechanism that selects each choice with probability $1/|C|$, independent of all reports.

Formalization targets

Fix a conflict outcome $c^*\in C$: the choice that occurs if bargaining fails. Its conflict payoff vector $t$ gives each player type the conditional expected utility from that fixed choice. A constant mechanism selects $c^*$ regardless of reports. It is incentive-compatible and generates $t$, so $t\in F^*$. The individually rational incentive-feasible set is

$$F^*_+=\{x\in F^*: x_{i,a_i}\ge t_{i,a_i}\text{ for all }i,a_i\}.$$

For $x\in F^*_+$, the generalized Nash product of equation (18) is

$$N(x)=\prod_{i\in I}\prod_{a_i\in A_i} (x_{i,a_i}-t_{i,a_i})^{R_i(a_i)}.$$

A bargaining solution is a vector in $F^*_+$ that maximizes $N$ over that set. Myerson's Theorem 3, the goal of this mission, says that if the constant conflict mechanism is not incentive-efficient—that is, an incentive-compatible mechanism strictly improves every player-type payoff over it—then exactly one such vector exists:

$$\neg\operatorname{Efficient}(\pi_{c^*}) \quad\Longrightarrow\quad \exists!x\in F^*_+\;\forall y\in F^*_+,\;N(y)\le N(x).$$

The milestones follow the paper's claims: the uniform mechanism is incentive-compatible; $F^*$ has the four properties in Theorem 1; the conflict vector belongs to $F^*$; every Nash-product maximizer strictly improves each conflict payoff when such improvement is feasible; and every implementing mechanism is incentive-efficient. The final claim concerns a mechanism that realizes the maximizing vector. It does not assert uniqueness of that mechanism.

What the result provides

Theorem 1 supplies a feasible set that respects truthful reporting. Theorem 3 selects a unique interim payoff vector from that set after a conflict outcome is specified. It thereby gives a well-defined allocation criterion for the paper's finite Bayesian collective choice problems. Myerson also observes that several mechanisms may implement the same solution. The allocation, rather than a unique mechanism, is the object selected by the theorem.

The result was proved in the 1979 paper. The work here is a machine-checked statement and, for solvers, a proof of that known result and its supporting claims in Lean. The mission's statements are open proof targets; the source paper's proof is not claimed to have been formalized already. A related platform item on Nash's two-player axiomatic characterization concerns a solution function on compact convex subsets of $\mathbb R^2$. It is a distinct result and supplies neither this paper's Bayesian model nor Theorem 3.

The mathematical obstacle

The set of all real-valued functions on choices and reports is much larger than the set of mechanisms: probabilities must be nonnegative and sum to one at every report profile. Bayesian incentive compatibility adds inequalities involving the true and reported type in different positions. Theorem 1 requires these constraints to give the compact, convex set of attainable interim payoffs, rather than merely a formal collection of payoff functions.

The Nash product also has a boundary: an individually rational vector may match the conflict payoff in one coordinate, making its product zero. Theorem 3's hypothesis has to rule out a zero maximum before uniqueness of an interior maximum can be concluded. The weights $R_i(a_i)$ matter in that uniqueness statement, and the result ranges over all player-type coordinates, not only one aggregate payoff per player. Restricting the maximization to an arbitrary small subset, fixing two players, or assuming a positive maximum would change the theorem.

Formalization scope

Lean represents players, each type set, and choices as finite nonempty types. Type profiles are dependent functions $\prod_i A_i$; interim vectors are real functions on the disjoint union $\sum_i A_i$, with the product topology. A mechanism is a real function $\pi:C\to(\prod_i A_i)\to\mathbb R$ subject to explicit nonnegativity and sum-to-one constraints. Both $F$ and $F^*$ quantify only over functions satisfying those constraints. Conditional beliefs use the common prior in equations (3)–(4), and positive marginal probabilities make every denominator meaningful without requiring positive probability for each full profile. The positivity of every $R_i(a_i)$ is an assumption the paper makes implicitly by dividing by it in (3); it is a field of the problem structure, not a hypothesis of the theorems. The subjective reading of $P_i$ and $R_i$ that the paper permits on p. 63, the response-plan equilibria of Section 3, and the numerical example of Section 6 are outside this mission.

Strict dominance means a strict gain for every player type. The constant mechanism, conflict vector, and individually rational set are defined from the problem data. The conflict vector is defined by equation (16), while its equality with the constant mechanism's payoff is a theorem item. The product uses real powers with the paper's marginal weights and is compared only on $F^*_+$, where each base is nonnegative. A solution is a maximizer property; it is not chosen in advance or supplied as a theorem hypothesis. These choices exclude vacuous encodings of incentive efficiency, unrestricted mechanisms, and a maximization domain that already contains only a nominated winner.

A complete proof development needs finite sums and products, continuous and convex maps on finite-dimensional real spaces, compactness of the constrained mechanism set, and facts about positive weighted real powers or logarithms on the strictly positive region. The model definitions can be reused for the paper's separate revelation-principle mission; this mission also welcomes proofs of the explicit claims about the uniform mechanism, the conflict mechanism, and product maximizers.

Selected references

• Roger B. Myerson, Incentive Compatibility and the Bargaining Problem, Econometrica 47(1), 61–73, 1979. DOI: 10.2307/1912346.
• John F. Nash, The Bargaining Problem, Econometrica 18(2), 155–162, 1950. DOI: 10.2307/1907266.
• John C. Harsanyi and Reinhard Selten, A Generalized Nash Solution for Two-Person Bargaining Games with Incomplete Information, Management Science 18(5), P80–P106, 1972. DOI: 10.1287/mnsc.18.5.80.