2026-08-25T09:00:28Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26982 2026-07-16T09:49:33Z ddc:004 open_access

Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley’s Entropy Integral Sonoda, Sho Kasaura, Kazumi Mizuno, Yuma Tsukamoto, Kei Onda, Naoto Lean generalization error bound Rademacher complexity McDiarmid’s inequality Hoeffding’s lemma symmetrization arguments chaining Dudley’s entropy integral 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 𝓁₂ and 𝓁₁ regularizations, and we also formalize a Dudley-type entropy integral bound based on covering numbers and a chaining construction. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sho Sonoda and Kazumi Kasaura and Yuma Mizuno and Kei Tsukamoto and Naoto Onda 2026 Is Part Of LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2026.8 urn:nbn:de:0030-drops-269824 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.8 eng https://creativecommons.org/licenses/by/4.0/legalcode