We introduce an abstraction which allows arguments involving iterated integrals to be formalized conveniently in type-theory-based proof assistants. We call this abstraction the marginal construction, since it is connected to the marginal distribution in probability theory. The marginal construction gracefully handles permutations to the order of integration (Tonelli’s theorem in several variables), as well as arguments involving an induction over dimension. We implement the marginal construction and several applications in the language Lean. The most difficult of these applications, the Gagliardo-Nirenberg-Sobolev inequality, is a foundational result in the theory of elliptic partial differential equations and has not previously been formalized.
@InProceedings{vandoorn_et_al:LIPIcs.ITP.2024.37, author = {van Doorn, Floris and Macbeth, Heather}, title = {{Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {37:1--37:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.37}, URN = {urn:nbn:de:0030-drops-207657}, doi = {10.4230/LIPIcs.ITP.2024.37}, annote = {Keywords: Sobolev inequality, measure theory, Lean, formalized mathematics} }
Feedback for Dagstuhl Publishing