Model spaces from t-orthogonal bases

A t-orthogonal basis whose vector norms are bounded above and bounded away from zero gives continuous linear coordinates in C₀(I, K). The inverse coordinate map is the unconditional sum against the chosen basis. Every t-orthogonal basis over a nontrivially normed field can be rescaled to satisfy these bounds, using powers of a fixed scalar of norm strictly between zero and one.

Consequently every complete ultrametric space of countable type over a complete nontrivially normed field is potentially orthonormalisable. In infinite dimension its model is C₀(ℕ, K). No discreteness assumption on the value group is needed. These coordinates allow the lifting property of model spaces to be applied to spaces of countable type.

References

• P. Schneider, Nonarchimedean Functional Analysis, Springer, 2002, §10.

theorem TauCeti.IsTOrthogonalBasis.exists_zeroAtInfty_hasSum {K : Type v} [NontriviallyNormedField K] [CompleteSpace K] {E : Type u} [NormedAddCommGroup E] [NormedSpace K E] [IsUltrametricDist E] {I : Type u_1} {t : NNReal} {e : I → E} [TopologicalSpace I] [DiscreteTopology I] (he : IsTOrthogonalBasis K t e) (ht : 0 < t) {δ : ℝ} (hδ : 0 < δ) (hl : ∀ (i : I), δ ≤ ‖e i‖) (x : E) : ∃ (a : ZeroAtInftyContinuousMap I K), HasSum (fun (i : I) => a i • e i) x

For a basis with vector norms bounded away from zero, every vector has coefficients vanishing at infinity.

theorem TauCeti.IsTOrthogonalBasis.linearCombination_bijective {K : Type v} [NontriviallyNormedField K] [CompleteSpace K] {E : Type u} [NormedAddCommGroup E] [NormedSpace K E] [IsUltrametricDist E] {I : Type u_1} {t : NNReal} {e : I → E} [TopologicalSpace I] [DiscreteTopology I] (he : IsTOrthogonalBasis K t e) (ht : 0 < t) (hb : Memℓp e ⊤) {δ : ℝ} (hδ : 0 < δ) (hl : ∀ (i : I), δ ≤ ‖e i‖) [CompleteSpace E] : Function.Bijective ⇑(ZeroAtInftyContinuousMap.linearCombination K ⟨e, hb⟩)

The linear combination map of a bounded t-orthogonal basis bounded away from zero is bijective.

noncomputable def TauCeti.IsTOrthogonalBasis.equivZeroAtInfty {K : Type v} [NontriviallyNormedField K] [CompleteSpace K] {E : Type u} [NormedAddCommGroup E] [NormedSpace K E] [IsUltrametricDist E] {I : Type u_1} {t : NNReal} {e : I → E} [TopologicalSpace I] [DiscreteTopology I] (he : IsTOrthogonalBasis K t e) (ht : 0 < t) (hb : Memℓp e ⊤) {δ : ℝ} (hδ : 0 < δ) (hl : ∀ (i : I), δ ≤ ‖e i‖) [CompleteSpace E] : E ≃L[K] ZeroAtInftyContinuousMap I K

Continuous linear coordinates for a bounded t-orthogonal basis whose vector norms are bounded away from zero. The inverse is summation against the specified basis.

@[simp]

theorem TauCeti.IsTOrthogonalBasis.equivZeroAtInfty_symm_apply {K : Type v} [NontriviallyNormedField K] [CompleteSpace K] {E : Type u} [NormedAddCommGroup E] [NormedSpace K E] [IsUltrametricDist E] {I : Type u_1} {t : NNReal} {e : I → E} [TopologicalSpace I] [DiscreteTopology I] (he : IsTOrthogonalBasis K t e) (ht : 0 < t) (hb : Memℓp e ⊤) {δ : ℝ} (hδ : 0 < δ) (hl : ∀ (i : I), δ ≤ ‖e i‖) [CompleteSpace E] (a : ZeroAtInftyContinuousMap I K) : (he.equivZeroAtInfty ht hb hδ hl).symm a = ∑' (i : I), a i • e i

The inverse coordinate map is the linear combination map of the chosen basis.

theorem TauCeti.IsTOrthogonalBasis.hasSum_equivZeroAtInfty {K : Type v} [NontriviallyNormedField K] [CompleteSpace K] {E : Type u} [NormedAddCommGroup E] [NormedSpace K E] [IsUltrametricDist E] {I : Type u_1} {t : NNReal} {e : I → E} [TopologicalSpace I] [DiscreteTopology I] (he : IsTOrthogonalBasis K t e) (ht : 0 < t) (hb : Memℓp e ⊤) {δ : ℝ} (hδ : 0 < δ) (hl : ∀ (i : I), δ ≤ ‖e i‖) [CompleteSpace E] (x : E) : HasSum (fun (i : I) => ((he.equivZeroAtInfty ht hb hδ hl) x) i • e i) x

Coordinates reconstruct the vector by unconditional summation.

