Lean formalization of generalization error bound by Rademacher complexity and Dudley’s entropy integral

Simple item page
dc.contributor.authorSonoda, Sho
dc.contributor.authorKasaura, Kazumi
dc.contributor.authorMizuno, Yuma
dc.contributor.authorTsukamoto, Kei
dc.contributor.authorOnda, Naoto
dc.contributor.editorKomendantskaya, Ekaterina
dc.contributor.editorKomendantskaya, Ekaterina
dc.contributor.editorNipkow, Tobias
dc.date.accessioned2026-09-07T14:48:01Z
dc.date.available2026-09-07T14:48:01Z
dc.date.issued2026-07-16
dc.description© 2026, Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, and Naoto Onda. Licensed under Creative Commons License CC-BY 4.0
dc.description.abstractUnderstanding 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.en
dc.format.extent17
dc.format.extent920716
dc.identifier.authororcidSonoda, Sho
dc.identifier.authororcidKasaura, Kazumi
dc.identifier.authororcidMizuno, Yuma
dc.identifier.authororcidTsukamoto, Kei
dc.identifier.authororcidOnda, Naoto
dc.identifier.authororcidKomendantskaya, Ekaterina
dc.identifier.authororcidKomendantskaya, Ekaterina
dc.identifier.authororcidNipkow, Tobias
dc.identifier.citationSonoda, 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
dc.identifier.citationconference
dc.identifier.doi10.4230/LIPIcs.ITP.2026.8
dc.identifier.endpage17
dc.identifier.isbn9783959774369
dc.identifier.issn1868-8969
dc.identifier.journaltitle17th International Conference on Interactive Theorem Proving, ITP 2026
dc.identifier.journaltitle17th International Conference on Interactive Theorem Proving, ITP 2026
dc.identifier.startpage1
dc.identifier.urihttps://hdl.handle.net/10468/19181
dc.identifier.urlhttps://www.scopus.com/pages/publications/105045843790
dc.language.isoeng
dc.publisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
dc.relation.ispartofseriesLeibniz International Proceedings in Informatics, LIPIcs
dc.rightscc_by
dc.subjectChaining
dc.subjectDudley’s entropy integral
dc.subjectGeneralization error bound
dc.subjectHoeffding’s lemma
dc.subjectLean
dc.subjectMcDiarmid’s inequality
dc.subjectRademacher complexity
dc.subjectSymmetrization arguments
dc.subject[Maths]
dc.subjectSoftware
dc.titleLean formalization of generalization error bound by Rademacher complexity and Dudley’s entropy integralen
dc.typeConference contribution (Peer reviewed)
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
LIPIcs.ITP.2026.8.pdf
Size:
899.14 KB
Format:
Adobe Portable Document Format
Description:
Published Version
Download
Collections
School of Mathematical Sciences