Absolute values and matrices #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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}
[comm_ring R]
[nontrivial R]
[linear_ordered_comm_ring S]
{n : Type u_3}
[fintype n]
[decidable_eq n]
{A : matrix n n R}
{abv : absolute_value 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}
[comm_ring R]
[nontrivial R]
[linear_ordered_comm_ring S]
{n : Type u_3}
[fintype n]
[decidable_eq n]
{ι : Type u_4}
(s : finset ι)
{A : ι → matrix n n R}
{abv : absolute_value R S}
{x : S}
(hx : ∀ (k : ι) (i j : n), ⇑abv (A k i j) ≤ x) :
theorem
matrix.det_sum_smul_le
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[nontrivial R]
[linear_ordered_comm_ring S]
{n : Type u_3}
[fintype n]
[decidable_eq n]
{ι : Type u_4}
(s : finset ι)
{c : ι → R}
{A : ι → matrix n n R}
{abv : absolute_value R S}
{x : S}
(hx : ∀ (k : ι) (i j : n), ⇑abv (A k i j) ≤ x)
{y : S}
(hy : ∀ (k : ι), ⇑abv (c k) ≤ y) :