theorem TauCeti.IsTOrthogonalBasis.equivZeroAtInfty_apply {K : Type v} [NontriviallyNormedField K] [CompleteSpace K] {E : Type u} [NormedAddCommGroup E] [NormedSpace K E] [IsUltrametricDist E] {I : Type u_1} {t : NNReal} {e : I → E} [TopologicalSpace I] [DiscreteTopology I] (he : IsTOrthogonalBasis K t e) (ht : 0 < t) (hb : Memℓp e ⊤) {δ : ℝ} (hδ : 0 < δ) (hl : ∀ (i : I), δ ≤ ‖e i‖) [CompleteSpace E] (x : E) (i : I) : ((he.equivZeroAtInfty ht hb hδ hl) x) i = ((he.toUnconditionalSchauderBasis ht).coord i) x

The model-space coordinates agree with those of the associated unconditional Schauder basis.

theorem TauCeti.IsTOrthogonalBasis.norm_equivZeroAtInfty_apply_le {K : Type v} [NontriviallyNormedField K] [CompleteSpace K] {E : Type u} [NormedAddCommGroup E] [NormedSpace K E] [IsUltrametricDist E] {I : Type u_1} {t : NNReal} {e : I → E} [TopologicalSpace I] [DiscreteTopology I] (he : IsTOrthogonalBasis K t e) (ht : 0 < t) (hb : Memℓp e ⊤) {δ : ℝ} (hδ : 0 < δ) (hl : ∀ (i : I), δ ≤ ‖e i‖) [CompleteSpace E] (x : E) : ‖(he.equivZeroAtInfty ht hb hδ hl) x‖ ≤ (↑t * δ)⁻¹ * ‖x‖

The norm of the coordinate vector is controlled by the orthogonality constant and the uniform lower bound on the basis-vector norms.

@[simp]

theorem TauCeti.IsTOrthogonalBasis.equivZeroAtInfty_apply_basis {K : Type v} [NontriviallyNormedField K] [CompleteSpace K] {E : Type u} [NormedAddCommGroup E] [NormedSpace K E] [IsUltrametricDist E] {I : Type u_1} {t : NNReal} {e : I → E} [TopologicalSpace I] [DiscreteTopology I] (he : IsTOrthogonalBasis K t e) (ht : 0 < t) (hb : Memℓp e ⊤) {δ : ℝ} (hδ : 0 < δ) (hl : ∀ (i : I), δ ≤ ‖e i‖) [CompleteSpace E] [DecidableEq I] (i : I) : (he.equivZeroAtInfty ht hb hδ hl) (e i) = ZeroAtInftyContinuousMap.single i 1

The coordinate isomorphism sends each basis vector to the corresponding unit vector.

theorem TauCeti.IsTOrthogonalBasis.equivZeroAtInfty_apply_eq_of_hasSum {K : Type v} [NontriviallyNormedField K] [CompleteSpace K] {E : Type u} [NormedAddCommGroup E] [NormedSpace K E] [IsUltrametricDist E] {I : Type u_1} {t : NNReal} {e : I → E} [TopologicalSpace I] [DiscreteTopology I] (he : IsTOrthogonalBasis K t e) (ht : 0 < t) (hb : Memℓp e ⊤) {δ : ℝ} (hδ : 0 < δ) (hl : ∀ (i : I), δ ≤ ‖e i‖) [CompleteSpace E] {a : I → K} {x : E} (ha : HasSum (fun (i : I) => a i • e i) x) (i : I) : ((he.equivZeroAtInfty ht hb hδ hl) x) i = a i

The coordinates are the coefficients of every unconditional expansion in the basis.

theorem TauCeti.IsTOrthogonalBasis.nonempty_equivZeroAtInfty {K : Type v} [NontriviallyNormedField K] [CompleteSpace K] {E : Type u} [NormedAddCommGroup E] [NormedSpace K E] [IsUltrametricDist E] {I : Type u_1} {t : NNReal} {e : I → E} [CompleteSpace E] [TopologicalSpace I] [DiscreteTopology I] (he : IsTOrthogonalBasis K t e) (ht : 0 < t) : Nonempty (E ≃L[K] ZeroAtInftyContinuousMap I K)

Every complete ultrametric space with a t-orthogonal basis, t > 0, is continuously linearly equivalent to the model space with the same index type.

theorem TauCeti.nonempty_continuousLinearEquiv_zeroAtInfty_nat_of_dense_span {K : Type v} [NontriviallyNormedField K] [CompleteSpace K] {E : Type u} [NormedAddCommGroup E] [NormedSpace K E] [IsUltrametricDist E] [CompleteSpace E] (hE : ¬FiniteDimensional K E) {v : ℕ → E} (hv : Dense ↑(Submodule.span K (Set.range v))) : Nonempty (E ≃L[K] ZeroAtInftyContinuousMap ℕ K)

An infinite-dimensional ultrametric Banach space of countable type (some sequence has dense span) over a complete nontrivially normed field is continuously linearly equivalent to C₀(ℕ, K).

theorem TauCeti.isPotentiallyONable_of_dense_span {K : Type v} [NontriviallyNormedField K] [CompleteSpace K] {E : Type u} [NormedAddCommGroup E] [NormedSpace K E] [IsUltrametricDist E] [CompleteSpace E] {v : ℕ → E} (hv : Dense ↑(Submodule.span K (Set.range v))) : IsPotentiallyONable K E

Every ultrametric Banach space of countable type over a complete nontrivially normed field is potentially orthonormalisable, including finite-dimensional and zero spaces.