2.1 Normed vector spaces over normed fields

One can consider the subspaces and quotient spaces of a semi-normed vector space E over a normed field K. Obviously, a subspace of E ( Submodule K E in Mathlib) automatically inherits the norm from E. On the other hand, the quotient space $E/D$ by a subspace $D\subseteq E$ carries the quotient semi-norm

$$ \begin{align*}\lVert x+D\rVert\mathrel{\mathop:}=\inf_{y\in D}\lVert x-y\rVert.\end{align*} $$

This is realized in Mathlib as an instance Submodule.Quotient.normedSpace , and the formula is reflected in the lemma QuotientGroup.norm_mk .

For (semi-)normed vector spaces $E,F$ over K, any continuous linear map $T\colon E\longrightarrow F$ can be endowed with the operator norm, which is defined as the infimum of the non-negative real numbers c such that $\lVert T(x)\rVert \leq c\cdot \lVert x\rVert $ for all $x\in E$ . This is formalized in Mathlib under the name ContinuousLinearMap.opNorm , and one can use the notation T to denote the operator norm of T. The set of all continuous linear maps from E to F, denoted by $\mathcal{L} (E,F)$ , forms a (semi-)normed vector spaces over K under the operator norm. This is formalized in Mathlib under the name ContinuousLinearMap.toNormedSpace .

2.2 Non-Archimedean property and number-theoretic preliminaries

Definition 2.4. A metric space $(X,d)$ is non-Archimedean or ultrametric if for any $x,y,z\in X$ , we have

$$ \begin{align*}d(x,z)\leq \max\left(d(x,y),d(y,z)\right).\end{align*} $$

This is defined as a class IsUltrametricDist in Mathlib.

Ultrametric spaces carry many interesting properties that are not shared by general metric spaces. For example, a frequently used result in this work is that any two closed balls in an ultrametric space are either disjoint or one is contained in the other. This is formalized in Mathlib under the name IsUltrametricDist.closedBall_subset_trichotomy .

closedBall x r ⊆ closedBall y s ∨ closedBall y s ⊆ closedBall x r ∨
Disjoint (closedBall x r) (closedBall y s)

One of the most important motivating examples of ultrametric spaces are the p-adic fields.

It is easy to verify, and is already formalized in Mathlib as instance Padic.instIsUltrametricDist , that the p-adic norm on $\textbf {Q}_p$ is ultrametric.

The p-adic norm extends uniquely to the algebraic closure $\textbf {Q}^{\mathrm {alg}}_p$ of $\textbf {Q}_p$ ( PadicAlgCl p in Mathlib). However, a non-trivial fact is that $\textbf {Q}^{\mathrm {alg}}_p$ is not complete with respect to the extended p-adic norm (cf. [Reference Robert31, Section 1.4]). This allows us to enlarge $\textbf {Q}^{\mathrm {alg}}_p$ to its completion, which is denoted by $\textbf {C}_p$ ( ℂ_[p] in Mathlib). Basic properties of $\textbf {C}_p$ are already formalized in Mathlib, including the fact that the extended p-adic norm on $\textbf {C}_p$ is ultrametric.

2.3 Conventions and notations

In the rest of this article, we adopt the following conventions and notations:

• • p will always denote a prime number.

• • $(\mathbb{K} ,\lVert \cdot \rVert )$ will be a non-trivially ultrametric normed field. Unless otherwise specified, any other fields appearing in this article are not assumed to be ultrametric.

• • By a normed space over $\mathbb{K} $ , we mean an ultrametric normed vector space over $\mathbb{K} $ .

• • By a ball in a metric space, we always mean a closed ball with non-negative radius.

• • For a vector space E over $\mathbb{K} $ and an element $a\in E$ , we denote by $[a]$ the subspace of E generated by a.

• • For a metric space $(X,d)$ , an element $x\in X$ , and a subset $A\subseteq X$ , we denote by $d(x,A)$ the distance from x to A, that is, $d(x,A)\mathrel {\mathop :}= \inf _{y\in A} d(x,y)$ . In Mathlib, this is named as Metric.infDist .

3.1 Definitions and basic operations

As mentioned in the introduction, a metric space is said to be spherically complete if every decreasing sequence of closed balls has a non-empty intersection. This is formalized as follows:

class SphericallyCompleteSpace (α : Type*) [PseudoMetricSpace α] : Prop where
  nonempty_iInter_of_antitone : ∀ ⦃ci : ℕ → α⦄, ∀ ⦃ri : ℕ → ℝ≥0⦄,
    Antitone (fun i => closedBall (ci i) (ri i)) →
      (⋂ i, closedBall (ci i) (ri i)).Nonempty

Here, Antitone means that the sequence of closed balls is decreasing.

In practice, it is often more convenient to work with sequences of balls with decreasing radius, which is equivalent to the above definition.

This theorem is formalized in Lean as follows:

theorem SphericallyCompleteSpace.iff_strictAnti_radius : -- (1) $\Leftrightarrow$ (2)
    SphericallyCompleteSpace α ↔
    ∀ ⦃ci : ℕ → α⦄, ∀ ⦃ri : ℕ → NNReal⦄, StrictAnti ri →
      Antitone (fun i ↦ closedBall (ci i) (ri i)) →
      (⋂ i, closedBall (ci i) (ri i)).Nonempty

theorem SphericallyCompleteSpace.iff_pairwise_inter_nonempty : -- (1) $\Leftrightarrow$ (3)
    SphericallyCompleteSpace α ↔
    (∀ S : Set (α × NNReal), S.Nonempty →
       (∀ w1 w2 : ↑S, (closedBall w1.val.1 w1.val.2 ∩ closedBall w2.val.1 w2.val.2).Nonempty) →
       (⋂ w : ↑S, closedBall w.val.1 w.val.2).Nonempty)

We conclude this section by recalling the following properties of spherically complete spaces, which are easy to prove and formalize, and useful in practice.

This theorem is formalized in this project as follows:

-- Product of 2 spherically complete spaces is still spherically complete
instance Prod.sphericallyCompleteSpace {E F : Type*}
    [PseudoMetricSpace E] [PseudoMetricSpace F]
    [SphericallyCompleteSpace E] [SphericallyCompleteSpace F] :
    SphericallyCompleteSpace (E × F)

-- Product of a finite family of spherically complete spaces is still spherically complete
instance Pi.sphericallyCompleteSpace {ι : Type*} [Fintype ι] {E : ι → Type*}
    [∀ i, PseudoMetricSpace (E i)] [∀ i, SphericallyCompleteSpace (E i)] :
    SphericallyCompleteSpace (∀ i, E i)

-- Spherical completeness is preserved under isometric isomorphisms
theorem SphericallyCompleteSpace.of_isometryEquiv {E F : Type*}
    [PseudoMetricSpace E] [PseudoMetricSpace F]
    [SphericallyCompleteSpace E]
    (f : E ≃ᵢ F) : SphericallyCompleteSpace F

-- Any quotient of spherically complete normed spaces over 𝕂 is spherically complete
theorem Quotient.sphericallyCompleteSpace (𝕜 : Type*) [NontriviallyNormedField 𝕜]
    {E : Type*} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
    [IsUltrametricDist E] [SphericallyCompleteSpace E]
    {F : Submodule 𝕜 E} :
    SphericallyCompleteSpace (E ⧸ F)

3.2 Relation with other topological conditions

theorem completeSpace_iff_nonempty_iInter_closedBall_of_tendsto_zero
    (α : Type*) [PseudoMetricSpace α] :
    CompleteSpace α ↔
    ∀ ⦃ci : ℕ → α⦄ ⦃ri : ℕ → NNReal⦄,
      Antitone (fun i ↦ closedBall (ci i) (ri i)) →
      Filter.Tendsto ri atTop (nhds 0) →
      (⋂ i, closedBall (ci i) (ri i)).Nonempty

instance instSphericallyCompleteSpaceOfProperSpace (α : Type*)
    [PseudoMetricSpace α] [ProperSpace α] : SphericallyCompleteSpace α where
  nonempty_iInter_of_antitone := by
    intro ci ri hanti
    exact IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed
      (fun i ↦ closedBall (ci i) ↑(ri i)) -- chain of balls
      (fun _ ↦ hanti (by linarith)) -- the chain is descending
      (fun h ↦ nonempty_closedBall.mpr (ri h).prop) -- balls are non-empty
      (isCompact_closedBall (ci 0) ↑(ri 0)) -- the first ball is compact
      fun _ ↦ isClosed_closedBall -- all balls are closed

4.1 A second glance at a result of Schikhof

Schikhof provides a proof of the following assertion.

When formalizing this result in Lean, we find that the denseness of the metric is not enough to ensure non-spherical completeness. In particular, a metric space consisting of a single point trivially has dense metric and is separable, but it is also spherically complete, as there is only one ball in this space.

-- Single point space is a separable ultrametric space with dense metric.
example : SeparableSpace PUnit := inferInstance
example : IsDenseMetric PUnit := inferInstance
example : IsUltrametricDist PUnit := inferInstance
-- Single point space is spherically complete, which disproofs Schikhof's result.
example : SphericallyCompleteSpace PUnit := inferInstance

