1 Search Results for "Dupuis, Frédéric"

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-dev.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}
}
  • Refine by Author
  • 1 Dupuis, Frédéric
  • 1 Lewis, Robert Y.
  • 1 Macbeth, Heather

  • Refine by Classification
  • 1 Mathematics of computing → Functional analysis

  • Refine by Keyword
  • 1 Functional analysis
  • 1 Hilbert space
  • 1 Lean
  • 1 linear algebra
  • 1 semilinear

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact