zetesis-puremath

A collection of pure-mathematics results I have needed in my formalization projects (the formal-learning-theory-kernel, SMFE, and others) that are absent from Mathlib or specialized in a way Mathlib's current formulation does not support directly. Every declaration is proved in Lean 4. Zero sorry. Only the standard Lean kernel axioms appear in the axiom closure.

Navigate

What is in here

• Analytic sets are NullMeasurableSet under finite Borel measures on Polish spaces; Kechris 30.13 (capacitability for analytic sets).
• ℝ-valued metric total variation distance with nonempty/bounded set-lemmas.
• Binary KL with full derivative/monotonicity chain; Pinsker's inequality with the sharp constant; ℝ-valued mutual information with zero-iff-product.
• Chebyshev-via-majority concentration bound; FintypePMF with linarith-compatible arithmetic and a bridge to Mathlib.PMF.
• Multiplicative-weights-update (MWU) approximate minimax with T = O(log N / ε²).
• Kernel mean embedding of a measure into an RKHS; Maximum Mean Discrepancy and IsCharacteristic; Hilbert-Schmidt Independence Criterion.
• Assouad's dual VC bound VCdim(Mᵀ) ≤ 2^(d+1) − 1 for binary matrices.