Matrices of continuous linear maps between model spaces

Let R be a seminormed ring and I, J discrete index types. A continuous linear map u : C₀(J, R) →L[R] C₀(I, R) between the model spaces of nonarchimedean functional analysis has the matrix (only the input index J needs to be discrete for the definition)

u.matrixCoeff i j = (u (single j 1)) i,

with the output index first, as for Mathlib's LinearMap.toMatrix': the columns of the matrix are the images of the coordinate vectors. This file develops the dictionary between such maps and their matrices.

• Every column tends to zero along the cofinite filter (tendsto_matrixCoeff_cofinite), and over a ring with a multiplicative pseudo-uniformiser every entry is bounded by the operator norm (norm_matrixCoeff_le), so convergence in operator norm gives uniform convergence of the entries (tendstoUniformly_matrixCoeff_of_tendsto).
• The value of u is given by the convergent matrix action: (u x) i = ∑ j, A i j * x j over a commutative ring (hasSum_matrixCoeff_mul), and the matrix of a composite is the convergent matrix product (hasSum_matrixCoeff_comp).
• A map is determined by its matrix (matrixCoeff_injective). Conversely a matrix with null columns and bounded entries over a complete ultrametric ring is the matrix of the map Matrix.toZeroAtInftyCLM (matrixCoeff_toZeroAtInftyCLM), which acts by the same convergent sums (hasSum_toZeroAtInftyCLM_apply). Over Tate scalars this characterises the matrices of continuous linear maps (mem_range_matrixCoeff_iff).
• Over an ultrametric ring a bound C on the entries gives ‖u x‖ ≤ C * ‖x‖ (norm_apply_le_of_forall_norm_matrixCoeff_le), so the operator norm is bounded by the supremum of the entries, and over Tate scalars it equals that supremum (ringOpNorm_eq_iSup_norm_matrixCoeff), which is Mathlib's operator norm over a nontrivially normed field (opNorm_eq_iSup_norm_matrixCoeff).
• For finite index types the matrix is the usual matrix of the underlying linear map R ^ J → R ^ I (matrixCoeff_eq_toMatrix').
• A matrix over R with null columns and bounded entries also acts on the module-valued model space C₀(J, E) of a complete ultrametric normed R-module E with contractive action, by (A x) i = ∑ j, A i j • x j (Matrix.toZeroAtInftySMulCLM). This is linear over every semiring acting on E compatibly with R, and a bound C on the entries bounds it by C (Matrix.norm_toZeroAtInftySMulCLM_apply_le). The map Matrix.toZeroAtInftyCLM, which multiplies by the entries on the right, is the case of the matrix over the opposite ring Rᵐᵒᵖ acting on R (Matrix.toZeroAtInftySMulCLM_map_op).

Decay of the rows i ↦ ⨆ j, ‖A i j‖, which is uniform in the input index, is a strictly stronger condition than decay of each column: over a nonzero norm-one ring, the identity of C₀(ℕ, R) has null columns, but every row has norm one.

Main definitions

• ContinuousLinearMap.matrixCoeff: the matrix of a continuous linear map between model spaces.
• Matrix.toZeroAtInftyCLM: the continuous linear map defined by a matrix with null columns and bounded entries.
• Matrix.toZeroAtInftySMulCLM: the continuous linear map C₀(J, E) → C₀(I, E) defined by such a matrix acting on module-valued null families.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §§2–3.
• P. Schneider, Nonarchimedean Functional Analysis, Springer, 2002, §10.

noncomputable def ContinuousLinearMap.matrixCoeff {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedRing R] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) : Matrix I J R

The matrix of a continuous linear map u : C₀(J, R) →L[R] C₀(I, R) between model spaces: its entry in row i and column j is the i-th coordinate of the image of the coordinate vector single j 1. Rows are indexed by output coordinates.

theorem ContinuousLinearMap.matrixCoeff_apply {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedRing R] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (i : I) (j : J) : u.matrixCoeff i j = (u (ZeroAtInftyContinuousMap.single j 1)) i

@[simp]

theorem ContinuousLinearMap.matrixCoeff_zero {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedRing R] : matrixCoeff 0 = 0

@[simp]

theorem ContinuousLinearMap.matrixCoeff_add {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedRing R] (u v : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) : (u + v).matrixCoeff = u.matrixCoeff + v.matrixCoeff

@[simp]

theorem ContinuousLinearMap.matrixCoeff_neg {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedRing R] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) : (-u).matrixCoeff = -u.matrixCoeff

@[simp]

theorem ContinuousLinearMap.matrixCoeff_sub {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedRing R] (u v : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) : (u - v).matrixCoeff = u.matrixCoeff - v.matrixCoeff

@[simp]

theorem ContinuousLinearMap.matrixCoeff_sum {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedRing R] {ι : Type u_5} (s : Finset ι) (u : ι → ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) : (∑ k ∈ s, u k).matrixCoeff = ∑ k ∈ s, (u k).matrixCoeff

@[simp]

theorem ContinuousLinearMap.matrixCoeff_id {J : Type u_2} {R : Type u_4} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedRing R] : (ContinuousLinearMap.id R (ZeroAtInftyContinuousMap J R)).matrixCoeff = 1

@[simp]

theorem ContinuousLinearMap.matrixCoeff_one {J : Type u_2} {R : Type u_4} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedRing R] : matrixCoeff 1 = 1

theorem ContinuousLinearMap.tendsto_matrixCoeff_cofinite {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedRing R] [DiscreteTopology I] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (j : J) : Filter.Tendsto (fun (i : I) => u.matrixCoeff i j) Filter.cofinite (nhds 0)

Null columns: each column of the matrix of a continuous linear map tends to zero along the cofinite filter.

theorem ContinuousLinearMap.hasSum_mul_matrixCoeff {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedRing R] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (x : ZeroAtInftyContinuousMap J R) (i : I) : HasSum (fun (j : J) => x j * u.matrixCoeff i j) ((u x) i)

The matrix action: the i-th coordinate of u x is the unconditional sum of the x j * u.matrixCoeff i j. Over a commutative ring this is hasSum_matrixCoeff_mul.

theorem ContinuousLinearMap.norm_matrixCoeff_le {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedRing R] [TauCeti.NormedRing.IsTate R] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (i : I) (j : J) : ‖u.matrixCoeff i j‖ ≤ ‖u‖

Over Tate scalars, every entry of the matrix is bounded by the operator norm.

theorem ContinuousLinearMap.tendstoUniformly_matrixCoeff_of_tendsto {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedRing R] [TauCeti.NormedRing.IsTate R] {α : Type u_5} {l : Filter α} {w : α → ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R} {w₀ : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R} (h : Filter.Tendsto (fun (a : α) => ‖w a - w₀‖) l (nhds 0)) : TendstoUniformly (fun (a : α) (p : I × J) => (w a).matrixCoeff p.1 p.2) (fun (p : I × J) => w₀.matrixCoeff p.1 p.2) l

Over Tate scalars, convergence in operator norm gives uniform convergence of the matrix entries.

@[simp]

theorem ContinuousLinearMap.matrixCoeff_smul {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedCommRing R] (c : R) (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) : (c • u).matrixCoeff = c • u.matrixCoeff

theorem ContinuousLinearMap.hasSum_matrixCoeff_mul {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedCommRing R] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (x : ZeroAtInftyContinuousMap J R) (i : I) : HasSum (fun (j : J) => u.matrixCoeff i j * x j) ((u x) i)

The matrix action over a commutative ring: the i-th coordinate of u x is the unconditional sum ∑ j, u.matrixCoeff i j * x j.

theorem ContinuousLinearMap.hasSum_matrixCoeff_comp {I : Type u_1} {J : Type u_2} {K : Type u_3} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedCommRing R] [TopologicalSpace K] [DiscreteTopology K] [DecidableEq K] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (v : ZeroAtInftyContinuousMap K R →L[R] ZeroAtInftyContinuousMap J R) (i : I) (k : K) : HasSum (fun (j : J) => u.matrixCoeff i j * v.matrixCoeff j k) ((u ∘SL v).matrixCoeff i k)

The matrix of a composite is the product of the matrices, an unconditionally convergent sum over the middle index.

theorem ContinuousLinearMap.matrixCoeff_eq_toMatrix' {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedCommRing R] [DiscreteTopology I] [Fintype I] [Fintype J] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) : u.matrixCoeff = LinearMap.toMatrix' (↑(ZeroAtInftyContinuousMap.equivFunOnFintype R R).toLinearEquiv ∘ₗ ↑u ∘ₗ ↑(ZeroAtInftyContinuousMap.equivFunOnFintype R R).symm.toLinearEquiv)

For finite index types, the matrix of u is the matrix, in the sense of LinearMap.toMatrix', of the linear map R ^ J → R ^ I obtained by identifying each model space with the space of all families.

theorem ContinuousLinearMap.matrixCoeff_injective {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedRing R] : Function.Injective matrixCoeff

A continuous linear map between model spaces is determined by its matrix.

@[simp]

theorem ContinuousLinearMap.matrixCoeff_inj {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedRing R] {u v : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R} : u.matrixCoeff = v.matrixCoeff ↔ u = v

theorem ContinuousLinearMap.norm_apply_le_of_forall_norm_matrixCoeff_le {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedRing R] [IsUltrametricDist R] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) {C : ℝ} (hC : 0 ≤ C) (h : ∀ (i : I) (j : J), ‖u.matrixCoeff i j‖ ≤ C) (x : ZeroAtInftyContinuousMap J R) : ‖u x‖ ≤ C * ‖x‖

Over an ultrametric ring, a uniform bound C on the entries of the matrix of u gives the uniform bound ‖u x‖ ≤ C * ‖x‖. No pseudo-uniformiser is needed.

theorem ContinuousLinearMap.ringOpNorm_le_of_forall_norm_matrixCoeff_le {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedRing R] [IsUltrametricDist R] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) {C : ℝ} (hC : 0 ≤ C) (h : ∀ (i : I) (j : J), ‖u.matrixCoeff i j‖ ≤ C) : ‖u‖ ≤ C

Over an ultrametric ring, a uniform bound C on the entries of the matrix bounds the operator norm.

theorem ContinuousLinearMap.ringOpNorm_le_iff_forall_norm_matrixCoeff_le {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] {u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R} {C : ℝ} (hC : 0 ≤ C) : ‖u‖ ≤ C ↔ ∀ (i : I) (j : J), ‖u.matrixCoeff i j‖ ≤ C

Over ultrametric Tate scalars, ‖u‖ ≤ C exactly when every entry of the matrix of u has norm at most C.

theorem ContinuousLinearMap.ringOpNorm_eq_iSup_norm_matrixCoeff {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedRing R] [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) : ‖u‖ = ⨆ (p : I × J), ‖u.matrixCoeff p.1 p.2‖

The sup-entry norm: over ultrametric Tate scalars, the operator norm of a map between model spaces is the supremum of the norms of the entries of its matrix.

theorem ContinuousLinearMap.matrixCoeff_comp {I : Type u_1} {J : Type u_2} {K : Type u_3} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] [TopologicalSpace K] [DiscreteTopology K] [DecidableEq K] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) (v : ZeroAtInftyContinuousMap K R →L[R] ZeroAtInftyContinuousMap J R) (i : I) (k : K) : (u ∘SL v).matrixCoeff i k = ∑' (j : J), u.matrixCoeff i j * v.matrixCoeff j k

The matrix of a composite is the product of the matrices, summed over the middle index.

theorem ContinuousLinearMap.matrixCoeff_mul {J : Type u_2} {R : Type u_4} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] (u v : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap J R) (i j : J) : (u * v).matrixCoeff i j = ∑' (k : J), u.matrixCoeff i k * v.matrixCoeff k j

The matrix of a product of endomorphisms of a model space is the product of the matrices.

theorem ContinuousLinearMap.submatrix_matrixCoeff_pow {J : Type u_2} {R : Type u_4} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] {w : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap J R} {F : Finset J} (hw : ∀ i ∉ F, ∀ (j : J), w.matrixCoeff i j = 0) (k : ℕ) : (w ^ k).matrixCoeff.submatrix Subtype.val Subtype.val = w.matrixCoeff.submatrix Subtype.val Subtype.val ^ k

If the rows of w outside a finite set F vanish, the block of w ^ k on F is the k-th power of the block of w on F.

theorem ContinuousLinearMap.submatrix_matrixCoeff_aeval_indicatorCLM_comp {J : Type u_2} {R : Type u_4} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedCommRing R] (S : Finset J) (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap J R) (Q : Polynomial R) : ((Polynomial.aeval (ZeroAtInftyContinuousMap.indicatorCLM R ↑S ∘SL u)) Q).matrixCoeff.submatrix Subtype.val Subtype.val = (Polynomial.aeval (u.matrixCoeff.submatrix Subtype.val Subtype.val)) Q

For a finite set S of output coordinates and any polynomial Q, the block on S of the matrix of Q(π_S ∘ u) is Q(A), where A is the block of u on S: the rows of π_S ∘ u outside S vanish, so the products of matrices only involve indices in S.

noncomputable def Matrix.toZeroAtInftyCLM {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DiscreteTopology I] [NormedRing R] [IsUltrametricDist R] [CompleteSpace R] (A : Matrix I J R) (hcol : ∀ (j : J), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) (hbdd : ∃ (C : ℝ), ∀ (i : I) (j : J), ‖A i j‖ ≤ C) : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R

The continuous linear map C₀(J, R) →L[R] C₀(I, R) defined by a matrix A whose columns tend to zero along the cofinite filter and whose entries are uniformly bounded, over a complete ultrametric normed ring. It sends x to the family i ↦ ∑ j, x j * A i j, and its matrix is A (ContinuousLinearMap.matrixCoeff_toZeroAtInftyCLM).

@[simp]

