Topological properties of matrices #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file is a place to collect topological results about matrices.
Main definitions: #
matrix.topological_ring: square matrices form a topological ring
Main results #
- Continuity:
continuous.matrix_det: the determinant is continuous over a topological ring.continuous.matrix_adjugate: the adjugate is continuous over a topological ring.
- Infinite sums
matrix.transpose_tsum: transpose commutes with infinite sumsmatrix.diagonal_tsum: diagonal commutes with infinite sumsmatrix.block_diagonal_tsum: block diagonal commutes with infinite sumsmatrix.block_diagonal'_tsum: non-uniform block diagonal commutes with infinite sums
@[protected, instance]
def
matrix.topological_space
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space R] :
topological_space (matrix m n R)
Equations
@[protected, instance]
def
matrix.t2_space
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space R]
[t2_space R] :
Lemmas about continuity of operations #
@[protected, instance]
def
matrix.has_continuous_const_smul
{α : Type u_2}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space R]
[has_smul α R]
[has_continuous_const_smul α R] :
has_continuous_const_smul α (matrix m n R)
@[protected, instance]
def
matrix.has_continuous_smul
{α : Type u_2}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space R]
[topological_space α]
[has_smul α R]
[has_continuous_smul α R] :
has_continuous_smul α (matrix m n R)
@[protected, instance]
def
matrix.has_continuous_add
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space R]
[has_add R]
[has_continuous_add R] :
has_continuous_add (matrix m n R)
@[protected, instance]
def
matrix.has_continuous_neg
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space R]
[has_neg R]
[has_continuous_neg R] :
has_continuous_neg (matrix m n R)
@[protected, instance]
def
matrix.topological_add_group
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space R]
[add_group R]
[topological_add_group R] :
topological_add_group (matrix m n R)
@[continuity]
theorem
continuous_matrix
{α : Type u_2}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space R]
[topological_space α]
{f : α → matrix m n R}
(h : ∀ (i : m) (j : n), continuous (λ (a : α), f a i j)) :
To show a function into matrices is continuous it suffices to show the coefficients of the resulting matrix are continuous
theorem
continuous.matrix_elem
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
{A : X → matrix m n R}
(hA : continuous A)
(i : m)
(j : n) :
continuous (λ (x : X), A x i j)
@[continuity]
theorem
continuous.matrix_map
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{S : Type u_7}
{R : Type u_8}
[topological_space X]
[topological_space R]
[topological_space S]
{A : X → matrix m n S}
{f : S → R}
(hA : continuous A)
(hf : continuous f) :
continuous (λ (x : X), (A x).map f)
@[continuity]
theorem
continuous.matrix_transpose
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
{A : X → matrix m n R}
(hA : continuous A) :
continuous (λ (x : X), (A x).transpose)
theorem
continuous.matrix_conj_transpose
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
[has_star R]
[has_continuous_star R]
{A : X → matrix m n R}
(hA : continuous A) :
continuous (λ (x : X), (A x).conj_transpose)
@[protected, instance]
def
matrix.has_continuous_star
{m : Type u_4}
{R : Type u_8}
[topological_space R]
[has_star R]
[has_continuous_star R] :
has_continuous_star (matrix m m R)
@[continuity]
theorem
continuous.matrix_col
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
{A : X → n → R}
(hA : continuous A) :
continuous (λ (x : X), matrix.col (A x))
@[continuity]
theorem
continuous.matrix_row
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
{A : X → n → R}
(hA : continuous A) :
continuous (λ (x : X), matrix.row (A x))
@[continuity]
theorem
continuous.matrix_diagonal
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
[has_zero R]
[decidable_eq n]
{A : X → n → R}
(hA : continuous A) :
continuous (λ (x : X), matrix.diagonal (A x))
@[continuity]
theorem
continuous.matrix_dot_product
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
[fintype n]
[has_mul R]
[add_comm_monoid R]
[has_continuous_add R]
[has_continuous_mul R]
{A B : X → n → R}
(hA : continuous A)
(hB : continuous B) :
continuous (λ (x : X), matrix.dot_product (A x) (B x))
@[continuity]
theorem
continuous.matrix_mul
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{p : Type u_6}
{R : Type u_8}
[topological_space X]
[topological_space R]
[fintype n]
[has_mul R]
[add_comm_monoid R]
[has_continuous_add R]
[has_continuous_mul R]
{A : X → matrix m n R}
{B : X → matrix n p R}
(hA : continuous A)
(hB : continuous B) :
continuous (λ (x : X), (A x).mul (B x))
For square matrices the usual continuous_mul can be used.
@[protected, instance]
def
matrix.has_continuous_mul
{n : Type u_5}
{R : Type u_8}
[topological_space R]
[fintype n]
[has_mul R]
[add_comm_monoid R]
[has_continuous_add R]
[has_continuous_mul R] :
has_continuous_mul (matrix n n R)
@[protected, instance]
def
matrix.topological_semiring
{n : Type u_5}
{R : Type u_8}
[topological_space R]
[fintype n]
[non_unital_non_assoc_semiring R]
[topological_semiring R] :
topological_semiring (matrix n n R)
@[protected, instance]
def
matrix.topological_ring
{n : Type u_5}
{R : Type u_8}
[topological_space R]
[fintype n]
[non_unital_non_assoc_ring R]
[topological_ring R] :
topological_ring (matrix n n R)
@[continuity]
theorem
continuous.matrix_vec_mul_vec
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
[has_mul R]
[has_continuous_mul R]
{A : X → m → R}
{B : X → n → R}
(hA : continuous A)
(hB : continuous B) :
continuous (λ (x : X), matrix.vec_mul_vec (A x) (B x))
@[continuity]
theorem
continuous.matrix_mul_vec
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
[non_unital_non_assoc_semiring R]
[has_continuous_add R]
[has_continuous_mul R]
[fintype n]
{A : X → matrix m n R}
{B : X → n → R}
(hA : continuous A)
(hB : continuous B) :
continuous (λ (x : X), (A x).mul_vec (B x))
@[continuity]
theorem
continuous.matrix_vec_mul
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
[non_unital_non_assoc_semiring R]
[has_continuous_add R]
[has_continuous_mul R]
[fintype m]
{A : X → m → R}
{B : X → matrix m n R}
(hA : continuous A)
(hB : continuous B) :
continuous (λ (x : X), matrix.vec_mul (A x) (B x))
@[continuity]
theorem
continuous.matrix_submatrix
{X : Type u_1}
{l : Type u_3}
{m : Type u_4}
{n : Type u_5}
{p : Type u_6}
{R : Type u_8}
[topological_space X]
[topological_space R]
{A : X → matrix l n R}
(hA : continuous A)
(e₁ : m → l)
(e₂ : p → n) :
continuous (λ (x : X), (A x).submatrix e₁ e₂)
@[continuity]
theorem
continuous.matrix_reindex
{X : Type u_1}
{l : Type u_3}
{m : Type u_4}
{n : Type u_5}
{p : Type u_6}
{R : Type u_8}
[topological_space X]
[topological_space R]
{A : X → matrix l n R}
(hA : continuous A)
(e₁ : l ≃ m)
(e₂ : n ≃ p) :
continuous (λ (x : X), ⇑(matrix.reindex e₁ e₂) (A x))
@[continuity]
theorem
continuous.matrix_diag
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
{A : X → matrix n n R}
(hA : continuous A) :
continuous (λ (x : X), (A x).diag)
@[continuity]
theorem
continuous.matrix_trace
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
[fintype n]
[add_comm_monoid R]
[has_continuous_add R]
{A : X → matrix n n R}
(hA : continuous A) :
continuous (λ (x : X), (A x).trace)
@[continuity]
theorem
continuous.matrix_det
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
[fintype n]
[decidable_eq n]
[comm_ring R]
[topological_ring R]
{A : X → matrix n n R}
(hA : continuous A) :
continuous (λ (x : X), (A x).det)
@[continuity]
theorem
continuous.matrix_update_column
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
[decidable_eq n]
(i : n)
{A : X → matrix m n R}
{B : X → m → R}
(hA : continuous A)
(hB : continuous B) :
continuous (λ (x : X), (A x).update_column i (B x))
@[continuity]
theorem
continuous.matrix_update_row
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
[decidable_eq m]
(i : m)
{A : X → matrix m n R}
{B : X → n → R}
(hA : continuous A)
(hB : continuous B) :
continuous (λ (x : X), (A x).update_row i (B x))
@[continuity]
theorem
continuous.matrix_cramer
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
[fintype n]
[decidable_eq n]
[comm_ring R]
[topological_ring R]
{A : X → matrix n n R}
{B : X → n → R}
(hA : continuous A)
(hB : continuous B) :
continuous (λ (x : X), ⇑((A x).cramer) (B x))
@[continuity]
theorem
continuous.matrix_adjugate
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[topological_space X]
[topological_space R]
[fintype n]
[decidable_eq n]
[comm_ring R]
[topological_ring R]
{A : X → matrix n n R}
(hA : continuous A) :
continuous (λ (x : X), (A x).adjugate)
theorem
continuous_at_matrix_inv
{n : Type u_5}
{R : Type u_8}
[topological_space R]
[fintype n]
[decidable_eq n]
[comm_ring R]
[topological_ring R]
(A : matrix n n R)
(h : continuous_at ring.inverse A.det) :
When ring.inverse is continuous at the determinant (such as in a normed_ring, or a
topological_field), so is matrix.has_inv.
@[continuity]
theorem
continuous.matrix_from_blocks
{X : Type u_1}
{l : Type u_3}
{m : Type u_4}
{n : Type u_5}
{p : Type u_6}
{R : Type u_8}
[topological_space X]
[topological_space R]
{A : X → matrix n l R}
{B : X → matrix n m R}
{C : X → matrix p l R}
{D : X → matrix p m R}
(hA : continuous A)
(hB : continuous B)
(hC : continuous C)
(hD : continuous D) :
continuous (λ (x : X), matrix.from_blocks (A x) (B x) (C x) (D x))
@[continuity]
theorem
continuous.matrix_block_diagonal
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{p : Type u_6}
{R : Type u_8}
[topological_space X]
[topological_space R]
[has_zero R]
[decidable_eq p]
{A : X → p → matrix m n R}
(hA : continuous A) :
continuous (λ (x : X), matrix.block_diagonal (A x))
@[continuity]
theorem
continuous.matrix_block_diag
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{p : Type u_6}
{R : Type u_8}
[topological_space X]
[topological_space R]
{A : X → matrix (m × p) (n × p) R}
(hA : continuous A) :
continuous (λ (x : X), (A x).block_diag)
@[continuity]
theorem
continuous.matrix_block_diagonal'
{X : Type u_1}
{l : Type u_3}
{R : Type u_8}
{m' : l → Type u_9}
{n' : l → Type u_10}
[topological_space X]
[topological_space R]
[has_zero R]
[decidable_eq l]
{A : X → Π (i : l), matrix (m' i) (n' i) R}
(hA : continuous A) :
continuous (λ (x : X), matrix.block_diagonal' (A x))
@[continuity]
theorem
continuous.matrix_block_diag'
{X : Type u_1}
{l : Type u_3}
{R : Type u_8}
{m' : l → Type u_9}
{n' : l → Type u_10}
[topological_space X]
[topological_space R]
{A : X → matrix (Σ (i : l), m' i) (Σ (i : l), n' i) R}
(hA : continuous A) :
continuous (λ (x : X), (A x).block_diag')
Lemmas about infinite sums #
theorem
has_sum.matrix_transpose
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
{f : X → matrix m n R}
{a : matrix m n R}
(hf : has_sum f a) :
theorem
summable.matrix_transpose
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
{f : X → matrix m n R}
(hf : summable f) :
@[simp]
theorem
summable_matrix_transpose
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
{f : X → matrix m n R} :
theorem
has_sum.matrix_conj_transpose
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
[star_add_monoid R]
[has_continuous_star R]
{f : X → matrix m n R}
{a : matrix m n R}
(hf : has_sum f a) :
has_sum (λ (x : X), (f x).conj_transpose) a.conj_transpose
theorem
summable.matrix_conj_transpose
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
[star_add_monoid R]
[has_continuous_star R]
{f : X → matrix m n R}
(hf : summable f) :
summable (λ (x : X), (f x).conj_transpose)
@[simp]
theorem
summable_matrix_conj_transpose
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
[star_add_monoid R]
[has_continuous_star R]
{f : X → matrix m n R} :
summable (λ (x : X), (f x).conj_transpose) ↔ summable f
theorem
matrix.conj_transpose_tsum
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
[star_add_monoid R]
[has_continuous_star R]
[t2_space R]
{f : X → matrix m n R} :
(∑' (x : X), f x).conj_transpose = ∑' (x : X), (f x).conj_transpose
theorem
has_sum.matrix_diagonal
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
[decidable_eq n]
{f : X → n → R}
{a : n → R}
(hf : has_sum f a) :
has_sum (λ (x : X), matrix.diagonal (f x)) (matrix.diagonal a)
theorem
summable.matrix_diagonal
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
[decidable_eq n]
{f : X → n → R}
(hf : summable f) :
summable (λ (x : X), matrix.diagonal (f x))
@[simp]
theorem
summable_matrix_diagonal
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
[decidable_eq n]
{f : X → n → R} :
summable (λ (x : X), matrix.diagonal (f x)) ↔ summable f
theorem
matrix.diagonal_tsum
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
[decidable_eq n]
[t2_space R]
{f : X → n → R} :
matrix.diagonal (∑' (x : X), f x) = ∑' (x : X), matrix.diagonal (f x)
theorem
has_sum.matrix_diag
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
{f : X → matrix n n R}
{a : matrix n n R}
(hf : has_sum f a) :
theorem
summable.matrix_diag
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
{f : X → matrix n n R}
(hf : summable f) :
theorem
has_sum.matrix_block_diagonal
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{p : Type u_6}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
[decidable_eq p]
{f : X → p → matrix m n R}
{a : p → matrix m n R}
(hf : has_sum f a) :
has_sum (λ (x : X), matrix.block_diagonal (f x)) (matrix.block_diagonal a)
theorem
summable.matrix_block_diagonal
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{p : Type u_6}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
[decidable_eq p]
{f : X → p → matrix m n R}
(hf : summable f) :
summable (λ (x : X), matrix.block_diagonal (f x))
theorem
summable_matrix_block_diagonal
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{p : Type u_6}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
[decidable_eq p]
{f : X → p → matrix m n R} :
summable (λ (x : X), matrix.block_diagonal (f x)) ↔ summable f
theorem
matrix.block_diagonal_tsum
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{p : Type u_6}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
[decidable_eq p]
[t2_space R]
{f : X → p → matrix m n R} :
matrix.block_diagonal (∑' (x : X), f x) = ∑' (x : X), matrix.block_diagonal (f x)
theorem
has_sum.matrix_block_diag
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{p : Type u_6}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
{f : X → matrix (m × p) (n × p) R}
{a : matrix (m × p) (n × p) R}
(hf : has_sum f a) :
has_sum (λ (x : X), (f x).block_diag) a.block_diag
theorem
summable.matrix_block_diag
{X : Type u_1}
{m : Type u_4}
{n : Type u_5}
{p : Type u_6}
{R : Type u_8}
[add_comm_monoid R]
[topological_space R]
{f : X → matrix (m × p) (n × p) R}
(hf : summable f) :
summable (λ (x : X), (f x).block_diag)
theorem
has_sum.matrix_block_diagonal'
{X : Type u_1}
{l : Type u_3}
{R : Type u_8}
{m' : l → Type u_9}
{n' : l → Type u_10}
[add_comm_monoid R]
[topological_space R]
[decidable_eq l]
{f : X → Π (i : l), matrix (m' i) (n' i) R}
{a : Π (i : l), matrix (m' i) (n' i) R}
(hf : has_sum f a) :
has_sum (λ (x : X), matrix.block_diagonal' (f x)) (matrix.block_diagonal' a)
theorem
summable.matrix_block_diagonal'
{X : Type u_1}
{l : Type u_3}
{R : Type u_8}
{m' : l → Type u_9}
{n' : l → Type u_10}
[add_comm_monoid R]
[topological_space R]
[decidable_eq l]
{f : X → Π (i : l), matrix (m' i) (n' i) R}
(hf : summable f) :
summable (λ (x : X), matrix.block_diagonal' (f x))
theorem
summable_matrix_block_diagonal'
{X : Type u_1}
{l : Type u_3}
{R : Type u_8}
{m' : l → Type u_9}
{n' : l → Type u_10}
[add_comm_monoid R]
[topological_space R]
[decidable_eq l]
{f : X → Π (i : l), matrix (m' i) (n' i) R} :
summable (λ (x : X), matrix.block_diagonal' (f x)) ↔ summable f
theorem
matrix.block_diagonal'_tsum
{X : Type u_1}
{l : Type u_3}
{R : Type u_8}
{m' : l → Type u_9}
{n' : l → Type u_10}
[add_comm_monoid R]
[topological_space R]
[decidable_eq l]
[t2_space R]
{f : X → Π (i : l), matrix (m' i) (n' i) R} :
matrix.block_diagonal' (∑' (x : X), f x) = ∑' (x : X), matrix.block_diagonal' (f x)
theorem
has_sum.matrix_block_diag'
{X : Type u_1}
{l : Type u_3}
{R : Type u_8}
{m' : l → Type u_9}
{n' : l → Type u_10}
[add_comm_monoid R]
[topological_space R]
{f : X → matrix (Σ (i : l), m' i) (Σ (i : l), n' i) R}
{a : matrix (Σ (i : l), m' i) (Σ (i : l), n' i) R}
(hf : has_sum f a) :
has_sum (λ (x : X), (f x).block_diag') a.block_diag'
theorem
summable.matrix_block_diag'
{X : Type u_1}
{l : Type u_3}
{R : Type u_8}
{m' : l → Type u_9}
{n' : l → Type u_10}
[add_comm_monoid R]
[topological_space R]
{f : X → matrix (Σ (i : l), m' i) (Σ (i : l), n' i) R}
(hf : summable f) :
summable (λ (x : X), (f x).block_diag')