License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.10
URN: urn:nbn:de:0030-drops-167191
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16719/
Go to the corresponding LIPIcs Volume Portal

Dupuis, Frédéric ; Lewis, Robert Y. ; Macbeth, Heather

Formalized functional analysis with semilinear maps

pdf-format:
LIPIcs-ITP-2022-10.pdf (0.8 MB)

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.

BibTeX - Entry

@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/opus/volltexte/2022/16719},
  URN =		{urn:nbn:de:0030-drops-167191},
  doi =		{10.4230/LIPIcs.ITP.2022.10},
  annote =	{Keywords: Functional analysis, Lean, linear algebra, semilinear, Hilbert space}
}

Keywords: Functional analysis, Lean, linear algebra, semilinear, Hilbert space
Collection: 13th International Conference on Interactive Theorem Proving (ITP 2022)
Issue Date: 2022
Date of publication: 03.08.2022
Supplementary Material: InteractiveResource (Project Website): https://robertylewis.com/semilinear-paper/

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI