All missions

Motivation

Two impossibility theorems frame the theory of collective choice. Arrow's theorem (1951) says that a rule aggregating individual preference orderings into a social ordering, subject to a short list of reasonable conditions, must be dictatorial. The Gibbard–Satterthwaite theorem (Gibbard 1973, Satterthwaite 1975) says that a voting procedure selecting a single alternative, which no voter can manipulate by misreporting, must be dictatorial once at least three outcomes are possible. Both conclusions are the same, and the two conditions—Arrow's axioms and strategy-proofness—look unrelated: one is about the coherence of a social ranking, the other about voters' incentives.

Satterthwaite's paper (Northwestern Discussion Paper No. 122, 1974; J. Econ. Theory 10, 1975) shows that the two conditions are in fact the same condition. Section 4 constructs a one-to-one correspondence between strict strategy-proof voting procedures with full range and strict social welfare functions satisfying Arrow's conditions, under which each social welfare function's top choice is the voting procedure's outcome. This mission formalizes that correspondence.

Timeline. Arrow (1951, 2nd ed. 1963) proved the general possibility theorem with conditions of non-negative response (NNR), citizens' sovereignty (CS), independence of irrelevant alternatives (IIA) and non-dictatorship. Gibbard (1973) proved that strategy-proof game forms with at least three outcomes are dictatorial, by first showing that a strategy-proof procedure induces an Arrovian social welfare function and then applying Arrow's theorem. Satterthwaite (1974/75) gave an independent direct proof of the voting-procedure theorem and proved the correspondence theorem (Theorem 2), which turns Gibbard's construction into an exact equivalence.

Setting

A committee $I_n$ of $n$ individuals chooses from a finite set $S_m$ of $m$ alternatives. A strong order on $S_m$ is a complete, transitive relation $R$ with no indifference between distinct alternatives; $x\,\bar R\,y$ denotes strict preference. Let $\rho_m$ be the set of strong orders and $\rho_m^n$ the set of strict ballot sets $B=(B_1,\dots,B_n)$.

• A strict voting procedure is a map $v:\rho_m^n\to S_m$; its range is $T_p=\{v(B):B\in\rho_m^n\}$. It is strategy-proof if no individual $i$, at any $B$, has a ballot $B_i'$ with $v(B_1,\dots,B_i',\dots,B_n)\,\bar B_i\,v(B)$.
• A strict social welfare function is a map $u:\rho_m^n\to\rho_m$; $A_B=u(B)$ is the social ordering.
• For $W\subseteq S_m$, $\Psi_W(R)$ is the set of $R$-best elements of $W$, and $\theta_W(R)$ is the restriction of $R$ to $W$.
• $u$ underlies $v$, and $v$ is derived from $u$, if $\Psi_{S_m}[u(B)]=\{v(B)\}$ for every $B$.

Arrow's conditions on $u$: CS—for all $x\ne y$ some $B$ gives $x\,\bar A_B\,y$; IIA—if $\theta_W(C_i)=\theta_W(D_i)$ for all $i$ then $\Psi_W(A_C)=\Psi_W(A_D)$; NNR—raising an alternative $x$ in individual ballots, with the order of the other alternatives unchanged, never lowers $x$ against any other alternative in the social ordering. PO (Pareto optimality): unanimous strict preference for $x$ over $y$ yields $x\,\bar A\,y$.

Formalization targets

Goal: Theorem 2 (p. 35)

For $n\ge2$ and $m\ge3$ there is a bijection

$$\lambda:\{v \text{ strict, strategy-proof},\ T_p=S_m\}\ \longrightarrow\ \{u \text{ strict},\ \text{CS},\ \text{NNR},\ \text{IIA}\}$$

with $\Psi_{S_m}[\lambda(v)(B)]=\{v(B)\}$ for every $v$ and every $B\in\rho_m^n$.

Milestones

1. CS, NNR and IIA imply PO (p. 31, after Arrow), and PO implies CS (p. 31).
2. Lemma 7 (p. 30): the voting procedure derived from a strict $u$ with CS, NNR, IIA exists, is strategy-proof and has range $S_m$.
3. Gibbard's claim (p. 33): for a strict strategy-proof $v$ with range $S_m$ and a fixed strong order $Q$, the relation $P(B)$ defined by $x\,\bar P\,y\iff x=v[\Delta_{xy}(B_1),\dots,\Delta_{xy}(B_n)]$ is a strong order, and $\mu:B\mapsto P(B)$ underlies $v$ and satisfies PO and IIA.
4. Uniqueness (p. 34): at most one strict $u$ with PO and IIA underlies a strict strategy-proof $v$.
5. NNR (p. 34): such an underlying $u$ satisfies NNR.
6. Lemma 8 (p. 35): a strict strategy-proof $v$ with range $S_m$ has exactly one underlying strict $u$ with CS, NNR, IIA.

Significance

The correspondence explains why the two impossibility theorems have the same conclusion: for strict preferences, a strategy-proof procedure with full range and an Arrovian social welfare function are two descriptions of one object. In particular either impossibility theorem, together with Theorem 2, yields the other. The paper draws a second consequence: a social welfare function violating rationality or IIA has a derived voting procedure that is manipulable, so Arrow's much-debated conditions are forced by the practical requirement of strategy-proofness.

On the formal side, the platform already has machine-checked proofs of the strict Arrow theorem (AGT.arrow_theorem, unanimity and pairwise IIA) and of the strict full-range Gibbard–Satterthwaite theorem (AGT.gibbard_satterthwaite). Together these determine both sides of Theorem 2 as sets of dictatorships, but neither states the correspondence, the derived/underlying relation, Gibbard's construction or NNR, and nothing on the platform states Lemmas 7 or 8. The milestones here formalize the paper's direct argument, which does not pass through the impossibility theorems.

Difficulty

The obvious argument fails in two places. First, a strategy-proof voting procedure determines only the top of a social ordering, and the whole ordering must be recovered; Gibbard's relation $P$ does this, but proving that $P$ is transitive is the core of Gibbard's proof of the Gibbard–Satterthwaite theorem, which the paper cites rather than proves. Second, NNR as stated allows many individuals to move $x$ at once, while the manipulation argument works with one ballot at a time; one must pass from a single-voter change to an arbitrary one without losing IIA or PO along the way.

A newcomer's first idea is to prove both sides are dictatorships and match dictators. That proves the bijection but needs both impossibility theorems as inputs, and the correspondence must still carry the underlying relation for every procedure.

Formalization scope

