Topological properties of matrices #

This file is a place to collect topological results about matrices.

Main definitions: #

• Matrix.topologicalRing: 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 sums
• Matrix.diagonal_tsum: diagonal commutes with infinite sums
• Matrix.blockDiagonal_tsum: block diagonal commutes with infinite sums
• Matrix.blockDiagonal'_tsum: non-uniform block diagonal commutes with infinite sums
instance instTopologicalSpaceMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [] :
Equations
• instTopologicalSpaceMatrix = Pi.topologicalSpace
instance instT2SpaceMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] :
T2Space (Matrix m n R)
Equations
• =

Lemmas about continuity of operations #

instance instContinuousConstSMulMatrix {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [SMul α R] [] :
Equations
• =
instance instContinuousSMulMatrix {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] [SMul α R] [] :
Equations
• =
instance instContinuousAddMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [Add R] [] :
Equations
• =
instance instContinuousNegMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [Neg R] [] :
Equations
• =
instance instTopologicalAddGroupMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] :
Equations
• =
theorem continuous_matrix {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] {f : αMatrix m n R} (h : ∀ (i : m) (j : n), Continuous fun (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} [] [] {A : XMatrix m n R} (hA : ) (i : m) (j : n) :
Continuous fun (x : X) => A x i j
theorem Continuous.matrix_map {X : Type u_1} {m : Type u_4} {n : Type u_5} {S : Type u_7} {R : Type u_8} [] [] [] {A : XMatrix m n S} {f : SR} (hA : ) (hf : ) :
Continuous fun (x : X) => (A x).map f
theorem Continuous.matrix_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] {A : XMatrix m n R} (hA : ) :
Continuous fun (x : X) => (A x).transpose
theorem Continuous.matrix_conjTranspose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] [Star R] [] {A : XMatrix m n R} (hA : ) :
Continuous fun (x : X) => (A x).conjTranspose
instance instContinuousStarMatrix {m : Type u_4} {R : Type u_8} [] [Star R] [] :
Equations
• =
theorem Continuous.matrix_col {X : Type u_1} {n : Type u_5} {R : Type u_8} [] [] {ι : Type u_11} {A : XnR} (hA : ) :
Continuous fun (x : X) => Matrix.col ι (A x)
theorem Continuous.matrix_row {X : Type u_1} {n : Type u_5} {R : Type u_8} [] [] {ι : Type u_11} {A : XnR} (hA : ) :
Continuous fun (x : X) => Matrix.row ι (A x)
theorem Continuous.matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [] [] [Zero R] [] {A : XnR} (hA : ) :
Continuous fun (x : X) => Matrix.diagonal (A x)
theorem Continuous.matrix_dotProduct {X : Type u_1} {n : Type u_5} {R : Type u_8} [] [] [] [Mul R] [] [] [] {A : XnR} {B : XnR} (hA : ) (hB : ) :
Continuous fun (x : X) => Matrix.dotProduct (A x) (B x)
theorem Continuous.matrix_mul {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [] [] [] [Mul R] [] [] [] {A : XMatrix m n R} {B : XMatrix n p R} (hA : ) (hB : ) :
Continuous fun (x : X) => A x * B x

For square matrices the usual continuous_mul can be used.

instance instContinuousMulMatrixOfContinuousAdd {n : Type u_5} {R : Type u_8} [] [] [Mul R] [] [] [] :
Equations
• =
instance instTopologicalSemiringMatrix {n : Type u_5} {R : Type u_8} [] [] :
Equations
• =
instance Matrix.topologicalRing {n : Type u_5} {R : Type u_8} [] [] [] :
Equations
• =
theorem Continuous.matrix_vecMulVec {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] [Mul R] [] {A : XmR} {B : XnR} (hA : ) (hB : ) :
Continuous fun (x : X) => Matrix.vecMulVec (A x) (B x)
theorem Continuous.matrix_mulVec {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] [] [] [] {A : XMatrix m n R} {B : XnR} (hA : ) (hB : ) :
Continuous fun (x : X) => (A x).mulVec (B x)
theorem Continuous.matrix_vecMul {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] [] [] [] {A : XmR} {B : XMatrix m n R} (hA : ) (hB : ) :
Continuous fun (x : X) => Matrix.vecMul (A x) (B x)
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} [] [] {A : XMatrix l n R} (hA : ) (e₁ : ml) (e₂ : pn) :
Continuous fun (x : X) => (A x).submatrix e₁ e₂
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} [] [] {A : XMatrix l n R} (hA : ) (e₁ : l m) (e₂ : n p) :
Continuous fun (x : X) => (Matrix.reindex e₁ e₂) (A x)
theorem Continuous.matrix_diag {X : Type u_1} {n : Type u_5} {R : Type u_8} [] [] {A : XMatrix n n R} (hA : ) :
Continuous fun (x : X) => (A x).diag
theorem continuous_matrix_diag {n : Type u_5} {R : Type u_8} [] :
Continuous Matrix.diag
theorem Continuous.matrix_trace {X : Type u_1} {n : Type u_5} {R : Type u_8} [] [] [] [] [] {A : XMatrix n n R} (hA : ) :
Continuous fun (x : X) => (A x).trace
theorem Continuous.matrix_det {X : Type u_1} {n : Type u_5} {R : Type u_8} [] [] [] [] [] [] {A : XMatrix n n R} (hA : ) :
Continuous fun (x : X) => (A x).det
theorem Continuous.matrix_updateColumn {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] [] (i : n) {A : XMatrix m n R} {B : XmR} (hA : ) (hB : ) :
Continuous fun (x : X) => (A x).updateColumn i (B x)
theorem Continuous.matrix_updateRow {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] [] (i : m) {A : XMatrix m n R} {B : XnR} (hA : ) (hB : ) :
Continuous fun (x : X) => (A x).updateRow i (B x)
theorem Continuous.matrix_cramer {X : Type u_1} {n : Type u_5} {R : Type u_8} [] [] [] [] [] [] {A : XMatrix n n R} {B : XnR} (hA : ) (hB : ) :
Continuous fun (x : X) => (A x).cramer (B x)
theorem Continuous.matrix_adjugate {X : Type u_1} {n : Type u_5} {R : Type u_8} [] [] [] [] [] [] {A : XMatrix n n R} (hA : ) :
Continuous fun (x : X) => (A x).adjugate
theorem continuousAt_matrix_inv {n : Type u_5} {R : Type u_8} [] [] [] [] [] (A : Matrix n n R) (h : ContinuousAt Ring.inverse A.det) :
ContinuousAt Inv.inv A

When Ring.inverse is continuous at the determinant (such as in a NormedRing, or a topological field), so is Matrix.inv.

theorem Continuous.matrix_fromBlocks {X : Type u_1} {l : Type u_3} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [] [] {A : XMatrix n l R} {B : XMatrix n m R} {C : XMatrix p l R} {D : XMatrix p m R} (hA : ) (hB : ) (hC : ) (hD : ) :
Continuous fun (x : X) => Matrix.fromBlocks (A x) (B x) (C x) (D x)
theorem Continuous.matrix_blockDiagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [] [] [Zero R] [] {A : XpMatrix m n R} (hA : ) :
Continuous fun (x : X) => Matrix.blockDiagonal (A x)
theorem Continuous.matrix_blockDiag {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [] [] {A : XMatrix (m × p) (n × p) R} (hA : ) :
Continuous fun (x : X) => (A x).blockDiag
theorem Continuous.matrix_blockDiagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : lType u_9} {n' : lType u_10} [] [] [Zero R] [] {A : X(i : l) → Matrix (m' i) (n' i) R} (hA : ) :
Continuous fun (x : X) =>
theorem Continuous.matrix_blockDiag' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : lType u_9} {n' : lType u_10} [] [] {A : XMatrix ((i : l) × m' i) ((i : l) × n' i) R} (hA : ) :
Continuous fun (x : X) => (A x).blockDiag'