To isolate the issue, we revisit Schikhof’s proof. Suppose, for contradiction, that $(X,d)$ is a spherically complete separable ultrametric space with dense metric. Let $\{a_0,a_1,\ldots \}$ be a countableFootnote ³ dense subset of X. Take $r_0>0$ to be the distance between two distinct points of X, and take a sequence of real numbers $r_1,r_2,\ldots $ such that $r_0>r_1>\cdots >r_n>\cdots >\frac {1}{2}r_0$ .

Schikhof’s proof depends on the following claim.

With this claim, one can recursively construct a decreasing sequence of balls ${B_1\supseteq B_2\supseteq \cdots \supseteq B_n\supseteq \cdots }$ such that $\mathrm {diam}(B_n)=r_n$ and $a_{n-1}\notin B_n$ for each ${n\geq 1}$ . The spherical completeness of X implies that $\bigcap _{n=1}^\infty B_n$ is non-empty and consequently contains a non-empty ball of radius $\frac {1}{2}r_0>0$ . This ball is disjoint from the dense set $\{a_0,a_1,\ldots \}$ , which leads to a contradiction.

The subtlety appears in the proof of Claim 4.5. Schikhof partitions B into at least two disjoint balls of radius $r'$ via the relation $x\sim y \Longleftrightarrow d(x,y)\leq r'$ , and one of them, say $B'$ , does not contain x. Although this is sound, it is not clear why $\mathrm {diam}(B')=r'$ . The denseness of the metric only ensures that there are subballs of B with diameter arbitrarily close to $r'$ ; it does not guarantee that the distances approximating $r'$ from below can always be realized between points in the same subball, let alone that we can find such a subball that does not contain x.

To fix this issue, we introduce a stronger condition than the denseness of the metric.

class IsSphericallyDense (α : Type*) [PseudoMetricSpace α] : Prop where
  spherically_dense : ∀ (c : α) (r : ℝ≥0) , diam (closedBall c r) = r

In our project, Claim 4.5 is formalized as follows:

lemma exists_sub_closedBall_not_mem {α : Type*}
    [PseudoMetricSpace α] [IsUltrametricDist α] [IsSphericallyDense α]
    (c₀ : α) (r₀ : ℝ≥0) (r₁ : ℝ≥0) (hr : r₁ < r₀) (z : α) :
    ∃ c₁ : α,
    closedBall c₁ r₁ ⊆ closedBall c₀ r₀ ∧
    z ∉ closedBall c₁ r₁osedBall c₁ r₁ ⊆ closedBall c₀ r₀ ∧ z ∉ closedBall c₁ r₁

And the non-spherical completeness of separable spherically dense ultrametric spaces is formalized as follows:

theorem not_sphericallyCompleteSpace_of_isSphericallyDense_separable_ ultrametric
    (α : Type*) [MetricSpace α]
    [IsUltrametricDist α] [IsSphericallyDense α] [Nonempty α] [SeparableSpace α] :
    ¬ SphericallyCompleteSpace α

The following proposition shows that spherical denseness is a reasonable replacement for the dense metric condition and is satisfied by the important example $\textbf {C}_p$ .

4.2 The non-spherical completeness of $\textbf {C}_p$

Fix a prime number p:

variable (p : ℕ) [hp : Fact (Nat.Prime p)]

To apply Theorem 4.7 to $\textbf {C}_p$ in Lean, one needs to provide the instances of DenselyNormedField and TopologicalSpace.SeparableSpace for $\textbf {C}_p$ , which are not yet formalized in Mathlib. In this section, we demonstrate our implementation of these two instances.

5.1 Definition and basic properties

In Hilbert spaces over $\textbf {R}$ or $\textbf {C}$ , the orthogonality between two vectors $x,y$ is defined via the inner product. However, there is no inner product in the ultrametric world: the parallelogram law fails in general.Footnote ⁵ The concept of Birkhoff–James orthogonality provides a way to define an orthogonality in normed spaces without inner products.

In [Reference van Rooij32] and in our project, the Birkhoff–James orthogonality is restated as follows.

This is formalized in our project as follows:

def IsMOrtho (x : E) (D : Subspace 𝕜 E) := Metric.infDist x D = ‖x‖

def IsVOrtho (x y : E) := Metric.infDist x (𝕜 ∙ y) = ‖x‖

def IsOrtho (F1 : Subspace 𝕜 E) (F2 : Subspace 𝕜 E) := ∀ x ∈ F1, IsMOrtho 𝕜 x F2

notation:50 x " ⟂ₘ " F => IsMOrtho _ x F
notation:50 F " ⟂ₛ " G => IsOrtho _ F G
notation:50 x " ⟂[" 𝕜 "] " y => IsVOrtho 𝕜 x y

Various properties of the Birkhoff–James orthogonality—symmetry, homogeneity, etc.—are formalized in our project. Among them, we prove that this formulation of orthogonality is equivalent to James’s original definition:

lemma IsVOrtho.iff_birkhoffJames (x y : E) : (x ⟂[𝕜] y) ↔ ∀ c : 𝕜, ‖x‖ ≤ ‖x + c • y‖

5.2 Orthogonal projection and orthogonal complement

As is indicated in the definition, the orthogonal complement may not exist in general. However, if the subspace is spherically complete, then one can always find an orthogonal complement.

This theorem is a direct consequence of the following result.

theorem exists_orthProj_of_sphericallyComplete [SphericallyCompleteSpace D] :
    ∃ T : E →L[𝕜] ↥D, (∀ a ∈ D, T a = a) ∧ ‖T‖ ≤ 1

Proof of Theorem 5.5.

Let $D^{\perp }$ be the kernel of T in Proposition 5.6. We claim that $D^{\perp }$ is an orthogonal complement of D and T is the orthogonal projection onto D along $D^{\perp }$ .

If $x\in D\cap D^{\perp }$ , then $x=T x =0$ . On the other hand, for any $x\in E$ , one has $x-T x\in D^{\perp }$ and $T x\in D$ , thus $x=(x-T x)+T x\in D+D^{\perp }$ . This shows that $D^{\perp }$ is a complement of D.

To show that $D \perp _{\textrm {s}} D^{\perp }$ , let $x\in D^{\perp }$ and $y\in D$ . Then one has

$$ \begin{align*}\left\lVert y\right\rVert=\left\lVert T(x-y)\right\rVert\leq\left\lVert x-y\right\rVert,\end{align*} $$

which implies by the ultrametric inequality that $\left \lVert x\right \rVert \leq \left \lVert x-y\right \rVert $ . As a result, one obtains $\left \lVert x\right \rVert \leq \mathrm {dist}(x,D)$ and consequently $x\perp _{\textrm {m}} D$ .

It is a common strategy of defining the data required in a proof, followed by the specifications of the said data in Lean formalizations. Specialized to the orthogonal projection and orthogonal complement, we first prove the existence of the continuous linear map T in Proposition 5.6, and then define the orthogonal projection and orthogonal complement via T.

-- The orthogonal projection
def orthProj [SphericallyCompleteSpace D] : E →L[𝕜] ↥D :=
  (exists_orthProj_of_sphericallyComplete 𝕜 D).choose -- the map $T$ in $Proposition$ $5.6$

-- The orthogonal complement
def orthComp : Submodule 𝕜 E :=(exists_orthProj_of_sphericallyComplete 𝕜 D).choose

and formalize their properties as theorems:

theorem IsOrtho.orthComp : (D ⟂ₛ (orthComp 𝕜 D))

theorem isCompl_orthComp : IsCompl D (orthComp 𝕜 D)

theorem norm_orthProj_le_one : ‖orthProj 𝕜 D‖ ≤ 1

theorem orthProj_id : ∀ a ∈ D, (orthProj 𝕜 D) a = a

5.3 Application: Finite dimensional normed spaces

As an application—seemingly unrelated to the orthogonality at first glance—we prove the following result.

theorem of_finiteDimensional [FiniteDimensional 𝕜 E] : SphericallyCompleteSpace E

The strategy is a direct induction on the dimension:

1. 1. The $0$ -dimensional case is trivial.

2. 2. The $1$ -dimensional spaces are isometric to the base field, which is spherically complete by assumption.

   
   instance instSphericallyCompleteSpaceSpanSingleton
       [SphericallyCompleteSpace 𝕜] (z : E) :
       SphericallyCompleteSpace (Submodule.span 𝕜 {z})
   

3. 3. Assume that there exists an n-dimensional spherically complete subspace D of E, where $n <\mathrm {dim}E$ . Since D is a proper subspace, one may pick, by Proposition 5.8, an element $a\in E$ with $a\notin D$ and $a\perp _{\textrm {s}} D$ .

4. 4. Since D and $[a]$ are both spherically complete, so is their product space $D\times [a]$ (cf. Proposition 3.4). The orthogonality $a\perp _{\textrm {s}} D$ makes the isomorphism

   (a) $$ \begin{align} D\oplus[a]\cong D\times [a] \end{align} $$
   an isometry (again by Proposition 5.8), so that spherical completeness transfers from $D\times [a]$ to $D\oplus [a]$ via (2) of Proposition 3.4.

Without $a\perp _{\textrm {s}} D$ the isomorphism (a) need not be an isometry, and spherical completeness would not transfer. The existence of such an a and the resulting isometry are exactly the following proposition.

