English
The vecMul of a block matrix equals the sum of vecMul of its blocks split by the vector x: x ᵥ* fromBlocks A B C D = Sum.elim ((x ∘ Sum.inl) ᵥ* A + (x ∘ Sum.inr) ᵥ* C) ((x ∘ Sum.inl) ᵥ* B + (x ∘ Sum.inr) ᵥ* D).
Русский
Векторное умножение-умножение на блок-матрицу равно сумме по блокам: x ᵥ* fromBlocks A B C D = Sum.elim ((x ∘ Sum.inl) ᵥ* A + (x ∘ Sum.inr) ᵥ* C) ((x ∘ Sum.inl) ᵥ* B + (x ∘ Sum.inr) ᵥ* D).
LaTeX
$$$ x ᵥ* \\text{fromBlocks } A B C D = \\text{Sum.elim } \\big( (x \\circ Sum.inl) ᵥ* A + (x \\circ Sum.inr) ᵥ* C \\big) \\big( (x \\circ Sum.inl) ᵥ* B + (x \\circ Sum.inr) ᵥ* D \\big) $$$
Lean4
theorem vecMul_fromBlocks [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α] (A : Matrix n l α) (B : Matrix n m α)
(C : Matrix o l α) (D : Matrix o m α) (x : n ⊕ o → α) :
x ᵥ* fromBlocks A B C D =
Sum.elim ((x ∘ Sum.inl) ᵥ* A + (x ∘ Sum.inr) ᵥ* C) ((x ∘ Sum.inl) ᵥ* B + (x ∘ Sum.inr) ᵥ* D) :=
by
ext i
cases i <;> simp [vecMul, dotProduct]
