Continuity of principal-minor coefficients

For ultrametric seminormed coefficient rings, the coefficients of det (1 - T A) satisfy the entrywise perturbation estimate

‖A.charCoeff n - B.charCoeff n‖ ≤ ε * M ^ (n - 1)

when both matrices have entries of norm at most M, corresponding entries differ by at most ε, and the size-n principal-minor families are summable. There is no factor depending on the number of minors or on the size of the index type. Over complete coefficient rings, the estimate applies in particular to matrices with null row majorants, by Matrix.summable_principalMinor.

Consequently uniform entrywise convergence to a bounded matrix implies convergence of each coefficient, provided the principal-minor sums converge. This is the coefficientwise continuity needed to pass from finite-dimensional determinant identities to Fredholm determinants. It does not assert convergence in Gauss norm without additional control of coefficient tails.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §§4–5.

theorem TauCeti.norm_charCoeff_sub_le {ι : Type u_1} {R : Type u_2} [DecidableEq ι] [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {A B : Matrix ι ι R} {n : ℕ} {M ε : ℝ} (hM : 0 ≤ M) (hε : 0 ≤ ε) (hA : ∀ (i j : ι), ‖A i j‖ ≤ M) (hB : ∀ (i j : ι), ‖B i j‖ ≤ M) (hAB : ∀ (i j : ι), ‖A i j - B i j‖ ≤ ε) (hAs : Summable fun (s : { s : Finset ι // s.card = n }) => A.principalMinor ↑s) (hBs : Summable fun (s : { s : Finset ι // s.card = n }) => B.principalMinor ↑s) : ‖A.charCoeff n - B.charCoeff n‖ ≤ ε * M ^ (n - 1)

Fredholm coefficients are Lipschitz on entrywise bounded sets whenever the defining principal-minor sums converge. In particular, over a complete coefficient ring this applies to matrices with null row majorants (Matrix.summable_principalMinor). Neither completeness nor Hausdorffness is needed once summability is supplied.

theorem TauCeti.tendsto_charCoeff_of_tendstoUniformly {ι : Type u_1} {R : Type u_2} [DecidableEq ι] [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {α : Type u_3} {l : Filter α} {A : α → Matrix ι ι R} {B : Matrix ι ι R} {M : ℝ} (n : ℕ) (hB : ∀ (i j : ι), ‖B i j‖ ≤ M) (hAs : ∀ᶠ (a : α) in l, Summable fun (s : { s : Finset ι // s.card = n }) => (A a).principalMinor ↑s) (hBs : Summable fun (s : { s : Finset ι // s.card = n }) => B.principalMinor ↑s) (hAB : TendstoUniformly (fun (a : α) (p : ι × ι) => A a p.1 p.2) (fun (p : ι × ι) => B p.1 p.2) l) : Filter.Tendsto (fun (a : α) => (A a).charCoeff n) l (nhds (B.charCoeff n))

Uniform entrywise convergence to a bounded matrix implies convergence of each principal-minor coefficient, as long as the relevant principal-minor sums are summable. The uniform entry bound is required only for the limit matrix.