theorem exists_isMOrtho_vec_of_finrank_lt
    [SphericallyCompleteSpace D] (hF : Module.finrank 𝕜 D < Module.finrank 𝕜 E) :
    ∃ (x : E), x ≠ 0 ∧ (x ⟂ₘ D)

def IsMOrtho.directProdIsoSum (x : E) (hxF : x ⟂ₘ D) :
    (Submodule.span 𝕜 {x}) × D≃ₛₗᵢ[RingHom.id 𝕜] (Submodule.span 𝕜 {x}) + D

The isometric isomorphism $D\times [a_0]\cong D+[a_0]$ in Proposition 5.8 is not free: it hinges on the spherical completeness of D. This is easy to overlook in informal writing, where a single symbol $\cong $ is used for isomorphisms living in different categories. In the category of vector spaces, a direct sum is always naturally isomorphic to the direct product; but for normed spaces the “same” isomorphism need not be an isometry. Here formalization earns its keep: a strict type system forbids conflating the two $\cong $ ’s and forces one to pin down the category of each.

6.1 Reduce to the case of codimension 1

In the proof of [Reference van Rooij32, Lemma 4.4], van Rooij writes:

To translate this assertion into a formalized proof, we need to clarify the partially ordered set $\mathfrak{P} $ we are working with. In this context, $\mathfrak{P} $ consists of the pairs $(M,T)$ , where M is a submodule of E and $T\in \mathcal{L} (M,K)$ is a continuous linear map, satisfying the following conditions:

1. 1. for any $x\in D$ , $T x = S x$ ;

2. 2. for any $x\in M$ and $U\in \mathcal{U} $ , $\lVert T x - U x\rVert \leq \epsilon _U\lVert x\rVert $ ;

3. 3. $(M_1,T_1)\leq (M_2,T_2)$ if $M_1\subseteq M_2$ and $T_2$ extends $T_1$ .

In our project, this set $\mathfrak{P} $ is formalized as a structure:

structure PartialExtension where
  M : Submodule 𝕜 E
  hDM : D ≤ M -- D is a submodule of M
  T : M →L[𝕜] F
  hT : ∀ x : D, T ⟨x, hDM x.prop⟩ = S x -- Condition 1
  hU : ∀ U : ↑𝒰, ∀ x : M, ‖T x- U.val x‖ ≤ (ε U) * ‖x‖ -- Condition 2

And we formalize the partial order on $\mathfrak{P} $ as an instance:

instance instPartialOrderPartialExtension : -- Condition 3
    PartialOrder (PartialExtension 𝕜 E F S 𝒰 h𝒰 ε) where
    le a b := ∃ hab : a.M ≤ b.M , ∀ x : a.M, b.T ⟨x.val, hab x.prop⟩ = a.T x
    ... -- Proof of reflexivity, antisymmetry and transitivity. Omitted.

To apply Zorn’s lemma, we need to show that every chain $\{(M_\alpha ,T_\alpha )\}_{\alpha \in I} \subseteq \mathfrak{P} $ has an upper bound. It is easy to verify that if one takes $M_{\max }$ to be the union of all the $M_\alpha $ ’s, then $M_{\max }$ is still a submodule of E, and the $T_\alpha $ ’s can be glued together to form a linear map $T_{\max }\in \mathcal{L} (M_{\max },F)$ . Moreover, we have the following lemma.

Proof. Take an arbitrary $U\in \mathcal{U} $ and set $C\mathrel {\mathop :}= \max \{\epsilon _U,\lVert U\rVert \}$ . For any ${x\in M_{\max }}$ , there exists some $\alpha \in I$ such that $x\in M_\alpha $ . One computes that

$$ \begin{align*}\left\lVert T_{\max}x\right\rVert=\left\lVert T_\alpha x\right\rVert\leq \max\{\left\lVert T_\alpha x - U x\right\rVert, \left\lVert U x\right\rVert\}\leq \max\{\epsilon_U\left\lVert x\right\rVert,\left\lVert U\right\rVert\left\lVert x\right\rVert\}\leq C \left\lVert x\right\rVert.\end{align*} $$

This shows that $T_{\max }$ is bounded, hence continuous.

When formalizing the fact that $T_{\max }$ is linear and continuous, the locally-defined nature of $T_{\max }$ forces us to repeatedly use Classical.choose_spec and the fact that chains are directed in the formalized proof, which makes the code quite verbose and less transparent. Notwithstanding these challenges, we successfully formalize the existence of upper bounds in our project:

lemma bddAbove_of_chain_of_partial_extension
    (P : Set (PartialExtension 𝕜 E F S 𝒰 h𝒰 ε))
    (hP : IsChain (fun x1 x2 ↦ x1 ≤ x2) P) (hhP : P.Nonempty) : BddAbove P

