Document Open Access Logo

Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley’s Entropy Integral

Authors Sho Sonoda , Kazumi Kasaura , Yuma Mizuno , Kei Tsukamoto , Naoto Onda

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.8.pdf
  • Filesize: 0.87 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Sample complexity and generalization bounds
  • Theory of computation → Logic and verification
Keywords
  • Lean
  • generalization error bound
  • Rademacher complexity
  • McDiarmid’s inequality
  • Hoeffding’s lemma
  • symmetrization arguments
  • chaining
  • Dudley’s entropy integral

Metrics

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 𝓁₂ and 𝓁₁ regularizations, and we also formalize a Dudley-type entropy integral bound based on covering numbers and a chaining construction.

Cite As Get BibTex

Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, and Naoto Onda. Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley’s Entropy Integral. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.8

Author Details

Sho Sonoda
  • RIKEN AIP, Tokyo, Japan
  • CyberAgent Inc., Tokyo, Japan
Kazumi Kasaura
  • OMRON SINIC X Corporation, Tokyo, Japan
Yuma Mizuno
  • University College Cork, Ireland
Kei Tsukamoto
  • The University of Tokyo, Japan
Naoto Onda
  • OMRON SINIC X Corporation, Tokyo, Japan

Funding

This work was supported by JSPS KAKENHI 24K21316, and JST Moonshot R&D Program JPMJMS2236, PRESTO JPMJPR2125, BOOST JPMJBY24E2, and CREST JPMJCR25I5.

Acknowledgements

We thank the reviewers for useful feedback on our manuscript.

Supplementary Materials

References

  1. Reynald Affeldt, Alessandro Bruni, Yves Bertot, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Pierre Roux, Kazuhiko Sakaguchi, Zachary Stone, Pierre-Yves Strub, and Laurent Théry. Mathcomp-analysis: Analysis library compatible with mathematical components, 2025. URL: https://github.com/math-comp/analysis.
  2. Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, and Takafumi Saikawa. Formalizing concentration inequalities in Rocq: Infrastructure and automation. In Yannick Forster and Chantal Keller, editors, 16th International Conference on Interactive Theorem Proving (ITP 2025), volume 352, pages 21:1-21:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.ITP.2025.21.
  3. Francis Bach. Learning Theory from First Principles. MIT Press, 2024. URL: https://mitpress.mit.edu/9780262049443/learning-theory-from-first-principles/.
  4. Alexander Bagnall and Gordon Stewart. Certifying the True Error: Machine Learning in Coq with Verified Generalization Guarantees. Proceedings of the AAAI Conference on Artificial Intelligence, 33(01):2662-2669, 2019. URL: https://doi.org/10.1609/AAAI.V33I01.33012662.
  5. Peter L Bartlett and Shahar Mendelson. Rademacher and Gaussian Complexities: Risk Bounds and Structural Results. Journal of Machine Learning Research, 3:463-482, 2002. URL: http://www.jmlr.org/papers/volume3/bartlett02a/bartlett02a.pdf.
  6. Alexander Bentkamp. Expressiveness of deep learning. Archive of Formal Proofs, 2016. URL: https://isa-afp.org/entries/Deep_Learning.html.
  7. Alexander Bentkamp, Jasmin Christian Blanchette, and Dietrich Klakow. A formal proof of the expressiveness of deep learning. Journal of Automated Reasoning, 63(2):347-368, 2019. URL: https://doi.org/10.1007/s10817-018-9481-5.
  8. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In International Conference on Automated Deduction, CADE 28, pages 625-635. Springer International Publishing, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  9. R M Dudley. The sizes of compact subsets of hilbert space and continuity of gaussian processes. Journal of Functional Analysis, 1:290-330, 1967. URL: https://doi.org/10.1016/0022-1236(67)90017-1.
  10. Manuel Eberl. The laws of large numbers. Archive of Formal Proofs, February 2021. URL: https://isa-afp.org/entries/Laws_of_Large_Numbers.html.
  11. Michikazu Hirata. No-free-lunch theorem for machine learning. Archive of Formal Proofs, 2025. URL: https://isa-afp.org/entries/No_Free_Lunch_ML.html.
  12. Emin Karayel and Yong Kiam Tan. Concentration Inequalities. Archive of Formal Proofs, 2023. URL: https://www.isa-afp.org/entries/Concentration_Inequalities.html.
  13. Martin J. Wainwright. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. URL: https://doi.org/10.1017/9781108627771.
  14. Mehryar Mohri, Afshin Rostamizadeh, and Ameet Talwalkar. Foundations of Machine Learning. Adaptive Computation and Machine Learning series. MIT Press, second edition, 2018. URL: https://mitpress.mit.edu/9780262039406/foundations-of-machine-learning/.
  15. Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, and Naoto Onda. auto-res/lean-rademacher. Software, (visited on 2026-07-13). URL: https://github.com/auto-res/lean-rademacher/tree/f34ab4f0a9029682f1af3179a3fe9b5e114e511f
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.27120
  16. Joseph Tassarotti and Robert Harper. Verified tail bounds for randomized programs. In Jeremy Avigad and Assia Mahboubi, editors, Interactive Theorem Proving (ITP2018), pages 560-578. Springer International Publishing, 2018. URL: https://doi.org/10.1007/978-3-319-94821-8_33.
  17. Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, and Jean-Baptiste Tristan. A Formal Proof of PAC Learnability for Decision Stumps. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, pages 5-17. Association for Computing Machinery, 2021. URL: https://doi.org/10.1145/3437992.3439917.
  18. Matus Telgarsky. Deep learning theory lecture notes, 2021. URL: https://mjt.cs.illinois.edu/dlt/.
  19. The mathlib community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 367-381, 2020. URL: http://doi.org/10.1145/3372885.3373824.
  20. Koundinya Vajjha, Avraham Shinnar, Barry Trager, Vasily Pestun, and Nathan Fulton. CertRL: formalizing convergence proofs for value and policy iteration in Coq. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, pages 18-31. Association for Computing Machinery, 2021. URL: https://doi.org/10.1145/3437992.3439927.
  21. Koundinya Vajjha, Barry Trager, Avraham Shinnar, and Vasily Pestun. Formalization of a Stochastic Approximation Theorem. In 13th International Conference on Interactive Theorem Proving, ITP 2022, volume 237 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.31.
  22. L. G. Valiant. A theory of the learnable. Communications of the ACM, 27(11):1134-1142, 1984. URL: https://doi.org/10.1145/1968.1972.
  23. Vladimir N Vapnik and A. Ya Chervonenkis. On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities. Theory of Probability and Its Applications, 16(2):264-280, 1971. URL: http://doi.org/10.1137/1116025.
  24. Yuanhe Zhang, Jason D Lee, and Fanghui Liu. Statistical learning theory in lean 4: Empirical processes from scratch. arXiv preprint: 2602.02285, 2026. URL: https://doi.org/10.48550/arXiv.2602.02285.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact