1.1 What is formalized here

Six substrates, each with its own chapter below:

• Measure theory on Polish spaces. Analytic sets are null-measurable under finite Borel measures; Kechris 30.13 capacitability theorem for analytic sets; real-valued metric total variation distance.

• Information theory. Real-valued Kullback-Leibler bridge to Mathlib’s ENNReal-valued klDiv; binary KL with a full derivative / monotonicity chain; Pinsker’s inequality with the sharp constant; mutual information and its zero-iff-product characterization.

• Probability. BoundedRandomVariable typeclass with a Chebyshev-via-majority bound; double-sample / ValidSplit / SplitMeasure exchangeability infrastructure; FintypePMF (an \(\mathbb {R}\)-valued, linarith- compatible specialization of Mathlib’s PMF).

• Decision theory. Covering-based minimax; multiplicative-weights-update (MWU) in the Freund-Schapire \(\beta = (1-\eta )\) convention; approximate-minimax bound \(T = \mathcal{O}(\log N / \varepsilon ^2)\).

• Reproducing-kernel Hilbert spaces. Kernel mean embedding with the reproducing property; Maximum Mean Discrepancy (MMD) and characteristic kernels; Hilbert-Schmidt Independence Criterion (HSIC).

• Combinatorics. Assouad’s 1983 dual VC bound \(\mathrm{VCdim}(M^\top ) \le 2^{d+1} - 1\).