t-orthogonal families and bases of nonarchimedean normed modules

Let R be a normed ring, M a normed R-module and t a nonnegative real number. A family e : I → M is t-orthogonal (TauCeti.IsTOrthogonalFamily R t e) if every finite linear combination satisfies

t * max_{i ∈ s} ‖a i • e i‖ ≤ ‖∑ i ∈ s, a i • e i‖,

with the empty maximum zero. In an ultrametric module the reverse inequality with t = 1 always holds, so 1-orthogonality is the familiar condition that the norm of a combination is the largest norm of its terms (TauCeti.isTOrthogonalFamily_one_iff); an orthonormal family is 1-orthogonal. For 0 < t < 1 the condition is the approximate orthogonality with which bases of Banach spaces of countable type are built over an arbitrary complete nonarchimedean field, where exactly orthogonal bases need not exist.

A t-orthogonal basis (TauCeti.IsTOrthogonalBasis R t e) is a t-orthogonal family of nonzero vectors with dense span. The main results are:

• TauCeti.IsTOrthogonalFamily.mul_iSup_norm_smul_le_of_hasSum: t-orthogonality passes to unconditional sums, t * ⨆ i, ‖a i • e i‖ ≤ ‖∑' i, a i • e i‖; together with the ultrametric bound IsUltrametricDist.norm_tsum_le this pins the norm of an infinite combination between t times the largest norm of its terms and that largest norm;
• TauCeti.IsTOrthogonalBasis.exists_hasSum and TauCeti.IsTOrthogonalBasis.eq_of_hasSum: for t > 0, over a complete normed ring acting norm-multiplicatively on an ultrametric module, every vector is the unconditional sum of a unique family a i • e i;
• TauCeti.IsTOrthogonalBasis.toUnconditionalSchauderBasis: over a complete nontrivially normed field K, a t-orthogonal basis with t > 0 is an unconditional Schauder basis in the sense of Mathlib's UnconditionalSchauderBasis, whose coordinate functionals satisfy t * ‖coord i x‖ * ‖e i‖ ≤ ‖x‖ and ‖coord i x‖ * ‖e i‖ → 0 along the cofinite filter.

Existence and uniqueness of expansions need neither completeness of M nor a discrete valuation. Completeness of M is used only in TauCeti.IsTOrthogonalBasis.coord_tsum, to sum an arbitrary family of coefficients with ‖a i‖ * ‖e i‖ → 0, so that the coordinates identify M with such families. The comparison with Mathlib's Schauder bases lets the general projection theory of GeneralSchauderBasis apply to t-orthogonal bases without being duplicated here.

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.

def TauCeti.IsTOrthogonalFamily (R : Type u_1) {I : Type u_3} {M : Type u_5} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] (t : NNReal) (e : I → M) : Prop

A family e : I → M is t-orthogonal if for every finite linear combination ∑ i ∈ s, a i • e i, the product of t with the largest norm s.sup fun i ↦ ‖a i • e i‖₊ of its terms (the empty maximum being zero) is at most the norm of the combination.

theorem TauCeti.isTOrthogonalFamily_def {R : Type u_1} {I : Type u_3} {M : Type u_5} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {t : NNReal} {e : I → M} : IsTOrthogonalFamily R t e ↔ ∀ (s : Finset I) (a : I → R), (t * s.sup fun (i : I) => ‖a i • e i‖₊) ≤ ‖∑ i ∈ s, a i • e i‖₊

A t-orthogonal family is characterized by the lower bound for every finite linear combination. This is the introduction and elimination interface for IsTOrthogonalFamily.

structure TauCeti.IsTOrthogonalBasis (R : Type u_1) {I : Type u_3} {M : Type u_5} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] (t : NNReal) (e : I → M) : Prop

A t-orthogonal basis of a normed module is a t-orthogonal family of nonzero vectors whose span is dense.

• isTOrthogonalFamily : IsTOrthogonalFamily R t e

  A t-orthogonal basis is a t-orthogonal family.

