Search Results

Documents authored by Sonoda, Sho

Artifact
Software
DOI: 10.4230/artifacts.27120
auto-res/lean-rademacher

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

Abstract
Cite as

Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda. auto-res/lean-rademacher (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-27120,
   title = {{auto-res/lean-rademacher}}, 
   author = {Sonoda, Sho and Kasaura, Kazumi and Mizuno, Yuma and Tsukamoto, Kei and Onda, Naoto},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:06614ca069f4562b630fca2903e3b286a426e317;origin=https://github.com/auto-res/lean-rademacher;visit=swh:1:snp:d3bc817a59894cb2cbb2258c50aee2a4e7f63d3e;anchor=swh:1:rev:f34ab4f0a9029682f1af3179a3fe9b5e114e511f}{\texttt{swh:1:dir:06614ca069f4562b630fca2903e3b286a426e317}} (visited on 2026-07-16)},
   url = {https://github.com/auto-res/lean-rademacher/tree/f34ab4f0a9029682f1af3179a3fe9b5e114e511f},
   doi = {10.4230/artifacts.27120},
}
Document
DOI: 10.4230/LIPIcs.ITP.2026.8
Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley’s Entropy Integral

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

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{sonoda_et_al:LIPIcs.ITP.2026.8,
  author =	{Sonoda, Sho and Kasaura, Kazumi and Mizuno, Yuma and Tsukamoto, Kei and Onda, Naoto},
  title =	{{Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley’s Entropy Integral}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{8:1--8:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.8},
  URN =		{urn:nbn:de:0030-drops-269824},
  doi =		{10.4230/LIPIcs.ITP.2026.8},
  annote =	{Keywords: Lean, generalization error bound, Rademacher complexity, McDiarmid’s inequality, Hoeffding’s lemma, symmetrization arguments, chaining, Dudley’s entropy integral}
}
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