det_sum_smul_le — Mathlib

English

Let s be a finite index set and for each k in ι let A_k be an n×n matrix over a commutative ring R. Suppose there exist x and y in an ordered codomain S of an absolute value abv such that abv(A_k,i j) ≤ x for all k,i,j and abv(c_k) ≤ y for all k. Then the absolute value of the determinant of the sum det(∑_{k∈s} c_k A_k) is bounded by n! times (|s| · y · x)^{n}.

Русский

Пусть s − конечное множество индексов ι и для каждого k∈ι матрица A_k ∈ M_n(R). Пусть существуют x∈S и y∈S такие, что для всех k,i,j выполняется abv(A_k,i j) ≤ x и abv(c_k) ≤ y для всех k. Тогда абсолютизированное значение детерминанта суммы det(∑_{k∈s} c_k A_k) удовлетворяет неравенству: abv(det(∑_{k∈s} c_k A_k)) ≤ factorial(n) · (#s · y · x)^{n}.

LaTeX

$$$$\\operatorname{abv}\\left(\\det\\left(\\sum_{k \\in s} c_k \\cdot A_k\\right)\\right) \\le \\operatorname{factorial}\\left(Fintype.card\,n\\right) \\cdot (\\#s \\cdot y \\cdot x)^{Fintype.card\,n}$$$$

Lean4

theorem det_sum_smul_le {ι : Type*} (s : Finset ι) {c : ι → R} {A : ι → Matrix n n R} {abv : AbsoluteValue R S} {x : S}
    (hx : ∀ k i j, abv (A k i j) ≤ x) {y : S} (hy : ∀ k, abv (c k) ≤ y) :
    abv (det (∑ k ∈ s, c k • A k)) ≤ Nat.factorial (Fintype.card n) • (#s • y * x) ^ Fintype.card n := by
  simpa only [smul_mul_assoc] using
    det_sum_le s fun k i j =>
      calc
        abv (c k * A k i j) = abv (c k) * abv (A k i j) := abv.map_mul _ _
        _ ≤ y * x := mul_le_mul (hy k) (hx k i j) (abv.nonneg _) ((abv.nonneg _).trans (hy k))

Похожие утверждения