• ne_zero (i : I) : e i ≠ 0

  The vectors of a t-orthogonal basis are nonzero.

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

  The span of a t-orthogonal basis is dense.

@[simp]

theorem TauCeti.isTOrthogonalFamily_zero {R : Type u_1} {I : Type u_3} {M : Type u_5} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] (e : I → M) : IsTOrthogonalFamily R 0 e

Every family is 0-orthogonal.

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

In an ultrametric module a family is 1-orthogonal exactly when the norm of every finite linear combination is the largest norm of its terms.

theorem TauCeti.IsTOrthogonalFamily.mono {R : Type u_1} {I : Type u_3} {M : Type u_5} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {t t' : NNReal} {e : I → M} (he : IsTOrthogonalFamily R t e) (h : t' ≤ t) : IsTOrthogonalFamily R t' e

A t-orthogonal family is t'-orthogonal for every t' ≤ t.

theorem TauCeti.IsTOrthogonalFamily.mul_norm_smul_le {R : Type u_1} {I : Type u_3} {M : Type u_5} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {t : NNReal} {e : I → M} (he : IsTOrthogonalFamily R t e) {s : Finset I} {i : I} (hi : i ∈ s) (a : I → R) : ↑t * ‖a i • e i‖ ≤ ‖∑ j ∈ s, a j • e j‖

In a finite linear combination of a t-orthogonal family, t times the norm of each term is at most the norm of the combination.

theorem TauCeti.IsTOrthogonalFamily.mul_norm_smul_le_norm_linearCombination {R : Type u_1} {I : Type u_3} {M : Type u_5} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {t : NNReal} {e : I → M} (he : IsTOrthogonalFamily R t e) (c : I →₀ R) (i : I) : ↑t * ‖c i • e i‖ ≤ ‖(Finsupp.linearCombination R e) c‖

The finitely supported version of IsTOrthogonalFamily.mul_norm_smul_le: t times the norm of each term of a finitely supported combination is at most the norm of the combination.

theorem TauCeti.IsTOrthogonalFamily.comp {R : Type u_1} {I : Type u_3} {J : Type u_4} {M : Type u_5} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {t : NNReal} {e : I → M} (he : IsTOrthogonalFamily R t e) {f : J → I} (hf : Function.Injective f) : IsTOrthogonalFamily R t (e ∘ f)

Reindexing a t-orthogonal family along an injective map gives a t-orthogonal family.

theorem TauCeti.IsTOrthogonalFamily.map {R : Type u_1} {I : Type u_3} {M : Type u_5} {N : Type u_6} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {t : NNReal} {e : I → M} [SeminormedAddCommGroup N] [Module R N] (he : IsTOrthogonalFamily R t e) (u : M →ₗᵢ[R] N) : IsTOrthogonalFamily R t (⇑u ∘ e)

The image of a t-orthogonal family under a linear isometry is t-orthogonal.

theorem TauCeti.IsTOrthogonalFamily.mul_norm_smul_le_of_hasSum {R : Type u_1} {I : Type u_3} {M : Type u_5} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {t : NNReal} {e : I → M} (he : IsTOrthogonalFamily R t e) {a : I → R} {x : M} (h : HasSum (fun (i : I) => a i • e i) x) (i : I) : ↑t * ‖a i • e i‖ ≤ ‖x‖

t-orthogonality of unconditional sums: if x is the unconditional sum of the a i • e i for a t-orthogonal family e, then t times the norm of each term is at most ‖x‖.

theorem TauCeti.IsTOrthogonalFamily.mul_iSup_norm_smul_le_of_hasSum {R : Type u_1} {I : Type u_3} {M : Type u_5} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {t : NNReal} {e : I → M} (he : IsTOrthogonalFamily R t e) {a : I → R} {x : M} (h : HasSum (fun (i : I) => a i • e i) x) : ↑t * ⨆ (i : I), ‖a i • e i‖ ≤ ‖x‖

t-orthogonality of unconditional sums, supremum form: if x is the unconditional sum of the a i • e i for a t-orthogonal family e, then t * ⨆ i, ‖a i • e i‖ ≤ ‖x‖. The reverse ultrametric bound ‖x‖ ≤ ⨆ i, ‖a i • e i‖ is IsUltrametricDist.norm_tsum_le.

