Orthonormal bases of nonarchimedean normed modules

Let R be a normed ring and M a normed R-module. A family e : I → M is orthonormal (TauCeti.IsOrthonormalFamily R e) if the norm of every finite linear combination is the maximum of the norms of its coefficients:

‖∑ i ∈ s, a i • e i‖ = max_{i ∈ s} ‖a i‖,

with the empty maximum zero. The condition is on the norms of the scalar coefficients, not on the norms of the terms a i • e i; over a ring the latter, weaker, condition would allow torsion. An orthonormal basis (TauCeti.IsOrthonormalBasis R e) is an orthonormal family whose span is dense. This is neither a Hamel basis nor an orthonormal basis of an inner product space: the vectors of M are the convergent infinite combinations of the e i.

Perturbing each vector of an orthonormal family by norm less than one preserves orthonormality (IsOrthonormalFamily.of_norm_sub_lt_one). The bound can depend on the index; only finitely many errors occur in each linear combination.

Over a ring satisfying the strong rank condition, a dense-range continuous linear map from a module with an I-indexed dense spanning family to a module with a J-indexed orthonormal family implies #J ≤ #I (IsOrthonormalFamily.lift_mk_le_of_denseRange). Consequently orthonormal bases of continuously linearly equivalent ultrametric modules have equally many vectors (IsOrthonormalBasis.lift_mk_eq_of_continuousLinearEquiv), without any completeness assumption.

The model example is the family of unit coordinate vectors single i 1 of C₀(I, R) (TauCeti.isOrthonormalBasis_single_one), and every orthonormal basis is of this form: over a complete ring R and for a complete ultrametric module M with contractive scalar action,

• an orthonormal family e defines the linear isometry IsOrthonormalFamily.linearIsometry : C₀(I, R) →ₗᵢ[R] M, a ↦ ∑' i, a i • e i;
• for an orthonormal basis it is surjective, and its inverse IsOrthonormalBasis.repr : M ≃ₗᵢ[R] C₀(I, R) sends x to its coefficients: x is the unconditional sum of the repr x i • e i (IsOrthonormalBasis.hasSum_repr_smul), these are its only unconditional expansion in the e i (IsOrthonormalBasis.repr_apply_of_hasSum), and repr (e i) = single i 1;
• conversely a linear isometry c : M ≃ₗᵢ[R] C₀(I, R) pulls the coordinate vectors back to the orthonormal basis i ↦ c.symm (single i 1), whose coefficient isometry is c again.

Thus a chosen basis and a chosen model isometry determine each other (TauCeti.exists_isOrthonormalBasis_iff), and a module is orthonormalisable (TauCeti.IsONable R M), that is linearly isometric to some C₀(I, R), exactly when it has an orthonormal basis (TauCeti.isONable_iff_exists_isOrthonormalBasis); the model spaces themselves are orthonormalisable for index types in every universe (TauCeti.isONable_zeroAtInfty). Completeness is essential: the finitely supported families in C₀(ℕ, ℚ_[p]) contain the coordinate vectors, which are orthonormal with dense span, but they do not form a complete space: the partial sums of ∑' n, p ^ n • single n 1 are finitely supported, but their limit is not. Some nondiscreteness of R is needed here: over a finite field with the trivial norm, every family tending to zero is finitely supported.

These characterisations need neither commutativity of R nor a norm-one or ultrametric hypothesis on R; the ultrametric inequality is assumed on M, where it makes the series ∑' i, a i • e i converge.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §1.
• P. Schneider, Nonarchimedean Functional Analysis, Springer, 2002, §10.
• K. Buzzard, Eigenvarieties, in L-functions and Galois Representations, LMS Lecture Note Series 320 (2007), §2.

def TauCeti.IsOrthonormalFamily (R : Type u_1) {I : Type u_2} {M : Type u_3} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] (e : I → M) : Prop

A family e : I → M is orthonormal if the norm of every finite linear combination ∑ i ∈ s, a i • e i is the maximum s.sup fun i ↦ ‖a i‖₊ of the norms of its coefficients, with the empty maximum zero.

theorem TauCeti.isOrthonormalFamily_def {R : Type u_1} {I : Type u_2} {M : Type u_3} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {e : I → M} : IsOrthonormalFamily R e ↔ ∀ (s : Finset I) (a : I → R), ‖∑ i ∈ s, a i • e i‖₊ = s.sup fun (i : I) => ‖a i‖₊

