The ℓ¹ and ultrametric forms of Hadamard's determinant bound

For a square matrix A and an absolute value abv, the absolute value of the determinant is at most the product over the rows of the ℓ¹ norms of the rows: abv A.det ≤ ∏ i, ∑ j, abv (A i j), and the same holds with columns in place of rows. When abv is nonarchimedean (IsNonarchimedean abv), the ultrametric inequality on the Leibniz sum replaces the ℓ¹ sum by an entrywise row or column bound: if abv (A i j) ≤ b i (or b j), then abv A.det ≤ ∏ i, b i (or ∏ j, b j).

The proof is the Leibniz expansion. Each permutation contributes one product ∏ i, abv (A i (σ i)), and expanding the product of the row sums gives the sum of ∏ i, abv (A i (f i)) over all maps f, of which the permutations are a part. In the nonarchimedean case, IsNonarchimedean.finset_image_add_of_nonempty bounds abv A.det by a single permutation term instead of the sum. These bounds complement Mathlib's Matrix.det_le, which bounds the determinant by n! · x ^ n from a uniform entrywise bound x; the ℓ¹ form is sharper when the rows have very different sizes, as for the logarithmic embeddings of a family of units in the bound on the regulator.

Main results

• Matrix.abv_det_le_prod_sum_abv: abv A.det ≤ ∏ i, ∑ j, abv (A i j), the row form.
• Matrix.abv_det_le_prod_sum_abv': abv A.det ≤ ∏ j, ∑ i, abv (A i j), the column form.
• Matrix.abs_det_le_prod_sum_abs and Matrix.abs_det_le_prod_sum_abs': the same bounds for |·| over a linearly ordered commutative ring.
• Matrix.abv_det_le_prod_of_le and Matrix.abv_det_le_prod_of_le': for nonarchimedean abv, entrywise row bounds b i or column bounds b j give abv A.det ≤ ∏ i, b i and abv A.det ≤ ∏ j, b j.
• Matrix.abv_det_le_factorial_mul_of_forall_perm: a bound on each permutation product gives the same bound on the determinant, multiplied by the factorial of the matrix size.

theorem Matrix.abv_det_le_prod_sum_abv' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {n : Type u_3} [Fintype n] [DecidableEq n] (A : Matrix n n R) (abv : AbsoluteValue R S) : abv A.det ≤ ∏ j : n, ∑ i : n, abv (A i j)

Hadamard's bound, ℓ¹ column form. The absolute value of a determinant is at most the product of the ℓ¹ norms of the columns.

theorem Matrix.abv_det_le_prod_sum_abv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {n : Type u_3} [Fintype n] [DecidableEq n] (A : Matrix n n R) (abv : AbsoluteValue R S) : abv A.det ≤ ∏ i : n, ∑ j : n, abv (A i j)

Hadamard's bound, ℓ¹ row form. The absolute value of a determinant is at most the product of the ℓ¹ norms of the rows.

theorem Matrix.abs_det_le_prod_sum_abs' {S : Type u_2} [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {n : Type u_3} [Fintype n] [DecidableEq n] (A : Matrix n n S) : |A.det| ≤ ∏ j : n, ∑ i : n, |A i j|

Hadamard's bound, ℓ¹ column form, for |·|. Over a linearly ordered commutative ring, |det A| is at most the product of the ℓ¹ norms of the columns of A.

theorem Matrix.abs_det_le_prod_sum_abs {S : Type u_2} [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {n : Type u_3} [Fintype n] [DecidableEq n] (A : Matrix n n S) : |A.det| ≤ ∏ i : n, ∑ j : n, |A i j|

Hadamard's bound, ℓ¹ row form, for |·|. Over a linearly ordered commutative ring, |det A| is at most the product of the ℓ¹ norms of the rows of A.

theorem Matrix.abv_det_le_prod_of_le' {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {n : Type u_3} [Fintype n] [DecidableEq n] (A : Matrix n n R) {abv : AbsoluteValue R S} (habv : IsNonarchimedean ⇑abv) {b : n → S} (hA : ∀ (i j : n), abv (A i j) ≤ b j) : abv A.det ≤ ∏ j : n, b j

Ultrametric Hadamard bound, column form. For a nonarchimedean absolute value abv, if column j of A is bounded entrywise in abv by b j, then abv A.det ≤ ∏ j, b j.

theorem Matrix.abv_det_le_prod_of_le {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {n : Type u_3} [Fintype n] [DecidableEq n] (A : Matrix n n R) {abv : AbsoluteValue R S} (habv : IsNonarchimedean ⇑abv) {b : n → S} (hA : ∀ (i j : n), abv (A i j) ≤ b i) : abv A.det ≤ ∏ i : n, b i

Ultrametric Hadamard bound, row form. For a nonarchimedean absolute value abv, if row i of A is bounded entrywise in abv by b i, then abv A.det ≤ ∏ i, b i.

theorem Matrix.abv_det_le_factorial_mul_of_forall_perm {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {n : Type u_3} [Fintype n] [DecidableEq n] (A : Matrix n n R) (abv : AbsoluteValue R S) {B : S} (hA : ∀ (σ : Equiv.Perm n), ∏ i : n, abv (A (σ i) i) ≤ B) : abv A.det ≤ ↑(Fintype.card n).factorial * B

A uniform bound on the absolute values of all permutation products bounds the determinant by the same bound times the factorial of the matrix size. Unlike an entrywise bound, this can retain correlations between the factors in each permutation product.