Formalization of non-Archimedean functional analysis 1: spherically complete spaces

TL;DR

This paper formalizes spherically complete spaces in non-archimedean functional analysis, including their properties, examples, and applications like orthogonality and the Hahn-Banach theorem, with accompanying code.

Contribution

It provides a comprehensive formalization of spherically complete spaces and key theorems in non-archimedean functional analysis, including examples and applications.

Findings

Formal definitions and properties of spherically complete spaces

Formalization of the Hahn-Banach extension theorem in this context

Implementation of spherical completion for non-archimedean Banach spaces

Abstract

In this article, we present a formalization of spherically complete spaces, which is a fundamental notion in non-archimedean functional analysis. This work includes the equivalent definitions of spherically complete spaces, their basic properties, examples and non-examples such as the field $\mathbf{C}_p$ of $p$-adic complex numbers. As applications, we formalize the Birkhoff-James orthogonality, Hahn-Banach extension theorem and the spherical completion for non-archimedean Banach spaces. Code available at https://github.com/YijunYuan/SphericalCompleteness