theorem TauCeti.IsTOrthogonalFamily.linearIndependent {R : Type u_1} {I : Type u_3} {M : Type u_5} [SeminormedRing R] [NormedAddCommGroup M] [Module R M] {t : NNReal} {e : I → M} [NoZeroSMulDivisors R M] (he : IsTOrthogonalFamily R t e) (ht : 0 < t) (h0 : ∀ (i : I), e i ≠ 0) : LinearIndependent R e

A t-orthogonal family of nonzero vectors with t > 0 is linearly independent over a ring acting without zero divisors.

theorem TauCeti.IsTOrthogonalFamily.smul_eq_smul_of_hasSum {R : Type u_1} {I : Type u_3} {M : Type u_5} [SeminormedRing R] [NormedAddCommGroup M] [Module R M] {t : NNReal} {e : I → M} (he : IsTOrthogonalFamily R t e) (ht : 0 < t) {a b : I → R} {x : M} (ha : HasSum (fun (i : I) => a i • e i) x) (hb : HasSum (fun (i : I) => b i • e i) x) (i : I) : a i • e i = b i • e i

Uniqueness of terms of expansions: for a t-orthogonal family with t > 0, two unconditional expansions ∑ a i • e i and ∑ b i • e i of the same vector have the same terms.

theorem TauCeti.IsOrthonormalFamily.isTOrthogonalFamily {R : Type u_1} {I : Type u_3} {M : Type u_5} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {e : I → M} (he : IsOrthonormalFamily R e) {t : NNReal} (ht : t ≤ 1) : IsTOrthogonalFamily R t e

An orthonormal family is t-orthogonal for every t ≤ 1.

theorem TauCeti.IsOrthonormalBasis.isTOrthogonalBasis {R : Type u_1} {I : Type u_3} {M : Type u_5} [NormedRing R] [Nontrivial R] [SeminormedAddCommGroup M] [Module R M] {e : I → M} (he : IsOrthonormalBasis R e) {t : NNReal} (ht : t ≤ 1) : IsTOrthogonalBasis R t e

Over a nontrivial normed ring, an orthonormal basis is a t-orthogonal basis for every t ≤ 1.

theorem TauCeti.mul_max_nnnorm_le_nnnorm_smul_add {K : Type u_2} {M : Type u_5} [NormedField K] [NormedAddCommGroup M] [NormedSpace K M] [IsUltrametricDist M] {F : Submodule K M} {w : M} {r : NNReal} (hr : r ≤ 1) (hw : ∀ z ∈ F, r * ‖w‖₊ ≤ ‖w - z‖₊) (c : K) {z : M} (hz : z ∈ F) : r * max ‖c • w‖₊ ‖z‖₊ ≤ ‖c • w + z‖₊

If w is r-orthogonal to a submodule F (that is, r * ‖w‖ ≤ ‖w - z‖ for z ∈ F) with r ≤ 1, then in an ultrametric space r * max ‖c • w‖ ‖z‖ ≤ ‖c • w + z‖ for every scalar c and every z ∈ F.

theorem TauCeti.IsTOrthogonalFamily.finCons {K : Type u_2} {M : Type u_5} [NormedField K] [NormedAddCommGroup M] [NormedSpace K M] [IsUltrametricDist M] {n : ℕ} {e : Fin n → M} (he : IsTOrthogonalFamily K 1 e) {w : M} (hw : ∀ z ∈ Submodule.span K (Set.range e), ‖w‖ ≤ ‖w - z‖) : IsTOrthogonalFamily K 1 (Fin.cons w e)

Adjoining a vector orthogonal to the span of a finite orthogonal family preserves orthogonality. Zero vectors are allowed.