By applying Zorn’s lemma, we obtain a maximal element $(M_{\max },T_{\max })$ in $\mathfrak{P} $ . This reduces the proof of Theorem 6.3 to the case where E is of codimension 1 over D.

The corresponding formalized proof of this lemma is integrated in the proof of Proposition 6.6, which we omit here for brevity.

6.2 Remarks on the codimension 1 case

Now we assume that there exists some $a\in E\backslash D$ such that $E=D+[a]$ .

It is shown in [Reference van Rooij32] that the spherical completeness of F implies the existence of an element $z_0\in F$ such that

$$ \begin{align*}\left\lVert S x+z_0 - U(x + a)\right\rVert\leq \epsilon_U\left\lVert x + a\right\rVert\end{align*} $$

holds for every $U\in \mathcal{U} $ and $x\in D$ .

lemma exists_extensionValue_norm_le [SphericallyCompleteSpace F]
    {a : E} (ha1 : a ∉ D) :
    ∃ z0 : F, ∀ (x : ↥D) (U : ↑𝒰), ‖S x + z0 - U.val (↑x + a)‖ ≤ ε U * ‖↑x + a‖

Then the desired extension is given by

$$ \begin{align*}\overline{S}\colon x + \lambda\cdot a \longmapsto S x + \lambda\cdot z_0.\end{align*} $$

def codimOneExtension [SphericallyCompleteSpace F] {a : E} (ha1 : a ∉ D) :
    (D + Submodule.span 𝕜 {a}) → F := fun M => by
    have := Submodule.mem_sup.1 M.prop -- $M = x + y$ with $x \in D$ and $y\in [a]$
    let lambda := (Submodule.mem_span_singleton.1
      this.choose_spec.2.choose_spec.1).choose -- There exists $\lambda\in\ $𝕜 such that $y = \lambda\cdot a$
    use S ⟨this.choose, this.choose_spec.1⟩ +
      lambda • (exists_extensionValue_norm_le ha1 S h𝒰 hε1 hε2 hε3).choose

We prove that $\overline {S}$ is continuous and linear by showing that it is a bounded linear map:

def isBoundedLinearMap_codimOneExtension [SphericallyCompleteSpace F]
    {a : E} (ha1 : a ∉ D) :
    IsBoundedLinearMap 𝕜 (codimOneExtension ha1 S h𝒰 hε1 hε2 hε3)

The structure ContinuousLinearMap can then be obtained by IsBoundedLinearMap.toContinuousLinearMap .

6.3 Application: Spherical completeness of $\mathcal{L} (E,F)$

Besides its use in constructing the orthogonal complement (cf. Proposition 5.6) and proving the ultrametric Hahn–Banach theorem (Theorem 6.3), Proposition 6.6 can also be applied to show the spherical completeness of the space of continuous linear maps to a spherically complete codomain.

The proof of Theorem 6.10 in [Reference van Rooij32] is concise:

During the formalization, we recognized that there are extra details that need to be taken care of:

1. 1. To apply Proposition 6.6, one has to verify that $\epsilon _U>0$ for every $U\in \mathcal{U} $ in the current context. To do so, the extra condition that the radii of these balls are strictly decreasing is required. By Theorem 3.3, this extra condition does not incur any loss of generality.

2. 2. The second point is more serious. The declaration “ $\epsilon _{T_n}=\epsilon _n$ ” implicitly uses the composition

   $$ \begin{align*}\mathcal{U}\longrightarrow \textbf{N}\longrightarrow \textbf{R},\ T_n\longmapsto n\longmapsto \epsilon_n,\end{align*} $$
   which is not well-defined in general, as the map $n\longmapsto T_n$ may not be injective. To bypass this issue, we consider the condition:
   (a) $$ \begin{align} {\textbf{for any }n\in\textbf{N}\textbf{, there exists }N\in\textbf{N}\textbf{ such that for any }i>N\textbf{, }T_n\neq T_i,} \end{align} $$
   or, equivalently, any element of $\mathcal{U} $ only appears finitely many times in the sequence $\{T_n\}_{n\in \textbf {N}}$ .

   If this condition holds, then one can take a subsequence $\{T_{n_k}\}_{k\in \textbf {N}}$ of $\{T_n\}_{n\in \textbf {N}}$ such that the map $k\longmapsto T_{n_k}$ is injective.

   
   theorem exists_injective_subseq_of_finite_duplication {α : Type*} (seq : ℕ → α)
       (hseq : ∀ n : ℕ, ∃ N, ∀ i > N, seq n ≠ seq i) :
       ∃ φ : ℕ → ℕ, StrictMono φ ∧ Function.Injective (seq ∘ φ)
   

   Then van Rooij’s original argument can be applied to the balls $\{B(T_{n_k},\epsilon _{n_k})\}_{k\in \textbf {N}}$ , which yields a desired element in the intersection of all the $B(T_{n_k},\epsilon _{n_k})$ and consequently of all the $B(T_n,\epsilon _n)$ .

   Conversely, if (a) does not hold, then there exists some $T\in \mathcal{U} $ such that $T=T_n$ for infinitely many n. Then T itself witnesses the non-emptiness of the intersection of all the $B(T_n,\epsilon _n)$ .

