Determinant estimates for matrices over ultrametric seminormed rings

Over an ultrametric seminormed commutative ring R with ‖1‖ = 1, the Leibniz expansion of a determinant is a sum of signed products, so the ultrametric inequality bounds the determinant by the largest of those products rather than by their sum. If the entries satisfy ‖A i j‖ ≤ c i * d j, every Leibniz product is bounded by (∏ i, c i) * ∏ j, d j, and hence so is the determinant (Matrix.norm_det_le_prod_mul_prod). No multiplicativity of the norm and no nonnegativity of c or d is assumed; the norm need only be submultiplicative.

Taking d = 1 gives the bound of a determinant by the product of row bounds (Matrix.norm_det_le_prod_of_norm_le), and hence the corresponding bound for a principal minor (Matrix.norm_principalMinor_le). Applied to the principal minors of the expansion Matrix.coeff_charpolyRev, these bounds control the coefficients of det (1 - X A) (Matrix.norm_coeff_charpolyRev_le). These are the estimates from which convergence and growth of Fredholm determinants of compact operators on nonarchimedean Banach spaces are derived.

Over a normed field, with no ultrametric assumption, a principal minor whose rows are rescaled by nonzero (d i)⁻¹ to a minor of norm one has norm exactly ∏ i ∈ s, ‖d i‖ (Matrix.norm_principalMinor_eq_prod).

