semilinear-paper

Formalized functional analysis with semilinear maps

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.

Where to find our code

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:

A guide through our contributions

Important pull requests

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.