An orthonormal family is characterized by the norm formula for every finite linear combination. This is the introduction and elimination interface for IsOrthonormalFamily.

structure TauCeti.IsOrthonormalBasis (R : Type u_1) {I : Type u_2} {M : Type u_3} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] (e : I → M) : Prop

An orthonormal basis of a normed module is an orthonormal family whose span is dense.

• isOrthonormalFamily : IsOrthonormalFamily R e

  An orthonormal basis is an orthonormal family.

• dense_span : Dense ↑(Submodule.span R (Set.range e))

  The span of an orthonormal basis is dense.

def TauCeti.IsONable (R : Type u_1) [SeminormedRing R] (M : Type u) [SeminormedAddCommGroup M] [Module R M] : Prop

A normed module is orthonormalisable if it is linearly isometric to a model space C₀(I, R) of families on a discrete index type tending to zero along the cofinite filter.

theorem TauCeti.isONable_def (R : Type u_1) [SeminormedRing R] (M : Type u) [SeminormedAddCommGroup M] [Module R M] : IsONable R M ↔ ∃ (I : Type u) (x : TopologicalSpace I) (_ : DiscreteTopology I), Nonempty (M ≃ₗᵢ[R] ZeroAtInftyContinuousMap I R)

A module is orthonormalisable exactly when it is linearly isometric to C₀(I, R) for some discrete index type I. This is the introduction and elimination interface for IsONable.

theorem TauCeti.isONable_zeroAtInfty {R : Type u_1} (I : Type u_2) [SeminormedRing R] [TopologicalSpace I] [DiscreteTopology I] : IsONable R (ZeroAtInftyContinuousMap I R)

A model space C₀(I, R) is orthonormalisable, for an index type I in any universe.

theorem TauCeti.IsOrthonormalFamily.norm_sum_smul {R : Type u_1} {I : Type u_2} {M : Type u_3} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {e : I → M} (he : IsOrthonormalFamily R e) (s : Finset I) (a : I → R) : ‖∑ i ∈ s, a i • e i‖ = ↑(s.sup fun (i : I) => ‖a i‖₊)

The norm of a finite linear combination of an orthonormal family, as a real number.

theorem TauCeti.IsOrthonormalFamily.norm_le_norm_sum_smul {R : Type u_1} {I : Type u_2} {M : Type u_3} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {e : I → M} (he : IsOrthonormalFamily R e) {s : Finset I} (a : I → R) {i : I} (hi : i ∈ s) : ‖a i‖ ≤ ‖∑ i ∈ s, a i • e i‖

A coefficient of a finite linear combination of an orthonormal family has norm at most the norm of the combination.

theorem TauCeti.IsOrthonormalFamily.norm_smul {R : Type u_1} {I : Type u_2} {M : Type u_3} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {e : I → M} (he : IsOrthonormalFamily R e) (i : I) (r : R) : ‖r • e i‖ = ‖r‖

A multiple of a vector of an orthonormal family has the norm of its coefficient.

theorem TauCeti.IsOrthonormalFamily.norm_apply {R : Type u_1} {I : Type u_2} {M : Type u_3} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {e : I → M} (he : IsOrthonormalFamily R e) (i : I) : ‖e i‖ = ‖1‖

A vector of an orthonormal family has the norm of 1 : R.

theorem TauCeti.IsOrthonormalFamily.norm_apply_eq_one {R : Type u_1} {I : Type u_2} {M : Type u_3} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {e : I → M} [NormOneClass R] (he : IsOrthonormalFamily R e) (i : I) : ‖e i‖ = 1

Over a norm-one ring, the vectors of an orthonormal family are unit vectors.

theorem TauCeti.IsOrthonormalFamily.map {R : Type u_1} {I : Type u_2} {M : Type u_3} {N : Type u_4} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {e : I → M} [SeminormedAddCommGroup N] [Module R N] (he : IsOrthonormalFamily R e) (u : M →ₗᵢ[R] N) : IsOrthonormalFamily R (⇑u ∘ e)

The image of an orthonormal family under a linear isometry is orthonormal.

theorem TauCeti.IsOrthonormalFamily.of_norm_sub_lt_one {R : Type u_1} {I : Type u_2} {M : Type u_3} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] {e v : I → M} (he : IsOrthonormalFamily R e) (hv : ∀ (i : I), ‖e i - v i‖ < 1) : IsOrthonormalFamily R v

