data.matrix.block - mathlib3 docs

source

theorem matrix.dot_product_block {m : Type u_2} {n : Type u_3} {α : Type u_12} [fintype m] [fintype n] [has_mul α] [add_comm_monoid α] (v w : m ⊕ n → α) :

matrix.dot_product v w = matrix.dot_product (v ∘ sum.inl) (w ∘ sum.inl) + matrix.dot_product (v ∘ sum.inr) (w ∘ sum.inr)

source

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 α) :

matrix (n ⊕ o) (l ⊕ m) α

We can form a single large matrix by flattening smaller 'block' matrices of compatible dimensions.

Equations

matrix.from_blocks A B C D = ⇑matrix.of (sum.elim (λ (i : n), sum.elim (A i) (B i)) (λ (i : o), sum.elim (C i) (D i)))

source

@[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

source

@[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

source

@[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

source

@[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

source

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.

Equations

M.to_blocks₁₁ = ⇑matrix.of (λ (i : n) (j : l), M (sum.inl i) (sum.inl j))

source

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.

Equations

M.to_blocks₁₂ = ⇑matrix.of (λ (i : n) (j : m), M (sum.inl i) (sum.inr j))

source

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.

Equations

M.to_blocks₂₁ = ⇑matrix.of (λ (i : o) (j : l), M (sum.inr i) (sum.inl j))

source

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.

Equations

M.to_blocks₂₂ = ⇑matrix.of (λ (i : o) (j : m), M (sum.inr i) (sum.inr j))

source

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) α) :

matrix.from_blocks M.to_blocks₁₁ M.to_blocks₁₂ M.to_blocks₂₁ M.to_blocks₂₂ = M

source

@[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

source

@[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

source

@[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

source

@[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

source

theorem matrix.ext_iff_blocks {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {A B : matrix (n ⊕ o) (l ⊕ m) α} :

A = B ↔ A.to_blocks₁₁ = B.to_blocks₁₁ ∧ A.to_blocks₁₂ = B.to_blocks₁₂ ∧ A.to_blocks₂₁ = B.to_blocks₂₁ ∧ A.to_blocks₂₂ = B.to_blocks₂₂

Two block matrices are equal if their blocks are equal.

source

@[simp]

theorem matrix.from_blocks_inj {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 α} {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' ↔ A = A' ∧ B = B' ∧ C = C' ∧ D = D'

source

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)

source

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

source

theorem matrix.from_blocks_conj_transpose {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [has_star α] (A : matrix n l α) (B : matrix n m α) (C : matrix o l α) (D : matrix o m α) :

(matrix.from_blocks A B C D).conj_transpose = matrix.from_blocks A.conj_transpose C.conj_transpose B.conj_transpose D.conj_transpose

source

@[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

source

@[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

source

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

source

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)

source

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.

Equations

M.to_block p q = M.submatrix coe coe

source

@[simp]

theorem matrix.to_block_apply {m : Type u_2} {n : Type u_3} {α : Type u_12} (M : matrix m n α) (p : m → Prop) (q : n → Prop) (i : {a // p a}) (j : {a // q a}) :

M.to_block p q i j = M ↑i ↑j

source

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.to_block (λ (a : m), p a) (λ (a : m), p a)

source

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

source

def matrix.to_square_block {m : Type u_2} {α : Type u_12} {β : Type u_13} (M : matrix m m α) (b : m → β) (k : β) :

matrix {a // b a = k} {a // b a = k} α

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.to_square_block_prop (λ (a : m), b a = k)

source

theorem matrix.to_square_block_def {m : Type u_2} {α : Type u_12} {β : Type u_13} (M : matrix m m α) (b : m → β) (k : β) :

M.to_square_block b k = λ (i j : {a // b a = k}), M ↑i ↑j

source

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)

source

theorem matrix.from_blocks_neg {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_10} [has_neg R] (A : matrix n l R) (B : matrix n m R) (C : matrix o l R) (D : matrix o m R) :

-matrix.from_blocks A B C D = matrix.from_blocks (-A) (-B) (-C) (-D)

source

@[simp]

theorem matrix.from_blocks_zero {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [has_zero α] :

matrix.from_blocks 0 0 0 0 = 0

source

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')

source

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 α) :

(matrix.from_blocks A B C D).mul (matrix.from_blocks A' B' C' D') = matrix.from_blocks (A.mul A' + B.mul C') (A.mul B' + B.mul D') (C.mul A' + D.mul C') (C.mul B' + D.mul D')

source

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 → α) :

(matrix.from_blocks A B C D).mul_vec x = sum.elim (A.mul_vec (x ∘ sum.inl) + B.mul_vec (x ∘ sum.inr)) (C.mul_vec (x ∘ sum.inl) + D.mul_vec (x ∘ sum.inr))

source

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)

source

theorem matrix.to_block_diagonal_self {m : Type u_2} {α : Type u_12} [decidable_eq m] [has_zero α] (d : m → α) (p : m → Prop) :

(matrix.diagonal d).to_block p p = matrix.diagonal (λ (i : subtype p), d ↑i)

source

theorem matrix.to_block_diagonal_disjoint {m : Type u_2} {α : Type u_12} [decidable_eq m] [has_zero α] (d : m → α) {p q : m → Prop} (hpq : disjoint p q) :

(matrix.diagonal d).to_block p q = 0

source

@[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₂)

source

@[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

source

@[simp]

theorem matrix.to_block_one_self {m : Type u_2} {α : Type u_12} [decidable_eq m] [has_zero α] [has_one α] (p : m → Prop) :

1.to_block p p = 1

source

theorem matrix.to_block_one_disjoint {m : Type u_2} {α : Type u_12} [decidable_eq m] [has_zero α] [has_one α] {p q : m → Prop} (hpq : disjoint p q) :

1.to_block p q = 0

source

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 (m × o) (n × o) α

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 = ⇑matrix.of (λ (_x : m × o), matrix.block_diagonal._match_2 M _x)
matrix.block_diagonal._match_2 M (i, k) = λ (_x : n × o), matrix.block_diagonal._match_1 M i k _x
matrix.block_diagonal._match_1 M i k (j, k') = ite (k = k') (M k i j) 0

source

theorem matrix.block_diagonal_apply' {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) (k : o) (j : n) (k' : o) :

matrix.block_diagonal M (i, k) (j, k') = ite (k = k') (M k i j) 0

source

theorem matrix.block_diagonal_apply {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 α) (ik : m × o) (jk : n × o) :

matrix.block_diagonal M ik jk = ite (ik.snd = jk.snd) (M ik.snd ik.fst jk.fst) 0

source

@[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

source

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

source

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)

source

@[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)

source

@[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)

source

@[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 α] :

matrix.block_diagonal 0 = 0

source

@[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)

source

@[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 α] :

matrix.block_diagonal 1 = 1

source

@[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 α) :

matrix.block_diagonal (M + N) = matrix.block_diagonal M + matrix.block_diagonal N

source

@[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

source

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 α] :

(o → matrix m n α) →+ matrix (m × o) (n × o) α

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' := _}

source

@[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 α) :

matrix.block_diagonal (-M) = -matrix.block_diagonal M

source

@[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 α) :

matrix.block_diagonal (M - N) = matrix.block_diagonal M - matrix.block_diagonal N

source

@[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)

source

@[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

source

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 α] :

(o → matrix m m α) →+* matrix (m × o) (m × o) α

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' := _}

source

@[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

source

@[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

source

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 = ⇑matrix.of (λ (i : m) (j : n), M (i, k) (j, k))

source

theorem matrix.block_diag_apply {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : matrix (m × o) (n × o) α) (k : o) (i : m) (j : n) :

M.block_diag k i j = M (i, k) (j, k)

source

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

source

@[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

source

@[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

source

@[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

source

@[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))

source

@[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

source

theorem matrix.block_diagonal_injective {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [has_zero α] [decidable_eq o] :

function.injective matrix.block_diagonal

source

@[simp]

theorem matrix.block_diagonal_inj {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [has_zero α] [decidable_eq o] {M N : o → matrix m n α} :

matrix.block_diagonal M = matrix.block_diagonal N ↔ M = N

source

@[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

source

@[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

source

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 (m × o) (n × o) α →+ o → matrix m n α

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' := _}

source

@[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

source

@[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

source

@[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

source

@[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

source

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.

Equations

matrix.block_diagonal' M = ⇑matrix.of (λ (_x : Σ (i : o), m' i), matrix.block_diagonal'._match_2 M _x)
matrix.block_diagonal'._match_2 M ⟨k, i⟩ = λ (_x : Σ (i : o), n' i), matrix.block_diagonal'._match_1 M k i _x
matrix.block_diagonal'._match_1 M k i ⟨k', j⟩ = dite (k = k') (λ (h : k = k'), M k i (cast _ j)) (λ (h : ¬k = k'), 0)

source

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) α) (k : o) (i : m' k) (k' : o) (j : n' k') :

matrix.block_diagonal' M ⟨k, i⟩ ⟨k', j⟩ = dite (k = k') (λ (h : k = k'), M k i (cast _ j)) (λ (h : ¬k = k'), 0)

source

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⟩

source

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 α) :

(matrix.block_diagonal' M).submatrix (prod.to_sigma ∘ prod.swap) (prod.to_sigma ∘ prod.swap) = matrix.block_diagonal M

source

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) :

matrix.block_diagonal' M ik jk = dite (ik.fst = jk.fst) (λ (h : ik.fst = jk.fst), M ik.fst ik.snd (cast _ jk.snd)) (λ (h : ¬ik.fst = jk.fst), 0)

source

@[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

source

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

source

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)

source

@[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)

source

@[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)

source

@[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 α] :

matrix.block_diagonal' 0 = 0

source

@[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)

source

@[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 α] :

matrix.block_diagonal' 1 = 1

source

@[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) α) :

matrix.block_diagonal' (M + N) = matrix.block_diagonal' M + matrix.block_diagonal' N

source

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 α] :

(Π (i : o), matrix (m' i) (n' i) α) →+ matrix (Σ (i : o), m' i) (Σ (i : o), n' i) α

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' := _}

source

@[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

source

@[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) α) :

matrix.block_diagonal' (-M) = -matrix.block_diagonal' M

source

@[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) α) :

matrix.block_diagonal' (M - N) = matrix.block_diagonal' M - matrix.block_diagonal' N

source

@[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)

source

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 α] :

(Π (i : o), matrix (m' i) (m' i) α) →+* matrix (Σ (i : o), m' i) (Σ (i : o), m' i) α

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' := _}

source

@[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) α) :

⇑(matrix.block_diagonal'_ring_hom m' α) M = matrix.block_diagonal' M

source

@[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

source

@[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

source

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 = ⇑matrix.of (λ (i : m' k) (j : n' k), M ⟨k, i⟩ ⟨k, j⟩)

source

theorem matrix.block_diag'_apply {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) (i : m' k) (j : n' k) :

M.block_diag' k i j = M ⟨k, i⟩ ⟨k, j⟩

source

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

source

@[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

source

@[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

source

@[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

source

@[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⟩)

source

@[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) α) :

(matrix.block_diagonal' M).block_diag' = M

source

theorem matrix.block_diagonal'_injective {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [has_zero α] [decidable_eq o] :

function.injective matrix.block_diagonal'

source

@[simp]

theorem matrix.block_diagonal'_inj {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [has_zero α] [decidable_eq o] {M N : Π (i : o), matrix (m' i) (n' i) α} :

matrix.block_diagonal' M = matrix.block_diagonal' N ↔ M = N

source

@[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

source

@[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'

source

@[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

source

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 (Σ (i : o), m' i) (Σ (i : o), n' i) α →+ Π (i : o), matrix (m' i) (n' i) α

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' := _}

source

@[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'

source

@[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'

source

@[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'

source

theorem matrix.to_block_mul_eq_mul {R : Type u_10} [comm_ring R] {m : Type u_1} {n : Type u_2} {k : Type u_3} [fintype n] (p : m → Prop) (q : k → Prop) (A : matrix m n R) (B : matrix n k R) :

(A.mul B).to_block p q = (A.to_block p ⊤).mul (B.to_block ⊤ q)

source

theorem matrix.to_block_mul_eq_add {R : Type u_10} [comm_ring R] {m : Type u_1} {n : Type u_2} {k : Type u_3} [fintype n] (p : m → Prop) (q : n → Prop) [decidable_pred q] (r : k → Prop) (A : matrix m n R) (B : matrix n k R) :

(A.mul B).to_block p r = (A.to_block p q).mul (B.to_block q r) + (A.to_block p (λ (i : n), ¬q i)).mul (B.to_block (λ (i : n), ¬q i) r)

mathlib3 documentation

Block Matrices #

Main definitions #