Documentation

Mathlib.Topology.Instances.Matrix

Topological properties of matrices #

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

Main definitions: #

Main results #

instance instTopologicalSpaceMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] :
Equations
  • instTopologicalSpaceMatrix = Pi.topologicalSpace
instance instT2SpaceMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [T2Space R] :
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} [TopologicalSpace R] [SMul α R] [ContinuousConstSMul α R] :
Equations
  • =
instance instContinuousSMulMatrix {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [TopologicalSpace α] [SMul α R] [ContinuousSMul α R] :
Equations
  • =
instance instContinuousAddMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Add R] [ContinuousAdd R] :
Equations
  • =
instance instContinuousNegMatrix {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Neg R] [ContinuousNeg R] :
Equations
  • =
Equations
  • =
theorem continuous_matrix {α : Type u_2} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [TopologicalSpace α] {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} [TopologicalSpace X] [TopologicalSpace R] {A : XMatrix m n R} (hA : Continuous A) (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} [TopologicalSpace X] [TopologicalSpace R] [TopologicalSpace S] {A : XMatrix m n S} {f : SR} (hA : Continuous A) (hf : Continuous f) :
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} [TopologicalSpace X] [TopologicalSpace R] {A : XMatrix m n R} (hA : Continuous A) :
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} [TopologicalSpace X] [TopologicalSpace R] [Star R] [ContinuousStar R] {A : XMatrix m n R} (hA : Continuous A) :
Continuous fun (x : X) => (A x).conjTranspose
Equations
  • =
theorem Continuous.matrix_col {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {ι : Type u_11} {A : XnR} (hA : Continuous A) :
Continuous fun (x : X) => Matrix.col ι (A x)
theorem Continuous.matrix_row {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] {ι : Type u_11} {A : XnR} (hA : Continuous A) :
Continuous fun (x : X) => Matrix.row ι (A x)
theorem Continuous.matrix_diagonal {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Zero R] [DecidableEq n] {A : XnR} (hA : Continuous A) :
Continuous fun (x : X) => Matrix.diagonal (A x)
theorem Continuous.matrix_dotProduct {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [Mul R] [AddCommMonoid R] [ContinuousAdd R] [ContinuousMul R] {A : XnR} {B : XnR} (hA : Continuous A) (hB : Continuous B) :
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} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [Mul R] [AddCommMonoid R] [ContinuousAdd R] [ContinuousMul R] {A : XMatrix m n R} {B : XMatrix n p R} (hA : Continuous A) (hB : Continuous B) :
Continuous fun (x : X) => A x * B x

For square matrices the usual continuous_mul can be used.

Equations
  • =
theorem Continuous.matrix_vecMulVec {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Mul R] [ContinuousMul R] {A : XmR} {B : XnR} (hA : Continuous A) (hB : Continuous B) :
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} [TopologicalSpace X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [ContinuousAdd R] [ContinuousMul R] [Fintype n] {A : XMatrix m n R} {B : XnR} (hA : Continuous A) (hB : Continuous B) :
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} [TopologicalSpace X] [TopologicalSpace R] [NonUnitalNonAssocSemiring R] [ContinuousAdd R] [ContinuousMul R] [Fintype m] {A : XmR} {B : XMatrix m n R} (hA : Continuous A) (hB : Continuous B) :
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} [TopologicalSpace X] [TopologicalSpace R] {A : XMatrix l n R} (hA : Continuous A) (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} [TopologicalSpace X] [TopologicalSpace R] {A : XMatrix l n R} (hA : Continuous A) (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} [TopologicalSpace X] [TopologicalSpace R] {A : XMatrix n n R} (hA : Continuous A) :
Continuous fun (x : X) => (A x).diag
theorem continuous_matrix_diag {n : Type u_5} {R : Type u_8} [TopologicalSpace R] :
Continuous Matrix.diag
theorem Continuous.matrix_trace {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [AddCommMonoid R] [ContinuousAdd R] {A : XMatrix n n R} (hA : Continuous A) :
Continuous fun (x : X) => (A x).trace
theorem Continuous.matrix_det {X : Type u_1} {n : Type u_5} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [DecidableEq n] [CommRing R] [TopologicalRing R] {A : XMatrix n n R} (hA : Continuous A) :
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} [TopologicalSpace X] [TopologicalSpace R] [DecidableEq n] (i : n) {A : XMatrix m n R} {B : XmR} (hA : Continuous A) (hB : Continuous B) :
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} [TopologicalSpace X] [TopologicalSpace R] [DecidableEq m] (i : m) {A : XMatrix m n R} {B : XnR} (hA : Continuous A) (hB : Continuous B) :
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} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [DecidableEq n] [CommRing R] [TopologicalRing R] {A : XMatrix n n R} {B : XnR} (hA : Continuous A) (hB : Continuous B) :
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} [TopologicalSpace X] [TopologicalSpace R] [Fintype n] [DecidableEq n] [CommRing R] [TopologicalRing R] {A : XMatrix n n R} (hA : Continuous A) :
Continuous fun (x : X) => (A x).adjugate
theorem continuousAt_matrix_inv {n : Type u_5} {R : Type u_8} [TopologicalSpace R] [Fintype n] [DecidableEq n] [CommRing R] [TopologicalRing R] (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} [TopologicalSpace X] [TopologicalSpace R] {A : XMatrix n l R} {B : XMatrix n m R} {C : XMatrix p l R} {D : XMatrix p m R} (hA : Continuous A) (hB : Continuous B) (hC : Continuous C) (hD : Continuous D) :
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} [TopologicalSpace X] [TopologicalSpace R] [Zero R] [DecidableEq p] {A : XpMatrix m n R} (hA : Continuous A) :
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} [TopologicalSpace X] [TopologicalSpace R] {A : XMatrix (m × p) (n × p) R} (hA : Continuous A) :
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} [TopologicalSpace X] [TopologicalSpace R] [Zero R] [DecidableEq l] {A : X(i : l) → Matrix (m' i) (n' i) R} (hA : Continuous A) :
Continuous fun (x : X) => Matrix.blockDiagonal' (A 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} [TopologicalSpace X] [TopologicalSpace R] {A : XMatrix ((i : l) × m' i) ((i : l) × n' i) R} (hA : Continuous A) :
Continuous fun (x : X) => (A x).blockDiag'

Lemmas about infinite sums #

theorem HasSum.matrix_transpose {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] {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} [AddCommMonoid R] [TopologicalSpace R] {f : XMatrix m n R} (hf : Summable f) :
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} [AddCommMonoid R] [TopologicalSpace R] {f : XMatrix m n R} :
(Summable fun (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} [AddCommMonoid R] [TopologicalSpace R] [T2Space R] {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} [AddCommMonoid R] [TopologicalSpace R] [StarAddMonoid R] [ContinuousStar R] {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} [AddCommMonoid R] [TopologicalSpace R] [StarAddMonoid R] [ContinuousStar R] {f : XMatrix m n R} (hf : Summable f) :
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} [AddCommMonoid R] [TopologicalSpace R] [StarAddMonoid R] [ContinuousStar R] {f : XMatrix m n R} :
(Summable fun (x : X) => (f x).conjTranspose) Summable f
theorem Matrix.conjTranspose_tsum {X : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [StarAddMonoid R] [ContinuousStar R] [T2Space R] {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} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq n] {f : XnR} {a : nR} (hf : HasSum f a) :
HasSum (fun (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} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq n] {f : XnR} (hf : Summable f) :
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} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq n] {f : XnR} :
(Summable fun (x : X) => Matrix.diagonal (f x)) Summable f
theorem Matrix.diagonal_tsum {X : Type u_1} {n : Type u_5} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq n] [T2Space R] {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} [AddCommMonoid R] [TopologicalSpace R] {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} [AddCommMonoid R] [TopologicalSpace R] {f : XMatrix n n R} (hf : Summable f) :
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} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq p] {f : XpMatrix m n R} {a : pMatrix m n R} (hf : HasSum f a) :
theorem Summable.matrix_blockDiagonal {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq p] {f : XpMatrix m n R} (hf : Summable f) :
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} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq p] {f : XpMatrix m n R} :
(Summable fun (x : X) => Matrix.blockDiagonal (f x)) Summable f
theorem Matrix.blockDiagonal_tsum {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq p] [T2Space R] {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} [AddCommMonoid R] [TopologicalSpace R] {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} [AddCommMonoid R] [TopologicalSpace R] {f : XMatrix (m × p) (n × p) R} (hf : Summable f) :
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} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq l] {f : X(i : l) → Matrix (m' i) (n' i) R} {a : (i : l) → Matrix (m' i) (n' i) R} (hf : HasSum f a) :
theorem Summable.matrix_blockDiagonal' {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : lType u_9} {n' : lType u_10} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq l] {f : X(i : l) → Matrix (m' i) (n' i) R} (hf : Summable f) :
Summable fun (x : X) => Matrix.blockDiagonal' (f 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} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq l] {f : X(i : l) → Matrix (m' i) (n' i) R} :
(Summable fun (x : X) => Matrix.blockDiagonal' (f x)) Summable f
theorem Matrix.blockDiagonal'_tsum {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : lType u_9} {n' : lType u_10} [AddCommMonoid R] [TopologicalSpace R] [DecidableEq l] [T2Space R] {f : X(i : l) → Matrix (m' i) (n' i) R} :
Matrix.blockDiagonal' (∑' (x : X), f x) = ∑' (x : X), Matrix.blockDiagonal' (f 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} [AddCommMonoid R] [TopologicalSpace R] {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} [AddCommMonoid R] [TopologicalSpace R] {f : XMatrix ((i : l) × m' i) ((i : l) × n' i) R} (hf : Summable f) :
Summable fun (x : X) => (f x).blockDiag'