t-orthogonal bases and subspaces of normed spaces of countable type

Let K be a complete nontrivially normed field and E an ultrametric normed K-space. The space E is of countable type if some sequence v : ℕ → E has dense span. Over a field whose value group is not discrete, such a space need not have an orthogonal basis, but for every t < 1 it has a t-orthogonal one. This file constructs these bases by an approximate Gram–Schmidt process.

• TauCeti.exists_isTOrthogonalFamily_span_image_Iio_eq: every sequence w : ℕ → E can be replaced by a t-orthogonal sequence e with the same initial spans, span (e '' Iio n) = span (w '' Iio n). The vector e n is w n minus an almost best approximation of w n in the span of the previous vectors (TauCeti.riesz_lemma_translate); the losses at the successive steps are chosen with product at least t.
• TauCeti.exists_isTOrthogonalBasis_of_dense_span: a space of countable type has a t-orthogonal basis indexed by a set of natural numbers.
• TauCeti.exists_basis_isTOrthogonalFamily: a finite-dimensional space has a t-orthogonal basis in the sense of Module.Basis, indexed by Fin (finrank K E).
• TauCeti.exists_isTOrthogonalBasis_nat_of_dense_span: an infinite-dimensional space of countable type has a t-orthogonal basis indexed by ℕ.
• Submodule.exists_finiteDimensional_le_infDist_le: for a closed subspace D, a finite-dimensional subspace G and c > 1, some finite-dimensional W ≤ D satisfies infDist g W ≤ c * infDist g D for every g ∈ G. The subspace W is cut out of D by lifts of a t-orthogonal basis of the image of G in E ⧸ D.
• Submodule.exists_dense_span_of_dense_span: every subspace of a space of countable type, closed or not, is of countable type. The approximation theorem is applied to the closed subspace closure D: the finite-dimensional subspaces W ≤ closure D attached to the initial spans of a densely spanning sequence together span a dense subspace of closure D, and each of their countably many spanning vectors is then replaced by a sequence in D converging to it.

Neither a discrete valuation nor completeness of E is needed: only the finite-dimensional subspaces spanned by initial segments have to be closed, which holds over a complete field. The constant c in the approximation theorem does not depend on G; this uniformity is what lets the subspaces W attached to the increasing initial spans together span a dense subspace of the closure of D. Quotients of spaces of countable type are of countable type by DenseRange.dense_span_range_comp, applied to the quotient map. Together with TauCeti.IsTOrthogonalBasis.toUnconditionalSchauderBasis, these bases give the coordinates in which Banach spaces of countable type are compared with C₀(ℕ, K).

References

• C. Perez-Garcia and W. H. Schikhof, Locally Convex Spaces over Non-Archimedean Valued Fields, Cambridge Studies in Advanced Mathematics 119, Cambridge University Press, 2010, Chapter 2.

theorem TauCeti.exists_isTOrthogonalFamily_span_image_Iio_eq {K : Type u_1} {E : Type u_2} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace K] [IsUltrametricDist E] (w : ℕ → E) {t : NNReal} (ht : t < 1) : ∃ (e : ℕ → E), IsTOrthogonalFamily K t e ∧ ∀ (n : ℕ), Submodule.span K (e '' Set.Iio n) = Submodule.span K (w '' Set.Iio n)

Approximate Gram–Schmidt process: over a complete nontrivially normed field, every sequence w in an ultrametric normed space can be replaced, for each t < 1, by a t-orthogonal sequence e with the same initial spans: span K (e '' Iio n) = span K (w '' Iio n) for every n.

theorem TauCeti.exists_isTOrthogonalBasis_of_dense_span {K : Type u_1} {E : Type u_2} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace K] [IsUltrametricDist E] {v : ℕ → E} (hv : Dense ↑(Submodule.span K (Set.range v))) {t : NNReal} (ht : t < 1) : ∃ (S : Set ℕ) (e : ↑S → E), IsTOrthogonalBasis K t e

t-orthogonal bases of spaces of countable type: over a complete nontrivially normed field, if a sequence v has dense span in an ultrametric normed space E, then for every t < 1 the space E has a t-orthogonal basis indexed by a set of natural numbers.

theorem TauCeti.exists_basis_isTOrthogonalFamily {K : Type u_1} {E : Type u_2} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace K] [IsUltrametricDist E] [FiniteDimensional K E] {t : NNReal} (ht : t < 1) : ∃ (b : Module.Basis (Fin (Module.finrank K E)) K E), IsTOrthogonalFamily K t ⇑b

t-orthogonal bases of finite-dimensional spaces: over a complete nontrivially normed field, a finite-dimensional ultrametric normed space has, for every t < 1, a basis indexed by Fin (finrank K E) which is a t-orthogonal family.

theorem TauCeti.exists_isTOrthogonalBasis_nat_of_dense_span {K : Type u_1} {E : Type u_2} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace K] [IsUltrametricDist E] (hE : ¬FiniteDimensional K E) {v : ℕ → E} (hv : Dense ↑(Submodule.span K (Set.range v))) {t : NNReal} (ht : t < 1) : ∃ (e : ℕ → E), IsTOrthogonalBasis K t e

t-orthogonal bases of infinite-dimensional spaces of countable type: over a complete nontrivially normed field, if a sequence has dense span in an infinite-dimensional ultrametric normed space E, then for every t < 1 the space E has a t-orthogonal basis indexed by ℕ.

theorem Submodule.exists_finiteDimensional_le_infDist_le {K : Type u_1} {E : Type u_2} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace K] [IsUltrametricDist E] (D G : Submodule K E) (hD : IsClosed ↑D) [FiniteDimensional K ↥G] {c : ℝ} (hc : 1 < c) : ∃ W ≤ D, FiniteDimensional K ↥W ∧ ∀ g ∈ G, Metric.infDist g ↑W ≤ c * Metric.infDist g ↑D

Relative approximation by finite-dimensional subspaces: let D be a closed subspace and G a finite-dimensional subspace of an ultrametric normed space over a complete nontrivially normed field. For every c > 1 there is a finite-dimensional subspace W ≤ D such that every g ∈ G is within c * infDist g D of W.

theorem Submodule.exists_dense_span_of_dense_span {K : Type u_1} {E : Type u_2} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace K] [IsUltrametricDist E] (D : Submodule K E) {v : ℕ → E} (hv : Dense ↑(span K (Set.range v))) : ∃ (w : ℕ → ↥D), Dense ↑(span K (Set.range w))

Subspaces of spaces of countable type: over a complete nontrivially normed field, if a sequence has dense span in an ultrametric normed space E, then every subspace D of E, closed or not, is of countable type: some sequence in D has dense span in D.