Motivation

In high-dimensional regression the number of candidate predictors $M$ can far exceed the number of observations $n$. A regression function can then be estimated only if it is well approximated by a combination of a few elements of a large dictionary. The Lasso is the most widely used estimator in this regime. The question this mission formalizes is how well the Lasso predicts when the truth is not assumed to be sparse, or even to lie in the span of the dictionary.

A sparsity oracle inequality answers it. It bounds the prediction error of the estimator by the error of the best sparse approximation of the truth, which only an oracle knowing the truth could compute, plus a remainder proportional to the sparsity of that approximation times $\log M/n$. Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 37(4), 2009) proved such an inequality for the Lasso under their restricted eigenvalue (RE) condition. Earlier oracle inequalities for Lasso-type estimators in fixed design (Bunea, Tsybakov and Wegkamp, 2006–2007) required the Gram matrix to be positive definite or to satisfy a mutual-coherence condition. The RE condition is weaker and allows $M\gg n$, and it is now the standard hypothesis in this literature.

Setting

A dictionary $f_1,\dots,f_M$ is evaluated at fixed points $Z_1,\dots,Z_n$. This gives the design matrix $X=(f_j(Z_i))\in\mathbb R^{n\times M}$ and, for an unknown regression function $f$, the vector $f=(f(Z_1),\dots,f(Z_n))^\top$. The observations are

$$y=f+W,\qquad W_1,\dots,W_n\ \text{independent}\ \mathcal N(0,\sigma^2),\ \sigma>0 .$$

Nothing is assumed about $f$. For $v\in\mathbb R^n$ the empirical norm is $\|v\|_n=(\frac1n\sum_iv_i^2)^{1/2}$, and for $\beta\in\mathbb R^M$ we write $f_\beta=X\beta$. The column norms $\|f_j\|_n$ are assumed nonzero, with $f_{\max}=\max_j\|f_j\|_n$ and $f_{\min}=\min_j\|f_j\|_n$. The support of $\beta$ is $J(\beta)=\{j:\beta_j\neq0\}$ and its sparsity is $\mathcal M(\beta)=|J(\beta)|$.

The Lasso $\hat\beta_L$ is any minimiser of

$$\frac1n\sum_{i=1}^n\big(y_i-(X\beta)_i\big)^2+2r\sum_{j=1}^M\|f_j\|_n|\beta_j|,\qquad r=A\sigma\sqrt{\frac{\log M}{n}},\ A>2\sqrt2,$$

and $\hat f_L=X\hat\beta_L$.

Assumption RE$(s,c_0)$ holds with constant $\kappa>0$ if, for every $J_0\subseteq\{1,\dots,M\}$ with $|J_0|\le s$ and every $\delta\neq0$ with $|\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1$,

$$\kappa\sqrt n\,|\delta_{J_0}|_2\le|X\delta|_2 .$$

The paper's $\kappa(s,c_0)$ is the largest such constant.

Formalization targets

Goal: Theorem 6.1

Fix $\varepsilon>0$, $n\ge1$, $M\ge2$, $1\le s\le M$, and let RE$(s,(3+4/\varepsilon)f_{\max}/f_{\min})$ hold with constant $\kappa$. With probability at least $1-M^{1-A^2/8}$, every Lasso solution satisfies, simultaneously for all $\beta$ with $\mathcal M(\beta)\le s$,

$$\|\hat f_L-f\|_n^2\le(1+\varepsilon)\Big\{\|f_\beta-f\|_n^2+C(\varepsilon)\frac{f_{\max}^2A^2\sigma^2}{\kappa^2}\,\frac{\mathcal M(\beta)\log M}{n}\Big\},\qquad C(\varepsilon)=\frac{4(2+\varepsilon)^2}{\varepsilon(1+\varepsilon)} .$$

Milestones

1. (B.4): the noise event $\mathcal A=\bigcap_j\{2|V_j|\le r\|f_j\|_n\}$, with $V_j=n^{-1}\sum_iX_{ij}W_i$, satisfies $P(\mathcal A^c)\le M^{1-A^2/8}$.
2. (B.1) on $\mathcal A$: for every Lasso solution and every $\beta$,

$$\|\hat f_L-f\|_n^2+r\sum_j\|f_j\|_n|\hat\beta_j-\beta_j|\le\|f_\beta-f\|_n^2+4r\sum_{j\in J(\beta)}\|f_j\|_n|\hat\beta_j-\beta_j| .$$

3. Lemma B.1: the same inequality with probability at least $1-M^{1-A^2/8}$.
4. Cone step: in the case $\varepsilon\|f_\beta-f\|_n^2<4r\sum_{J(\beta)}\|f_j\|_n|\hat\beta_j-\beta_j|$, the difference $\hat\beta_L-\beta$ lies in the cone with constant $(3+4/\varepsilon)f_{\max}/f_{\min}$ at $J(\beta)$.
5. Inequality before decoupling: $\|\hat f_L-f\|_n^2\le\|f_\beta-f\|_n^2+4rf_{\max}\kappa^{-1}\sqrt{\mathcal M(\beta)}\,(\|\hat f_L-f\|_n+\|f_\beta-f\|_n)$.
6. Decoupled bound: $\|\hat f_L-f\|_n^2\le\frac{b+1}{b-1}\|f_\beta-f\|_n^2+\frac{8b^2f_{\max}^2}{(b-1)\kappa^2}r^2\mathcal M(\beta)$ for all $b>1$.
7. Corollary 6.2: the same oracle inequality with $\gamma$ in place of $\kappa$ and no global RE assumption. The infimum runs over those $\beta$ with $\mathcal M(\beta)\le s$ whose support alone satisfies the restricted eigenvalue inequality with constant $\gamma$.

Significance

The theorem says that, up to the factor $1+\varepsilon$ and a remainder of order $\mathcal M(\beta)\log M/n$, the Lasso predicts as well as the best $s$-sparse linear combination of the dictionary. This is the case even when $f$ is not sparse and not in the span of the dictionary. The remainder is the parametric rate for $\mathcal M(\beta)$ parameters, inflated by $\log M$ and by the ill-posedness factor $f_{\max}^2/\kappa^2$. Together with Theorem 5.1 of the same paper (mission II of this series), it shows that the Lasso and the Dantzig selector are within the same distance of the sparse oracle. The oracle inequality is used in aggregation, in model selection, and as a black box in later sparse-estimation papers.

The result is proved in the paper. It has not been formalized: at the time of writing, no Lasso oracle inequality and no probabilistic Lasso bound exist on Prove2Me or in Mathlib. What this mission contributes is a machine-checked proof of the paper's Theorem 6.1 with an explicit constant $C(\varepsilon)$. The paper leaves $C(\varepsilon)$ unspecified, and its proof fixes the value used here. The mission also formalizes the Gaussian-tail step (B.4) and the deterministic basic inequality (B.1), both of which are shared with the paper's other Lasso results.

Difficulty

