DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2024.37

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

Authors: Floris van Doorn and Heather Macbeth

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

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.

Cite as

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)

Copy BibTex To Clipboard

@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}
}

Document

DOI: 10.4230/LIPIcs.ITP.2022.10

Formalized functional analysis with semilinear maps

Authors: Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth

Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)

Abstract

Semilinear maps are a generalization of linear maps between vector spaces where we allow the scalar action to be twisted by a ring homomorphism such as complex conjugation. In particular, this generalization unifies the concepts of linear and conjugate-linear maps. We implement this generalization in Lean’s mathlib library, along with a number of important results in functional analysis which previously were impossible to formalize properly. Specifically, we prove the Fréchet-Riesz representation theorem and the spectral theorem for compact self-adjoint operators generically over real and complex Hilbert spaces. We also show that semilinear maps have applications beyond functional analysis by formalizing the one-dimensional case of a theorem of Dieudonné and Manin that classifies the isocrystals over an algebraically closed field with positive characteristic.

Cite as

Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth. Formalized functional analysis with semilinear maps. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dupuis_et_al:LIPIcs.ITP.2022.10,
  author =	{Dupuis, Fr\'{e}d\'{e}ric and Lewis, Robert Y. and Macbeth, Heather},
  title =	{{Formalized functional analysis with semilinear maps}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.10},
  URN =		{urn:nbn:de:0030-drops-167191},
  doi =		{10.4230/LIPIcs.ITP.2022.10},
  annote =	{Keywords: Functional analysis, Lean, linear algebra, semilinear, Hilbert space}
}

Search Results

Documents authored by Macbeth, Heather

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

Abstract

Cite as

Formalized functional analysis with semilinear maps

Abstract

Cite as

Thanks for your feedback!

Could not send message