Common row majorants for convergent sequences

A norm-convergent sequence of row-compact maps between model spaces has a common nonnegative null row majorant, including its limit. This permits estimates depending on row decay to be applied uniformly to such sequences.

theorem TauCeti.exists_common_row_majorant_of_tendsto_ringOpNorm {I : Type u_1} {J : Type u_2} {R : Type u_3} [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedRing R] [NormedRing.IsTate R] {u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R} {v : ℕ → ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R} (h : Filter.Tendsto (fun (n : ℕ) => ‖u - v n‖) Filter.atTop (nhds 0)) (hv : ∀ (n : ℕ), (v n).IsRowCompact) : ∃ (r : I → ℝ), (∀ (i : I), 0 ≤ r i) ∧ Filter.Tendsto r Filter.cofinite (nhds 0) ∧ (∀ (i : I) (j : J), ‖u.matrixCoeff i j‖ ≤ r i) ∧ ∀ (n : ℕ) (i : I) (j : J), ‖(v n).matrixCoeff i j‖ ≤ r i

A norm-convergent sequence of row-compact maps and its limit admit a common nonnegative null row majorant. Neither completeness nor ultrametricity is required. In particular the limit's row decay need not be assumed separately.