fromBlocks_mulVec — Mathlib

English

Multiplication by a block matrix times a concatenated vector splits according to blocks: (fromBlocks A B C D) *ᵥ x equals the appropriate blockwise sums of A,B with the left part of x and C,D with the right part.

Русский

Умножение блочной матрицы на вектор-строку: (fromBlocks A B C D) *ᵥ x равно соответствующим блочным суммам A,B и C,D, разделённым по частям x.

LaTeX

$$$ (\\text{fromBlocks } A B C D) *\\!\\!\\!\\! ᵥ x = \\text{Sum.elim } (A *ᵥ (x \\circ Sum.inl) + B *ᵥ (x \\circ Sum.inr)) (C *ᵥ (x \\circ Sum.inl) + D *ᵥ (x \\circ Sum.inr)) $$$

Lean4

theorem fromBlocks_mulVec [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix n l α) (B : Matrix n m α)
    (C : Matrix o l α) (D : Matrix o m α) (x : l ⊕ m → α) :
    (fromBlocks A B C D) *ᵥ x =
      Sum.elim (A *ᵥ (x ∘ Sum.inl) + B *ᵥ (x ∘ Sum.inr)) (C *ᵥ (x ∘ Sum.inl) + D *ᵥ (x ∘ Sum.inr)) :=
  by
  ext i
  cases i <;> simp [mulVec, dotProduct]

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