Absolute values and matrices

This file proves some bounds on matrices involving absolute values.

Main results

• Matrix.det_le: if the entries of an n × n matrix are bounded by x, then the determinant is bounded by n! x^n
• Matrix.det_sum_le: if we have s n × n matrices and the entries of each matrix are bounded by x, then the determinant of their sum is bounded by n! (s * x)^n
• Matrix.det_sum_smul_le: if we have s n × n matrices each multiplied by a constant bounded by y, and the entries of each matrix are bounded by x, then the determinant of the linear combination is bounded by n! (s * y * x)^n

theorem Matrix.det_le {R : Type u_1} {S : Type u_2} [CommRing R] [Nontrivial R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {n : Type u_3} [Fintype n] [DecidableEq n] {A : Matrix n n R} {abv : AbsoluteValue R S} {x : S} (hx : ∀ (i j : n), abv (A i j) ≤ x) : abv A.det ≤ (Fintype.card n).factorial • x ^ Fintype.card n

theorem Matrix.det_sum_le {R : Type u_1} {S : Type u_2} [CommRing R] [Nontrivial R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {n : Type u_3} [Fintype n] [DecidableEq n] {ι : Type u_4} (s : Finset ι) {A : ι → Matrix n n R} {abv : AbsoluteValue R S} {x : S} (hx : ∀ (k : ι) (i j : n), abv (A k i j) ≤ x) : abv (∑ k ∈ s, A k).det ≤ (Fintype.card n).factorial • (s.card • x) ^ Fintype.card n

theorem Matrix.det_sum_smul_le {R : Type u_1} {S : Type u_2} [CommRing R] [Nontrivial R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] {n : Type u_3} [Fintype n] [DecidableEq n] {ι : Type u_4} (s : Finset ι) {c : ι → R} {A : ι → Matrix n n R} {abv : AbsoluteValue R S} {x : S} (hx : ∀ (k : ι) (i j : n), abv (A k i j) ≤ x) {y : S} (hy : ∀ (k : ι), abv (c k) ≤ y) : abv (∑ k ∈ s, c k • A k).det ≤ (Fintype.card n).factorial • (s.card • y * x) ^ Fintype.card n