theorem HasSum.matrix_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] {f : XMatrix m n R} {a : Matrix m n R} (hf : HasSum f a) :
HasSum (fun (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} [] [] {f : XMatrix m n R} (hf : ) :
Summable fun (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} [] [] {f : XMatrix m n R} :
(Summable fun (x : X) => (f x).transpose)
theorem Matrix.transpose_tsum {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] [] {f : XMatrix m n R} :
(∑' (x : X), f x).transpose = ∑' (x : X), (f x).transpose
theorem HasSum.matrix_conjTranspose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] [] [] {f : XMatrix m n R} {a : Matrix m n R} (hf : HasSum f a) :
HasSum (fun (x : X) => (f x).conjTranspose) a.conjTranspose
theorem Summable.matrix_conjTranspose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] [] [] {f : XMatrix m n R} (hf : ) :
Summable fun (x : X) => (f x).conjTranspose
@[simp]
theorem summable_matrix_conjTranspose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] [] [] {f : XMatrix m n R} :
(Summable fun (x : X) => (f x).conjTranspose)
theorem Matrix.conjTranspose_tsum {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [] [] [] [] [] {f : XMatrix m n R} :
(∑' (x : X), f x).conjTranspose = ∑' (x : X), (f x).conjTranspose
theorem HasSum.matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [] [] [] {f : XnR} {a : nR} (hf : HasSum f a) :
HasSum (fun (x : X) => Matrix.diagonal (f x)) ()
theorem Summable.matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [] [] [] {f : XnR} (hf : ) :
Summable fun (x : X) => Matrix.diagonal (f x)
@[simp]
theorem summable_matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [] [] [] {f : XnR} :
(Summable fun (x : X) => Matrix.diagonal (f x))
theorem Matrix.diagonal_tsum {X : Type u_1} {n : Type u_5} {R : Type u_8} [] [] [] [] {f : XnR} :
Matrix.diagonal (∑' (x : X), f x) = ∑' (x : X), Matrix.diagonal (f x)
theorem HasSum.matrix_diag {X : Type u_1} {n : Type u_5} {R : Type u_8} [] [] {f : XMatrix n n R} {a : Matrix n n R} (hf : HasSum f a) :
HasSum (fun (x : X) => (f x).diag) a.diag
theorem Summable.matrix_diag {X : Type u_1} {n : Type u_5} {R : Type u_8} [] [] {f : XMatrix n n R} (hf : ) :
Summable fun (x : X) => (f x).diag
theorem HasSum.matrix_blockDiagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [] [] [] {f : XpMatrix m n R} {a : pMatrix m n R} (hf : HasSum f a) :
HasSum (fun (x : X) => Matrix.blockDiagonal (f x))
theorem Summable.matrix_blockDiagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [] [] [] {f : XpMatrix m n R} (hf : ) :
Summable fun (x : X) => Matrix.blockDiagonal (f x)
theorem summable_matrix_blockDiagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [] [] [] {f : XpMatrix m n R} :
(Summable fun (x : X) => Matrix.blockDiagonal (f x))
theorem Matrix.blockDiagonal_tsum {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [] [] [] [] {f : XpMatrix m n R} :
Matrix.blockDiagonal (∑' (x : X), f x) = ∑' (x : X), Matrix.blockDiagonal (f x)
theorem HasSum.matrix_blockDiag {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [] [] {f : XMatrix (m × p) (n × p) R} {a : Matrix (m × p) (n × p) R} (hf : HasSum f a) :
HasSum (fun (x : X) => (f x).blockDiag) a.blockDiag
theorem Summable.matrix_blockDiag {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [] [] {f : XMatrix (m × p) (n × p) R} (hf : ) :
Summable fun (x : X) => (f x).blockDiag
theorem HasSum.matrix_blockDiagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : lType u_9} {n' : lType u_10} [] [] [] {f : X(i : l) → Matrix (m' i) (n' i) R} {a : (i : l) → Matrix (m' i) (n' i) R} (hf : HasSum f a) :
HasSum (fun (x : X) => )
theorem Summable.matrix_blockDiagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : lType u_9} {n' : lType u_10} [] [] [] {f : X(i : l) → Matrix (m' i) (n' i) R} (hf : ) :
Summable fun (x : X) =>
theorem summable_matrix_blockDiagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : lType u_9} {n' : lType u_10} [] [] [] {f : X(i : l) → Matrix (m' i) (n' i) R} :
(Summable fun (x : X) => )
theorem Matrix.blockDiagonal'_tsum {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : lType u_9} {n' : lType u_10} [] [] [] [] {f : X(i : l) → Matrix (m' i) (n' i) R} :
Matrix.blockDiagonal' (∑' (x : X), f x) = ∑' (x : X),
theorem HasSum.matrix_blockDiag' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : lType u_9} {n' : lType u_10} [] [] {f : XMatrix ((i : l) × m' i) ((i : l) × n' i) R} {a : Matrix ((i : l) × m' i) ((i : l) × n' i) R} (hf : HasSum f a) :
HasSum (fun (x : X) => (f x).blockDiag') a.blockDiag'
theorem Summable.matrix_blockDiag' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : lType u_9} {n' : lType u_10} [] [] {f : XMatrix ((i : l) × m' i) ((i : l) × n' i) R} (hf : ) :
Summable fun (x : X) => (f x).blockDiag'