Two-sided entry bounds also control each principal minor by the product of the diagonal factors c i * d i (Matrix.norm_principalMinor_le_prod_mul). For a matrix indexed by ℕ with antitone row bounds r, every principal minor of size n + 1 other than the leading one on range (n + 1) is bounded by (∏ i ∈ range n, r i) * r (n + 1) (Matrix.norm_principalMinor_le_prod_range_mul). The two-sided form ‖A i j‖ ≤ σ ^ (w i - w' j), with integer weights w, w' and 0 < σ ≤ 1, bounds each principal minor by σ ^ (∑ i ∈ s, (w i - w' i)) (Matrix.norm_principalMinor_le_zpow) and the k-th coefficient by σ ^ m whenever m is a lower bound for the sums ∑ i ∈ s, (w i - w' i) over the k-element sets s (Matrix.norm_coeff_charpolyRev_le_zpow). The bound depends only on the differences w i - w' i along the diagonal, although the entry bounds compare a row weight with an unrelated column weight.

Main results

• Matrix.norm_det_le_prod_mul_prod, Matrix.norm_det_le_prod_of_norm_le, Matrix.norm_principalMinor_le, Matrix.norm_principalMinor_le_prod_mul, Matrix.norm_principalMinor_le_zpow, Matrix.norm_principalMinor_le_prod_range_mul: determinant and principal-minor bounds.
• Matrix.norm_principalMinor_eq_prod: the exact norm of a principal minor from a normalised minor of norm one.
• TauCeti.norm_coeff_charpolyRev_le_of_principalMinor_le, Matrix.norm_coeff_charpolyRev_le, Matrix.norm_coeff_charpolyRev_le_of_norm_le, Matrix.norm_coeff_charpolyRev_le_zpow: coefficient bounds for det (1 - X A).
• Matrix.norm_coeff_det_le_of_natDegree_le_one: the same bounds for the coefficients of determinants of polynomials of degree at most one, from the product bound TauCeti.norm_coeff_prod_le_of_natDegree_le_one.
• Matrix.norm_sum_coeff_charpolyRev_smul_pow_apply_le: the entries of the coefficients of the Fredholm resolvent adjugate (1 - X A) obey the row-bound estimate of det (1 - X A).
• TauCeti.norm_det_sub_le, TauCeti.norm_principalMinor_sub_le: perturbation bounds on entrywise bounded sets.

References

• J.-P. Serre, Endomorphismes complètement continus des espaces de Banach p-adiques, Publ. Math. IHÉS 12 (1962), 69–85, §§4–5.
• K. S. Kedlaya, A little p-adic numerical analysis, MIT 18.787 notes (2007), §3.

theorem TauCeti.norm_coeff_charpolyRev_le_of_principalMinor_le {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [SeminormedCommRing R] [IsUltrametricDist R] {A : Matrix ι ι R} {k : ℕ} {C : ℝ} (hC : 0 ≤ C) (hs : ∀ (s : Finset ι), s.card = k → ‖A.principalMinor s‖ ≤ C) : ‖A.charpolyRev.coeff k‖ ≤ C

A common nonnegative bound on the size-k principal minors bounds the k-th coefficient of det (1 - X A) over an ultrametric seminormed commutative ring.

theorem Matrix.norm_det_le_prod_mul_prod {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {A : Matrix ι ι R} {c d : ι → ℝ} (h : ∀ (i j : ι), ‖A i j‖ ≤ c i * d j) : ‖A.det‖ ≤ (∏ i : ι, c i) * ∏ j : ι, d j

Two-sided determinant bound. Over an ultrametric seminormed ring with ‖1‖ = 1, if ‖A i j‖ ≤ c i * d j for all entries, then ‖det A‖ ≤ (∏ i, c i) * ∏ j, d j.

theorem Matrix.norm_det_le_prod_of_norm_le {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {A : Matrix ι ι R} {c : ι → ℝ} (h : ∀ (i j : ι), ‖A i j‖ ≤ c i) : ‖A.det‖ ≤ ∏ i : ι, c i

Row bound. Over an ultrametric seminormed ring with ‖1‖ = 1, the determinant is bounded by the product of bounds for its rows.

theorem Matrix.norm_principalMinor_le {ι : Type u_1} {R : Type u_2} [DecidableEq ι] [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {A : Matrix ι ι R} {r : ι → ℝ} (hA : ∀ (i j : ι), ‖A i j‖ ≤ r i) (s : Finset ι) : ‖A.principalMinor s‖ ≤ ∏ i ∈ s, r i

Minor bound. Over an ultrametric seminormed ring with ‖1‖ = 1, a principal minor is bounded by the product of the row bounds over its indices.

theorem Matrix.norm_principalMinor_le_prod_mul {ι : Type u_1} {R : Type u_2} [DecidableEq ι] [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {A : Matrix ι ι R} {c d : ι → ℝ} (hA : ∀ (i j : ι), ‖A i j‖ ≤ c i * d j) (s : Finset ι) : ‖A.principalMinor s‖ ≤ ∏ i ∈ s, c i * d i

Two-sided entry bounds bound each principal minor by the product of their diagonal products. Neither factor separately needs to be bounded.

theorem Matrix.norm_principalMinor_le_zpow {ι : Type u_1} {R : Type u_2} [DecidableEq ι] [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {A : Matrix ι ι R} {σ : ℝ} (hσ : 0 < σ) {w w' : ι → ℤ} (hA : ∀ (i j : ι), ‖A i j‖ ≤ σ ^ (w i - w' j)) (s : Finset ι) : ‖A.principalMinor s‖ ≤ σ ^ ∑ i ∈ s, (w i - w' i)

An integer two-sided weight bound controls a principal minor by the sum of the weight differences on its index set, including negative differences.

theorem Matrix.norm_principalMinor_le_prod_range_mul {R : Type u_2} [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {A : Matrix ℕ ℕ R} {r : ℕ → ℝ} (hr : Antitone r) (hA : ∀ (i j : ℕ), ‖A i j‖ ≤ r i) {s : Finset ℕ} {n : ℕ} (hs : s.card = n + 1) (hne : s ≠ Finset.range (n + 1)) : ‖A.principalMinor s‖ ≤ (∏ i ∈ Finset.range n, r i) * r (n + 1)

Nonleading minors. If ‖A i j‖ ≤ r i with r antitone, every principal minor of size n + 1 other than the leading one on range (n + 1) has norm at most (∏ i ∈ range n, r i) * r (n + 1).

theorem Matrix.norm_coeff_charpolyRev_le {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {A : Matrix ι ι R} {c d : ι → ℝ} (h : ∀ (i j : ι), ‖A i j‖ ≤ c i * d j) {k : ℕ} {C : ℝ} (hC : 0 ≤ C) (hs : ∀ (s : Finset ι), s.card = k → (∏ i ∈ s, c i) * ∏ i ∈ s, d i ≤ C) : ‖A.charpolyRev.coeff k‖ ≤ C

Coefficient bound. If ‖A i j‖ ≤ c i * d j for all entries and C ≥ 0 bounds (∏ i ∈ s, c i) * ∏ i ∈ s, d i for every k-element set s, then C bounds the k-th coefficient of det (1 - X A).

theorem Matrix.norm_coeff_charpolyRev_le_of_norm_le {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {A : Matrix ι ι R} {c : ι → ℝ} (h : ∀ (i j : ι), ‖A i j‖ ≤ c i) {k : ℕ} {C : ℝ} (hC : 0 ≤ C) (hs : ∀ (s : Finset ι), s.card = k → ∏ i ∈ s, c i ≤ C) : ‖A.charpolyRev.coeff k‖ ≤ C

Coefficient bound from row bounds. If c i bounds the i-th row of A and C ≥ 0 bounds ∏ i ∈ s, c i for every k-element set s, then C bounds the k-th coefficient of det (1 - X A).

theorem Matrix.norm_coeff_charpolyRev_le_zpow {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {A : Matrix ι ι R} {σ : ℝ} (hσ₀ : 0 < σ) (hσ₁ : σ ≤ 1) {w w' : ι → ℤ} (h : ∀ (i j : ι), ‖A i j‖ ≤ σ ^ (w i - w' j)) {k : ℕ} {m : ℤ} (hm : ∀ (s : Finset ι), s.card = k → m ≤ ∑ i ∈ s, (w i - w' i)) : ‖A.charpolyRev.coeff k‖ ≤ σ ^ m

Two-sided weighted coefficient bound. Let 0 < σ ≤ 1 and let w, w' be integer weights with ‖A i j‖ ≤ σ ^ (w i - w' j). If m ≤ ∑ i ∈ s, (w i - w' i) for every k-element set s, then ‖coeff k (det (1 - X A))‖ ≤ σ ^ m.

theorem Matrix.norm_coeff_det_le_of_natDegree_le_one {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {M : Matrix ι ι (Polynomial R)} {r : ι → ℝ} (hdeg : ∀ (i j : ι), (M i j).natDegree ≤ 1) (h₀ : ∀ (i j : ι), ‖(M i j).coeff 0‖ ≤ 1) (h₁ : ∀ (i j : ι), ‖(M i j).coeff 1‖ ≤ r i) {m : ℕ} {c : ℝ} (hc : 0 ≤ c) (hs : ∀ (s : Finset ι), s.card = m → ∏ i ∈ s, r i ≤ c) : ‖M.det.coeff m‖ ≤ c

Coefficients of a determinant of linear polynomials. Over an ultrametric seminormed ring with ‖1‖ = 1, let M be a matrix of polynomials of degree at most one whose constant coefficients have norm at most one and whose linear coefficients in row i have norm at most r i. If c ≥ 0 bounds ∏ i ∈ s, r i for every m-element set s, then c bounds the m-th coefficient of det M.

theorem Matrix.norm_sum_coeff_charpolyRev_smul_pow_apply_le {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {A : Matrix ι ι R} {r : ι → ℝ} (hA : ∀ (i j : ι), ‖A i j‖ ≤ r i) {m : ℕ} {c : ℝ} (hc : 0 ≤ c) (hs : ∀ (s : Finset ι), s.card = m → ∏ i ∈ s, r i ≤ c) (i j : ι) : ‖(∑ k ∈ Finset.range (m + 1), A.charpolyRev.coeff k • A ^ (m - k)) i j‖ ≤ c

Fredholm resolvent bound. If r i bounds the i-th row of A and c ≥ 0 bounds ∏ i ∈ s, r i for every m-element set s, then c bounds every entry of the m-th coefficient ∑ k ∈ range (m + 1), c k • A ^ (m - k) of adjugate (1 - X A), where c k are the coefficients of det (1 - X A). This is the same bound as for the m-th coefficient of det (1 - X A) itself (Matrix.norm_coeff_charpolyRev_le_of_norm_le).

theorem Matrix.norm_principalMinor_eq_prod {K : Type u_3} [NormedField K] {ι : Type u_4} [DecidableEq ι] {A : Matrix ι ι K} {d : ι → K} {s : Finset ι} (hd : ∀ i ∈ s, d i ≠ 0) (hminor : ‖(of fun (i j : ι) => (d i)⁻¹ * A i j).principalMinor s‖ = 1) : ‖A.principalMinor s‖ = ∏ i ∈ s, ‖d i‖

Minors of a normalised matrix. If the matrix with entries (d i)⁻¹ * A i j has a principal minor of norm one on s, and the d i with i ∈ s are nonzero, then the principal minor of A on s has norm ∏ i ∈ s, ‖d i‖.

theorem TauCeti.norm_det_sub_le {ι : Type u_1} {R : Type u_2} [Fintype ι] [DecidableEq ι] [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {A B : Matrix ι ι R} {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‖ ≤ ε) : ‖A.det - B.det‖ ≤ ε * M ^ (Fintype.card ι - 1)

Determinants over an ultrametric seminormed ring are Lipschitz on entrywise bounded sets, with constant M ^ (Fintype.card ι - 1) and no factorial loss. This includes empty matrices.

theorem TauCeti.norm_principalMinor_sub_le {ι : Type u_1} {R : Type u_2} [DecidableEq ι] [SeminormedCommRing R] [NormOneClass R] [IsUltrametricDist R] {A B : Matrix ι ι R} {M ε : ℝ} {s : Finset ι} (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‖ ≤ ε) : ‖A.principalMinor s - B.principalMinor s‖ ≤ ε * M ^ (s.card - 1)

Principal minors are Lipschitz on entrywise bounded sets, independently of the choice of indices. The empty principal minors are both one, so the estimate also includes s = ∅.