Papers With

← All papers
First page of Formalization of non-Archimedean functional analysis 1: spherically complete spaces

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

Yijun Yuan

math.NT Jan 29, 2026 · v3 cs.LO math.FA
formalization mathlib analysis number-theory
Read PDF arXiv abstract Code
TL;DR
Formalizes spherically complete spaces, Birkhoff–James orthogonality, the ultrametric Hahn–Banach theorem and spherical completions in Lean 4 on top of Mathlib.
Abstract
In this article, we present a formalization of spherically complete spaces, a fundamental notion in non-Archimedean functional analysis, using the Lean theorem prover (v4.31.0), building over Mathlib. 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 notion of Birkhoff-James orthogonality, the Hahn-Banach extension theorem and the spherical completion for non-Archimedean Banach spaces. URL of code: https://github.com/YijunYuan/SphericalCompleteness/tree/paper
Problem

Spherical completeness, where every decreasing sequence of closed balls has nonempty intersection, is central to non-Archimedean functional analysis. Mathlib did not cover it. Key results such as the ultrametric Hahn–Banach theorem depend on it.

Approach

Defines a SphericallyCompleteSpace class in Lean 4.31.0 over Mathlib and proves equivalent characterizations, basic properties and examples (R, C, Q_p). It also proves non-examples, including the non-spherical completeness of C_p, via separable ultrametric spaces with dense metric. On this basis it formalizes Birkhoff–James orthogonality, a Hahn–Banach pair class with instances for spherically complete D or F, and spherical completions in van Rooij's sense.

Results

The formalization proves the equivalence theorems, the ultrametric Hahn–Banach extension theorem, and Fleischer's existence and uniqueness of spherical completions. It also found that a stated result of Schikhof is false as stated: the single-point space is a counterexample.