theorem TauCeti.isTOrthogonalFamily_Iio_of_mul_nnnorm_le_nnnorm_sub {K : Type u_2} {M : Type u_5} [NormedField K] [NormedAddCommGroup M] [NormedSpace K M] [IsUltrametricDist M] {e : ℕ → M} {T : ℕ → NNReal} (hT : Antitone T) (hT' : ∀ (n : ℕ), 0 < T n ∧ T n ≤ 1) (he : ∀ (N : ℕ), ∀ z ∈ Submodule.span K (e '' Set.Iio N), T (N + 1) / T N * ‖e N‖₊ ≤ ‖e N - z‖₊) (N : ℕ) : IsTOrthogonalFamily K (T N) fun (i : ↑(Set.Iio N)) => e ↑i

If each e N is T (N + 1) / T N-orthogonal to the span of the previous vectors, for a non-increasing sequence T of positive constants at most one, then in an ultrametric space the vectors e i with i < N form a T N-orthogonal family.

theorem TauCeti.IsTOrthogonalBasis.comp_equiv {R : Type u_1} {I : Type u_3} {J : Type u_4} {M : Type u_5} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] {t : NNReal} {e : I → M} (he : IsTOrthogonalBasis R t e) (σ : J ≃ I) : IsTOrthogonalBasis R t (e ∘ ⇑σ)

Reindexing a t-orthogonal basis along an equivalence gives a t-orthogonal basis.

theorem TauCeti.IsTOrthogonalBasis.eq_of_hasSum {R : Type u_1} {I : Type u_3} {M : Type u_5} [SeminormedRing R] [NormedAddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {t : NNReal} {e : I → M} (he : IsTOrthogonalBasis R t e) (ht : 0 < t) {a b : I → R} {x : M} (ha : HasSum (fun (i : I) => a i • e i) x) (hb : HasSum (fun (i : I) => b i • e i) x) : a = b

Uniqueness of expansions in a t-orthogonal basis: for t > 0, over a ring acting without zero divisors, two unconditional expansions ∑ a i • e i and ∑ b i • e i of the same vector have the same coefficients.

theorem TauCeti.IsTOrthogonalBasis.exists_hasSum {R : Type u_1} {I : Type u_3} {M : Type u_5} [NormedRing R] [NormedAddCommGroup M] [Module R M] [NormSMulClass R M] {t : NNReal} {e : I → M} [CompleteSpace R] [IsUltrametricDist M] (he : IsTOrthogonalBasis R t e) (ht : 0 < t) (x : M) : ∃ (a : I → R), HasSum (fun (i : I) => a i • e i) x

Existence of expansions in a t-orthogonal basis: for t > 0, over a complete normed ring acting norm-multiplicatively on an ultrametric module, every vector x is the unconditional sum of a family a i • e i. Completeness of the module is not needed.

theorem TauCeti.IsTOrthogonalBasis.existsUnique_hasSum {R : Type u_1} {I : Type u_3} {M : Type u_5} [NormedRing R] [NormedAddCommGroup M] [Module R M] [NormSMulClass R M] {t : NNReal} {e : I → M} [CompleteSpace R] [IsUltrametricDist M] (he : IsTOrthogonalBasis R t e) (ht : 0 < t) (x : M) : ∃! a : I → R, HasSum (fun (i : I) => a i • e i) x

Expansions in a t-orthogonal basis: for t > 0, over a complete normed ring acting norm-multiplicatively on an ultrametric module, every vector is the unconditional sum of the a i • e i for exactly one family of coefficients a.

noncomputable def TauCeti.IsTOrthogonalBasis.toUnconditionalSchauderBasis {K : Type u_2} {I : Type u_3} {M : Type u_5} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup M] [NormedSpace K M] [IsUltrametricDist M] {t : NNReal} {e : I → M} (he : IsTOrthogonalBasis K t e) (ht : 0 < t) : UnconditionalSchauderBasis I K M

A t-orthogonal basis is an unconditional Schauder basis: for t > 0, a t-orthogonal basis e of an ultrametric normed space over a complete nontrivially normed field, with the coordinate functionals sending a vector to its coefficients in its unique unconditional expansion ∑ i, a i • e i.

@[simp]

