mathlib3 documentation

topology.instances.matrix

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

Main results #

@[protected, instance]
def matrix.topological_space {m : Type u_4} {n : Type u_5} {R : Type u_8} [topological_space 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] :
@[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] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[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]
@[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]
@[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)

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) :
@[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) :
has_sum (λ (x : X), (f x).transpose) a.transpose
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) :
summable (λ (x : X), (f x).transpose)
@[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} :
summable (λ (x : X), (f x).transpose) summable f
theorem matrix.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] [t2_space R] {f : X matrix m n R} :
(∑' (x : X), f x).transpose = ∑' (x : X), (f x).transpose
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) :
has_sum (λ (x : X), (f x).diag) a.diag
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) :
summable (λ (x : X), (f x).diag)
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) :
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} :
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} :
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) :
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} :
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} :
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')