Finite compressions of principal-minor series

The determinants of finite coordinate compressions of a matrix converge to its principal-minor series when the rows have a common bound tending to zero. Convergence holds coefficientwise and in every positive-radius Gauss norm. Thus the infinite determinant can be recovered from finite determinants without choosing an enumeration of the coordinates.

Finite compression means restriction to the same finite set of input and output coordinates. For an operator with finite output support this is its determinant after removing the zero complement. No decay of input tails is assumed.

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.coeff_charpolyRev_finiteCompression {ι : Type u_1} {R : Type u_2} [DecidableEq ι] [CommRing R] {A : Matrix ι ι R} (S : Finset ι) (n : ℕ) : (A.submatrix Subtype.val Subtype.val).charpolyRev.coeff n = (-1) ^ n * ∑ s ∈ Finset.powersetCard n S, A.principalMinor s

The n-th coefficient of det (1 - X A_S) for a finite compression A_S is (-1) ^ n times the sum of the size-n principal minors of A supported in S.

theorem TauCeti.tendsto_coeff_charpolyRev_finiteCompression {ι : Type u_1} {R : Type u_2} [DecidableEq ι] [CommRing R] [TopologicalSpace R] [ContinuousNeg R] {A : Matrix ι ι R} (n : ℕ) (hA : Summable fun (s : { s : Finset ι // s.card = n }) => A.principalMinor ↑s) : Filter.Tendsto (fun (S : Finset ι) => (A.submatrix Subtype.val Subtype.val).charpolyRev.coeff n) Filter.atTop (nhds (A.charCoeff n))

If the size-n principal minors are summable, the corresponding coefficients of finite compressions converge to the coefficient of the principal-minor series.

theorem TauCeti.tendsto_charpolyRev_finiteCompression {ι : Type u_1} {R : Type u_2} [DecidableEq ι] [CommRing R] [TopologicalSpace R] [ContinuousNeg R] {A : Matrix ι ι R} (hA : ∀ (n : ℕ), Summable fun (s : { s : Finset ι // s.card = n }) => A.principalMinor ↑s) : Filter.Tendsto (fun (S : Finset ι) => ↑(A.submatrix Subtype.val Subtype.val).charpolyRev) Filter.atTop (nhds A.charPowerSeries)

Finite compressions converge coefficientwise to the principal-minor series whenever all the defining families of minors are summable.

theorem TauCeti.charPowerSeries_outputTruncation {ι : Type u_1} {R : Type u_2} [DecidableEq ι] [CommRing R] [TopologicalSpace R] {A : Matrix ι ι R} (S : Finset ι) : (Matrix.of fun (i j : ι) => if i ∈ S then A i j else 0).charPowerSeries = ↑(A.submatrix Subtype.val Subtype.val).charpolyRev

The principal-minor series of an output truncation is the polynomial determinant on the retained coordinates. No convergence or row-decay hypothesis on the original matrix is needed for this finite-support identity.

theorem TauCeti.tendsto_gaussNorm_charpolyRev_finiteCompression_sub_charPowerSeries {ι : Type u_1} {R : Type u_2} [DecidableEq ι] [NormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {A : Matrix ι ι R} {r : ι → ℝ} [CompleteSpace R] (hA : ∀ (i j : ι), ‖A i j‖ ≤ r i) (hr : Filter.Tendsto r Filter.cofinite (nhds 0)) {ρ : ℝ} (hρ : 0 < ρ) : Filter.Tendsto (fun (S : Finset ι) => PowerSeries.gaussNorm norm ρ (↑(A.submatrix Subtype.val Subtype.val).charpolyRev - A.charPowerSeries)) Filter.atTop (nhds 0)

Finite coordinate determinants converge in every positive-radius Gauss norm to the principal-minor series of a matrix whose row bounds tend to zero. The finite sets are ordered by inclusion, so this limit does not depend on an enumeration of the index type.