There is no sparse truth, so the usual argument does not apply. That argument places the error $\hat\beta_L-\beta^*$ in the RE cone and reads off a rate. Here the competitor $\beta$ is arbitrary, and the approximation error $\|f_\beta-f\|_n$ can dominate the penalty terms, in which case the error is not in the cone. The RE assumption can be used only where the error does lie in a cone, and the cone constant available there depends on $\varepsilon$ and on the column-norm ratio $f_{\max}/f_{\min}$, because the penalty is weighted while RE is stated for unweighted vectors. What RE then yields is an inequality quadratic in $\|\hat f_L-f\|_n$ with a cross term, not the $(1+\varepsilon)$ form directly, and the constant $C(\varepsilon)$ is determined by how that cross term is absorbed. On the probabilistic side, the whole argument must run on one event of probability at least $1-M^{1-A^2/8}$. That event may depend neither on $\beta$ nor on the choice of minimiser. The Lasso need not have a unique solution.

Formalization scope

• The dictionary enters only through $X\in\mathbb R^{n\times M}$ (Matrix (Fin n) (Fin M) ℝ) and the target only through $f\in\mathbb R^n$, which is arbitrary. The noise is a family W : Fin n → Ω → ℝ of measurable, independent random variables, each with law gaussianReal 0 σ², and $\sigma>0$.
• The Lasso is an argmin predicate, and every statement is made for every minimiser. "With probability at least $p$" means a measurable event $E$ with $P(E)\ge p$, chosen before the competitor $\beta$ and the minimiser.
• RE is stated through a witness $\kappa>0$. Since $\kappa(s,c_0)$ is attained and every bound decreases in $\kappa$, this is equivalent to the paper's form, and it avoids a real infimum over an empty set.
• The infimum over $\{\beta:\mathcal M(\beta)\le s\}$ is written as "for every such $\beta$". This is equivalent, because the set contains $\beta=0$ and the bracket is nonnegative.
• Correction/strengthening. The printed theorem has an unspecified $C(\varepsilon)>0$. The goal instead uses the value $C(\varepsilon)=4(2+\varepsilon)^2/(\varepsilon(1+\varepsilon))$ that the proof yields with $b=1+2/\varepsilon$, and this implies the printed statement. Corollary 6.2 uses the same explicit constant.
• The standing assumptions of Section 2 ($M\ge2$ and every $\|f_j\|_n\neq0$) are hypotheses of every theorem.
• Some formalizations would make the result trivial, and they are excluded here. The noise must be exactly i.i.d. $\mathcal N(0,\sigma^2)$ with $\sigma>0$ and must enter only through $y=f+W$. The target $f$ must not be restricted to $X\beta^*$. The event must be measurable. The constant must depend on $\varepsilon$ alone.
• A single definition file provides the empirical norms, $f_{\max}$, $f_{\min}$, support and sparsity, the weighted Lasso, RE and its single-set version (the family $\Lambda_{s,\gamma,c_0}$ of Corollary 6.2), the Gaussian noise model and the event $\mathcal A$. The same objects appear in the other missions of this series. Gaussian-tail and union-bound lemmas proved along the way are reusable, and contributions of such lemmas are welcome.

Selected references

• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. Cited version: arXiv:0801.1095v3; DOI 10.1214/08-AOS620.
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Sparsity oracle inequalities for the Lasso, Electron. J. Statist. 1, 169–194, 2007. DOI 10.1214/07-EJS008.
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Aggregation for Gaussian regression, Ann. Statist. 35(4), 1674–1697, 2007. DOI 10.1214/009053606000001587.
• R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Stat. Soc. B 58(1), 267–288, 1996. DOI 10.1111/j.2517-6161.1996.tb02080.x.

Motivation

Maximizing a submodular set function without constraints contains Max Cut, Max Directed Cut, maximum facility location and several graph and hypergraph cut problems as special cases, and it appears in operations research wherever a value exhibits diminishing returns but is not monotone (profit that combines coverage with a cost, for example). These problems are NP-hard, so the question is which fraction of the optimum an efficient algorithm can guarantee when the function is accessible only through a value oracle that returns $f(S)$ for a queried set $S$.

Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave the first constant-factor approximation algorithms for maximizing a general nonnegative submodular function. The simplest of them returns a uniformly random set and achieves $1/4$ of the optimum; this mission is about the next one, a nonadaptive algorithm: it decides all of its oracle queries before seeing any answer, then computes a set from the answers. Such an algorithm can be run in one round of parallel queries. The paper shows that this restricted access already beats $1/4$ and reaches $1/3$.

Timeline. For Max Directed Cut, a random cut achieves $1/4$. Feige, Mirrokni and Vondrák (FOCS 2007; journal version 2011) proved $1/4$ for a random set and $1/3$ nonadaptively for general nonnegative submodular functions, $1/3$ and $2/5$ by adaptive local search, and that $1/2$ requires exponentially many queries. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012, SIAM J. Comput. 2015) later reached the optimal $1/2$ with a randomized double-greedy algorithm.

Setting

Let $X$ be a finite ground set with $n = |X| \ge 1$ elements. A function $f : 2^X \to \mathbb{R}$ is submodular (Definition 1.1) if

$$f(S \cup T) + f(S \cap T) \le f(S) + f(T) \qquad \text{for all } S, T \subseteq X .$$

Throughout, $f$ is nonnegative, the paper's standing assumption, and $OPT = \max_{S \subseteq X} f(S)$.

For $p \in [0,1]$, $X(p)$ denotes the random subset of $X$ containing each element independently with probability $p$; $R = X(1/2)$ is a uniformly random subset. For a set $A \subseteq X$, $A(p)$ is the analogous random subset of $A$. The averaged marginal value of an element (Definition 2.4) is

$$\omega(x) = \mathbf{E}\big[f(R \cup \{x\}) - f(R \setminus \{x\})\big], \qquad R = X(1/2).$$

Algorithm NA (p. 1139):

1. by random sampling, compute estimates $\tilde\omega(x)$ with $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ for all $x$, with high probability;
2. independently, sample $R = X(1/2)$;
3. with probability $8/9$ return $R$;
4. with probability $1/9$ return $A = \{x \in X : \tilde\omega(x) > 0\}$.

Given the estimates, the expected value NA returns is $\tfrac89\,\mathbf{E}[f(X(1/2))] + \tfrac19 f(A)$.

Formalization targets

Goal: Theorem 2.6 in the explicit form of its proof

For every nonnegative submodular $f$ and every estimate $\tilde\omega$ with $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ for all $x$,

$$\frac89\,\mathbf{E}[f(X(1/2))] + \frac19\, f\big(\{x : \tilde\omega(x) > 0\}\big) \ \ge\ \Big(\frac13 - \frac{4}{9n}\Big)\, OPT .$$

The printed theorem says "at least $(1/3 - o(1))\,OPT$"; the term $4/(9n)$ is what the proof establishes (p. 1140, last display).

Milestones

1. Lemma 2.2: $\mathbf{E}[g(A(p))] \ge (1-p)\,g(\emptyset) + p\,g(A)$ for submodular $g$.
2. Lemma 2.3: $\mathbf{E}[f(A(p) \cup B(q))] \ge (1-p)(1-q) f(\emptyset) + p(1-q) f(A) + (1-p)q f(B) + pq f(A \cup B)$ for independently sampled, possibly overlapping $A, B$.
3. For $B = X \setminus A$ and any $C$: $f(A) + f(B \cap C) + f(B \cup C) \ge f(C)$.
4. If $\omega \le OPT/n^2$ on $B$: $\mathbf{E}[f(R \cup (B \cap C))] \le \mathbf{E}[f(R)] + OPT/(2n)$.
5. $\mathbf{E}[f(R \cup (B \cap C))] \ge \tfrac14 f(B \cap C) + \tfrac14 f(C)$.
6. If $\omega \ge -OPT/n^2$ on $A$ and $B = X \setminus A$: $\mathbf{E}[f(R)] \ge \mathbf{E}[f(R \cap (B \cup C))] - OPT/(2n)$.
7. $\mathbf{E}[f(R \cap (B \cup C))] \ge \tfrac14 f(C) + \tfrac14 f(B \cup C)$.

Milestones 3–7 are the displayed steps of the proof of Theorem 2.6, stated for arbitrary sets where the page's argument does not use the optimality of $C$.

Significance

The theorem shows that nonadaptive access, a fixed batch of polynomially many value queries followed by a computation, suffices for a $1/3$-approximation of unconstrained nonnegative submodular maximization, strictly better than the $1/4$ of any algorithm that must return one of its queried sets (the paper shows $1/4$ is optimal in that class, §4.2). The quantity $\omega$ generalizes the in-degree/out-degree test for Max Directed Cut to arbitrary submodular functions, and Lemmas 2.2 and 2.3 are general sampling inequalities for submodular functions that the paper reuses for its adaptive smooth local search.

Formalizing it produces machine-checked versions of Lemmas 2.2 and 2.3 as statements about exact finite averages, a reusable expectation operator on product-distributed random subsets, and a checked version of the $1/3$ argument with its explicit error term. The result is proved in the paper; to our knowledge none of it has been formalized in a proof assistant.

Difficulty

The two regimes the proof separates, "$A$ is already good" and "one of $f(B \cap C)$, $f(B \cup C)$ is large", must be tied to the value of a uniformly random set, whereas the elements of $A$ and $B$ are chosen from estimated averages, not from the optimal set $C$. The natural attempt, comparing $f(R)$ with $f(C)$ element by element, fails because $f$ is not monotone: adding elements of $C$ to $R$ can decrease the value. The accuracy $OPT/n^2$ of the estimates must also be propagated through a sum over up to $n$ elements, which is where the error term $4/(9n)$ comes from. The sampling lemmas require handling expectations over pairs of independent random subsets of possibly overlapping sets.

Formalization scope

• The ground set is a Fintype X with DecidableEq, assumed Nonempty, so $n = |X| \ge 1$ and the divisions by $n$ and $n^2$ are genuine; sets are Finset X; $f$ is real valued with nonnegativity $\forall S,\ 0 \le f(S)$ as an explicit hypothesis. Lemmas 2.2 and 2.3 are stated for real $f$ with no sign condition, as printed.
• $OPT$ is Finset.univ.sup' _ f, the true maximum over all subsets.
• Every expectation over an independently sampled random set is the exact finite sum $F(x) = \sum_{S} f(S)\prod_{i \in S} x_i \prod_{i \notin S}(1 - x_i)$; $X(1/2)$ is $x \equiv 1/2$. Expectations over two independent samples (Lemma 2.3) are the corresponding iterated sums. Sampling probabilities carry the hypotheses $0 \le p, q \le 1$.
• The goal quantifies over every estimate $\tilde\omega$ satisfying the printed accuracy $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ (strict), with $A = \{x : \tilde\omega(x) > 0\}$ (strict). The "with high probability" of NA's first step is this hypothesis; the sampling estimate that makes it likely (Lemma 2.5, a Chernoff-bound argument) is not part of the goal. When $OPT = 0$ the hypothesis is unsatisfiable, but then $f \equiv 0$ and nothing is lost.
• The left-hand side is exactly the mixture $\tfrac89\,\mathbf{E}[f(X(1/2))] + \tfrac19 f(A)$. A statement with the maximum of the two terms, with exact values $\tilde\omega = \omega$, or with the $o(1)$ replaced by an existential constant or a limit, is a different (and weaker or stronger) theorem and does not close this mission.
• Printed slip corrected: in the second display on p. 1140, the "$=$" before $-|A \setminus C|\,OPT/(2n^2)$ should be "$\ge$"; milestone 6 states the inequality.

Welcome contributions: proofs of Lemmas 2.2 and 2.3 (reusable for mission IV of this series), the identity $\mathbf{E}[f(R \cup \{x\}) - f(R)] = \tfrac12\omega(x)$, and general lemmas about the operator $F$ (splitting a uniform random set along a partition).

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205

Motivation

A maximal independent set (MIS) of a graph is a set of vertices, no two adjacent, to which no further vertex can be added. Sequentially an MIS is found greedily in linear time, but the greedy scan is inherently serial. Whether an MIS can be found fast in parallel was a central question of parallel complexity in the early 1980s: an MIS algorithm is a subroutine for maximal matching, vertex colouring with $\Delta + 1$ colours, and many other symmetry-breaking tasks.

• Karp and Wigderson (STOC 1984; J. ACM 32, 1985) gave the first fast parallel algorithms for MIS: a randomized one and a deterministic one, both with running time $O((\log n)^4)$, placing MIS in NC$^4$.
• Luby (SIAM J. Comput. 15(4), 1986) gave the Monte Carlo algorithms analysed in this mission, together with a derandomization that yields a deterministic EREW P-RAM algorithm with $O((\log n)^2)$ running time, placing MIS in NC$^2$. Alon, Babai and Itai (J. Algorithms 7, 1986) independently found a Monte Carlo algorithm similar to Algorithm B.

Luby's algorithm is the standard textbook example of a randomized parallel algorithm and remains the basis of distributed MIS algorithms in the LOCAL model. Its analysis rests on one statement, Theorem 1 of the paper, which this mission formalizes.

Setting

All algorithms in the paper run the same loop on a finite simple undirected input graph $G = (V, E)$ with $n = |V|$ vertices. The current graph is $G' = (V', E')$, initially $G$. For $W \subseteq V'$ the neighbourhood is $N(W) = \{ i \in V' : \exists j \in W,\ (i,j) \in E' \}$. One execution of the loop body selects a set $I' \subseteq V'$ independent in $G'$, adds it to the output, and replaces $G'$ by the subgraph induced on $V' - (I' \cup N(I'))$. The loop stops when $G'$ is empty.

For $i \in V'$ write $\mathrm{adj}(i)$ for its neighbours and $d(i) = |\mathrm{adj}(i)|$ for its degree. The two Monte Carlo select steps are:

• Algorithm A. Every vertex draws a priority $\pi(i)$ uniformly from $\{1, \dots, n^4\}$, independently. A vertex enters $I'$ when its priority is strictly smaller than the priority of each of its neighbours.
• Algorithm B. Every vertex independently sets $\mathrm{coin}(i) = 1$ with probability $1/(2d(i))$, or always if $d(i) = 0$. Let $X$ be the set of vertices with coin $1$. A vertex of $X$ enters $I'$ when each of its neighbours in $X$ has strictly smaller degree.

Let $Y_k$ be the number of edges of $E'$ before the $k$-th execution of the loop body. The number of edges eliminated by that execution is $Y_k - Y_{k+1}$: exactly the edges of $G'$ with at least one endpoint in $I' \cup N(I')$. For $d(i) \ge 1$ the paper uses the weight $\mathrm{sum}(i) = \sum_{j \in \mathrm{adj}(i)} 1/d(j)$.

Formalization targets

Goal: Theorem 1

For the current graph $G'$ and $n \ge \max(1, |V'|)$,

$$E\big[Y_k^A - Y_{k+1}^A\big] \ge \tfrac18\, Y_k^A - \tfrac1{16}, \qquad E\big[Y_k^B - Y_{k+1}^B\big] \ge \tfrac18\, Y_k^B .$$

The constants are those printed in the paper. No connectivity, degree or size condition on $G'$ is assumed.

Milestones

1. §3.2, p. 1040. The priorities of Algorithm A are pairwise distinct with probability at least $1 - 1/(2n^2)$.
2. TECHNICAL LEMMA, p. 1043. For $p_1 \ge \dots \ge p_n \ge 0$ and $c > 0$, with $\alpha_l = \sum_{j \le l} p_j$, $\beta_l = \sum_{j < k \le l} p_j p_k$ and $\gamma_l = \alpha_l - c\beta_l$,

$$\max_{1 \le l \le n} \gamma_l \ge \tfrac12 \min\{\alpha_n, 1/c\}.$$

3. LEMMA A (Beame), p. 1041. For Algorithm A and $d(i) \ge 1$,

$$\Pr[i \in N(I')] \ge \big[\tfrac14\min\{\mathrm{sum}(i), 1\}\big]\big(1 - \tfrac{1}{2n^2}\big).$$

4. LEMMA B, p. 1042. For Algorithm B and $d(i) \ge 1$,

$$\Pr[i \in N(I')] \ge \tfrac14 \min\{\mathrm{sum}(i)/2, 1\}.$$

5. Proof of Theorem 1, first display, p. 1041. For any random choice of $I'$,

$$E[Y_k - Y_{k+1}] \ge \tfrac12 \sum_i d(i)\Pr[i \in I' \cup N(I')] \ge \tfrac12 \sum_i d(i) \Pr[i \in N(I')].$$

6. Proof of Theorem 1, closing chain, p. 1041.

$$\tfrac12 \sum_{\mathrm{sum}(i) \le 2} d(i)\,\mathrm{sum}(i) + \sum_{\mathrm{sum}(i) > 2} d(i) \ge |E'|.$$

Significance

Theorem 1 says that each round removes, in expectation, a constant fraction of the remaining edges. From it the paper derives that the expected number of rounds of either algorithm is $O(\log n)$, and hence that MIS has a Monte Carlo algorithm running in $O(\log n)$ expected time on a CRCW P-RAM and $O((\log n)^2)$ on an EREW P-RAM with $O(m)$ processors. Algorithm B and the proof of part (2) are also the basis of the paper's deterministic algorithm: the analysis of Lemma B uses only pairwise independence of the coins. The companion mission (A Simple Parallel Algorithm for the Maximal Independent Set Problem II) formalizes that derandomization and reuses the statements of milestones 2, 5 and 6.

The results are proved in the paper and reproduced in textbooks (e.g. Motwani and Raghavan, Randomized Algorithms), but not formalized: no statement of Theorem 1, Lemma A or Lemma B was found on the platform. A formal proof would make the per-round analysis of a standard parallel randomized algorithm reusable. That includes the degree-weighted counting of milestone 6 and the Bonferroni-type bound of the Technical Lemma, both of which recur in later analyses of distributed symmetry breaking.

Difficulty

The obvious argument tries to show that a fixed vertex enters $I'$ with good probability. That fails, because a high-degree vertex rarely wins against all its neighbours. The analysis instead bounds the probability that a vertex is removed, i.e. lands in $N(I')$. This event is a union over neighbours of dependent events, so the first Bonferroni inequality alone does not give a lower bound: the pairwise-intersection terms must be controlled. The union bound can also be very lossy when $\mathrm{sum}(i)$ is large, which is why the conclusion involves a minimum with a constant.

A second obstacle is the passage from vertices to edges: vertices of small $\mathrm{sum}(i)$ can have high degree while contributing little probability. The per-vertex bounds therefore have to be summed with degree weights and redistributed over edges. For Algorithm A there is an additional complication: priorities from $\{1, \dots, n^4\}$ can collide, so the argument about a uniformly random order holds only on the event that $\pi$ is injective. That event appears as the factor $1 - 1/(2n^2)$.

Formalization scope

• Graph. The current graph $G'$ is a SimpleGraph V on a finite type with decidable adjacency, and $V' = V$. The degree is SimpleGraph.degree, $\mathrm{adj}(i)$ is neighborFinset, and $Y_k = |E'|$ is edgeFinset.card.
• Conditional form. Theorem 1 is stated for a fixed current graph $G'$, i.e. conditionally on the first $k - 1$ rounds, as in the paper's proof. The unconditional statement follows by averaging.
• Input size. $n$ is a parameter with $1 \le n$ and $|V'| \le n$. It is not fixed to $|V'|$, which would cover only the first round.
• Select steps. Both endpoints' ALGEDGE runs are applied to every edge, since $E'$ contains each edge in both orientations. Hence Algorithm A keeps $i$ iff $\pi(i) < \pi(j)$ for all neighbours $j$. Algorithm B keeps $i \in X$ iff $d(j) < d(i)$ for all neighbours $j \in X$. Algorithm B's $I'$ starts at $X$; the page leaves $I'$ uninitialized in §3.3, and Algorithm D's code (p. 1047) has $I' \leftarrow X$.
• Laws. Probabilities and expectations are explicit finite sums: uniform over the $(n^4)^{|V|}$ priority vectors, and the product law over the $2^{|V|}$ coin vectors. A coin of an isolated vertex is $1$ with probability $1$, as on the page.
• Milestones. Milestone 5 is stated for an arbitrary finite distribution of $I'$, which contains both algorithms' laws. Milestone 6 divides out the common factor $\tfrac18$ of the printed chain.

Theorem 1 is false for arbitrary distributions of priorities or coins. A formalization that takes "Pr" as an unconstrained parameter, conditions on the event of interest, or replaces $n$ by $|V'|$ does not state the paper's theorem.

A complete development needs finite product probability spaces, inclusion–exclusion (Bonferroni) inequalities for finite unions, the symmetry of uniform priorities conditioned on injectivity, and degree-sum identities (SimpleGraph.sum_degrees_eq_twice_card_edges). The Technical Lemma and milestones 5 and 6 are reusable beyond this mission. Proofs of any milestone, and alternative proofs of Lemmas A and B, are welcome.

Selected references

• M. Luby, A Simple Parallel Algorithm for the Maximal Independent Set Problem, SIAM J. Comput. 15(4):1036–1053, 1986. https://doi.org/10.1137/0215074
• R. M. Karp and A. Wigderson, A Fast Parallel Algorithm for the Maximal Independent Set Problem, J. ACM 32(4):762–773, 1985. https://doi.org/10.1145/4221.4226
• N. Alon, L. Babai and A. Itai, A Fast and Simple Randomized Parallel Algorithm for the Maximal Independent Set Problem, J. Algorithms 7(4):567–583, 1986. https://doi.org/10.1016/0196-6774(86)90019-2
• R. Motwani and P. Raghavan, Randomized Algorithms, Cambridge University Press, 1995. https://doi.org/10.1017/CBO9780511814075

Motivation

Many combinatorial optimization problems ask for a subset of a finite ground set that maximizes a set function with diminishing returns: Max Cut and Max Directed Cut in graphs, facility location, maximum entropy sampling, and welfare problems in combinatorial auctions all fit this pattern. The common abstraction is the maximization of a submodular function, the discrete analogue of a concave function. Unlike the monotone case, where the objective only grows as elements are added, the non-monotone problem has no constraint at all and is still NP-hard, since Max Cut is a special case.

For Max Cut and Max Directed Cut, the simplest algorithm there is, putting every vertex on a side by an independent fair coin, already cuts half, respectively a quarter, of the optimum in expectation. Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011; extended abstract at FOCS 2007) showed that this is not a feature of cut functions: the same random choice achieves the same factors for every nonnegative submodular function, and for every symmetric one. This mission formalizes that result, Theorem 2.1 of the paper, together with the two sampling lemmas on which it rests. The paper's other results (a nonadaptive 1/3-approximation, deterministic and smoothed local search, and query lower bounds) are the subjects of companion missions in the same series.

Setting

Let $X$ be a finite set with $n = |X|$ elements. A set function assigns a real number $f(S)$ to every subset $S \subseteq X$. It is submodular if

$$f(S \cup T) + f(S \cap T) \le f(S) + f(T) \qquad \text{for all } S, T \subseteq X,$$

equivalently if the marginal value $f(B \cup \{x\}) - f(B)$ of an element $x$ does not increase as the set $B$ grows. It is symmetric if $f(X \setminus S) = f(S)$ for every $S \subseteq X$; the cut function of an undirected graph is the standard example. The optimum is

$$OPT = \max_{S \subseteq X} f(S).$$

For $p \in [0,1]$, $X(p)$ denotes the random subset of $X$ containing each element independently with probability $p$; similarly $A(p)$ is the random subset of a fixed $A \subseteq X$. The Random Set Algorithm (RS) returns $R = X(1/2)$, a uniformly random subset of $X$, without querying $f$. Its expected value is the average of $f$ over all subsets,

$$\mathbf{E}[f(R)] = F(\tfrac12, \dots, \tfrac12) = \frac{1}{2^n} \sum_{S \subseteq X} f(S),$$

where $F(x) = \sum_{S \subseteq X} f(S) \prod_{i \in S} x_i \prod_{i \notin S} (1 - x_i)$ is the multilinear extension of $f$, the expectation of $f$ on a random set that includes element $i$ independently with probability $x_i$.

Formalization targets

Goal: Theorem 2.1

For every nonnegative submodular $f : 2^X \to \mathbb{R}_+$,

$$\mathbf{E}[f(X(1/2))] \ge \tfrac14\, OPT,$$

and if $f$ is in addition symmetric,

$$\mathbf{E}[f(X(1/2))] \ge \tfrac12\, OPT.$$

Both parts form the goal, stated as one theorem. The constants $\tfrac14$ and $\tfrac12$ are exact, not asymptotic, and they are tight: the directed cut of a single arc attains $\tfrac14$, and the cut of a single edge attains $\tfrac12$.

Milestones

1. Lemma 2.2. For submodular $g : 2^X \to \mathbb{R}$, $A \subseteq X$ and $p \in [0,1]$,

$$\mathbf{E}[g(A(p))] \ge (1-p)\, g(\emptyset) + p\, g(A).$$

2. Lemma 2.3. For submodular $f : 2^X \to \mathbb{R}$, sets $A, B \subseteq X$ that need not be disjoint, independent samples $A(p)$, $B(q)$, and $p, q \in [0,1]$,

$$\mathbf{E}[f(A(p) \cup B(q))] \ge (1-p)(1-q) f(\emptyset) + p(1-q) f(A) + (1-p)q f(B) + pq f(A \cup B).$$

3. The display in the proof of Theorem 2.1. For submodular $f : 2^X \to \mathbb{R}$ and every $S \subseteq X$, with $\bar S = X \setminus S$,

$$\mathbf{E}[f(X(1/2))] \ge \tfrac14 f(\emptyset) + \tfrac14 f(S) + \tfrac14 f(\bar S) + \tfrac14 f(X).$$

The milestones need no sign on the function; nonnegativity enters only in the goal.

Significance

The result. Theorem 2.1 gives an algorithm that makes no query at all and is still a constant-factor approximation for unconstrained non-monotone submodular maximization. It sets the baseline that every later algorithm for the problem is measured against: the paper's own nonadaptive $\tfrac13$-algorithm and its local search algorithms with factors $\tfrac13$ and $\tfrac25$, followed by later work culminating in the tight $\tfrac12$-approximation of Buchbinder, Feldman, Naor and Schwartz (FOCS 2012). The paper also shows that $\tfrac14$ is optimal among nonadaptive algorithms required to return one of the queried sets, and that $\tfrac12$ is optimal for symmetric functions among all algorithms using polynomially many value queries, so both factors of Theorem 2.1 have a precise place in the complexity landscape. Lemma 2.3, the probabilistic inequality behind it, is reused in the analyses of the nonadaptive algorithm and of smooth local search.

Formalizing it. The result is proved, with a short proof. What this mission adds is a machine-checked version of the random-set guarantee and of the two sampling lemmas, stated for arbitrary finite ground sets and, for the lemmas, for real-valued submodular functions without a sign. To our knowledge none of these statements has a machine-checked proof; Mathlib has no theory of submodular set functions or of their multilinear extension.

Difficulty

The goal itself is a two-line consequence of the third milestone. The work sits in the lemmas and in one change of viewpoint.

Lemma 2.2 is not a pointwise statement: the random set $A(p)$ can be any subset of $A$, and $g$ can be smaller on it than both $g(\emptyset)$ and $g(A)$. The inequality holds only in expectation, and only because submodularity controls the marginal value of each element uniformly across the sets it can be added to. Lemma 2.3 needs a conditioning argument over two independent samples; the sets $A$ and $B$ may overlap, and on $A \cap B$ the union $A(p) \cup B(q)$ contains an element with probability $1 - (1-p)(1-q)$, so it is not the product distribution with probability $p$ on $A$ and $q$ on $B$. Finally, the third milestone requires identifying the uniform random subset $X(1/2)$ with the union of independent half-samples of $S$ and of its complement, as a statement about finite sums.

The obvious attempt at the goal, comparing $f(R)$ with $f(S^*)$ for an optimal $S^*$ set by set, fails: $f$ is not monotone, so a random set that contains most of $S^*$ may still have small value, and a random set can pick up elements that hurt.

Formalization scope

The ground set is a Lean type X with [Fintype X] [DecidableEq X]; subsets are Finset X and set functions are f : Finset X → ℝ. Submodularity is the lattice inequality of Definition 1.1, not the decreasing-marginals property. Nonnegativity, the paper's standing assumption $f : 2^X \to \mathbb{R}_+$, is the hypothesis ∀ S, 0 ≤ f S; it appears only in the goal. Symmetry is ∀ S, f Sᶜ = f S for all subsets, not only for an optimal one. $OPT$ is Finset.univ.sup' Finset.univ_nonempty f, a maximum over the always nonempty family of all subsets, so it is attained. The ground set may be empty; the goal holds there too and no nonemptiness is assumed.

Expectations are written as exact finite sums, not as integrals. $\mathbf{E}[f(X(1/2))]$ is the multilinear extension F f (fun _ => 1/2). $\mathbf{E}[g(A(p))]$ is $\sum_{T \subseteq A} p^{|T|}(1-p)^{|A \setminus T|} g(T)$, and $\mathbf{E}[f(A(p) \cup B(q))]$ is the double sum over independent samples $S \subseteq A$, $T \subseteq B$ with the product of the two weights. The ranges $0 \le p \le 1$ and $0 \le q \le 1$, implied in the paper by the word "probability", are explicit hypotheses; Lemma 2.2 is false without them.

Trivializing formalizations are excluded: the weights are exactly those of the uniform distribution on all $2^n$ subsets, $OPT$ is the true maximum rather than the value at one fixed set, and $f$ is required to be both nonnegative and submodular.

Reusable infrastructure produced by a complete development: the multilinear extension of a set function and its expression as an expectation, product-weight identities for independent sampling of subsets (including the decomposition of $X(1/2)$ along a set and its complement), and Lemmas 2.2 and 2.3, which the companion missions on the nonadaptive algorithm and on smooth local search also need. Proofs of any milestone are welcome independently.

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM Journal on Computing 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing non-monotone submodular functions, Proceedings of the 48th IEEE Symposium on Foundations of Computer Science (FOCS), 2007, pp. 461–471. https://doi.org/10.1109/FOCS.2007.29
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM Journal on Computing 44(5):1384–1402, 2015 (FOCS 2012). https://doi.org/10.1137/130929205
• G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An analysis of approximations for maximizing submodular set functions — I, Mathematical Programming 14:265–294, 1978. https://doi.org/10.1007/BF01588971

Free Energy Principle II: expected free energy, Markov blankets, Gaussian variational free energy, and Bayesian model reduction

Motivation

Mission Free Energy Principle I published the core variational step of the free energy principle (FEP): whatever recognition density a system carries, the posterior-form variational free energy never undercuts the data's surprisal, the bound is exact at the Bayesian posterior, and equality characterizes the posterior. That mission's shared finite substrate — normalized finite laws, finite kernels, entropy/cross-entropy/KL, and the finite generative model — now exists as platform definitions in the namespace FreeEnergyPrinciple.

The Free Energy Principle II mission formalizes the four structures the FEP literature builds on top of that core, all already machine-checked in the source repository fep_lean / fep_formal (Active Inference Institute):

• Expected free energy — the policy-selection functional of active inference: what a course of action is expected to cost in preference divergence and what it is expected to reveal. Its canonical decomposition [Friston et al. 2017] splits $G$ into risk (pragmatic divergence of predicted outcomes from preferences) plus ambiguity (expected entropy of outcomes given latent states), with epistemic value fixing the sign.
• Markov blankets — the partition that makes a self-organizing system statable: internal states are conditionally independent of external states given the sensory-active blanket. The source development proves this at the level of Mathlib's native conditional distributions, not as a finite mutual-information proxy.
• Gaussian variational free energy — the closed-form instantiation of the FEP-I bound for the exact scalar Gaussian filter, where the native Gaussian KL is exactly the squared mean error over twice the posterior variance.
• Bayesian model reduction — model comparison by Bayes factors: posterior odds equal prior odds times the likelihood ratio, the multiplicative update applied whenever a reduced model is compared against the model it was reduced from [Friston & Penny 2011].

Timeline of the mathematical content this mission formalizes:

• 2006/2010 — Friston's free energy principle: variational free energy as the quantity a self-organizing system minimizes (formalized in FEP-I).
• 2011 — Friston & Penny, Post hoc Bayesian model selection: Bayesian model reduction — evidence of reduced models evaluated by the free-energy difference; comparison by Bayes factors.
• 2015 — Friston, Rigoli, Sengupta, Pezzulo — the Markov-blanket partition (sensory/active states) as the geometry of the FEP.
• 2017 — Friston, FitzGerald, Rigoli, Schwartenbeck, Pezzulo, Active inference: a process theory: expected free energy $G(\pi) = \text{risk} + \text{ambiguity}$ drives policy selection.
• 2022 — Parr, Pezzulo, Friston, Active Inference (MIT Press): Gaussian treatments of filtering and the posterior-form free energy as the working equations.
• 2026 — fep_formal (Active Inference Institute): a machine-checked Lean 4 catalogue of 155 FEP topics compiled with zero proof holes against a pinned Mathlib. This mission transcribes the proved modules behind expected free energy, native Markov blankets, the scalar Gaussian filter/VFE, and Bayesian model reduction onto the platform.

Setting

Two carriers, both fully machine-checked in the source repository:

• Finite (reusing FEP-I's published substrate). Laws are normalized real mass functions on finite types; kernels are normalized rows. This mission's expected-free-energy, model-reduction, and Markov-blanket families import the published Definitions.Def_fep_finite_laws, Def_fep_finite_information, and Def_fep_generative_model — no substrate is re-published. Zero-mass atoms are handled by the same totalized conventions as FEP-I: entropy uses Real.negMulLog (so $0\log 0 = 0$ exactly), KL is the nonnegative klFun integrand, and division premises are explicit.
• Native Gaussian (self-contained on Mathlib). The Gaussian family is Mathlib's own gaussianReal/gaussianPDF at a fixed strictly positive variance; the scalar OU prediction and the closed filter update give the posterior mean/variance the recognition family varies over. The native KL between two family members is exactly $\frac{(\mu_1-\mu_2)^2}{2v}$ — proved against Mathlib's log-likelihood-ratio definition.

The four definition items of this mission package exactly these carriers:

• Def_fep2_expected_free_energy — the predicted state-outcome joint, preference risk, likelihood ambiguity, epistemic value, pragmatic cost, expected free energy (epistemic sign fixed by definition), the full-support contract, and the marginal/product/conditional-entropy/mutual-information lemmas the decomposition needs. Imports FEP-I.
• Def_fep2_gaussian_vfe — fixed-variance Gaussian family with its exact KL, scalar OU parameters, the exact scalar Gaussian filter (prediction, observation kernel, gain, closed posterior, evidence law), evidence surprisal, and the posterior-form Gaussian variational free energy. Self-contained.
• Def_fep2_bayesian_model_reduction — posterior odds, Bayes factor, and the model-odds update $odds \leftarrow odds \times Z_f/Z_r$, with totalized division boundaries kept explicit. Imports FEP-I.
• Def_fep2_native_blanket — the static blanket factorization, the Dirac-mass embedding of finite laws into native measures, blanket/internal/external coordinates, the conditional-pair kernel, and the marginal/composition identifications the independence proof needs. Imports FEP-I.

Formalization targets

Goal: expected free energy decomposes into risk plus ambiguity

For every finite generative model, every policy $\pi$, and every model with full support:

$$G[\pi] \;=\; \mathrm{KL}\big(P(o\mid\pi)\,\|\,C\big) \;+\; \sum_s P(s\mid\pi)\,H\big(A[\cdot\mid s]\big).$$

The epistemic-value sign is fixed by definition ($G[\pi] =$ pragmatic cost $-$ epistemic value); the decomposition follows from two entropy identities: epistemic value $I(s;o\mid\pi)$ is predicted outcome entropy minus ambiguity, and risk is cross-entropy minus the same entropy (Gibbs' inequality under full reference support). Nonnegativity of $G$ follows as a corollary — but the decomposition, not the bound, is the target.

Gaussian variational free energy in closed form

For the exact scalar Gaussian filter, the posterior-form variational free energy at recognition mean $\mu$ is

$$F[\mu] = \frac{(\mu - m^*)^2}{2v^*} + S(o),$$

the exact fixed-variance Gaussian KL (the recognition-to-posterior gap) plus the density-relative evidence surprisal. Equality with the surprisal holds exactly at the posterior mean — the Gaussian analogue of FEP-I's exactness theorem.

Odds recursion of Bayesian model reduction

Bayes' rule in odds form: at positive evidence,

$$\frac{P(h_f\mid e)}{P(h_r\mid e)} = \frac{P(h_f)}{P(h_r)}\cdot\frac{P(e\mid h_f)}{P(e\mid h_r)},$$

with the reference prior mass and reference likelihood as exact division premises. The multiplicative Bayes-factor structure (topic fep-120: factorized evidence ratios multiply; sequential model-odds updates agree with one update by product evidence) is available from the same definition layer as a further target.

Native Markov blanket conditional independence

The embedded static blanket factorization satisfies Mathlib's native CondIndepFun predicate: internal coordinates are conditionally independent of external coordinates given the blanket coordinate. The result is obtained by identifying the authored finite conditional kernels with Mathlib conditional distributions (the embedding preserves marginals and joints exactly on discrete carriers) — not by a finite mutual-information argument.

Significance

These four results are the load-bearing extensions of FEP-I's bound: expected free energy converts the variational principle into a theory of action selection; Markov blankets make "internal states" and "external states" well-defined relative to a blanket, which is what lets the FEP talk about self-organizing systems at all; the Gaussian filter is the tractable regime in which the variational machinery becomes the Kalman update; and Bayesian model reduction is the learning/comparison step that updates structure, not just parameters.

Formalizing them. All four families are proved with zero proof holes in the source repository, against a pinned Mathlib; the definition layer here is faithful (same carriers, same totalized conventions, same support contracts made explicit) and every item below compiles locally against the platform environment. The mission's value is reusable community infrastructure: the definition items publish the EFE layer, the Gaussian filter, the odds layer, and the native-blanket embedding in the shared namespace FreeEnergyPrinciple, so later missions (policy trees, collective inference, predictive coding) can import them instead of re-deriving. Status honesty: all eight items below are formalized and machine-checked locally against the platform environment; each is an open problem on the platform only in the sense that no proof has yet been submitted to it.

Difficulty

• The EFE decomposition looks like an algebraic rearrangement but the sign conventions are load-bearing: the epistemic value enters $G$ with a minus sign, and the two helper identities (epistemic value = outcome entropy $-$ ambiguity; risk = cross-entropy $-$ outcome entropy) both hold only under the full-support contract, which the definition makes explicit rather than hiding in a carrier.
• The Gaussian identity requires the exact native KL between Gaussian laws — the proof goes through Mathlib's log-likelihood-ratio definition and the Gaussian first moment — and the closed-form update's positivity (positive prediction variance, positive innovation variance) is what makes the recognition family genuine rather than degenerate.
• The odds recursion is a field-simp identity, but the premises are the point: a plausible rendering that hides division by zero behind totalized division changes the statement.
• The blanket theorem is the most intricate item: it must transport a finite factorization through the Dirac-mass embedding into Mathlib's conditional-distribution machinery, with nonemptiness premises for the conditional distributions to exist. A "proof" via finite mutual information would prove something weaker than the source.

Formalization scope

Committed conventions of this mission's Lean development:

• The expected-free-energy and model-reduction families reuse the published Free Energy Principle I finite substrate (namespace FreeEnergyPrinciple, definitions Def_fep_finite_laws, Def_fep_finite_information, Def_fep_generative_model); this mission adds definition items Def_fep2_expected_free_energy, Def_fep2_gaussian_vfe, Def_fep2_bayesian_model_reduction, and Def_fep2_native_blanket, all in the same namespace.
• The Gaussian family is deliberately native: Mathlib gaussianReal/gaussianPDF, no finite substrate, no manifold geometry, no singular (zero-variance) branch.
• Totalized real division boundaries (zero evidence, zero reference mass) are stated, never silently absorbed.
• The natural-gradient / dynamic-flow layer of the source's Gaussian module (natural gradient flow, strict descent away from the posterior) is deliberately left out of this mission and is a natural extension target; likewise the row-wise dynamical blanket theorem (every authored factorized transition row preserves the native blanket conditional independence), which follows directly from the static theorem via the source's nextStaticModel construction.
• Contributions welcome: the epistemic/pragmatic ENNReal balance (catalogue topic fep-021) onto this substrate, the treewise EFE decomposition (fep-133), Bayes-factor multiplicativity (fep-120), and blanket nonvacuity witnesses.

Selected references

• K. Friston, A free energy principle for the brain, Journal of Physiology (Paris) 100 (2006) 70–87. https://doi.org/10.1016/j.jphysparis.2006.10.001
• K. Friston, The free-energy principle: a unified brain theory?, Nature Reviews Neuroscience 11 (2010) 127–138. https://doi.org/10.1038/nrn2787
• K. Friston & W. Penny, Post hoc Bayesian model selection, NeuroImage 56 (2011) 2089–2099. https://doi.org/10.1016/j.neuroimage.2011.03.062
• K. Friston, T. FitzGerald, F. Rigoli, P. Schwartenbeck, G. Pezzulo, Active inference: a process theory, Neural Computation 29 (2017) 1–49. https://doi.org/10.1162/neco_a_00912
• T. Parr, G. Pezzulo, K. J. Friston, Active Inference: The Free Energy Principle in Mind, Brain, and Behavior, MIT Press (2022). https://mitpress.mit.edu/9780262045354/active-inference/
• D. A. Friedman, fep_formal: Towards Lean 4 Formalization of the Free Energy Principle (v1.2.0), Active Inference Institute (2026), the formal source of truth for this mission. https://github.com/ActiveInferenceInstitute/fep_formal
• D. A. Friedman, Towards Lean 4 Formalization of the Free Energy Principle: AI-Driven Theorem Sketching and Verification for Active Inference and Bayesian Mechanics, Active Inference Journal (2026). https://doi.org/10.5281/zenodo.19699233

Motivation

Chapter 26 bounded the rate of uniform convergence by the Rademacher complexity; Chapter 27 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), introduces a second, metric measure of the size of a set of vectors, its covering numbers $N(r, A)$, the smallest number of Euclidean balls of radius $r$ needed to cover $A$, and connects the two through Dudley's chaining. Covering numbers behave well under scaling and under coordinatewise Lipschitz maps (Lemmas 27.2–27.3), they are easily bounded for sets lying in a low-dimensional subspace (Example 27.1), and the chaining lemma turns a bound on $\log N(r, A)$ at all scales $r = c2^{-k}$ into a bound on $R(A)$ (Lemma 27.4), with the clean corollary $R(A) \le \frac{6c}{m}(\alpha + 2\beta)$ when $\sqrt{\log N(c2^{-k}, A)} \le \alpha + \beta k$ (Lemma 27.5). The chapter's example recovers $R(A) = O(c\sqrt{d\log d}/m)$ for sets in a $d$-dimensional subspace, the technique that the book says would sharpen the fundamental theorem's sample complexity from $d\log(d/\epsilon)/\epsilon^2$ to $d/\epsilon^2$.

Setting

For $A \subseteq \mathbb{R}^m$ with the Euclidean metric, $A'$ is an $r$-cover of $A$ if every $a \in A$ is within distance $r$ of some $a' \in A'$, and $N(r, A)$ is the cardinality of the smallest $r$-cover (Definition 27.1). The Rademacher complexity $R(A) = \frac1m\mathbb{E}_\sigma\sup_{a \in A}\langle\sigma, a\rangle$ is Mission XX's. Chaining is run at the scales $c2^{-k}$, $k = 1, \dots, M$, where $c$ is a radius of a ball containing $A$, the book's $c = \min_{\bar a}\max_{a \in A}\|a - \bar a\|$ being the smallest such radius.

Formalization targets

Goal: Lemma 27.4

For a nonempty $A \subseteq \mathbb{R}^m$, $m \ge 1$, contained in the ball of radius $c$ about some $\bar a$, and every integer $M > 0$,

$$R(A) \le \frac{c\,2^{-M}}{\sqrt m} + \frac{6c}{m}\sum_{k=1}^M 2^{-k}\sqrt{\log N(c\,2^{-k}, A)}.$$

Milestones

Example 27.1 (the grid $r$-cover of a set of norm at most $c$ in a $d$-dimensional subspace, of size $(2c\sqrt d/r + 1)^d$); Lemma 27.2 (scaling and translation); Lemma 27.3 (the contraction principle); Lemma 27.5 (the corollary of chaining). Further item: Example 27.2 ($R(A) = O(c\sqrt{d\log d}/m)$ for sets in a $d$-dimensional subspace).

Significance

Chaining is the standard way to get sharp uniform convergence rates: a single-scale union bound (Massart's lemma at one resolution) loses a logarithmic factor, and summing Massart bounds over a geometric sequence of scales, applied to the increments between successive nearest cover points, recovers it. Lemma 27.4 is the discrete Dudley integral, and Lemma 27.5 is the form in which it is used: any polynomial-in-$1/r$ covering number gives $R(A) = O(c\sqrt{\log N}/m)$-type bounds without the extra logarithm. On the platform these items complete the complexity toolbox begun in Mission XX and provide covering numbers as a reusable notion; the contraction and scaling lemmas mirror their Rademacher counterparts.

Difficulty

Lemmas 27.2 and 27.3 are immediate: the image of an $r$-cover under the affine map is an $rc$-cover, and under a coordinatewise $\rho$-Lipschitz map a $\rho r$-cover, since $\|\varphi(a) - \varphi(a')\|^2 = \sum_i(\varphi_i(a_i) - \varphi_i(a'_i))^2 \le \rho^2\|a - a'\|^2$; formally they are manipulations of the infimum in $\mathbb{N} \cup \{\infty\}$. Example 27.1 needs an orthonormal basis of the subspace (Gram–Schmidt, or Mathlib's orthonormal bases of finite-dimensional inner product subspaces of $\mathbb{R}^m$ with the Euclidean structure) and the rounding of coordinates to a grid. Lemma 27.4 is the real work: after centering, take minimal $c2^{-k}$-covers $B_k$, the near-maximizer $a^*$ of $\langle\sigma, a\rangle$ (which depends on $\sigma$), its nearest points $b^{(k)} \in B_k$, the telescoping $a^* = (a^* - b^{(M)}) + \sum_k(b^{(k)} - b^{(k-1)})$, the bound $\|b^{(k)} - b^{(k-1)}\| \le 3c2^{-k}$, and Massart's lemma (Mission XX) on the sets $\hat B_k$ of increments, of cardinality at most $N(c2^{-k}, A)^2$; a formal proof must handle the supremum not being attained (approximate maximizers) and the dependence of all choices on $\sigma$ inside the finite average. Lemma 27.5 lets $M \to \infty$ using $\sum_k 2^{-k} = 1$ and $\sum_k k2^{-k} = 2$. Example 27.2 combines Example 27.1 at the scales $c2^{-k}$ with Lemma 27.5, with the book's constant $\log(2\sqrt d)$. The book's derivation uses the count without $+1$, so a proof needs the volumetric covering bound $(1 + 2c/r)^d$ for $d \ge 2$ and a direct count for $d = 1$.

Formalization scope

Vectors are Fin m → ℝ with an explicit Euclidean norm, because Mathlib's norm on that type is the sup norm; covers are arbitrary finsets of $\mathbb{R}^m$ and $N(r, A)$ is an infimum in $\mathbb{N} \cup \{\infty\}$, so no junk value arises when no finite cover exists, and the chaining statements read $N$ through ENat.toNat for the bounded sets they concern, where it is finite. Subspaces are Mathlib Submodules with finrank = d. Two statements are given with the constants their proofs support, and the item texts say so. Example 27.1's grid has $2c/\epsilon + 1$ points per coordinate, so the cover has size $(2c\sqrt d/r + 1)^d$, not $(2c\sqrt d/r)^d$, which is less than $1$ for $r > 2c\sqrt d$ and cannot bound a covering number of a nonempty set; Example 27.2 correspondingly has $\log(4\sqrt d)$ in place of $\log(2\sqrt d)$. Lemma 27.4 is stated for any enclosing radius $c$ about any center, since the proof only uses that $\{\bar a\}$ is a $c$-cover of $A$; the book's minimal radius is the special case, and this is the form Example 27.2 needs (with $\bar a = 0$ and $c = \max\|a\|$). Lemma 27.5 keeps the book's $\alpha, \beta > 0$.

Not stated: nothing else is in the chapter beyond the bibliographic remarks.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 27. doi:10.1017/CBO9781107298019
• R. M. Dudley, Universal Donsker classes and metric entropy, Annals of Probability 15(4), 1987. doi:10.1214/aop/1176991978
• M. Anthony, P. L. Bartlett, Neural Network Learning: Theoretical Foundations, Cambridge University Press, 1999. doi:10.1017/CBO9780511624216
• M. Talagrand, Upper and Lower Bounds for Stochastic Processes, Springer, 2014. doi:10.1007/978-3-642-54075-2
• R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018. doi:10.1017/9781108231596