• Alternatives and individuals are finite types A, ι with decidable equality; $n=|\iota|\ge2$, $m=|A|\ge3$ throughout.
• Weak orders are a structure (relation, completeness, transitivity); strong orders are the subtype with no indifference between distinct elements. Strict ballot sets are functions ι → StrongOrder A, and voting procedures and social welfare functions are defined only on them. Two social welfare functions are therefore equal exactly when they agree on every strict ballot set; this is what makes uniqueness in Lemma 8 and the bijection in Theorem 2 meaningful.
• The range $T_p$ is the image of strict ballot sets; "$T_p\equiv S_m$" is Set.range v = Set.univ.
• $\theta_W(C_i)=\theta_W(D_i)$ is agreement of the two relations on $W\times W$.
• CS is stated for $x\ne y$: as printed ("for every $x,y$") it is unsatisfiable at $x=y$ for a strict social ordering, and every statement would become vacuous. NNR's "for some $x$" is read as "for every $x$".
• "Derived from" and "underlies" are the same relation $\Psi_{S_m}[u(B)]=\{v(B)\}$; Lemma 7 asserts existence of the derived procedure and its properties for every derived procedure.
• Gibbard's $\Delta_{xy}$ and $P$ are definitions; $P$ is the reflexive closure of the paper's $\bar P$.
• The PO claim, PO ⇒ CS, uniqueness and the NNR claim are unconditional in the paper; they are stated under §4's standing $n\ge2$, $m\ge3$, since with no individuals PO fails.
• Theorem 2 is stated as an Equiv together with "$\lambda(v)$ underlies $v$" for every $v$. A bare existence of a bijection between the two sets is a cardinality fact and is not the theorem.

Reusable beyond this mission: the strict-preference vocabulary (strong orders, $\Psi_W$, Arrow's conditions in the paper's form) and Gibbard's $\Delta_{xy}$ construction. Contributions welcome: proofs of each milestone, and bridges to AGT.arrow_theorem and AGT.gibbard_satterthwaite.

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; J. Econ. Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
• A. Gibbard, Manipulation of Voting Schemes: A General Result, Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083
• K. J. Arrow, Social Choice and Individual Values, 2nd ed., Wiley, 1963.

Motivation

A social welfare function turns the rankings of the members of a committee into one ranking for the committee. Arrow's general possibility theorem (Arrow, 1951/1963) shows that, once there are at least three alternatives, no such rule satisfies a short list of conditions that each look harmless unless it follows a single member's ranking. The theorem is the starting point of social choice theory and underlies the study of voting rules, preference aggregation in economics, and rank aggregation in computer science.

Arrow's own setting allows indifference: ballots and the social ordering are weak orders, and the conditions he imposed are citizens' sovereignty, non-negative response, and independence of irrelevant alternatives. Many textbook proofs, and the existing machine-checked versions, instead take strict ballots and replace the first two conditions by the Pareto condition.

Satterthwaite's discussion paper (Satterthwaite, Northwestern DP No. 122, 1974, journal version J. Econ. Theory 10 (1975)) gives a new proof of Arrow's theorem. Strict Arrovian social welfare functions correspond one-to-one to strategy-proof voting procedures with full range, and the Gibbard–Satterthwaite theorem then forces a dictator. His §6 extends the argument to weak orders by decomposing a social welfare function into a tie-breaking step followed by a strict one. This mission formalizes that weak-order extension and the strict theorem it rests on.

Timeline.

• 1951: Arrow proves the general possibility theorem for weak orders under CS, NNR, IIA and non-dictatorship. The second edition (1963) corrects the first edition's statement.
• 1973: Gibbard proves that every strategy-proof game form with at least three outcomes is dictatorial (Econometrica 41).
• 1975: Satterthwaite proves the same independently for voting procedures, and shows that strategy-proof procedures and Arrovian social welfare functions correspond. This gives a proof of Arrow's theorem by way of strategy-proofness.

Setting

A committee $I_n$ of $n$ individuals ranks a finite set $S_m$ of $m$ alternatives. A weak order $R$ on $S_m$ is a complete, transitive relation, and $x\,R\,y$ reads "$x$ is preferred or indifferent to $y$". Its strict part is $x\,\bar R\,y$: $x\,R\,y$ and not $y\,R\,x$. The weak orders form $\pi_m$. A strong order is a weak order with no indifference between distinct alternatives, and the strong orders form $\rho_m$. A ballot set is $B=(B_1,\dots,B_n)\in\pi_m^n$.

A social welfare function $u$ assigns to every ballot set a social ordering $A=u(B)\in\pi_m$. A strict social welfare function $\mu$ is defined only on strong ballot sets $\rho_m^n$ and takes values in $\rho_m$. For $W\subseteq S_m$, $\Psi_W(R)$ is the set of $R$-best elements of $W$, and $\theta_W(R)$ is the restriction of $R$ to $W$.

