This site documents the code for the journal version of the paper Formalized functional analysis with semilinear maps by Frédéric Dupuis, Robert Y. Lewis, and Heather Macbeth. For the conference version published at ITP 2022, see here.

All of the code that we describe in our paper is available on the semilinear-paper-update branch of the mathlib repository. This branch is frozen at the date of submission of the camera-ready version. We maintain a backup at another repository

Much of the code we decribe is already integrated into the master branch of the mathlib repository.
The only pieces remaining to be integrated are the proofs of the spectral theorems.
You can view the diff between the `semilinear-paper-update`

branch and the master branch at the time of submission.

To download the code and explore it yourself:

- Install Lean
`leanproject get mathlib:semilinear-paper-update`

- Use VSCode’s
`Open folder`

feature, or`code mathlib_semilinear-paper-update/`

, to open the root of the`mathlib`

repository.- You CANNOT interactively browse a single file by opening it in VSCode. You MUST open the directory.

- The core definitions of (semi)linear maps, equivalences, etc. are in
`algebra.module.linear_map`

and`data.equiv.module`

. - The type classes
`ring_hom_comp_triple`

and`ring_hom_inv_pair`

needed for composition and inversion of semilinear maps appear in`algebra.ring.comp_typeclasses`

, as do most of the “universal” instances of these type classes. The instance`star_ring_end.ring_hom_inv_pair`

needed for composition of conjugate-linear maps appears in`algebra.star.basic`

(the rest of that file was written by other authors). - A test file checks the behavior of the conjugate-linear map notation and type classes.
- Some files which required particular attention during the refactor to semilinear maps were
`linear_algebra.basic`

,`topology.algebra.module.basic`

,`analysis.normed_space.linear_isometry`

, and`analysis.normed_space.operator_norm`

. - The
`is_R_or_C`

type class is defined in`data.complex.is_R_or_C`

. - The Fréchet-Riesz representation theorem (
`inner_product_space.to_dual`

) is defined in`analysis.inner_product_space.dual`

. - The adjoint (
`continuous_linear_map.adjoint`

) is defined in`analysis.inner_product_space.adjoint`

, as is its finite-dimensional specialization (`linear_map.adjoint`

). The definitions of self-adjoint and normal operators (`self_adjoint`

,`is_star_normal`

) are in`algebra.star.self_adjoint`

; these definitions are made in the more abstract context of a`star_ring`

. The “implementation detail”`inner_product_space.is_normal`

is defined in`analysis.inner_product_space.basic`

(the file as a whole has many authors). - \(\ell^p\) spaces are defined in
`analysis.normed_space.lp_space`

. The Hilbert sum of a family of inner product spaces is found in`analysis.inner_product_space.l2_space`

. - Both the finite- and infinite-dimensional versions of the spectral theorem are in
`analysis.inner_product_space.spectrum`

, with many preliminaries in`analysis.inner_product_space.rayleigh`

. Preliminaries about compact operators can be found in`analysis.normed_space.compact_map`

. - The material about Fourier series and Parseval’s identity can be found in
`analysis/fourier.lean`

. The proof that continuous functions are dense in Lp can be found in`measure_theory/function/continuous_map_dense.lean`

, and the analogous fact for simple functions (our contribution was a refactor generalizing an existing result) is in`measure_theory/function/simple_func_dense_lp.lean`

. - The definition and classification of isocrystals can be found in
`ring_theory.witt_vector.isocrystal`

. The construction of the “Frobenius rotation,” the key lemma of the classification theorem, is done in`ring_theory.witt_vector.is_alg_closed`

with preliminary work in`ring_theory.witt_vector.mul_coeff`

. Preliminary work to show that the Witt vectors over a domain are a domain is done in`ring_theory.witt_vector.domain`

. The fact that Witt vectors are a discrete valuation ring can be found in`ring_theory/witt_vector/discrete_valuation_ring.lean`

.

Much of our work has already been merged into mathlib. We list some of the primary pull requests here for reference. This is far from a complete list of the PRs connected to this paper.

- #3934: adds
`is_R_or_C`

type class - #4057: generalizes
`inner_product_space`

from \(\mathbb{R}\) to`is_R_or_C`

- #4379: proves separate real/complex Fréchet–Riesz
- #6952: Fourier monomials on the circle are orthonormal
- #8035: span of Fourier monomials is dense in C^0
- #8114: simple functions are dense in Lp
- #8306: continuous functions are dense in Lp
- #8328: span of Fourier monomials is dense in L^p #8328
- #8857: introduces linear map composition notation
- #9272: introduces semilinear maps and equivalences
- #9539: generalizes continuous linear maps to semilinear
- #9840: proves the Rayleigh quotient produces eigenvectors
- #9924: unifies the two Fréchet–Riesz statements
- #9995: proves diagonalization theorem for self-adjoint endomorphisms in finite dimension
- #10317: proves further variations on the diagonalization theorem
- #10825: defines the adjoint
- #11015: defines the space \(\ell^p\)
- #11094: proves completeness of \(\ell^p\)
- #11135: defines
`self_adjoint`

- #11255: define Hilbert bases and show that every Hilbert space admits a Hilbert basis
- #11315: constructs inner product space structure on the Hilbert sum
- #11320: Fourier series for functions in L2; Parseval’s identity
- #11346: proves Witt vectors form a domain
- #12041: classify 1D isocrystals
- #12213: Witt vectors are a DVR