This kind of subtlety can easily be overlooked in traditional mathematical writing, but has to be addressed carefully in a formalized proof. In our project, we successfully formalize the proof of Theorem 6.10 as an instance by taking these details into account.

7.1 Immediate extensions

The concept of immediate extensions is closely related to the spherical completeness of ultrametric normed spaces, and plays a key role in the proof of Theorem 7.3. In [Reference van Rooij32], van Rooij defines immediate extensions as follows.

As an experiment, we tried to formalize this definition using Claude Opus, a large language model developed by Anthropic. It gave a literal translation:

def IsImmediateExtension (D : Submodule 𝕜 E) : Prop := ∀ v : E, (v ⟂ₘ D) → v = 0

While this formalization is mathematically correct, it is not a good design choice. One may need to handle two independent immediate extensions $E_1/D$ , $E_2/D$ of D in the proof of Theorem 7.3. In this case, if one defines D to be of type Submodule 𝕜 E₁ , then an awkward coercion is required to express the condition that $E_2$ is an immediate extension of D, which makes the code less concise. To resolve this issue, we reformulate Definition 7.6 in the following more flexible way.

def IsImmediate (f : E →ₗᵢ[𝕜] F) : Prop := ∀ v : F, (v ⟂ₘ LinearMap.range f) → v = 0

Compared to Definition 7.6, this definition allows E and F to be independent types, which makes the statements of related results more convenient to work with. For example, van Rooij proved the following result, which is crucial for the uniqueness argument in Theorem 7.3.

With our new definition, this is restated in our project as follows.

Lemma 7.9. Let $E, F, H$ be normed spaces over $\mathbb{K} $ , with H spherically complete. If there exists a linear isometry $f\colon E\longrightarrow H$ , then it factors through any immediate map $E\longrightarrow F$ .

theorem IsImmediate.exists_linearIsometry_comp_eq {H : Type*}
    [NormedAddCommGroup H] [NormedSpace 𝕜 H] [IsUltrametricDist H]
    [SphericallyCompleteSpace H]
    (f : E →ₗᵢ[𝕜] F) (hf : IsImmediate f) (g : E →ₗᵢ[𝕜] H) :
    ∃ (h : F →ₗᵢ[𝕜] H), LinearIsometry.comp (h : F →ₗᵢ[𝕜] H) (f : E →ₗᵢ[𝕜] F) = g

7.2 Maximal immediate extensions: A Zorn’s lemma argument

In [Reference van Rooij32], the spherical completion is constructed via the following result.

The set S is formalized as follows:

def IsImmediate.immediateExtensionSubmodules
    (f : E →ₗᵢ[𝕜] F) : Set (Submodule 𝕜 F) :=
    {M : Submodule 𝕜 F | ∃ hc : f.range ≤ M,
      ∀ v : M, (v ⟂ₘ LinearMap.range (Submodule.inclusion hc)) → v = 0 }

After this definition, we apply Zorn’s lemma to show the existence of maximal elements in IsImmediate.immediateExtensionSubmodules. Given a chain C in this set, an upper bound $M_{\max }$ is given by the union of all elements of C. We verify that $M_{\max }$ lies in this set by showing that the inclusion map $\mathrm {Im}(f)\longrightarrow M_{\max }$ is immediate. This yields the formalized proof of the first assertion of Proposition 7.11:

theorem IsImmediate.exists_maximal_immediateExtensionSubmodule (f : E →ₗᵢ[𝕜] F) :
    ∃ m, Maximal (fun x ↦ x ∈ immediateExtensionSubmodules E F f) m

We define maximalImmediateExtensionEmbedding f to be the inclusion map of E into its maximal immediate extension in F, and prove that it gives a spherical completion of E when F is spherically complete:

instance instIsSphericalCompletionOfMaximalImmediateExtensionSubmodule
    [SphericallyCompleteSpace F] (f : E →ₗᵢ[𝕜] F) :
    IsSphericalCompletion (maximalImmediateExtensionEmbedding f)

7.3 Existence of spherically complete extension

