Documentation

Mathlib.LinearAlgebra.Matrix.AbsoluteValue

Absolute values and matrices #

This file proves some bounds on matrices involving absolute values.

Main results #

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 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] [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 (ks, 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] [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 (ks, c k A k).det (Fintype.card n).factorial (s.card y * x) ^ Fintype.card n