Block Matrices #
Main definitions #
matrix.from_blocks: build a block matrix out of 4 blocksmatrix.to_blocks₁₁,matrix.to_blocks₁₂,matrix.to_blocks₂₁,matrix.to_blocks₂₂: extract each of the four blocks frommatrix.from_blocks.matrix.block_diagonal: block diagonal of equally sized blocks. On square blocks, this is a ring homomorphisms,matrix.block_diagonal_ring_hom.matrix.block_diag: extract the blocks from the diagonal of a block diagonal matrix.matrix.block_diagonal': block diagonal of unequally sized blocks. On square blocks, this is a ring homomorphisms,matrix.block_diagonal'_ring_hom.matrix.block_diag': extract the blocks from the diagonal of a block diagonal matrix.
def
matrix.from_blocks
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
We can form a single large matrix by flattening smaller 'block' matrices of compatible dimensions.
@[simp]
theorem
matrix.from_blocks_apply₁₁
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(i : n)
(j : l) :
matrix.from_blocks A B C D (sum.inl i) (sum.inl j) = A i j
@[simp]
theorem
matrix.from_blocks_apply₁₂
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(i : n)
(j : m) :
matrix.from_blocks A B C D (sum.inl i) (sum.inr j) = B i j
@[simp]
theorem
matrix.from_blocks_apply₂₁
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(i : o)
(j : l) :
matrix.from_blocks A B C D (sum.inr i) (sum.inl j) = C i j
@[simp]
theorem
matrix.from_blocks_apply₂₂
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(i : o)
(j : m) :
matrix.from_blocks A B C D (sum.inr i) (sum.inr j) = D i j
def
matrix.to_blocks₁₁
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(M : matrix (n ⊕ o) (l ⊕ m) α) :
matrix n l α
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "top left" submatrix.
def
matrix.to_blocks₁₂
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(M : matrix (n ⊕ o) (l ⊕ m) α) :
matrix n m α
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "top right" submatrix.
def
matrix.to_blocks₂₁
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(M : matrix (n ⊕ o) (l ⊕ m) α) :
matrix o l α
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "bottom left" submatrix.
def
matrix.to_blocks₂₂
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(M : matrix (n ⊕ o) (l ⊕ m) α) :
matrix o m α
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "bottom right" submatrix.
theorem
matrix.from_blocks_to_blocks
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(M : matrix (n ⊕ o) (l ⊕ m) α) :
@[simp]
theorem
matrix.to_blocks_from_blocks₁₁
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
(matrix.from_blocks A B C D).to_blocks₁₁ = A
@[simp]
theorem
matrix.to_blocks_from_blocks₁₂
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
(matrix.from_blocks A B C D).to_blocks₁₂ = B
@[simp]
theorem
matrix.to_blocks_from_blocks₂₁
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
(matrix.from_blocks A B C D).to_blocks₂₁ = C
@[simp]
theorem
matrix.to_blocks_from_blocks₂₂
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
(matrix.from_blocks A B C D).to_blocks₂₂ = D
theorem
matrix.from_blocks_map
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
{β : Type u_13}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(f : α → β) :
(matrix.from_blocks A B C D).map f = matrix.from_blocks (A.map f) (B.map f) (C.map f) (D.map f)
theorem
matrix.from_blocks_transpose
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
(matrix.from_blocks A B C D).transpose = matrix.from_blocks A.transpose C.transpose B.transpose D.transpose
@[simp]
theorem
matrix.from_blocks_submatrix_sum_swap_left
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{p : Type u_5}
{α : Type u_12}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(f : p → l ⊕ m) :
(matrix.from_blocks A B C D).submatrix sum.swap f = (matrix.from_blocks C D A B).submatrix id f
@[simp]
theorem
matrix.from_blocks_submatrix_sum_swap_right
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{p : Type u_5}
{α : Type u_12}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(f : p → n ⊕ o) :
(matrix.from_blocks A B C D).submatrix f sum.swap = (matrix.from_blocks B A D C).submatrix f id
theorem
matrix.from_blocks_submatrix_sum_swap_sum_swap
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_5}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
(matrix.from_blocks A B C D).submatrix sum.swap sum.swap = matrix.from_blocks D C B A
def
matrix.is_two_block_diagonal
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[has_zero α]
(A : matrix (n ⊕ o) (l ⊕ m) α) :
Prop
A 2x2 block matrix is block diagonal if the blocks outside of the diagonal vanish
Equations
- A.is_two_block_diagonal = (A.to_blocks₁₂ = 0 ∧ A.to_blocks₂₁ = 0)
def
matrix.to_block
{m : Type u_2}
{n : Type u_3}
{α : Type u_12}
(M : matrix m n α)
(p : m → Prop)
(q : n → Prop) :
matrix {a // p a} {a // q a} α
Let p pick out certain rows and q pick out certain columns of a matrix M. Then
to_block M p q is the corresponding block matrix.
def
matrix.to_square_block
{m : Type u_2}
{α : Type u_12}
(M : matrix m m α)
{n : ℕ}
(b : m → fin n)
(k : fin n) :
Let b map rows and columns of a square matrix M to blocks. Then
to_square_block M b k is the block k matrix.
Equations
- M.to_square_block b k = M.submatrix coe coe
Alternate version with b : m → nat. Let b map rows and columns of a square matrix M to
blocks. Then to_square_block' M b k is the block k matrix.
Equations
- M.to_square_block' b k = M.submatrix coe coe
@[simp]
theorem
matrix.to_square_block_def'
{m : Type u_2}
{α : Type u_12}
(M : matrix m m α)
(b : m → ℕ)
(k : ℕ) :
M.to_square_block' b k = λ (i j : {a // b a = k}), M ↑i ↑j
def
matrix.to_square_block_prop
{m : Type u_2}
{α : Type u_12}
(M : matrix m m α)
(p : m → Prop) :
matrix {a // p a} {a // p a} α
Let p pick out certain rows and columns of a square matrix M. Then
to_square_block_prop M p is the corresponding block matrix.
Equations
- M.to_square_block_prop p = M.submatrix coe coe
@[simp]
theorem
matrix.to_square_block_prop_def
{m : Type u_2}
{α : Type u_12}
(M : matrix m m α)
(p : m → Prop) :
M.to_square_block_prop p = λ (i j : {a // p a}), M ↑i ↑j
theorem
matrix.from_blocks_smul
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{R : Type u_10}
{α : Type u_12}
[has_smul R α]
(x : R)
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
x • matrix.from_blocks A B C D = matrix.from_blocks (x • A) (x • B) (x • C) (x • D)
theorem
matrix.from_blocks_add
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[has_add α]
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(A' : matrix n l α)
(B' : matrix n m α)
(C' : matrix o l α)
(D' : matrix o m α) :
matrix.from_blocks A B C D + matrix.from_blocks A' B' C' D' = matrix.from_blocks (A + A') (B + B') (C + C') (D + D')
theorem
matrix.from_blocks_multiply
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{p : Type u_5}
{q : Type u_6}
{α : Type u_12}
[fintype l]
[fintype m]
[non_unital_non_assoc_semiring α]
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(A' : matrix l p α)
(B' : matrix l q α)
(C' : matrix m p α)
(D' : matrix m q α) :
theorem
matrix.from_blocks_mul_vec
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[fintype l]
[fintype m]
[non_unital_non_assoc_semiring α]
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(x : l ⊕ m → α) :
theorem
matrix.vec_mul_from_blocks
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[fintype n]
[fintype o]
[non_unital_non_assoc_semiring α]
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(x : n ⊕ o → α) :
matrix.vec_mul x (matrix.from_blocks A B C D) = sum.elim (matrix.vec_mul (x ∘ sum.inl) A + matrix.vec_mul (x ∘ sum.inr) C) (matrix.vec_mul (x ∘ sum.inl) B + matrix.vec_mul (x ∘ sum.inr) D)
@[simp]
theorem
matrix.from_blocks_diagonal
{l : Type u_1}
{m : Type u_2}
{α : Type u_12}
[decidable_eq l]
[decidable_eq m]
[has_zero α]
(d₁ : l → α)
(d₂ : m → α) :
matrix.from_blocks (matrix.diagonal d₁) 0 0 (matrix.diagonal d₂) = matrix.diagonal (sum.elim d₁ d₂)
@[simp]
theorem
matrix.from_blocks_one
{l : Type u_1}
{m : Type u_2}
{α : Type u_12}
[decidable_eq l]
[decidable_eq m]
[has_zero α]
[has_one α] :
matrix.from_blocks 1 0 0 1 = 1
def
matrix.block_diagonal
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : o → matrix m n α) :
matrix.block_diagonal M turns a homogenously-indexed collection of matrices
M : o → matrix m n α' into a m × o-by-n × o block matrix which has the entries of M along
the diagonal and zero elsewhere.
See also matrix.block_diagonal' if the matrices may not have the same size everywhere.
Equations
- matrix.block_diagonal M (i, k) (j, k') = ite (k = k') (M k i j) 0
@[simp]
theorem
matrix.block_diagonal_apply_eq
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : o → matrix m n α)
(i : m)
(j : n)
(k : o) :
matrix.block_diagonal M (i, k) (j, k) = M k i j
theorem
matrix.block_diagonal_apply_ne
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : o → matrix m n α)
(i : m)
(j : n)
{k k' : o}
(h : k ≠ k') :
matrix.block_diagonal M (i, k) (j, k') = 0
theorem
matrix.block_diagonal_map
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
{β : Type u_13}
[decidable_eq o]
[has_zero α]
[has_zero β]
(M : o → matrix m n α)
(f : α → β)
(hf : f 0 = 0) :
(matrix.block_diagonal M).map f = matrix.block_diagonal (λ (k : o), (M k).map f)
@[simp]
theorem
matrix.block_diagonal_transpose
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : o → matrix m n α) :
(matrix.block_diagonal M).transpose = matrix.block_diagonal (λ (k : o), (M k).transpose)
@[simp]
theorem
matrix.block_diagonal_conj_transpose
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[decidable_eq o]
{α : Type u_1}
[add_monoid α]
[star_add_monoid α]
(M : o → matrix m n α) :
(matrix.block_diagonal M).conj_transpose = matrix.block_diagonal (λ (k : o), (M k).conj_transpose)
@[simp]
theorem
matrix.block_diagonal_zero
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α] :
@[simp]
theorem
matrix.block_diagonal_diagonal
{m : Type u_2}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
[decidable_eq m]
(d : o → m → α) :
matrix.block_diagonal (λ (k : o), matrix.diagonal (d k)) = matrix.diagonal (λ (ik : m × o), d ik.snd ik.fst)
@[simp]
theorem
matrix.block_diagonal_one
{m : Type u_2}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
[decidable_eq m]
[has_one α] :
@[simp]
theorem
matrix.block_diagonal_add
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[add_zero_class α]
(M N : o → matrix m n α) :
@[simp]
theorem
matrix.block_diagonal_add_monoid_hom_apply
(m : Type u_2)
(n : Type u_3)
(o : Type u_4)
(α : Type u_12)
[decidable_eq o]
[add_zero_class α]
(M : o → matrix m n α) :
⇑(matrix.block_diagonal_add_monoid_hom m n o α) M = matrix.block_diagonal M
def
matrix.block_diagonal_add_monoid_hom
(m : Type u_2)
(n : Type u_3)
(o : Type u_4)
(α : Type u_12)
[decidable_eq o]
[add_zero_class α] :
matrix.block_diagonal as an add_monoid_hom.
Equations
- matrix.block_diagonal_add_monoid_hom m n o α = {to_fun := matrix.block_diagonal (add_zero_class.to_has_zero α), map_zero' := _, map_add' := _}
@[simp]
theorem
matrix.block_diagonal_neg
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[add_group α]
(M : o → matrix m n α) :
@[simp]
theorem
matrix.block_diagonal_sub
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[add_group α]
(M N : o → matrix m n α) :
@[simp]
theorem
matrix.block_diagonal_mul
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{p : Type u_5}
{α : Type u_12}
[decidable_eq o]
[fintype n]
[fintype o]
[non_unital_non_assoc_semiring α]
(M : o → matrix m n α)
(N : o → matrix n p α) :
matrix.block_diagonal (λ (k : o), (M k).mul (N k)) = (matrix.block_diagonal M).mul (matrix.block_diagonal N)
@[simp]
theorem
matrix.block_diagonal_ring_hom_apply
(m : Type u_2)
(o : Type u_4)
(α : Type u_12)
[decidable_eq o]
[decidable_eq m]
[fintype o]
[fintype m]
[non_assoc_semiring α]
(M : o → matrix m m α) :
⇑(matrix.block_diagonal_ring_hom m o α) M = matrix.block_diagonal M
def
matrix.block_diagonal_ring_hom
(m : Type u_2)
(o : Type u_4)
(α : Type u_12)
[decidable_eq o]
[decidable_eq m]
[fintype o]
[fintype m]
[non_assoc_semiring α] :
matrix.block_diagonal as a ring_hom.
Equations
- matrix.block_diagonal_ring_hom m o α = {to_fun := matrix.block_diagonal (mul_zero_class.to_has_zero α), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
matrix.block_diagonal_pow
{m : Type u_2}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[decidable_eq m]
[fintype o]
[fintype m]
[semiring α]
(M : o → matrix m m α)
(n : ℕ) :
matrix.block_diagonal (M ^ n) = matrix.block_diagonal M ^ n
@[simp]
theorem
matrix.block_diagonal_smul
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
{R : Type u_1}
[monoid R]
[add_monoid α]
[distrib_mul_action R α]
(x : R)
(M : o → matrix m n α) :
matrix.block_diagonal (x • M) = x • matrix.block_diagonal M
def
matrix.block_diag
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(M : matrix (m × o) (n × o) α)
(k : o) :
matrix m n α
Extract a block from the diagonal of a block diagonal matrix.
This is the block form of matrix.diag, and the left-inverse of matrix.block_diagonal.
Equations
- M.block_diag k i j = M (i, k) (j, k)
theorem
matrix.block_diag_map
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
{β : Type u_13}
(M : matrix (m × o) (n × o) α)
(f : α → β) :
(M.map f).block_diag = λ (k : o), (M.block_diag k).map f
@[simp]
theorem
matrix.block_diag_transpose
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
(M : matrix (m × o) (n × o) α)
(k : o) :
M.transpose.block_diag k = (M.block_diag k).transpose
@[simp]
theorem
matrix.block_diag_conj_transpose
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_1}
[add_monoid α]
[star_add_monoid α]
(M : matrix (m × o) (n × o) α)
(k : o) :
M.conj_transpose.block_diag k = (M.block_diag k).conj_transpose
@[simp]
theorem
matrix.block_diag_zero
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[has_zero α] :
0.block_diag = 0
@[simp]
theorem
matrix.block_diag_diagonal
{m : Type u_2}
{o : Type u_4}
{α : Type u_12}
[has_zero α]
[decidable_eq o]
[decidable_eq m]
(d : m × o → α)
(k : o) :
(matrix.diagonal d).block_diag k = matrix.diagonal (λ (i : m), d (i, k))
@[simp]
theorem
matrix.block_diag_block_diagonal
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[has_zero α]
[decidable_eq o]
(M : o → matrix m n α) :
(matrix.block_diagonal M).block_diag = M
@[simp]
theorem
matrix.block_diag_one
{m : Type u_2}
{o : Type u_4}
{α : Type u_12}
[has_zero α]
[decidable_eq o]
[decidable_eq m]
[has_one α] :
1.block_diag = 1
@[simp]
theorem
matrix.block_diag_add
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[add_zero_class α]
(M N : matrix (m × o) (n × o) α) :
(M + N).block_diag = M.block_diag + N.block_diag
def
matrix.block_diag_add_monoid_hom
(m : Type u_2)
(n : Type u_3)
(o : Type u_4)
(α : Type u_12)
[add_zero_class α] :
matrix.block_diag as an add_monoid_hom.
Equations
- matrix.block_diag_add_monoid_hom m n o α = {to_fun := matrix.block_diag α, map_zero' := _, map_add' := _}
@[simp]
theorem
matrix.block_diag_add_monoid_hom_apply
(m : Type u_2)
(n : Type u_3)
(o : Type u_4)
(α : Type u_12)
[add_zero_class α]
(M : matrix (m × o) (n × o) α)
(k : o) :
⇑(matrix.block_diag_add_monoid_hom m n o α) M k = M.block_diag k
@[simp]
theorem
matrix.block_diag_neg
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[add_group α]
(M : matrix (m × o) (n × o) α) :
(-M).block_diag = -M.block_diag
@[simp]
theorem
matrix.block_diag_sub
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[add_group α]
(M N : matrix (m × o) (n × o) α) :
(M - N).block_diag = M.block_diag - N.block_diag
@[simp]
theorem
matrix.block_diag_smul
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
{R : Type u_1}
[monoid R]
[add_monoid α]
[distrib_mul_action R α]
(x : R)
(M : matrix (m × o) (n × o) α) :
(x • M).block_diag = x • M.block_diag
def
matrix.block_diagonal'
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : Π (i : o), matrix (m' i) (n' i) α) :
matrix (Σ (i : o), m' i) (Σ (i : o), n' i) α
matrix.block_diagonal' M turns M : Π i, matrix (m i) (n i) α into a
Σ i, m i-by-Σ i, n i block matrix which has the entries of M along the diagonal
and zero elsewhere.
This is the dependently-typed version of matrix.block_diagonal.
theorem
matrix.block_diagonal'_eq_block_diagonal
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : o → matrix m n α)
{k k' : o}
(i : m)
(j : n) :
matrix.block_diagonal M (i, k) (j, k') = matrix.block_diagonal' M ⟨k, i⟩ ⟨k', j⟩
theorem
matrix.block_diagonal'_submatrix_eq_block_diagonal
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : o → matrix m n α) :
theorem
matrix.block_diagonal'_apply
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : Π (i : o), matrix (m' i) (n' i) α)
(ik : Σ (i : o), m' i)
(jk : Σ (i : o), n' i) :
@[simp]
theorem
matrix.block_diagonal'_apply_eq
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : Π (i : o), matrix (m' i) (n' i) α)
(k : o)
(i : m' k)
(j : n' k) :
matrix.block_diagonal' M ⟨k, i⟩ ⟨k, j⟩ = M k i j
theorem
matrix.block_diagonal'_apply_ne
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : Π (i : o), matrix (m' i) (n' i) α)
{k k' : o}
(i : m' k)
(j : n' k')
(h : k ≠ k') :
matrix.block_diagonal' M ⟨k, i⟩ ⟨k', j⟩ = 0
theorem
matrix.block_diagonal'_map
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
{β : Type u_13}
[decidable_eq o]
[has_zero α]
[has_zero β]
(M : Π (i : o), matrix (m' i) (n' i) α)
(f : α → β)
(hf : f 0 = 0) :
(matrix.block_diagonal' M).map f = matrix.block_diagonal' (λ (k : o), (M k).map f)
@[simp]
theorem
matrix.block_diagonal'_transpose
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
(M : Π (i : o), matrix (m' i) (n' i) α) :
(matrix.block_diagonal' M).transpose = matrix.block_diagonal' (λ (k : o), (M k).transpose)
@[simp]
theorem
matrix.block_diagonal'_conj_transpose
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
[decidable_eq o]
{α : Type u_1}
[add_monoid α]
[star_add_monoid α]
(M : Π (i : o), matrix (m' i) (n' i) α) :
(matrix.block_diagonal' M).conj_transpose = matrix.block_diagonal' (λ (k : o), (M k).conj_transpose)
@[simp]
theorem
matrix.block_diagonal'_zero
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[has_zero α] :
@[simp]
theorem
matrix.block_diagonal'_diagonal
{o : Type u_4}
{m' : o → Type u_7}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
[Π (i : o), decidable_eq (m' i)]
(d : Π (i : o), m' i → α) :
matrix.block_diagonal' (λ (k : o), matrix.diagonal (d k)) = matrix.diagonal (λ (ik : Σ (i : o), m' i), d ik.fst ik.snd)
@[simp]
theorem
matrix.block_diagonal'_one
{o : Type u_4}
{m' : o → Type u_7}
{α : Type u_12}
[decidable_eq o]
[has_zero α]
[Π (i : o), decidable_eq (m' i)]
[has_one α] :
@[simp]
theorem
matrix.block_diagonal'_add
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[add_zero_class α]
(M N : Π (i : o), matrix (m' i) (n' i) α) :
def
matrix.block_diagonal'_add_monoid_hom
{o : Type u_4}
(m' : o → Type u_7)
(n' : o → Type u_8)
(α : Type u_12)
[decidable_eq o]
[add_zero_class α] :
matrix.block_diagonal' as an add_monoid_hom.
Equations
- matrix.block_diagonal'_add_monoid_hom m' n' α = {to_fun := matrix.block_diagonal' (add_zero_class.to_has_zero α), map_zero' := _, map_add' := _}
@[simp]
theorem
matrix.block_diagonal'_add_monoid_hom_apply
{o : Type u_4}
(m' : o → Type u_7)
(n' : o → Type u_8)
(α : Type u_12)
[decidable_eq o]
[add_zero_class α]
(M : Π (i : o), matrix ((λ (i : o), m' i) i) ((λ (i : o), n' i) i) α) :
⇑(matrix.block_diagonal'_add_monoid_hom m' n' α) M = matrix.block_diagonal' M
@[simp]
theorem
matrix.block_diagonal'_neg
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[add_group α]
(M : Π (i : o), matrix (m' i) (n' i) α) :
@[simp]
theorem
matrix.block_diagonal'_sub
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
[add_group α]
(M N : Π (i : o), matrix (m' i) (n' i) α) :
@[simp]
theorem
matrix.block_diagonal'_mul
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{p' : o → Type u_9}
{α : Type u_12}
[decidable_eq o]
[non_unital_non_assoc_semiring α]
[Π (i : o), fintype (n' i)]
[fintype o]
(M : Π (i : o), matrix (m' i) (n' i) α)
(N : Π (i : o), matrix (n' i) (p' i) α) :
matrix.block_diagonal' (λ (k : o), (M k).mul (N k)) = (matrix.block_diagonal' M).mul (matrix.block_diagonal' N)
def
matrix.block_diagonal'_ring_hom
{o : Type u_4}
(m' : o → Type u_7)
(α : Type u_12)
[decidable_eq o]
[Π (i : o), decidable_eq (m' i)]
[fintype o]
[Π (i : o), fintype (m' i)]
[non_assoc_semiring α] :
matrix.block_diagonal' as a ring_hom.
Equations
- matrix.block_diagonal'_ring_hom m' α = {to_fun := matrix.block_diagonal' (mul_zero_class.to_has_zero α), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
matrix.block_diagonal'_ring_hom_apply
{o : Type u_4}
(m' : o → Type u_7)
(α : Type u_12)
[decidable_eq o]
[Π (i : o), decidable_eq (m' i)]
[fintype o]
[Π (i : o), fintype (m' i)]
[non_assoc_semiring α]
(M : Π (i : o), matrix ((λ (i : o), m' i) i) ((λ (i : o), m' i) i) α) :
@[simp]
theorem
matrix.block_diagonal'_pow
{o : Type u_4}
{m' : o → Type u_7}
{α : Type u_12}
[decidable_eq o]
[Π (i : o), decidable_eq (m' i)]
[fintype o]
[Π (i : o), fintype (m' i)]
[semiring α]
(M : Π (i : o), matrix (m' i) (m' i) α)
(n : ℕ) :
matrix.block_diagonal' (M ^ n) = matrix.block_diagonal' M ^ n
@[simp]
theorem
matrix.block_diagonal'_smul
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[decidable_eq o]
{R : Type u_1}
[semiring R]
[add_comm_monoid α]
[module R α]
(x : R)
(M : Π (i : o), matrix (m' i) (n' i) α) :
matrix.block_diagonal' (x • M) = x • matrix.block_diagonal' M
def
matrix.block_diag'
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
(M : matrix (Σ (i : o), m' i) (Σ (i : o), n' i) α)
(k : o) :
matrix (m' k) (n' k) α
Extract a block from the diagonal of a block diagonal matrix.
This is the block form of matrix.diag, and the left-inverse of matrix.block_diagonal'.
Equations
- M.block_diag' k i j = M ⟨k, i⟩ ⟨k, j⟩
theorem
matrix.block_diag'_map
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
{β : Type u_13}
(M : matrix (Σ (i : o), m' i) (Σ (i : o), n' i) α)
(f : α → β) :
(M.map f).block_diag' = λ (k : o), (M.block_diag' k).map f
@[simp]
theorem
matrix.block_diag'_transpose
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
(M : matrix (Σ (i : o), m' i) (Σ (i : o), n' i) α)
(k : o) :
M.transpose.block_diag' k = (M.block_diag' k).transpose
@[simp]
theorem
matrix.block_diag'_conj_transpose
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_1}
[add_monoid α]
[star_add_monoid α]
(M : matrix (Σ (i : o), m' i) (Σ (i : o), n' i) α)
(k : o) :
M.conj_transpose.block_diag' k = (M.block_diag' k).conj_transpose
@[simp]
theorem
matrix.block_diag'_zero
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[has_zero α] :
0.block_diag' = 0
@[simp]
theorem
matrix.block_diag'_diagonal
{o : Type u_4}
{m' : o → Type u_7}
{α : Type u_12}
[has_zero α]
[decidable_eq o]
[Π (i : o), decidable_eq (m' i)]
(d : (Σ (i : o), m' i) → α)
(k : o) :
(matrix.diagonal d).block_diag' k = matrix.diagonal (λ (i : m' k), d ⟨k, i⟩)
@[simp]
theorem
matrix.block_diag'_block_diagonal'
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[has_zero α]
[decidable_eq o]
(M : Π (i : o), matrix (m' i) (n' i) α) :
@[simp]
theorem
matrix.block_diag'_one
{o : Type u_4}
{m' : o → Type u_7}
{α : Type u_12}
[has_zero α]
[decidable_eq o]
[Π (i : o), decidable_eq (m' i)]
[has_one α] :
1.block_diag' = 1
@[simp]
theorem
matrix.block_diag'_add
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[add_zero_class α]
(M N : matrix (Σ (i : o), m' i) (Σ (i : o), n' i) α) :
(M + N).block_diag' = M.block_diag' + N.block_diag'
@[simp]
theorem
matrix.block_diag'_add_monoid_hom_apply
{o : Type u_4}
(m' : o → Type u_7)
(n' : o → Type u_8)
(α : Type u_12)
[add_zero_class α]
(M : matrix (Σ (i : o), (λ (i : o), m' i) i) (Σ (i : o), (λ (i : o), n' i) i) α)
(k : o) :
⇑(matrix.block_diag'_add_monoid_hom m' n' α) M k = M.block_diag' k
def
matrix.block_diag'_add_monoid_hom
{o : Type u_4}
(m' : o → Type u_7)
(n' : o → Type u_8)
(α : Type u_12)
[add_zero_class α] :
matrix.block_diag' as an add_monoid_hom.
Equations
- matrix.block_diag'_add_monoid_hom m' n' α = {to_fun := matrix.block_diag' α, map_zero' := _, map_add' := _}
@[simp]
theorem
matrix.block_diag'_neg
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[add_group α]
(M : matrix (Σ (i : o), m' i) (Σ (i : o), n' i) α) :
(-M).block_diag' = -M.block_diag'
@[simp]
theorem
matrix.block_diag'_sub
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
[add_group α]
(M N : matrix (Σ (i : o), m' i) (Σ (i : o), n' i) α) :
(M - N).block_diag' = M.block_diag' - N.block_diag'
@[simp]
theorem
matrix.block_diag'_smul
{o : Type u_4}
{m' : o → Type u_7}
{n' : o → Type u_8}
{α : Type u_12}
{R : Type u_1}
[monoid R]
[add_monoid α]
[distrib_mul_action R α]
(x : R)
(M : matrix (Σ (i : o), m' i) (Σ (i : o), n' i) α) :
(x • M).block_diag' = x • M.block_diag'