theorem Matrix.toZeroAtInftyCLM_single_apply {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [DiscreteTopology I] [NormedRing R] [IsUltrametricDist R] [CompleteSpace R] (A : Matrix I J R) (hcol : ∀ (j : J), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) (hbdd : ∃ (C : ℝ), ∀ (i : I) (j : J), ‖A i j‖ ≤ C) (j : J) (r : R) (i : I) : ((A.toZeroAtInftyCLM hcol hbdd) (ZeroAtInftyContinuousMap.single j r)) i = r * A i j

The map defined by a matrix A sends the coordinate vector single j r to r times the j-th column of A.

@[simp]

theorem ContinuousLinearMap.matrixCoeff_toZeroAtInftyCLM {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [DiscreteTopology I] [NormedRing R] [IsUltrametricDist R] [CompleteSpace R] (A : Matrix I J R) (hcol : ∀ (j : J), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) (hbdd : ∃ (C : ℝ), ∀ (i : I) (j : J), ‖A i j‖ ≤ C) : (A.toZeroAtInftyCLM hcol hbdd).matrixCoeff = A

The matrix of the map defined by a matrix A with null columns and bounded entries is A.

theorem ContinuousLinearMap.hasSum_toZeroAtInftyCLM_apply {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DiscreteTopology I] [NormedRing R] [IsUltrametricDist R] [CompleteSpace R] (A : Matrix I J R) (hcol : ∀ (j : J), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) (hbdd : ∃ (C : ℝ), ∀ (i : I) (j : J), ‖A i j‖ ≤ C) (x : ZeroAtInftyContinuousMap J R) (i : I) : HasSum (fun (j : J) => x j * A i j) (((A.toZeroAtInftyCLM hcol hbdd) x) i)

The map defined by a matrix A with null columns and bounded entries sends x to the family of unconditional sums i ↦ ∑ j, x j * A i j.

theorem ContinuousLinearMap.toZeroAtInftyCLM_matrixCoeff {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [DiscreteTopology I] [NormedRing R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) : u.matrixCoeff.toZeroAtInftyCLM ⋯ ⋯ = u

Over Tate scalars, every continuous linear map between model spaces is the map defined by its matrix.

theorem ContinuousLinearMap.mem_range_matrixCoeff_iff {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [DiscreteTopology I] [NormedRing R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R] {A : Matrix I J R} : A ∈ Set.range matrixCoeff ↔ (∀ (j : J), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) ∧ ∃ (C : ℝ), ∀ (i : I) (j : J), ‖A i j‖ ≤ C

Matrices of continuous linear maps: over a complete ultrametric ring with a multiplicative pseudo-uniformiser, a matrix is the matrix of a continuous linear map C₀(J, R) →L[R] C₀(I, R) exactly when its columns tend to zero along the cofinite filter and its entries are uniformly bounded.

theorem ContinuousLinearMap.opNorm_eq_iSup_norm_matrixCoeff {I : Type u_1} {J : Type u_2} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] {𝕜 : Type u_5} [NontriviallyNormedField 𝕜] [IsUltrametricDist 𝕜] (u : ZeroAtInftyContinuousMap J 𝕜 →L[𝕜] ZeroAtInftyContinuousMap I 𝕜) : ‖u‖ = ⨆ (p : I × J), ‖u.matrixCoeff p.1 p.2‖

The sup-entry norm over a nontrivially normed ultrametric field: Mathlib's operator norm of a map between model spaces is the supremum of the norms of the entries of its matrix.

Matrices acting on module-valued model spaces

noncomputable def Matrix.toZeroAtInftySMulCLM {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DiscreteTopology I] {E : Type u_5} [NormedAddCommGroup E] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_6) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass R S E] (A : Matrix I J R) (hcol : ∀ (j : J), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) (hbdd : ∃ (C : ℝ), ∀ (i : I) (j : J), ‖A i j‖ ≤ C) : ZeroAtInftyContinuousMap J E →L[S] ZeroAtInftyContinuousMap I E

The continuous linear map C₀(J, E) →L[S] C₀(I, E) defined by a matrix A over R whose columns tend to zero along the cofinite filter and whose entries are uniformly bounded, for a complete ultrametric normed R-module E with contractive action. It sends x to the family i ↦ ∑ j, A i j • x j (Matrix.hasSum_toZeroAtInftySMulCLM_apply), and it is linear over every semiring S whose action on E commutes with that of R.

theorem Matrix.hasSum_toZeroAtInftySMulCLM_apply {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DiscreteTopology I] {E : Type u_5} [NormedAddCommGroup E] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_6) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass R S E] (A : Matrix I J R) (hcol : ∀ (j : J), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) (hbdd : ∃ (C : ℝ), ∀ (i : I) (j : J), ‖A i j‖ ≤ C) (x : ZeroAtInftyContinuousMap J E) (i : I) : HasSum (fun (j : J) => A i j • x j) (((toZeroAtInftySMulCLM S A hcol hbdd) x) i)

The map defined by a matrix A with null columns and bounded entries sends x to the family of unconditional sums i ↦ ∑ j, A i j • x j.

theorem Matrix.toZeroAtInftySMulCLM_apply {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DiscreteTopology I] {E : Type u_5} [NormedAddCommGroup E] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_6) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass R S E] (A : Matrix I J R) (hcol : ∀ (j : J), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) (hbdd : ∃ (C : ℝ), ∀ (i : I) (j : J), ‖A i j‖ ≤ C) (x : ZeroAtInftyContinuousMap J E) (i : I) : ((toZeroAtInftySMulCLM S A hcol hbdd) x) i = ∑' (j : J), A i j • x j

The coordinates of the map defined by a matrix A.

@[simp]

