mathlib documentation

linear_algebra.matrix.absolute_value

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} [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) :
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) :
abv (∑ (k : ι) in s, A k).det (fintype.card n)! (s.card x) ^ fintype.card n
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) :
abv (∑ (k : ι) in s, c k A k).det (fintype.card n)! ((s.card y) * x) ^ fintype.card n