• CS (citizens' sovereignty): for all distinct $x,y$ some ballot set yields $x\,\bar A\,y$.
• IIA (independence of irrelevant alternatives): if $\theta_W(C_i)=\theta_W(D_i)$ for every $i$, then $\Psi_W(A_C)=\Psi_W(A_D)$.
• NNR (non-negative response): if $D$ differs from $C$ only by raising an alternative $x$ on some ballots, then $x\,\bar A_C\,z$ implies $x\,\bar A_D\,z$ for all $z\neq x$.
• Dictatorial: some $i$ exists such that $x\,\bar B_i\,y$ implies $x\,\bar A\,y$ for every ballot set and all $x,y$.

A tie-breaking function $\alpha$ maps every weak ballot set to a strong one while keeping every strict preference. It is regular if each individual's ties are broken by a fixed strong order $Q_i$.

Formalization targets

Goal: Theorem 3' (p. 49)

For $n\ge 2$, $m\ge 3$ and any social welfare function $u$ on weak ballot sets,

$$u \text{ satisfies CS, NNR, IIA} \;\Longrightarrow\; \exists\, i\;\forall B\;\forall x,y:\; x\,\bar B_i\,y \Rightarrow x\,\overline{u(B)}\,y .$$

The converse is false with indifference, so the goal is one-directional.

Milestones

1. Theorem 3 (p. 36): for strict $\mu$, CS, NNR and IIA hold if and only if $\mu$ is dictatorial.
2. Lemma 10, first sentence (p. 44): if $u$ has range in $\rho_m$ and $u=\mu\circ\gamma$ with $\gamma$ regular and $\mu$ strict Arrovian, then $u$ satisfies IIA, CS and NNR.
3. Lemma 10, second sentence (p. 44): if $u$ has range in $\rho_m$ and satisfies IIA, CS and NNR, then $u=\mu\circ\alpha$ for a tie-breaking function $\alpha$ and a strict $\mu$ satisfying IIA, CS and NNR.
4. Lemma 11 (p. 48): breaking the ties of each social ordering $u(B)$ by a strong order $Q$ preserves CS, NNR and IIA and gives range in $\rho_m$.

Significance

Theorem 3' is Arrow's theorem in the setting Arrow stated it: weak-order ballots, a weak social ordering, and the conditions CS and NNR instead of the Pareto condition. Lemma 10 and Lemma 11 together say that Arrovian social welfare functions with indifference are determined by strict ones up to tie-breaking. This is the structural fact the paper also uses for its weak-order correspondence (Theorem 2').

All results here are proved in the paper. None is formalized as stated. The platform holds a proved strict Arrow theorem, AGT.arrow_theorem, for social welfare functions on strict total orders under unanimity and pairwise IIA. Theorem 3's only-if half follows from it once CS, NNR and IIA are shown to imply the Pareto condition and the two encodings are bridged. The weak-order statement, the tie-breaking lemmas, and the "if" half of Theorem 3 are new to the platform.

Difficulty

Passing from strict to weak orders is the hard step. Restricting a weak ordering to a pair of alternatives does not determine its choice sets on larger sets once ties are present. A social welfare function that satisfies IIA on weak orders need not induce one on strong orders through an arbitrary tie-breaker. Breaking ties ballot by ballot with a non-regular rule can destroy IIA, and breaking ties in the social ordering can destroy NNR unless the same fixed order is used throughout. The obvious reduction is "break all ties and apply the strict theorem", and it fails: the dictator of the tie-broken function could depend on the tie-breaking order. The fact that it does not is part of what must be shown.

Formalization scope

• Alternatives and individuals are finite types A and ι with decidable equality. $n$ = Fintype.card ι, $m$ = Fintype.card A, and $n\ge 2$, $m\ge 3$ are hypotheses as printed. All statements live in StrategyProofArrow.WeakArrow.
• A weak order is a structure (a relation with completeness and transitivity). A strong order is the subtype with no indifference between distinct elements. Strong ballot sets are functions into that subtype, so a strict social welfare function is defined on admissible profiles only.
• $\theta_W(C)=\theta_W(D)$ is agreement of the two relations on $W\times W$. $\Psi_W$ is a set, compared as a set, since weak orders can have several best elements.
• CS is stated for distinct $x\neq y$. As printed ("for every $x,y$") it is unsatisfiable at $x=y$, and every theorem would become vacuous. No other trivializing reading is possible: the dictator conclusion is the paper's one-directional negation of ND, not $u(B)=B_i$, which would be false for weak orders.
• Lemma 11's tie-breaker acts on a single ordering. It is encoded as breaking the ties of $u(B)$ by a strong order $Q$, the "tie-breaking order for $\gamma$" of the proof of Theorem 3'.
• Lemma 10's printed $u^{nm}(B)=u^{nm}[\gamma(B)]$ is read $u(B)=\mu(\gamma(B))$, following the proof.

The definitions duplicate objects drafted in the sibling missions of this series (weak and strong orders, CS, NNR, IIA). Proofs of the strict theorem from the Gibbard–Satterthwaite theorem, bridges to AGT.arrow_theorem, and reusable lemmas about tie-breaking of weak orders are all welcome.

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, 1974 (rev. Dec. 12, 1974); J. Econ. Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
• K. J. Arrow, Social Choice and Individual Values, 2nd ed., Yale University Press, 1963. https://doi.org/10.12987/9780300186987
• A. Gibbard, Manipulation of Voting Schemes: A General Result, Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083

Motivation

The method of multipliers (augmented Lagrangian method), proposed independently by Hestenes and Powell in 1969, solves a constrained optimization problem by a sequence of unconstrained minimizations of a penalized Lagrangian, updating a multiplier estimate between them. It became one of the standard algorithms of nonlinear programming and is the ancestor of ADMM and of the proximal-point view of dual methods. Rockafellar's 1973 paper (Math. Programming 5, 354–373) extended the method to inequality constraints with the penalty Lagrangian $L_r$ and reinterpreted it as unconstrained maximization of a smooth concave dual function $g_r$. Its §4 shows that primal points recovered from any maximizing dual sequence are asymptotically minimizing; its §5, the subject of this mission, asks how fast they converge.

Timeline. 1969: Hestenes and Powell introduce multiplier methods for equality constraints. 1973: Rockafellar treats inequality constraints in the convex case through $L_r$ and its dual (this paper), and in the same year applies the multiplier method of Hestenes and Powell to convex programming (J. Optim. Theory Appl. 12). 1976: Rockafellar's "Augmented Lagrangians and applications of the proximal point algorithm in convex programming" (Math. Oper. Res. 1) gives the general convergence theory.

Setting

Let $X \subset \mathbb R^n$ be convex and $f_0, f_1, \dots, f_m : X \to \mathbb R$ convex. The problem is

$$\text{(P)}\qquad \text{minimize } f_0(x) \text{ over } x \in X \text{ subject to } f_i(x) \le 0,\ i = 1, \dots, m.$$

With $\theta(t) = \max\{0, t\}$ and a parameter $r > 0$, the penalty Lagrangian is

$$L_r(x, y) = f_0(x) + \frac{1}{4r}\sum_{i=1}^m \big[\theta(y_i + 2 r f_i(x))^2 - y_i^2\big], \qquad x \in X,\ y \in \mathbb R^m,$$

and the dual problem $(D_r)$ maximizes $g_r(y) = \inf_{x \in X} L_r(x, y)$ over all $y \in \mathbb R^m$; $\sup g_r$ is its supremum. A maximizing sequence is a sequence $\{y^k\}$ with $g_r(y^k) \to \sup g_r$. The dual method of Theorem 4.1 takes a bounded maximizing sequence $\{y^k\}$ and, for each $k$, a point $x^k \in X$ that minimizes $L_r(\cdot, y^k)$ to within a tolerance $\alpha_k$:

$$L_r(x^k, y^k) - g_r(y^k) \le \alpha_k, \qquad \alpha_k \to 0. \qquad (4.7)$$

The standing assumptions of §5 concern a point $\bar x \in \operatorname{int} X$ that is an optimal solution of (P), near which $f_0, \dots, f_m$ are twice continuously differentiable, and a multiplier vector $\bar y$ satisfying with $\bar x$ the Kuhn–Tucker conditions ($\bar y_i \ge 0$, $f_i(\bar x) \le 0$, $\bar y_i f_i(\bar x) = 0$, and $\bar x$ minimizes $f_0 + \sum_i \bar y_i f_i$ over $X$). With $I = \{i : f_i(\bar x) = 0\}$ the active set and $H(x, y) = \nabla^2 f_0(x) + \sum_{i \in I} y_i \nabla^2 f_i(x)$, they are: (i) $\bar y_i \ne 0$ for $i \in I$; (ii) the $\nabla f_i(\bar x)$, $i \in I$, are linearly independent; (iii) $z \cdot H(\bar x, \bar y) z > 0$ for every nonzero $z$ with $z \cdot \nabla f_i(\bar x) = 0$ for all $i \in I$.

Formalization targets

Goal: Corollary 5.3

Under the standing assumptions, with $\{y^k\}, \{x^k\}, \{\alpha_k\}$ as in (4.7), if for some $q > 0$

$$\alpha_k \le q\,[\sup g_r - g_r(y^k)] \quad \text{for all sufficiently large } k, \qquad (5.18)$$

then there is a constant $s > 0$ with

$$|x^k - \bar x| \le s\,|y^k - \bar y| \quad \text{for all sufficiently large } k. \qquad (5.19)$$

No rate for $\{y^k\}$ is fixed: the statement compares the primal error with the dual error, whatever method produces the dual sequence.

Milestones

1. $\bar x$ is the unique optimal solution to (P) and $\bar y$ the unique optimal solution to the ordinary dual $(D_0)$ and every $(D_r)$ for $r > 0$ (§5, after (5.1)).
2. Theorem 5.1 (i)–(iii): for every $r, \beta > 0$ there are $\varepsilon, \alpha > 0$ such that $\sup g_r - g_r(y) \le \varepsilon$ and $L_r(x, y) - g_r(y) \le \alpha$ force $(x, y)$ into a $\beta$-neighborhood of $(\bar x, \bar y)$ with $x \in \operatorname{int} X$, where $L_r$ is $C^2$, given locally by (5.4), and $\nabla_x^2 L_r(x, y)$ is positive definite.
3. Theorem 5.1 (iv): the unique minimizer $\xi(y)$ of $L_r(\cdot, y)$ over $X$ is $C^1$ in $y$ with derivative (5.5).
4. Theorem 5.1 (v): $g_r$ is $C^2$ with negative definite Hessian (5.6)–(5.7).
5. Corollary 5.2 (5.14): $x^k \to \bar x$ and $y^k \to \bar y$.
6. Corollary 5.2 (5.15)–(5.17): $a|x^k - \xi(y^k)|^2 \le \alpha_k$, $b_1|y^k - \bar y|_I \le |\xi(y^k) - \bar x| \le b_2|y^k - \bar y|_I$, and $c_1|y^k - \bar y|^2 \le g_r(\bar y) - g_r(y^k) \le c_2|y^k - \bar y|^2$.

Significance

Corollary 5.3 is the paper's answer to the practical question of how accurately each inner minimization must be done. A tolerance proportional to the current dual gap costs nothing in the order of convergence: the primal iterates then converge at least as fast as the dual ones. Since $g_r$ is $C^2$ with a negative definite Hessian near $\bar y$ (Theorem 5.1 (v)), any locally linearly or superlinearly convergent unconstrained method applied to $g_r$ yields a primal sequence with the same rate. The estimates (5.15)–(5.17) are the quantitative bridge between inner accuracy, dual error and primal error, and reappear in later analyses of inexact augmented Lagrangian methods.

The results are proved in the paper (1973) and in textbook treatments; none of them has a machine-checked proof on this platform or in Mathlib. The mission produces a formal statement of the second-order theory of the penalty Lagrangian: the local smooth structure of $L_r$ and $g_r$, the implicit minimizer map $\xi$, and the rate comparison. Complete formal proofs of each milestone are the remaining work.

Difficulty

The obvious argument linearizes everything at $(\bar x, \bar y)$, but $L_r$ is only $C^1$ globally: $\theta^2$ has a kink in its second derivative, so smoothness of $L_r$ must first be established on a neighborhood of $(\bar x, \bar y)$, using complementary slackness and strict complementarity (i) to fix which branch of (2.4) each constraint follows. The sequence $\{(x^k, y^k)\}$ is not assumed to converge; localizing it into that neighborhood requires the uniform statement of Theorem 5.1 (i) (with $\varepsilon, \alpha$ chosen after $r, \beta$) and the uniqueness of $\bar x$ and $\bar y$. The minimizer map $\xi$ then comes from the implicit function theorem applied to $\nabla_x L_r(x, y) = 0$, and the formula for $\nabla^2 g_r$ needs the derivative of the envelope $g_r(y) = L_r(\xi(y), y)$.

Formalization scope

• Spaces. Primal points lie in EuclideanSpace ℝ (Fin n), multipliers in EuclideanSpace ℝ (Fin m); constraint indices are Fin m (0-based), and $f_0$ is a separate argument.
• Functions. The $f_i$ are total functions on $\mathbb R^n$; convexity is assumed on $X$ only (ConvexOn ℝ X, an explicit hypothesis of every theorem, the paper's standing assumption of p. 358), and twice continuous differentiability only on a neighborhood of $\bar x$. Smoothness of $L_r$ and $g_r$ is always a conclusion, never a hypothesis.
• Extended values. $g_0$, $g_r$, $\sup g_r$ and the infimum in (P) are computed in EReal, so (4.7), (5.2), (5.3) and (5.18) are differences in $[-\infty, +\infty]$; $r > 0$ is explicit for the penalty Lagrangian, while $L_0$ is defined separately.
• Derivatives. Hessians are quadratic forms $z \cdot D(\nabla\varphi)(x) z$; every inverse matrix appears together with positive definiteness of the same matrix, so Lean's convention that a non-invertible map has inverse $0$ never applies. Local identities such as (5.4) are stated as equality on a neighborhood, not globally.
• Choices. The assumption of Theorem 4.1 that the asymptotic optimal value is finite is omitted because it holds under the §5 assumptions. "Generated as in Theorem 4.1" is spelled out as its hypotheses. In (5.15)–(5.17), $\xi$ is any function that picks a minimizer of $L_r(\cdot, y)$ over $X$ whenever one exists; along $y^k$ it eventually coincides with the paper's unique minimizer. In (iv) and (v), the conclusions are stated for every $y$ with $\sup g_r - g_r(y) \le \varepsilon$, since they do not depend on $x$.
• Ruled out. The goal does not assume that $x^k$ or $y^k$ converge, nor that $y^k \ne \bar y$, and $s > 0$ is one constant valid for all large $k$; a formalization assuming convergence, or one with an unsatisfiable second-order hypothesis, would be trivial. The standing assumptions and all sequence hypotheses are satisfiable (checked on $f_0(x) = |x|^2$, $f_1(x) = 1 - e\cdot x$ in $\mathbb R^1$).
• Infrastructure. The proofs need the implicit function theorem (Mathlib's Analysis/Calculus/Implicit), second derivatives of compositions, envelope differentiation, and the quadratic-growth estimates of a $C^2$ function with definite Hessian. Results on Hessian forms and on strict complementarity are reusable beyond this mission. Proofs of individual milestones are welcome independently.

Selected references

• R. T. Rockafellar, A dual approach to solving nonlinear programming problems by unconstrained optimization, Mathematical Programming 5 (1973) 354–373. https://doi.org/10.1007/BF01580138
• M. R. Hestenes, Multiplier and gradient methods, Journal of Optimization Theory and Applications 4 (1969) 303–320. https://doi.org/10.1007/BF00927673
• M. J. D. Powell, A method for nonlinear constraints in minimization problems, in R. Fletcher (ed.), Optimization, Academic Press, 1969, 283–298.
• R. T. Rockafellar, The multiplier method of Hestenes and Powell applied to convex programming, Journal of Optimization Theory and Applications 12 (1973) 555–562. https://doi.org/10.1007/BF00934777
• R. T. Rockafellar, Augmented Lagrangians and applications of the proximal point algorithm in convex programming, Mathematics of Operations Research 1 (1976) 97–116. https://doi.org/10.1287/moor.1.2.97

Motivation

Volatility estimates from daily high, low and closing prices have been used since Parkinson (1980) and Garman and Klass (1980): the range of a day's log-price carries much more information about the volatility $\sigma$ than the close alone. Rogers and Satchell (1991) propose an estimator, $S_1(S_1-X_1)+I_1(I_1-X_1)$, that is unbiased for $\sigma^2$ whatever the drift of the log-price. The companion mission (Part I) formalizes that unbiasedness.

Every such estimator meets the same practical problem. The true high and low of the continuous path are never observed; one sees the maximum and minimum of the path sampled at $N$ times. The sampled maximum $S$ falls short of the true maximum $S_1$ by an amount $\Delta = S_1 - S \ge 0$, and the resulting downward bias is large in practice (Garman and Klass, and Beckers (1983), identified it). Section 3 of Rogers and Satchell proposes a correction: model $\Delta$ by a random variable with an explicit law, compute its first two moments exactly, and subtract their effect. The constants that appear,

$$a=\sqrt{2\pi}\Big[\tfrac14-\tfrac{\sqrt2-1}{6}\Big],\qquad b=\frac{1+3\pi/4}{12},$$

enter the corrected estimator directly. Their simulations (Tables 1–3 of the paper) show that the correction removes most of the bias.

Setting

Fix a volatility $\sigma>0$ and a sampling mesh $h>0$ (in the paper $h=1/N$). For a level $\alpha\ge0$ define

$$G_{\sigma,h}(\alpha)=\int_0^h e^{-2\alpha^2/(u\sigma^2)}\,\frac{du}{(4uh)^{1/2}} .$$

The factor $e^{-2\alpha^2/(u\sigma^2)}$ is the probability that a Brownian bridge of duration $u$ and volatility $\sigma$ climbs above level $\alpha$. The factor $(4uh)^{-1/2}$ is a probability density on $(0,h]$. Since $G_{\sigma,h}(0)=1$ and $G_{\sigma,h}$ decreases continuously to $0$, it is the survival function of a law on $(0,\infty)$. This law is the paper's display (9).

A real random variable $Z$ has distribution (9) if it is measurable and $P(Z>\alpha)=G_{\sigma,h}(\alpha)$ for every $\alpha\ge0$. In the paper, $Z$ is the overshoot of the continuous maximum over the sampled maximum $x$ in the sampling interval to the left of the time $t$ at which $x$ is attained, and $Z'$ is the overshoot in the interval to the right. The paper then assumes (p. 508) that $Z$ and $Z'$ are independent, each with distribution (9), and approximates $\Delta$ by $Z\vee Z'=\max(Z,Z')$. Write $Z\wedge Z'=\min(Z,Z')$.

In Lean, overshootSurvival σ h α is $G_{\sigma,h}(\alpha)$, HasOvershootLaw P σ h Z is "$Z$ has distribution (9) under $P$", and constA, constB are $a$ and $b$.

Formalization targets

Goal: the two moments of $Z\vee Z'$ (Eq. (11), p. 508, and the display on p. 509)

For $\sigma,h>0$ and $Z,Z'$ independent with distribution (9), the variables $Z\vee Z'$ and $(Z\vee Z')^2$ are integrable, and

$$E(Z\vee Z')=a\,\sigma\sqrt h,\qquad E\big[(Z\vee Z')^2\big]=b\,\sigma^2h .$$

Milestones, in the order the paper uses them

1. (9), p. 507. The two integral forms of the survival function agree:

$$\int_0^h e^{-2\alpha^2/(u\sigma^2)}\frac{du}{(4uh)^{1/2}}=\int_{h^{-1}}^\infty e^{-2\alpha^2s/\sigma^2}\frac{ds}{(4hs^3)^{1/2}} .$$

2. (10), p. 508. $EZ=\sigma(2\pi h)^{1/2}/8$.
3. Display before (11), p. 508. $E(Z\wedge Z')=\sqrt{2\pi h}\,(\sqrt2-1)\,\sigma/6$.
4. (12), p. 508. $EZ^2=\sigma^2h/6$.
5. (13), p. 509. $E[(Z\wedge Z')^2]=\frac{\sigma^2h}{4}\big(1-\frac\pi4\big)$.

The goal combines milestones 2–5 through $Z\vee Z'=Z+Z'-Z\wedge Z'$, which the paper uses in (11).

Significance

The result. The two identities are the coefficients of the corrected estimator (5): replacing $\Delta$ and $\Delta^2$ by $a\sigma\sqrt h$ and $b\sigma^2h$ turns the high–low estimator into an equation whose positive root $\hat\sigma_h$ largely removes the discretization bias. The same constants correct the Garman–Klass estimator (p. 509). Without exact values for $a$ and $b$ the correction has no concrete form.

Formalizing it. The paper does each of the four double integrals in a line and says "after some calculation" twice. A machine-checked derivation confirms the printed constants, which are reused in the high–low volatility literature. It also states precisely what is exact (moments of the model law (9) under independence) and what is approximation (that the model describes $\Delta$). To our knowledge none of these identities has been formalized before.

Difficulty

The statements are elementary but none of them is a one-line identity. Each moment is a double or triple improper integral with singular weights $(4hs^3)^{-1/2}$ on an unbounded domain. The minimum of $Z$ and $Z'$ couples two such integrals, and the resulting kernels $(s+u)^{-1/2}$ and $\sqrt{st}/(s+t)$ have to be integrated in closed form over the unit square. Matching $\sqrt2-1$ and $1-\pi/4$ exactly leaves no room for slack. In Lean, every exchange of integration order, change of variables and passage from survival functions to moments has to be justified for non-negative but unbounded functions, and the expectations must be shown finite: the Bochner integral of a non-integrable function is $0$.

Formalization scope

• Model. Random variables live on an arbitrary probability space (Ω, P) with [IsProbabilityMeasure P]. "Distribution (9)" is Measurable Z ∧ ∀ α ≥ 0, P.real {α < Z} = G σ h α, imposed only at levels $\alpha\ge0$: the formula is even in $\alpha$, and imposing it at negative levels would make the hypothesis unsatisfiable. Independence is IndepFun Z Z' P. $Z\vee Z'$ and $Z\wedge Z'$ are max and min.
• Parameters. $\sigma>0$ and $h>0$ only. The paper's $h=1/N\le1$ is not needed and not imposed.
• Explicit readings. "E" is the Bochner integral, and every expectation identity carries its integrability (Integrable, or MemLp … 2 for second moments). The conditioning "$\mid t-h<H_x<t,\ X_t=x$" in (9) and (10) is the modelling context in which the paper derives the law, not a hypothesis. The paper's "$E(Z\wedge Z')^2$" in (13) is read as $E[(Z\wedge Z')^2]$, as its first line shows. The integrals in (9) run over $(0,h]$ and $[h^{-1},\infty)$.
• Not formalized. The approximate statements $E\Delta\doteq a\sigma\sqrt h$ and $E\Delta^2\doteq b\sigma^2h$, the densities (6) and (7), and the independence remark of p. 508 are modelling approximations about the random walk, not theorems. The estimators (5) and $\hat\sigma^2_{GK,h}$ are definitions with no claim attached. The Brownian-bridge maximum (8) is not stated (its print also has a slip: $1-2/u$ for $1-s/u$). Section 4 (simulations) is out of scope.
• Non-triviality. The hypotheses are satisfiable for every $\sigma,h>0$: a probability measure on $\mathbb R$ with survival function $G_{\sigma,h}$ exists, and the two coordinates under its product measure are independent copies. A formalization that stated the survival condition for all $\alpha\in\mathbb R$ would be vacuous and is ruled out. So is one without the integrability conjuncts, which could hold with both sides $0$.
• Related items. The platform's generic identity survival_mean_ibp (mean as an integral of the survival function, under derivative hypotheses) is related but does not fit this setting. Mathlib's layer-cake formula is the general tool for passing between survival functions and moments.
• Welcome contributions. Closed forms for $\int_0^1\!\int_0^1(s+t)^{-1/2}\,ds\,dt$ and $\int_0^1\!\int_0^1\sqrt{st}/(s+t)\,ds\,dt$, which are reusable lemmas, and a general "moments of $\max$ and $\min$ of independent variables from their survival functions" lemma.

Selected references

• L. C. G. Rogers and S. E. Satchell, Estimating variance from high, low and closing prices, The Annals of Applied Probability 1(4) (1991), 504–512. https://doi.org/10.1214/aoap/1177005835
• M. B. Garman and M. J. Klass, On the estimation of security price volatilities from historical data, Journal of Business 53(1) (1980), 67–78. https://doi.org/10.1086/296072
• M. Parkinson, The extreme value method for estimating the variance of the rate of return, Journal of Business 53(1) (1980), 61–65. https://doi.org/10.1086/296071
• S. Beckers, Variances of security price returns based on high, low and closing prices, Journal of Business 56(1) (1983), 97–112.

Motivation

Concentration of measure on the symmetric group concerns random permutations. A uniformly random permutation of $N$ objects appears in random assignment problems, in sampling without replacement, in the longest increasing subsequence and in the analysis of randomized algorithms. A tail bound for a function of a random permutation is useful when it does not require computing the function's distribution. The symmetric group is not a product space, so the inequalities proved for product spaces do not apply to it directly.

Timeline. B. Maurey [Maurey 1979] gave the first concentration inequality on $S_N$, for distances that count the coordinates in which two permutations differ. Every permutation can be written uniquely as $\sigma=t_{N,i(N)}\circ\cdots\circ t_{2,i(2)}$ with $i(j)\le j$, where $t_{i,j}$ is the transposition of $i$ and $j$. Through this decomposition the Hamming bound (2.1.3) for product spaces carries over to $S_N$. Milman and Schechtman present the result in their monograph [Milman–Schechtman 1986]. In Chapter 5 of his 1995 memoir Talagrand 1995, M. Talagrand proves the analogue on $S_N$ of his convex hull inequality (Theorem 4.1.1 of the memoir). In the author's words, it improves Maurey's result in the way that Theorem 4.1.1 improves Proposition 2.1.1.

Setting

$S_N$ is the group of permutations of $\{1,\dots,N\}$ and $P_N$ is the uniform probability on it. Fix $A\subseteq S_N$ and $\sigma\in S_N$. A 0–1 vector $s$ is admissible if some $\tau\in A$ agrees with $\sigma$ at every coordinate where $s$ is zero:

$$U_A(\sigma)=\bigl\{s\in\{0,1\}^N:\ \exists\tau\in A,\ \forall\ell\le N,\ s_\ell=0\Rightarrow\tau(\ell)=\sigma(\ell)\bigr\}.$$

$V_A(\sigma)\subseteq[0,1]^N$ is the convex hull of $U_A(\sigma)$, and

$$f(A,\sigma)=\inf\Bigl\{\sum_{\ell\le N}s_\ell^2:\ s\in V_A(\sigma)\Bigr\}$$

is the squared convex distance from $\sigma$ to $A$. Unlike $f_c$ of Chapter 4, $f$ here is already squared. If $\sigma\in A$, then $0\in U_A(\sigma)$ and $f(A,\sigma)=0$. A permutation that agrees with some element of $A$ outside $k$ coordinates has $f(A,\sigma)\le k$.

The proof uses three variants. $f(A,\sigma,p)$ counts coordinate $p$ twice, $s_p^2+\sum_\ell s_\ell^2$. $f(A,\sigma,p,m)$, for $p\ne m$, restricts that infimum to the face $s_m=0$ (Eq. (5.5)). $g(A,\sigma,i,j)$ drops coordinates $i$ and $j$ (Eq. (5.6)). In $S_{N+1}$, $G_i=\{\sigma:\sigma(i)=N+1\}$ and $G'_i=\{\sigma:\sigma(N+1)=i\}$, with uniform probabilities $Q_i$ and $Q'_i$. $t_i$ is the transposition of $N+1$ and $i$. The maps $R(\rho)=\rho\circ t_i$ and $R'(\rho)=t_i\circ\rho$ send $G_i$ and $G'_i$, respectively, onto the permutations fixing $N+1$, that is, onto $S_N$.

Formalization targets

Goal: Theorem 5.1

For every $N$ and every $A\subseteq S_N$,

$$\int_{S_N}\exp\frac1{16}f(A,\sigma)\,dP_N(\sigma)\le\frac1{P_N(A)}.\tag{5.2}$$

The constant $1/16$ is the paper's.

Stronger: Proposition 5.2

For every $A\subseteq S_N$ and every $p\le N$,

$$\int\exp\tfrac1{16}f(A,\sigma,p)\,dP_N\le\tfrac1{P_N(A)}\quad(5.3)_N,\qquad\int\exp\tfrac1{16}f(A,\sigma,\sigma^{-1}(p))\,dP_N\le\tfrac1{P_N(A)}\quad(5.4)_N.$$

Since $f(A,\sigma)\le f(A,\sigma,p)$, this pair implies Theorem 5.1.

Milestones

The milestones are the numbered results of the induction step from $N$ to $N+1$, in the order of the paper:

• the deterministic inequalities Lemma 5.3 (5.7) and Lemma 5.7 (5.14);
• the transfer lemmas Lemma 5.4 (5.8) and Lemma 5.8 (5.15);
• the integral bounds Corollary 5.5 (5.10), Lemma 5.6 (5.11), Corollary 5.9 (5.16) and Lemma 5.10 (5.17).

Significance

The result. Theorem 5.1 has the same form as Theorem 4.1.1. By Markov's inequality, $P_N(A)\,P_N\{f(A,\cdot)\ge t\}\le e^{-t/16}$. Any function on $S_N$ that is controlled by the convex distance therefore concentrates around its median with Gaussian tails whose scale does not depend on $N$. Because the convex distance weighs coordinates by an arbitrary unit vector, this includes functions that are Lipschitz only in a weighted, configuration-dependent sense, which a Hamming-distance bound does not reach. This is the setting of random permutation problems such as the longest increasing subsequence and the assignment problem.

Formalizing it. The result has been proved since 1995. To the best of current knowledge none of Chapter 5 has a machine-checked proof, and the platform has no concentration statement on $S_N$. This mission formalizes the statements and the induction of the chapter. Its reusable output is the convex distance on $S_N$ and the embedding of $S_N$ into $S_{N+1}$ through the blocks $G_i$, $G'_i$.

Difficulty

$S_N$ sits inside $\{1,\dots,N\}^N$ through $\sigma\mapsto(\sigma(i))_{i\le N}$. If $S_N$ were the whole product, (5.2) would follow from Theorem 4.1.1. But $S_N$ is a very small subset of that product, and the uniform measure on $S_N$ is not a product measure. The decomposition into transpositions does give a product structure, but it is highly non-commutative. Coordinate distances in the decomposition do not match coordinate distances of the permutations, so it transfers only the weaker Hamming-type bound. The paper notes that a direct induction on $N$ for (5.2) itself apparently fails. The strengthened pair $(5.3)_N$, $(5.4)_N$ is needed, and its two halves cross: $(5.4)_{N+1}$ is proved from $(5.3)_N$, and $(5.3)_{N+1}$ from $(5.4)_N$.

Formalization scope

• $S_N$ is Equiv.Perm (Fin N), with indices from $0$. In $S_{N+1}$ the point $N+1$ is Fin.last N, and composition is the group product, so $\rho\circ t_i$ is ρ * t N i.
• $U_A(\sigma)\subseteq\mathbb R^N$, and $V_A(\sigma)$ is convexHull ℝ. The functionals $f$, $f(\cdot,\cdot,p)$, $f(\cdot,\cdot,p,m)$ and $g$ are infima of explicit sums of squares, so the sup norm on Fin N → ℝ plays no role. They take values in $[0,+\infty]$, so an empty infimum is $+\infty$ and $f(\emptyset,\sigma)=+\infty$. The integrand $\exp(z/16)$ is computed in EReal, so $\exp(+\infty)=+\infty$.
• The uniform probabilities $P_N$, $Q_i$ and $Q'_i$ are explicit finite averages over $S_N$, $G_i$ and $G'_i$. $Q_i(A)$ means $|A\cap G_i|/|G_i|$. $1/P_N(A)$ is computed in ℝ≥0∞, so $A=\emptyset$ gives $+\infty$ on both sides.
• $R(\sigma)$ and $R'(\sigma)$ enter through the relation Restricts ρ τ ($\rho(\ell)=\tau(\ell)$ for $\ell\le N$). $R(A_i)$ and $R'(A'_i)$ are the corresponding image sets.
• The integral bounds 5.5, 5.6, 5.9 and 5.10 are stated in the paper inside the induction step. Each carries the induction hypothesis it uses as an explicit binder: $(5.3)_N$, $(5.4)_N$, or "either" as a disjunction.
• A trivializing formalization is ruled out. The distance is the convex-hull distance with sums of squares, not a sup norm or Hamming count. The constant $1/16$ is kept, and the infimum over the empty set is $+\infty$, not a junk $0$.
• Lemma 4.1.3, the numerical inequality used in the Hölder step, belongs to mission V of this series and is not posed again here.

Contributions are welcome at every level: proofs of the deterministic lemmas, the bijections $G_i\to S_N$ and their measure-transport facts, and the final Hölder–Lemma 4.1.3 step.

Selected references

• M. Talagrand, Concentration of measure and isoperimetric inequalities in product spaces, Publ. Math. IHÉS 81 (1995), 73–205, Chapter 5, pp. 144–150. https://doi.org/10.1007/BF02699376
• B. Maurey, Construction de suites symétriques, C. R. Acad. Sci. Paris Sér. A 288 (1979), 679–681 (reference [M1] of the memoir; no DOI).
• V. D. Milman, G. Schechtman, Asymptotic theory of finite dimensional normed spaces, Lecture Notes in Math. 1200, Springer, 1986. https://doi.org/10.1007/978-3-540-38822-7

Motivation

Concentration of measure is the observation that, on a high-dimensional product probability space, any set that is not too small already contains most of the space within a small neighbourhood. For functions of many independent random variables this yields Gaussian-type tail bounds without any explicit computation of the distribution, and these bounds are the working tool behind the analysis of random combinatorial optimisation problems (bin packing, the travelling salesman problem, the longest increasing subsequence, the assignment problem), random graphs, and empirical processes.

M. Talagrand's 1995 memoir Talagrand 1995 develops a family of such inequalities that hold on an arbitrary product of probability spaces and are proved by induction on the number of coordinates. Chapter 2 opens with the simplest instance, control by one point: the distance from $x$ to a set $A$ is measured by the number of coordinates in which $x$ differs from the best single point $y \in A$. The method of this chapter is the template for every later chapter of the memoir.

Timeline. Bounds of the form (2.2.7) for the Hamming distance were first obtained with martingale (bounded differences) methods, collected in McDiarmid's survey McDiarmid 1989. Talagrand's 1995 memoir gives the induction proof reproduced here, with exponent $-\tfrac2N(k-\sqrt{\tfrac N2\log\tfrac1{P(A)}})^2$, which the paper notes is exactly the best bound obtained by martingales. Earlier, the isoperimetric inequality on the discrete cube (Harper, 1966) settles the case of the uniform measure on $\{0,1\}^N$.

Setting

Let $(\Omega,\Sigma,\mu)$ be a probability space and $N \ge 0$ an integer. Points of the product $\Omega^N$ are written $x=(x_1,\dots,x_N)$, and $P=\mu^N$ denotes the product probability. For a set $A \subseteq \Omega^N$ and a point $x$, the Hamming distance to $A$ is

$$f(A,x)=\min\big\{\operatorname{card}\{i\le N:\ x_i\ne y_i\}\ :\ y\in A\big\},$$

the least number of coordinates that must be changed to move $x$ into $A$; it is $+\infty$ when $A$ is empty. Given positive weights $(a_i)_{i\le N}$, the weighted Hamming distance replaces the count by $\sum\{a_i: x_i\neq y_i\}$.

Two families of constants appear. The first is

$$a(t)=\frac12+\frac{e^t+e^{-t}}4 ,$$

and the second, for $\alpha>0$ and $t>0$,

$$a(\alpha,t)=\frac{\alpha^{\alpha}}{(\alpha+1)^{\alpha+1}}\,\frac{(e^t-e^{-t/\alpha})^{1+\alpha}}{(1-e^{-t/\alpha})(e^t-1)^{\alpha}},$$

extended by its limit $a(\alpha,0)=1$; one checks $a(1,t)=a(t)$.

Formalization targets

Goal: Corollary 2.2.3

For every measurable $A\subseteq\Omega^N$, every $\alpha>0$ and every $t\ge0$,

$$\int e^{t f(A,x)}\,dP(x)\ \le\ \frac{1}{P(A)^{\alpha}}\exp\Big(N\frac{t^2}{8}\Big(1+\frac1\alpha\Big)\Big), \tag{2.2.6}$$

and, when $P(A)>0$, for every $k\ge\sqrt{\tfrac N2\log\tfrac1{P(A)}}$,

$$P\big(\{f(A,\cdot)\ge k\}\big)\ \le\ \exp\Big(-\frac2N\Big(k-\sqrt{\tfrac N2\log\tfrac1{P(A)}}\Big)^2\Big). \tag{2.2.7}$$

Milestones, in attack order

1. Lemma 2.1.2 — for measurable $0\le g\le1$ on $\Omega$: $\int\min(e^t,1/g)\,d\mu\int g\,d\mu\le a(t)$.
2. Proposition 2.1.1 — $\int e^{tf(A,x)}dP\le a(t)^N/P(A)\le e^{t^2N/4}/P(A)$ for $t>0$, and $P(f(A,\cdot)\ge k)\le e^{-k^2/N}/P(A)$.
3. Remark 2.1.3 — the same with the weighted Hamming distance and $\sum a_i^2$ in place of $N$.
4. Eq. (2.2.3) — $a(\alpha,t)=\sup_{0\le u\le1}(1+u(e^t-1))(1-u(1-e^{-t/\alpha}))^{\alpha}$.
5. Proposition 2.2.1 — $\int e^{tf(A,x)}dP\le a(\alpha,t)^N/P(A)^{\alpha}$ for $t\ge0$.
6. Lemma 2.2.2 — $a(\alpha,t)\le\exp\frac{t^2}8(1+\frac1\alpha)$.

The goal is the weakest statement of the section that is stated with fully explicit, closed-form constants; the milestones are the steps the paper's proof passes through.

Significance

The result. Inequality (2.2.7) shows that if $P(A)$ is bounded below, the set of points at Hamming distance at least $\sqrt{N/2\cdot\log(1/P(A))}+s$ from $A$ has probability at most $e^{-2s^2/N}$, with no assumption on $\Omega$ or $\mu$. Applied to $A=\{F\le M\}$ for a function $F$ that changes by at most one when a coordinate changes, it gives concentration of $F$ around its median at scale $\sqrt N$. The exponential moment bound (2.2.6) is the form that composes with other estimates, and the free parameter $\alpha$ is what makes the constant $2/N$ in (2.2.7) attainable rather than $1/N$ as in (2.1.3).

Formalizing it. The results are classical and fully proved in the paper; they are not available in Mathlib, and no machine-checked proof of them is known. A formalization supplies the one-coordinate inequalities (Lemma 2.1.2 and its $\alpha$-version) and the induction over $\Omega^{N+1}=\Omega^N\times\Omega$ as reusable components: every later chapter of the memoir (two-point space, penalties, $q$ points, convex hull distance) follows the same induction with a different one-coordinate lemma.

Difficulty

The bound does not follow from a union bound or from independence of coordinates, because $f(A,\cdot)$ depends on all coordinates jointly through an arbitrary set $A$: changing one coordinate of $x$ changes $f(A,x)$ by at most one, but which point of $A$ is nearest can change completely. A naive coordinate-by-coordinate estimate loses either the dependence on $P(A)$ or a constant factor in the exponent, and the constant $2/N$ in (2.2.7) is the sharp one, so no slack is available. The one-dimensional inequalities (Lemma 2.1.2 and its $\alpha$-version) are extremal problems over all measurable functions $0\le g\le1$ rather than over numbers, and Lemma 2.2.2 is a two-parameter inequality in which the closed form (2.2.2) is not convenient. On the measure-theoretic side, all integrands take values in $[0,\infty]$ and $f(A,\cdot)$ need not be measurable in general.

Formalization scope

• Space. $(\Omega,\Sigma,\mu)$ is an arbitrary measurable space with a probability measure; $\Omega^N$ is Fin N → Ω (0-based coordinates) and $P$ is Measure.pi (fun _ => μ). $\Omega$ is never restricted to a finite or countable set.
• Measurability. The paper ignores measurability and states Proposition 2.1.1 with an upper integral and outer probability. Here $A$ carries MeasurableSet A and the map $x\mapsto f(A,x)$ carries an explicit Measurable hypothesis; probabilities of arbitrary sets are Mathlib's outer measure.
• Values. Distances are in $[0,\infty]$ (ℝ≥0∞), so $f(\emptyset,x)=+\infty$; integrals are lower Lebesgue integrals ∫⁻ in $[0,\infty]$; $e^{tz}$ is EReal.exp; $P(A)^{-1}$ and $P(A)^{-\alpha}$ are computed in $[0,\infty]$, so $P(A)=0$ makes the right-hand sides $+\infty$.
• Constants. $a(\alpha,t)$ is formula (2.2.2) for $t\ne0$ and $1$ at $t=0$. Every constant ($1/4$, $1/8$, $2/N$) is the paper's.
• Ruled out. Defining $f$ through a real infimum (whose junk value on $\emptyset$ is $0$), or letting $a(\alpha,0)=0/0=0$, would make several statements false or trivial; neither is done.

Needed infrastructure: Fubini/Tonelli for Measure.pi split as $\Omega^N\times\Omega$, Chebyshev–Markov for ∫⁻, and one-variable calculus for (2.2.3)–(2.2.5). The one-coordinate lemmas and the induction scheme are reusable in the later missions of this series. Proofs of individual milestones and alternative proofs (for example via martingales for (2.2.7)) are welcome.

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
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics, LMS Lecture Note Ser. 141 (1989), 148–188. https://doi.org/10.1017/CBO9781107359949.008
• L. H. Harper, Optimal numberings and isoperimetric problems on graphs, J. Combin. Theory 1 (1966), 385–393. https://doi.org/10.1016/S0021-9800(66)80059-5