theorem TauCeti.IsTOrthogonalBasis.coe_toUnconditionalSchauderBasis {K : Type u_2} {I : Type u_3} {M : Type u_5} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup M] [NormedSpace K M] [IsUltrametricDist M] {t : NNReal} {e : I → M} (he : IsTOrthogonalBasis K t e) (ht : 0 < t) : ↑(he.toUnconditionalSchauderBasis ht) = e

The vectors of the Schauder basis attached to a t-orthogonal basis e are those of e.

theorem TauCeti.IsTOrthogonalBasis.coord_eq_of_hasSum {K : Type u_2} {I : Type u_3} {M : Type u_5} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup M] [NormedSpace K M] [IsUltrametricDist M] {t : NNReal} {e : I → M} (he : IsTOrthogonalBasis K t e) (ht : 0 < t) {a : I → K} {x : M} (h : HasSum (fun (i : I) => a i • e i) x) (i : I) : ((he.toUnconditionalSchauderBasis ht).coord i) x = a i

The coordinates of an expansion: if x is the unconditional sum of the a i • e i, then the coordinates of x in the Schauder basis attached to the t-orthogonal basis e are the a i.

theorem TauCeti.IsTOrthogonalBasis.mul_norm_coord_mul_norm_le {K : Type u_2} {I : Type u_3} {M : Type u_5} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup M] [NormedSpace K M] [IsUltrametricDist M] {t : NNReal} {e : I → M} (he : IsTOrthogonalBasis K t e) (ht : 0 < t) (i : I) (x : M) : ↑t * ‖((he.toUnconditionalSchauderBasis ht).coord i) x‖ * ‖e i‖ ≤ ‖x‖

Coordinate estimate: the i-th coordinate of x in the Schauder basis attached to a t-orthogonal basis e satisfies t * ‖coord i x‖ * ‖e i‖ ≤ ‖x‖.

theorem TauCeti.IsTOrthogonalBasis.norm_coord_le {K : Type u_2} {I : Type u_3} {M : Type u_5} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup M] [NormedSpace K M] [IsUltrametricDist M] {t : NNReal} {e : I → M} (he : IsTOrthogonalBasis K t e) (ht : 0 < t) (i : I) : ‖(he.toUnconditionalSchauderBasis ht).coord i‖ ≤ (↑t * ‖e i‖)⁻¹

The i-th coordinate functional of the Schauder basis attached to a t-orthogonal basis e has operator norm at most (t * ‖e i‖)⁻¹.

theorem TauCeti.IsTOrthogonalBasis.tendsto_norm_coord_mul_norm {K : Type u_2} {I : Type u_3} {M : Type u_5} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup M] [NormedSpace K M] [IsUltrametricDist M] {t : NNReal} {e : I → M} (he : IsTOrthogonalBasis K t e) (ht : 0 < t) (x : M) : Filter.Tendsto (fun (i : I) => ‖((he.toUnconditionalSchauderBasis ht).coord i) x‖ * ‖e i‖) Filter.cofinite (nhds 0)

Decay of coordinates: the coordinates of a vector in the Schauder basis attached to a t-orthogonal basis e satisfy ‖coord i x‖ * ‖e i‖ → 0 along the cofinite filter.

theorem TauCeti.IsTOrthogonalBasis.coord_tsum {K : Type u_2} {I : Type u_3} {M : Type u_5} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup M] [NormedSpace K M] [IsUltrametricDist M] {t : NNReal} {e : I → M} [CompleteSpace M] (he : IsTOrthogonalBasis K t e) (ht : 0 < t) {a : I → K} (ha : Filter.Tendsto (fun (i : I) => ‖a i‖ * ‖e i‖) Filter.cofinite (nhds 0)) (i : I) : ((he.toUnconditionalSchauderBasis ht).coord i) (∑' (j : I), a j • e j) = a i

Every null family of coefficients occurs: in a complete space, if ‖a i‖ * ‖e i‖ → 0 along the cofinite filter, then the coordinates of ∑' i, a i • e i in the Schauder basis attached to the t-orthogonal basis e are the a i.