Principal-minor series of infinite matrices #

For a square matrix A : Matrix ι ι R over a commutative topological ring, indexed by an arbitrary (possibly infinite) type ι, this file uses the principal minors A.principalMinor s = det (A i j)_{i, j ∈ s} on finite sets s of indices (Matrix.principalMinor) to define the coefficients

A.charCoeff n = (-1) ^ n * ∑' s : {s : Finset ι // s.card = n}, A.principalMinor s,

and the power series A.charPowerSeries with these coefficients. For a finite index type these are exactly the coefficients of det (1 - X A), Mathlib's Matrix.charpolyRev (Matrix.charCoeff_eq_coeff_charpolyRev). For infinite index types the series is the Fredholm determinant det (1 - T A) of Serre's theory of completely continuous endomorphisms of nonarchimedean Banach spaces, once the defining sums are known to converge.

Over an ultrametric seminormed commutative ring, a product majorant ‖A.principalMinor s‖ ≤ ∏ i ∈ s, r i controls convergence and growth:

any common nonnegative bound on the size-n principal minors bounds the coefficient (Matrix.norm_charCoeff_le_of_principalMinor_le);
if r tends to zero along the cofinite filter and the ring is complete, the principal minors of each size form a summable family (Matrix.summable_principalMinor_of_le_prod);
if ρ * r i ≤ q ≤ 1 off a finite set T and ρ * r i ≤ B everywhere, with ρ > 0, 0 ≤ q and 1 ≤ B, then ‖A.charCoeff n‖ * ρ ^ n ≤ B ^ #T * q ^ (n - #T) (Matrix.norm_charCoeff_mul_pow_le_of_le_prod);
if r tends to zero along the cofinite filter and the ring is normed, the series is restricted at every radius, that is, entire (Matrix.isRestricted_charPowerSeries_of_le_prod).

The last two estimates depend on the coefficients only through the bound ‖A.charCoeff n‖ ≤ c for every nonnegative bound c of the n-fold products of r. They are instances of the real estimates TauCeti.mul_pow_le_of_forall_prod_le and TauCeti.tendsto_mul_pow_of_forall_prod_le, which assume only that bound and so apply equally to the coefficients of the Fredholm resolvent.

Only summability requires completeness; none of these estimates requires ‖1‖ = 1. Over an ultrametric seminormed commutative ring with ‖1‖ = 1, row bounds ‖A i j‖ ≤ r i supply the product majorant (Matrix.norm_principalMinor_le). They give the row-bound corollaries Matrix.norm_charCoeff_le, Matrix.summable_principalMinor, and Matrix.norm_charCoeff_mul_pow_le. When the ring is normed, they also give Matrix.isRestricted_charPowerSeries.

The tail estimate depends on A only through r, so it is uniform over every family of matrices sharing one product majorant. The coefficients do not depend on an enumeration of the index type (Matrix.charCoeff_submatrix_equiv).

The series is compatible with the operations on matrices that act on each principal minor:

it is unchanged by transposition (Matrix.charPowerSeries_transpose);
it is unchanged by restriction to the range of an embedding of index types when the rows, or the columns, outside that range vanish, that is, under extension by zero (Matrix.charPowerSeries_submatrix_of_row_eq_zero, Matrix.charPowerSeries_submatrix_of_col_eq_zero);
when the principal minors of A are summable, a continuous ring morphism f carries it to the series of A.map f (Matrix.charPowerSeries_map), and the series of c • A is that of A with the variable scaled by c, det (1 - T (c • A)) = det (1 - (c T) A) (Matrix.charPowerSeries_smul).

The product-majorant results Matrix.summable_principalMinor_of_le_prod and Matrix.isRestricted_charPowerSeries_of_le_prod only require bounds on principal minors. They also apply to two-sided entry bounds whose diagonal products tend to zero, even when the rows themselves do not decay.

The summability hypotheses in Matrix.charPowerSeries_map and Matrix.charPowerSeries_smul are needed because the coefficients are unconditional sums: the image of a non-summable family of minors may be summable with a nonzero sum. The scaling identities require only continuity of multiplication by each fixed scalar.

Main definitions #

Matrix.charCoeff: the signed sum of the principal minors of a given size.
Matrix.charPowerSeries: the power series with coefficients Matrix.charCoeff.

Implementation notes #

The coefficients are defined by an unconditional tsum, which is zero when the family is not summable. Statements about their values that need convergence carry the corresponding row-decay or product-majorant hypotheses; the norm bounds hold without them.

References #

J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §§4–5.
R. Coleman, p-adic Banach spaces and families of modular forms, Invent. Math. 127 (1997), 417–479, Appendix A.