Formalized functional analysis with semilinear maps

DOI10.1007/S10817-024-09696-4MaRDI QIDQ6390785zbMATH OpenFDO

Authors F. Dupuis, Robert Y. Lewis, Heather Macbeth

Publication date 10 February 2022

Full work available at URL https://doi.org/10.1007/S10817-024-09696-4

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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 extsf{mathlib} library, along with a number of important results in functional analysis which previously were impossible to formalize properly. Specifically, we prove the Fr'echet--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'e and Manin that classifies the isocrystals over an algebraically closed field with positive characteristic.

Recommendations

• Type classes and filters for mathematical analysis in Isabelle/HOL
• Normal forms of semilinear operators
• Linear functionals on idempotent spaces. An algebraic approach
• Isomorphism between spaces of multilinear maps and nested compositions over real normed vector spaces
• Semilinear operators

Cited in

(1)

• Duality theory in linear optimization and its extensions -- formally verified

This page was built for publication: Formalized functional analysis with semilinear maps

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6390785)