Theorem 4 — uniform convergence in probability iff H^S(l)/l → 0

Proved

VapnikChervonenkis.Entropy.theorem4_entropy_criterion

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

learning-theoryp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1probabilityvc-theory

Let $(X, P)$ be a probability space and $S$ a collection of measurable events. For an independent sample $x_1, \dots, x_l$ from $P$ let

\pi^{(l)} = \sup_{A \in S} \bigl|\nu_A^{(l)} - P_A\bigr|

be the largest deviation of a relative frequency from its probability, and let $H^S(l) = \mathbf{E} \log_2 \Delta^S(x_1, \dots, x_l)$ be the entropy of $S$ in samples of size $l$ . Assume, as the paper does, that $\pi^{(l)}$ , the semi-sample deviation $\rho^{(l)}$ and the index $\Delta^S$ are measurable functions of the sample. Then the relative frequencies converge in probability to the probabilities uniformly over $S$ , that is,

\lim_{l \to \infty} \mathbf{P}\{\pi^{(l)} > \varepsilon\} = 0 \quad\text{for every } \varepsilon > 0,

if and only if

\lim_{l \to \infty} \frac{H^S(l)}{l} = 0 . \tag{21}

Unlike the distribution-free sufficient condition through the growth function (Theorem 2), this criterion depends on $P$ and is both necessary and sufficient.

Formalization Note. Samples are functions Fin l → X with the product law Measure.pi; probabilities are values in $[0, \infty]$ . The four measurability hypotheses are the paper's standing assumptions: the events of $S$ are measurable (p. 264), $\pi^{(l)}$ is a random variable (p. 265), $\rho^{(l)}$ is measurable (p. 268), and the index is measurable (p. 273).

Preamble

import Mathlib
import Definitions.Def_VapnikChervonenkis_Shared_index
import Definitions.Def_VapnikChervonenkis_Shared_deviation
import Definitions.Def_VapnikChervonenkis_Entropy_entropy

open MeasureTheory Filter Topology

Formal statement

namespace VapnikChervonenkis.Entropy

/-- **Theorem 4** of Vapnik and Chervonenkis (1971), p. 275: a necessary and sufficient condition
for the relative frequencies to converge (in probability) to the probabilities uniformly over the
class of events `S`, i.e. `P{π^(l) > ε} → 0` for every `ε > 0` (p. 265), is that (21)
`lim_{l→∞} H^S(l)/l = 0`. `hS`, `hπ`, `hρ`, `hΔ` are the paper's standing assumptions: the events
of `S` are measurable (p. 264), and `π^(l)` (p. 265), `ρ^(l)` (p. 268) and the index `Δ^S`
(p. 273) are measurable functions of the sample. -/
theorem theorem4_entropy_criterion {X : Type*} [MeasurableSpace X] (P : Measure X)
    [IsProbabilityMeasure P] (S : Set (Set X)) (hS : ∀ A ∈ S, MeasurableSet A)
    (hπ : ∀ l, Measurable (Shared.maxDeviation S P l))
    (hρ : ∀ l, Measurable (Shared.semiSampleDeviation S l))
    (hΔ : ∀ l : ℕ, Measurable (fun x : Fin l → X => Shared.index S x)) :
    (∀ ε : ℝ, 0 < ε → Tendsto (fun l : ℕ => Measure.pi (fun _ : Fin l => P)
        {x | ε < Shared.maxDeviation S P l x}) atTop (𝓝 0))
      ↔ Tendsto (fun l : ℕ => entropy S P l / (l : ℝ)) atTop (𝓝 0) := by sorry

end VapnikChervonenkis.Entropy

Source

Vapnik and Chervonenkis, On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities, Theory Probab. Appl. 16 (1971), p. 275, Theorem 4, Eq. (21)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Fix a measurable space $X$ , a probability measure $P$ on $X$ , and a family $S$ of subsets of $X$ (a set of events). For each sample size $l \in \mathbb{N}$ , write $X^l$ for the set of $l$ -tuples $x = (x_1,\dots,x_l)$ of points of $X$ . Give $X^l$ its product σ-algebra and the product probability measure $P^{l} = P \otimes \cdots \otimes P$ ( $l$ copies).

The statement uses four objects from the accompanying definition files. Their definitions are not reproduced in the code shown here, so this read-back can only name them and give their types:

$\pi^{(l)}_{S,P} : X^l \to \mathbb{R}$ (Shared.maxDeviation S P l) is a real-valued function of a sample of size $l$ . It depends on $S$ , $P$ and $l$ .
$\rho^{(l)}_S$ (Shared.semiSampleDeviation S l) is a function that depends on $S$ and $l$ . Neither its domain nor its codomain is visible. It appears only in a hypothesis, never in the conclusion.
$\Delta^S(x)$ (Shared.index S x) is a quantity attached to $S$ and a finite sample $x \in X^l$ . Its codomain is not visible.
$H^S_P(l) \in \mathbb{R}$ (entropy S P l) is a real number that depends on $S$ , $P$ and $l$ .

Hypotheses. The theorem assumes all of the following:

Every $A \in S$ is a measurable subset of $X$ .
For every $l \in \mathbb{N}$ , the map $x \mapsto \pi^{(l)}_{S,P}(x)$ is measurable on $X^l$ .
For every $l \in \mathbb{N}$ , the map $\rho^{(l)}_S$ is measurable with respect to whatever σ-algebras its domain and codomain carry.
For every $l \in \mathbb{N}$ , the map $x \mapsto \Delta^S(x)$ is measurable on $X^l$ .

Hypotheses 2–4 are stated as assumptions and are not derived from 1. Whether they can be satisfied, for a given $S$ and $P$ , depends on the hidden definitions.

Conclusion. Under these hypotheses, the following two statements are equivalent (each implies the other):

(A) For every real $\varepsilon > 0$ ,

\lim_{l\to\infty} P^{l}\bigl(\{\, x \in X^l : \pi^{(l)}_{S,P}(x) > \varepsilon \,\}\bigr) = 0.

Here the probabilities are values of a measure, so they lie in $[0,\infty]$ , and the limit is taken in that space. The inequality is strict: $\pi^{(l)}_{S,P}(x) > \varepsilon$ .

(B) The real sequence $H^S_P(l)/l$ tends to $0$ :

\lim_{l\to\infty} \frac{H^S_P(l)}{l} = 0.

Only $\pi^{(l)}_{S,P}$ and $H^S_P(l)$ appear in the equivalence. $\rho^{(l)}_S$ and $\Delta^S$ enter only through the measurability hypotheses 3 and 4.

Degenerate cases.

$X$ empty: a probability measure on an empty space cannot exist, so the theorem says nothing about an empty $X$ .
$l = 0$ : $X^0$ has exactly one element, the empty tuple, and $P^{0}$ puts mass $1$ on it. The quotient in (B) is a division by zero, which is evaluated as $0$ by convention. Both conditions are limits as $l \to \infty$ , so neither $l = 0$ value affects them.
$S$ empty, or $X$ a single point (so $S \subseteq \{\varnothing, X\}$ ): what $\pi^{(l)}_{S,P}$ and $H^S_P(l)$ equal here is fixed entirely by the hidden definitions. For example, if they are defined as a supremum or a logarithm, an empty class could give conventional default values rather than meaningful ones. The theorem then asserts the equivalence of (A) and (B) for whatever those values are.
Vacuity: if some choice of $S$ and $P$ makes one of hypotheses 2–4 false, the theorem asserts nothing about that choice.

Human review

Endorsed by Shuze Chen · Sep 28, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 28, 2026
Confirmed by the mission captain (proposal self-audit).

View graph