Gauss convergence of principal-minor series

A common null row majorant upgrades coefficientwise convergence of principal-minor series to convergence in every positive-radius Gauss norm. In particular, uniform entrywise convergence of matrices with a common null row majorant implies Gauss convergence of their determinants. This is the continuity needed to pass finite determinant identities to infinite determinants. Coefficientwise convergence alone, without uniform control of the tails, does not suffice.

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.tendsto_gaussNorm_charPowerSeries_sub_charPowerSeries_of_common_majorant {ι : Type u_1} {R : Type u_2} {α : Type u_3} [DecidableEq ι] [NormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {l : Filter α} {A : α → Matrix ι ι R} {B : Matrix ι ι R} {r : ι → ℝ} (hA : ∀ (a : α) (i j : ι), ‖A a i j‖ ≤ r i) (hB : ∀ (i j : ι), ‖B i j‖ ≤ r i) (hr : Filter.Tendsto r Filter.cofinite (nhds 0)) (hcoeff : ∀ (n : ℕ), Filter.Tendsto (fun (a : α) => (A a).charCoeff n) l (nhds (B.charCoeff n))) {ρ : ℝ} (hρ : 0 < ρ) : Filter.Tendsto (fun (a : α) => PowerSeries.gaussNorm norm ρ ((A a).charPowerSeries - B.charPowerSeries)) l (nhds 0)

A common null row majorant upgrades convergence of each principal-minor coefficient to Gauss convergence at every positive radius. No completeness is needed once coefficient convergence is supplied.

theorem TauCeti.tendsto_gaussNorm_charPowerSeries_sub_charPowerSeries_of_tendstoUniformly {ι : Type u_1} {R : Type u_2} {α : Type u_3} [DecidableEq ι] [NormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {l : Filter α} {A : α → Matrix ι ι R} {B : Matrix ι ι R} {r : ι → ℝ} [CompleteSpace R] (hA : ∀ (a : α) (i j : ι), ‖A a i j‖ ≤ r i) (hB : ∀ (i j : ι), ‖B i j‖ ≤ r i) (hr : Filter.Tendsto r Filter.cofinite (nhds 0)) (hAB : TendstoUniformly (fun (a : α) (p : ι × ι) => A a p.1 p.2) (fun (p : ι × ι) => B p.1 p.2) l) {ρ : ℝ} (hρ : 0 < ρ) : Filter.Tendsto (fun (a : α) => PowerSeries.gaussNorm norm ρ ((A a).charPowerSeries - B.charPowerSeries)) l (nhds 0)

Uniform entrywise convergence, with a common null row majorant, implies convergence of principal-minor series in every positive-radius Gauss norm. Completeness ensures that the principal-minor families defining the coefficients are summable.