Perturbing each vector of an orthonormal family by less than one preserves orthonormality in an ultrametric module. No uniform bound strictly below one is needed.

theorem TauCeti.IsOrthonormalFamily.linearIndependent {R : Type u_1} {I : Type u_2} {M : Type u_3} [NormedRing R] [SeminormedAddCommGroup M] [Module R M] {e : I → M} (he : IsOrthonormalFamily R e) : LinearIndependent R e

An orthonormal family over a normed ring is linearly independent.

theorem TauCeti.IsOrthonormalFamily.lift_mk_le_of_denseRange {R : Type u_1} {M : Type u_3} {N : Type u_4} {I : Type u} {J : Type v} [NormedRing R] [StrongRankCondition R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] [IsUltrametricDist N] {b : I → M} {e : J → N} (he : IsOrthonormalFamily R e) (hb : Dense ↑(Submodule.span R (Set.range b))) (f : M →L[R] N) (hf : DenseRange ⇑f) : Cardinal.lift.{u, v} (Cardinal.mk J) ≤ Cardinal.lift.{v, u} (Cardinal.mk I)

An orthonormal family in the target of a dense-range continuous linear map has cardinality at most that of any dense spanning family in the source.

theorem TauCeti.IsOrthonormalFamily.memℓp_infty {R : Type u_1} {I : Type u_2} {M : Type u_3} [SeminormedRing R] [NormedAddCommGroup M] [Module R M] {e : I → M} (he : IsOrthonormalFamily R e) : Memℓp e ⊤

An orthonormal family is bounded.

