Papers With

← All papers
First page of Formalized functional analysis with semilinear maps

Formalized functional analysis with semilinear maps

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

cs.LO Feb 10, 2022 · v1
formalization mathlib analysis
Read PDF arXiv abstract
TL;DR
Formalizes semilinear maps in mathlib enabling generic proofs over real and complex Hilbert spaces.
Abstract
Semilinear maps are a generalization of linear maps between vector spaces where the scalar action is twisted by a ring homomorphism. This generalization unifies the concepts of linear and conjugate-linear maps. The authors implement this in Lean's mathlib library and prove key results including the Frechet-Riesz representation theorem and the spectral theorem for compact self-adjoint operators generically over real and complex Hilbert spaces. They also formalize a case of a theorem by Dieudonne and Manin on isocrystals.
Problem

Linear and conjugate-linear maps are treated as separate concepts in formalized mathematics, despite being instances of a common generalization. This separation causes duplication when proving theorems that hold generically over real and complex Hilbert spaces.

Approach

Semilinear maps, which generalize linear maps by twisting the scalar action with a ring homomorphism, are implemented in Lean's mathlib library. This unifies linear and conjugate-linear maps under a single framework, enabling generic proofs over both real and complex settings.

Results

Key results formalized include the Frechet-Riesz representation theorem and the spectral theorem for compact self-adjoint operators, proved generically over real and complex Hilbert spaces. A case of a theorem by Dieudonne and Manin on isocrystals is also formalized.