With Proposition 7.11, the existence of spherical completions of E is reduced to the existence of a spherically complete extension of E. This is guaranteed by the following result.

Proposition 7.12 (cf. [Reference van Rooij32, Theorem 4.1]).

Let E be a normed space over $\mathbb{K} $ . Let $\ell ^\infty (E)$ be the space of all bounded $\textbf {N}$ -indexed E-sequences, equipped with the supremum norm. Let

$$ \begin{align*}c_0(E)\mathrel{\mathop:}= \left\{(f_n)_{n\in\textbf{N}}\in\ell^\infty(E)\colon \lvert f_n\rvert \to 0 \text{ as } n \to \infty\right\}.\end{align*} $$

Then

1. 1. $c_0(E)$ is a closed subspace of $\ell ^\infty (E)$ . In particular, $\ell ^\infty (E)/c_0(E)$ is a normed space over K.

2. 2. $\ell ^\infty (E)/c_0(E)$ is spherically complete.

3. 3. The diagonal embedding $i\colon E\to \ell ^\infty (E)/c_0(E),\ x\mapsto [(x,x,x,\ldots )]$ is an isometric linear embedding.

In particular, every normed space over $\mathbb{K} $ admits a spherically complete extension.

In Mathlib, $\ell ^\infty (E)$ is already formalized as lp E ⊤, which is a normed space over K. We formalize the subspace $c_0(E)$ as follows:

def c₀ (G : ℕ → Type*) [∀ i, NormedAddCommGroup (G i)]
    [∀ i, NormedSpace 𝕜 (G i)] : Submodule 𝕜 ↥(lp G ⊤) where
  carrier := {f : lp G ⊤ | Tendsto (fun n ↦ ‖f n‖) atTop (𝓝 0)} -- the underlying set
  add_mem' := ... -- closedness under addition. Omitted.
  zero_mem' := ... -- zero element is in c₀. Omitted.
  smul_mem' := ... -- closedness under scalar multiplication. Omitted.

The closedness of $c_0(E)$ and the resulting spherical completeness of the quotient space are not difficult to verify, and we implement them as two instances.

Finally, the diagonal embedding is formalized as a LinearIsometry:

def lpQuotientEmbedding :
    E →ₗᵢ[𝕜] ((lp (fun (_ : ℕ) ↦ E) ⊤)⧸ c₀ 𝕜 (fun (_ : ℕ) ↦ E)) where
  toFun x := by
    refine (QuotientAddGroup.mk' _) (⟨fun (_ : ℕ) ↦ x, ?_⟩)
    ... -- Proof of the fact that the diagonal embedding belongs to $\ell^\infty$. Omitted.
  ... -- map_add', map_smul', norm_map'. Omitted.

7.4 Weak universal properties of the spherical completion

As we mentioned at the beginning of this section, the spherical completion does not enjoy as good a universal property as the usual completion of metric spaces. Still, some weaker universal-property-like results can be established.

To begin with, following van Rooij, we observe that the uniqueness of spherical completions in Fleischer’s theorem (cf. Theorem 7.3) follows from Lemma 7.9: take two spherical completions $f_1\colon E\longrightarrow F_1$ and $f_2\colon E\longrightarrow F_2$ of E. Since $f_1$ is immediate and $F_2$ is spherically complete, Lemma 7.9 gives an isometric linear map $g\colon F_1\longrightarrow F_2$ such that $g\circ f_1=f_2$ . As a result, the image of g is a spherically complete subspace of $F_2$ , which equals $F_2$ by the minimality of $F_2$ . Hence g is surjective, and consequently an isometric isomorphism.

On the other hand, the spherical completion provides another way to describe the spherical completeness of ultrametric normed spaces.

theorem IsSphericalCompletion.iff_embedding_to_sphericalCompletion_surjective
    {ι : E →ₗᵢ[𝕜] F} (hF : IsSphericalCompletion ι) :
    SphericallyCompleteSpace E ↔ Function.Surjective ι

theorem iff_maximallyComplete :
    SphericallyCompleteSpace E ↔ MaximallyComplete 𝕜 E

The proof is not difficult, and we omit the details here.

Finally, we show that the spherical completion is minimal among all spherically complete extensions of E, which can be viewed as a weaker analogue of Theorem 7.1.

theorem IsSphericalCompletion.weak_universal_property
    {F' : Type*} [NormedAddCommGroup F'] [NormedSpace 𝕜 F'] [IsUltrametricDist F']
    [SphericallyCompleteSpace F'] (f : E →ₗᵢ[𝕜] F')
    {ι : E →ₗᵢ[𝕜] F} (hF : IsSphericalCompletion ι) :
    ∃ T : F →ₗᵢ[𝕜] F', T.comp ι = f