theorem TauCeti.IsOrthonormalFamily.norm_tsum_smul {R : Type u_1} {I : Type u_2} {M : Type u_3} [SeminormedRing R] [NormedAddCommGroup M] [Module R M] {e : I → M} (he : IsOrthonormalFamily R e) [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [TopologicalSpace I] [DiscreteTopology I] (a : ZeroAtInftyContinuousMap I R) : ‖∑' (i : I), a i • e i‖ = ‖a‖

Isometric coefficient expansion: for an orthonormal family e and a family a tending to zero, the norm of ∑' i, a i • e i is the sup norm of a.

noncomputable def TauCeti.IsOrthonormalFamily.linearIsometry {R : Type u_1} {I : Type u_2} {M : Type u_3} [SeminormedRing R] [NormedAddCommGroup M] [Module R M] {e : I → M} (he : IsOrthonormalFamily R e) [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [TopologicalSpace I] [DiscreteTopology I] : ZeroAtInftyContinuousMap I R →ₗᵢ[R] M

The coefficient isometry of an orthonormal family e in a complete ultrametric module: the linear isometry C₀(I, R) →ₗᵢ[R] M sending a to ∑' i, a i • e i. Its underlying continuous linear map is ZeroAtInftyContinuousMap.linearCombination.

theorem TauCeti.IsOrthonormalFamily.toContinuousLinearMap_linearIsometry {R : Type u_1} {I : Type u_2} {M : Type u_3} [SeminormedRing R] [NormedAddCommGroup M] [Module R M] {e : I → M} (he : IsOrthonormalFamily R e) [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [TopologicalSpace I] [DiscreteTopology I] : he.linearIsometry.toContinuousLinearMap = ZeroAtInftyContinuousMap.linearCombination R ⟨e, ⋯⟩

The coefficient isometry of an orthonormal family is its linear combination map.

theorem TauCeti.IsOrthonormalFamily.linearIsometry_apply {R : Type u_1} {I : Type u_2} {M : Type u_3} [SeminormedRing R] [NormedAddCommGroup M] [Module R M] {e : I → M} (he : IsOrthonormalFamily R e) [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [TopologicalSpace I] [DiscreteTopology I] (a : ZeroAtInftyContinuousMap I R) : he.linearIsometry a = ∑' (i : I), a i • e i

The value of the coefficient isometry is the sum ∑' i, a i • e i.

theorem TauCeti.IsOrthonormalFamily.hasSum_linearIsometry {R : Type u_1} {I : Type u_2} {M : Type u_3} [SeminormedRing R] [NormedAddCommGroup M] [Module R M] {e : I → M} (he : IsOrthonormalFamily R e) [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [TopologicalSpace I] [DiscreteTopology I] (a : ZeroAtInftyContinuousMap I R) : HasSum (fun (i : I) => a i • e i) (he.linearIsometry a)

The coefficient isometry he.linearIsometry a is the unconditional sum of the a i • e i.

@[simp]

theorem TauCeti.IsOrthonormalFamily.linearIsometry_single {R : Type u_1} {I : Type u_2} {M : Type u_3} [SeminormedRing R] [NormedAddCommGroup M] [Module R M] {e : I → M} (he : IsOrthonormalFamily R e) [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] (i : I) (r : R) : he.linearIsometry (ZeroAtInftyContinuousMap.single i r) = r • e i

The coefficient isometry sends the coordinate vector single i r to r • e i.

theorem TauCeti.IsOrthonormalBasis.lift_mk_eq_of_continuousLinearEquiv {R : Type u_1} {M : Type u_3} {N : Type u_4} {I : Type u} {J : Type v} [NormedRing R] [StrongRankCondition R] [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [SeminormedAddCommGroup N] [Module R N] [IsBoundedSMul R N] [IsUltrametricDist N] {b : I → M} {e : J → N} (hb : IsOrthonormalBasis R b) (he : IsOrthonormalBasis R e) (f : M ≃L[R] N) : Cardinal.lift.{v, u} (Cardinal.mk I) = Cardinal.lift.{u, v} (Cardinal.mk J)

Orthonormal bases of continuously linearly equivalent ultrametric modules have index types of equal cardinality, without assuming completeness.

theorem TauCeti.IsOrthonormalBasis.lift_mk_eq {R : Type u_1} {M : Type u_3} {I : Type u} {J : Type v} [NormedRing R] [StrongRankCondition R] [SeminormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] {b : I → M} {e : J → M} (hb : IsOrthonormalBasis R b) (he : IsOrthonormalBasis R e) : Cardinal.lift.{v, u} (Cardinal.mk I) = Cardinal.lift.{u, v} (Cardinal.mk J)

Any two orthonormal bases of an ultrametric module have index types of equal cardinality, without assuming completeness.

theorem TauCeti.IsOrthonormalBasis.map {R : Type u_1} {I : Type u_2} {M : Type u_3} {N : Type u_4} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] [SeminormedAddCommGroup N] [Module R N] {e : I → M} (he : IsOrthonormalBasis R e) (u : M ≃ₗᵢ[R] N) : IsOrthonormalBasis R (⇑u ∘ e)

The image of an orthonormal basis under a linear isometry equivalence is an orthonormal basis.

theorem TauCeti.IsOrthonormalBasis.surjective_linearIsometry {R : Type u_1} {I : Type u_2} {M : Type u_3} [NormedRing R] [CompleteSpace R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [TopologicalSpace I] [DiscreteTopology I] {e : I → M} (he : IsOrthonormalBasis R e) : Function.Surjective ⇑⋯.linearIsometry

Over a complete ring, the coefficient isometry of an orthonormal basis is surjective.

noncomputable def TauCeti.IsOrthonormalBasis.repr {R : Type u_1} {I : Type u_2} {M : Type u_3} [NormedRing R] [CompleteSpace R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [TopologicalSpace I] [DiscreteTopology I] {e : I → M} (he : IsOrthonormalBasis R e) : M ≃ₗᵢ[R] ZeroAtInftyContinuousMap I R

The coefficient isometry of an orthonormal basis e of a complete ultrametric module over a complete ring: the linear isometry equivalence M ≃ₗᵢ[R] C₀(I, R) sending a vector to the family of its coefficients in the basis. It is inverse to a ↦ ∑' i, a i • e i.

theorem TauCeti.IsOrthonormalBasis.repr_symm_apply {R : Type u_1} {I : Type u_2} {M : Type u_3} [NormedRing R] [CompleteSpace R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [TopologicalSpace I] [DiscreteTopology I] {e : I → M} (he : IsOrthonormalBasis R e) (a : ZeroAtInftyContinuousMap I R) : he.repr.symm a = ⋯.linearIsometry a

The inverse of the coefficient isometry is the sum a ↦ ∑' i, a i • e i.

theorem TauCeti.IsOrthonormalBasis.hasSum_repr_smul {R : Type u_1} {I : Type u_2} {M : Type u_3} [NormedRing R] [CompleteSpace R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [TopologicalSpace I] [DiscreteTopology I] {e : I → M} (he : IsOrthonormalBasis R e) (x : M) : HasSum (fun (i : I) => (he.repr x) i • e i) x

Unconditional expansion in an orthonormal basis: every vector x is the unconditional sum of the he.repr x i • e i.

@[simp]

theorem TauCeti.IsOrthonormalBasis.repr_self {R : Type u_1} {I : Type u_2} {M : Type u_3} [NormedRing R] [CompleteSpace R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [TopologicalSpace I] [DiscreteTopology I] {e : I → M} (he : IsOrthonormalBasis R e) [DecidableEq I] (i : I) : he.repr (e i) = ZeroAtInftyContinuousMap.single i 1

The coefficients of the basis vector e i are those of the coordinate vector single i 1.

theorem TauCeti.IsOrthonormalBasis.repr_apply_of_hasSum {R : Type u_1} {I : Type u_2} {M : Type u_3} [NormedRing R] [CompleteSpace R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [TopologicalSpace I] [DiscreteTopology I] {e : I → M} (he : IsOrthonormalBasis R e) {a : I → R} {x : M} (h : HasSum (fun (i : I) => a i • e i) x) (i : I) : (he.repr x) i = a i

Uniqueness of the expansion in an orthonormal basis: if x is the unconditional sum of the a i • e i for some family a : I → R, then a is the family of coefficients of x.

theorem TauCeti.isOrthonormalBasis_single_one {R : Type u_1} {I : Type u_2} [SeminormedRing R] [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] : IsOrthonormalBasis R fun (i : I) => ZeroAtInftyContinuousMap.single i 1

The unit coordinate vectors single i 1 form an orthonormal basis of the model space C₀(I, R).

theorem LinearIsometryEquiv.isOrthonormalBasis_symm_single {R : Type u_1} {I : Type u_2} {M : Type u_3} [SeminormedRing R] [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [SeminormedAddCommGroup M] [Module R M] (c : M ≃ₗᵢ[R] ZeroAtInftyContinuousMap I R) : TauCeti.IsOrthonormalBasis R fun (i : I) => c.symm (ZeroAtInftyContinuousMap.single i 1)

The pullback i ↦ c.symm (single i 1) of the coordinate vectors along a linear isometry c : M ≃ₗᵢ[R] C₀(I, R) is an orthonormal basis of M.

@[simp]

theorem TauCeti.repr_isOrthonormalBasis_single_one {R : Type u_1} {I : Type u_2} [NormedRing R] [CompleteSpace R] [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [IsUltrametricDist R] : ⋯.repr = LinearIsometryEquiv.refl R (ZeroAtInftyContinuousMap I R)

Over a complete ultrametric ring, the coefficient isometry of the coordinate vectors of C₀(I, R) is the identity.

@[simp]

theorem LinearIsometryEquiv.repr_isOrthonormalBasis_symm_single {R : Type u_1} {I : Type u_2} {M : Type u_3} [NormedRing R] [CompleteSpace R] [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] (c : M ≃ₗᵢ[R] ZeroAtInftyContinuousMap I R) : ⋯.repr = c

The coefficient isometry of the pullback of the coordinate vectors along a linear isometry c : M ≃ₗᵢ[R] C₀(I, R) is c itself.

theorem TauCeti.exists_isOrthonormalBasis_iff {R : Type u_1} {I : Type u_2} {M : Type u_3} [NormedRing R] [CompleteSpace R] [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] [TopologicalSpace I] [DiscreteTopology I] : (∃ (e : I → M), IsOrthonormalBasis R e) ↔ Nonempty (M ≃ₗᵢ[R] ZeroAtInftyContinuousMap I R)

Orthonormal bases are model isometries: over a complete ring, a complete ultrametric module with contractive scalar action has an orthonormal basis indexed by I exactly when it is linearly isometric to C₀(I, R).

theorem TauCeti.isONable_iff_exists_isOrthonormalBasis {R : Type u_1} [NormedRing R] [CompleteSpace R] {M : Type u} [NormedAddCommGroup M] [Module R M] [IsBoundedSMul R M] [IsUltrametricDist M] [CompleteSpace M] : IsONable R M ↔ ∃ (I : Type u) (e : I → M), IsOrthonormalBasis R e

Orthonormalisable modules are those with an orthonormal basis: over a complete ring, a complete ultrametric module with contractive scalar action is linearly isometric to a model space C₀(I, R) exactly when it has an orthonormal basis.