Absolute values and matrices #
This file proves some bounds on matrices involving absolute values.
Main results #
Matrix.det_le: if the entries of ann × nmatrix are bounded byx, then the determinant is bounded byn! x^nMatrix.det_sum_le: if we havesn × nmatrices and the entries of each matrix are bounded byx, then the determinant of their sum is bounded byn! (s * x)^nMatrix.det_sum_smul_le: if we havesn × nmatrices each multiplied by a constant bounded byy, and the entries of each matrix are bounded byx, then the determinant of the linear combination is bounded byn! (s * y * x)^n
theorem
Matrix.det_le
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Nontrivial R]
[LinearOrderedCommRing 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 (Matrix.det A) ≤ Nat.factorial (Fintype.card n) • x ^ Fintype.card n
theorem
Matrix.det_sum_le
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Nontrivial R]
[LinearOrderedCommRing 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 (Matrix.det (Finset.sum s fun (k : ι) => A k)) ≤ Nat.factorial (Fintype.card n) • (s.card • x) ^ Fintype.card n
theorem
Matrix.det_sum_smul_le
{R : Type u_1}
{S : Type u_2}
[CommRing R]
[Nontrivial R]
[LinearOrderedCommRing 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 (Matrix.det (Finset.sum s fun (k : ι) => c k • A k)) ≤ Nat.factorial (Fintype.card n) • (s.card • y * x) ^ Fintype.card n