Lean formalization of generalization error bound by Rademacher complexity and Dudley’s entropy integral
Loading...
Files
Published Version
Date
2026-07-16
Authors
Sonoda, Sho
Kasaura, Kazumi
Mizuno, Yuma
Tsukamoto, Kei
Onda, Naoto
Journal Title
Journal ISSN
Volume Title
Publisher
Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Published Version
Abstract
Understanding and certifying the generalization performance of machine learning algorithms - i.e. obtaining theoretical estimates of the test error from the training error - is a central theme of statistical learning theory. Among the many complexity measures used to derive such guarantees, Rademacher complexity yields sharp, data-dependent bounds that apply well beyond classical VC-dimension theory. In this study, we formalize the generalization error bound by Rademacher complexity in Lean 4, building on measure-theoretic probability theory available in the Mathlib library. Our development provides a mechanically-checked pipeline from the definitions of empirical and expected Rademacher complexity, through a formal symmetrization argument and a bounded-differences analysis, to high-probability uniform deviation bounds via a formally proved McDiarmid inequality. A key technical contribution is a reusable mechanism for lifting results from countable hypothesis classes (where measurability of suprema is straightforward in Mathlib) to separable topological index sets via a reduction to a countable dense subset. As worked applications of the abstract theorem, we mechanize standard empirical Rademacher bounds for linear predictors under ℓ2 and ℓ1 regularizations, and we also formalize a Dudley-type entropy integral bound based on covering numbers and a chaining construction.
Description
© 2026, Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, and Naoto Onda. Licensed under Creative Commons License CC-BY 4.0
Keywords
Chaining , Dudley’s entropy integral , Generalization error bound , Hoeffding’s lemma , Lean , McDiarmid’s inequality , Rademacher complexity , Symmetrization arguments , [Maths] , Software
Citation
Sonoda, S, Kasaura, K, Mizuno, Y, Tsukamoto, K & Onda, N 2026, Lean formalization of generalization error bound by Rademacher complexity and Dudley’s entropy integral. in E Komendantskaya, E Komendantskaya & T Nipkow (eds), 17th International Conference on Interactive Theorem Proving, ITP 2026., 8, Leibniz International Proceedings in Informatics, LIPIcs, vol. 382, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 1-17, 17th International Conference on Interactive Theorem Proving, ITP 2026, Lisbon, Portugal, 26/07/26. https://doi.org/10.4230/LIPIcs.ITP.2026.8
conference
conference
Link to publisher’s version
Collections
Copyright
cc_by