theorem Matrix.toZeroAtInftySMulCLM_single_apply {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DiscreteTopology I] {E : Type u_5} [NormedAddCommGroup E] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_6) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass R S E] [DecidableEq J] (A : Matrix I J R) (hcol : ∀ (j : J), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) (hbdd : ∃ (C : ℝ), ∀ (i : I) (j : J), ‖A i j‖ ≤ C) (j : J) (e : E) (i : I) : ((toZeroAtInftySMulCLM S A hcol hbdd) (ZeroAtInftyContinuousMap.single j e)) i = A i j • e

The map defined by a matrix A sends the coordinate vector single j e to the j-th column of A multiplied by e.

theorem Matrix.norm_toZeroAtInftySMulCLM_apply_le {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DiscreteTopology I] {E : Type u_5} [NormedAddCommGroup E] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_6) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass R S E] (A : Matrix I J R) (hcol : ∀ (j : J), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) (hbdd : ∃ (C : ℝ), ∀ (i : I) (j : J), ‖A i j‖ ≤ C) {C : ℝ} (hC0 : 0 ≤ C) (hC : ∀ (i : I) (j : J), ‖A i j‖ ≤ C) (x : ZeroAtInftyContinuousMap J E) : ‖(toZeroAtInftySMulCLM S A hcol hbdd) x‖ ≤ C * ‖x‖

A bound C on the entries of A gives ‖A x‖ ≤ C * ‖x‖.

theorem Matrix.toZeroAtInftySMulCLM_sub_apply {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DiscreteTopology I] {E : Type u_5} [NormedAddCommGroup E] [SeminormedRing R] [Module R E] [IsBoundedSMul R E] [IsUltrametricDist E] [CompleteSpace E] (S : Type u_6) [Semiring S] [Module S E] [ContinuousConstSMul S E] [SMulCommClass R S E] (A B : Matrix I J R) (hcol : ∀ (j : J), Filter.Tendsto (fun (i : I) => (A - B) i j) Filter.cofinite (nhds 0)) (hbdd : ∃ (C : ℝ), ∀ (i : I) (j : J), ‖(A - B) i j‖ ≤ C) (hA : ∀ (j : J), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) (hA' : ∃ (C : ℝ), ∀ (i : I) (j : J), ‖A i j‖ ≤ C) (hB : ∀ (j : J), Filter.Tendsto (fun (i : I) => B i j) Filter.cofinite (nhds 0)) (hB' : ∃ (C : ℝ), ∀ (i : I) (j : J), ‖B i j‖ ≤ C) (x : ZeroAtInftyContinuousMap J E) : (toZeroAtInftySMulCLM S (A - B) hcol hbdd) x = (toZeroAtInftySMulCLM S A hA hA') x - (toZeroAtInftySMulCLM S B hB hB') x

The map defined by a difference of matrices is the difference of their maps.

theorem Matrix.toZeroAtInftySMulCLM_map_op {I : Type u_1} {J : Type u_2} {R : Type u_4} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DiscreteTopology I] [NormedRing R] [IsUltrametricDist R] [CompleteSpace R] (A : Matrix I J R) (hcol : ∀ (j : J), Filter.Tendsto (fun (i : I) => A i j) Filter.cofinite (nhds 0)) (hbdd : ∃ (C : ℝ), ∀ (i : I) (j : J), ‖A i j‖ ≤ C) (hcol' : ∀ (j : J), Filter.Tendsto (fun (i : I) => A.map MulOpposite.op i j) Filter.cofinite (nhds 0)) (hbdd' : ∃ (C : ℝ), ∀ (i : I) (j : J), ‖A.map MulOpposite.op i j‖ ≤ C) : toZeroAtInftySMulCLM R (A.map MulOpposite.op) hcol' hbdd' = A.toZeroAtInftyCLM hcol hbdd

Right multiplication by the entries of A is the action of A through the opposite ring: the map Matrix.toZeroAtInftyCLM of a matrix over a complete ultrametric normed ring R is the map defined by the matrix A.map MulOpposite.op over Rᵐᵒᵖ, acting on R.