English
For a finite collection of matrices A_k with entrywise bound by x, the determinant of their sum is bounded by (n)! times (#s · x)^n.
Русский
Для конечной коллекции матриц A_k с покрайней величиной ограниченной на x, детерминант суммы ограничен (n)! · (#s · x)^n.
LaTeX
$$abv (det (s.sum fun k => A k)) ≤ (Fintype.card n)! · (#s · x) ^ Fintype.card n$$
Lean4
theorem det_sum_le {ι : Type*} (s : Finset ι) {A : ι → Matrix n n R} {abv : AbsoluteValue R S} {x : S}
(hx : ∀ k i j, abv (A k i j) ≤ x) : abv (det (∑ k ∈ s, A k)) ≤ (Fintype.card n)! • (#s • x) ^ Fintype.card n :=
det_le fun i j =>
calc
abv ((∑ k ∈ s, A k) i j) = abv (∑ k ∈ s, A k i j) := by simp only [sum_apply]
_ ≤ ∑ k ∈ s, abv (A k i j) := (abv.sum_le _ _)
_ ≤ ∑ _k ∈ s, x := by gcongr; apply hx
_ = #s • x := sum_const _
