Document Open Access Logo

Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality

Authors Floris van Doorn , Heather Macbeth

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.37.pdf
  • Filesize: 0.85 MB
  • 18 pages

Document Identifiers

Author Details

Floris van Doorn
  • Mathematical Institute, University of Bonn, Germany
Heather Macbeth
  • Department of Mathematics, Fordham University, New York, NY, USA

Acknowledgements

We thank Patrick Massot for useful comments on a draft of this article.

Cite AsGet BibTex

Floris van Doorn and Heather Macbeth. Integrals Within Integrals: A Formalization of the Gagliardo-Nirenberg-Sobolev Inequality. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 37:1-37:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.37

Abstract

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.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Continuous mathematics
  • Theory of computation → Logic and verification
Keywords
  • Sobolev inequality
  • measure theory
  • Lean
  • formalized mathematics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, and Micaela Mayero. A Coq formal proof of the Lax-Milgram theorem. In 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Paris, France, January 2017. URL: https://doi.org/10.1145/3018610.3018625.
  2. Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, and Houda Mouhcine. A Coq formalization of Lebesgue induction principle and Tonelli’s theorem. In 25th International Symposium on Formal Methods (FM 2023), volume 14000 of Lecture Notes in Computer Science, pages 39-55, Lübeck, Germany, March 2023. URL: https://doi.org/10.1007/978-3-031-27481-7_4.
  3. 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, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373824.
  4. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pages 378-388, Cham, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-21401-6_26.
  5. Elif Deniz, Adnan Rashid, Osman Hasan, and Sofiène Tahar. On the formalization of the heat conduction problem in HOL. In Intelligent Computer Mathematics: 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings, pages 21-37, Berlin, Heidelberg, 2022. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-16681-5_2.
  6. Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth. Formalized functional analysis with semilinear maps. Journal of Automated Reasoning, 237:10:1-10:19, 2022. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.10.
  7. Lawrence C. Evans. Partial differential equations, volume 19 of Grad. Stud. Math. Providence, RI: American Mathematical Society (AMS), 2nd ed. edition, 2010. Google Scholar
  8. David Gilbarg and Neil S. Trudinger. Elliptic partial differential equations of second order, volume 224 of Grundlehren Math. Wiss. Springer, Cham, 1977. URL: https://doi.org/10.1007/978-3-642-61798-0.
  9. Sébastien Gouëzel. A formalization of the change of variables formula for integrals in mathlib. In Kevin Buzzard and Temur Kutsia, editors, Intelligent Computer Mathematics - 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19-23, 2022, Proceedings, volume 13467 of Lecture Notes in Computer Science, pages 3-18. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-16681-5_1.
  10. John Harrison. Formalizing basic complex analysis. In R. Matuszewski and A. Zalewska, editors, From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, volume 10(23) of Studies in Logic, Grammar and Rhetoric, pages 151-165. University of Białystok, 2007. URL: http://mizar.org/trybulec65/.
  11. John Harrison. The HOL Light theory of Euclidean space. Journal of Automated Reasoning, 50(2):173-190, February 2013. URL: https://doi.org/10.1007/s10817-012-9250-9.
  12. Johannes Hölzl and Armin Heller. Three chapters of measure theory in Isabelle/HOL. In Interactive Theorem Proving, pages 135-151, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-22863-6_12.
  13. Yury Kudryashov. Formalizing the divergence theorem and the Cauchy integral formula in lean. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving (ITP 2022), volume 237 of Leibniz International Proceedings in Informatics (LIPIcs), pages 23:1-23:19, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2022.23.
  14. Shibo Liu. Gagliardo-Nirenberg-Sobolev inequality: An induction proof. The American Mathematical Monthly, 130(9):859-861, 2023. URL: https://doi.org/10.1080/00029890.2023.2240683.
  15. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings, pages 625-635, Berlin, Heidelberg, 2021. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  16. Keiko Narita, Noboru Endou, and Yasunari Shidama. The orthogonal projection and the Riesz representation theorem. Formaliz. Math., 23(3):243-252, 2015. URL: https://doi.org/10.1515/forma-2015-0020.
  17. L. Nirenberg. On elliptic partial differential equations. Annali della Scuola Normale Superiore di Pisa - Scienze Fisiche e Matematiche, Ser. 3, 13(2):115-162, 1959. URL: http://www.numdam.org/item/ASNSP_1959_3_13_2_115_0/.
  18. Mao-Pei Tsui. Partial differential equations I. Lecture notes for Math 6540, University of Toledo, 2008. URL: http://math.utoledo.edu/~mtsui/8540f08/hw/Sobolev-Inequality.pdf.
  19. Floris van Doorn. Formalized Haar measure. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 18:1-18:17, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.18.
  20. Théo Zimmermann and Hugo Herbelin. Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant. In Conference on Intelligent Computer Mathematics, Washington, D.C., United States, 2015. URL: https://hal.science/hal-01152588.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact