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 sumsMatrix.diagonal_tsum: diagonal commutes with infinite sumsMatrix.blockDiagonal_tsum: block diagonal commutes with infinite sumsMatrix.blockDiagonal'_tsum: non-uniform block diagonal commutes with infinite sums
instance
instTopologicalSpaceMatrix
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
:
TopologicalSpace (Matrix m n R)
Equations
- instTopologicalSpaceMatrix = Pi.topologicalSpace
instance
instT2SpaceMatrixInstTopologicalSpaceMatrix
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
[T2Space R]
:
Equations
- ⋯ = ⋯
Lemmas about continuity of operations #
instance
instContinuousConstSMulMatrixInstTopologicalSpaceMatrixSmul
{α : Type u_2}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
[SMul α R]
[ContinuousConstSMul α R]
:
ContinuousConstSMul α (Matrix m n R)
Equations
- ⋯ = ⋯
instance
instContinuousSMulMatrixSmulInstTopologicalSpaceMatrix
{α : Type u_2}
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
[TopologicalSpace α]
[SMul α R]
[ContinuousSMul α R]
:
ContinuousSMul α (Matrix m n R)
Equations
- ⋯ = ⋯
instance
instContinuousAddMatrixInstTopologicalSpaceMatrixAdd
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
[Add R]
[ContinuousAdd R]
:
ContinuousAdd (Matrix m n R)
Equations
- ⋯ = ⋯
instance
instContinuousNegMatrixInstTopologicalSpaceMatrixNeg
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
[Neg R]
[ContinuousNeg R]
:
ContinuousNeg (Matrix m n R)
Equations
- ⋯ = ⋯
instance
instTopologicalAddGroupMatrixInstTopologicalSpaceMatrixAddGroup
{m : Type u_4}
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
[AddGroup R]
[TopologicalAddGroup R]
:
TopologicalAddGroup (Matrix m n R)
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 : X → Matrix 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 : X → Matrix m n S}
{f : S → R}
(hA : Continuous A)
(hf : Continuous f)
:
Continuous fun (x : X) => Matrix.map (A x) 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 : X → Matrix m n R}
(hA : Continuous A)
:
Continuous fun (x : X) => Matrix.transpose (A x)
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 : X → Matrix m n R}
(hA : Continuous A)
:
Continuous fun (x : X) => Matrix.conjTranspose (A x)
instance
instContinuousStarMatrixInstTopologicalSpaceMatrixInstStarMatrix
{m : Type u_4}
{R : Type u_8}
[TopologicalSpace R]
[Star R]
[ContinuousStar R]
:
ContinuousStar (Matrix m m R)
Equations
- ⋯ = ⋯
theorem
Continuous.matrix_col
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace X]
[TopologicalSpace R]
{A : X → n → R}
(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]
{A : X → n → R}
(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 : X → n → R}
(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 : X → n → R}
{B : X → n → R}
(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 : X → Matrix m n R}
{B : X → Matrix 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.
instance
instContinuousMulMatrixInstTopologicalSpaceMatrixInstMulMatrix
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
[Fintype n]
[Mul R]
[AddCommMonoid R]
[ContinuousAdd R]
[ContinuousMul R]
:
ContinuousMul (Matrix n n R)
Equations
- ⋯ = ⋯
instance
instTopologicalSemiringMatrixInstTopologicalSpaceMatrixNonUnitalNonAssocSemiring
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
[Fintype n]
[NonUnitalNonAssocSemiring R]
[TopologicalSemiring R]
:
TopologicalSemiring (Matrix n n R)
Equations
- ⋯ = ⋯
instance
Matrix.topologicalRing
{n : Type u_5}
{R : Type u_8}
[TopologicalSpace R]
[Fintype n]
[NonUnitalNonAssocRing R]
[TopologicalRing R]
:
TopologicalRing (Matrix n n R)
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 : X → m → R}
{B : X → n → R}
(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 : X → Matrix m n R}
{B : X → n → R}
(hA : Continuous A)
(hB : Continuous B)
:
Continuous fun (x : X) => Matrix.mulVec (A x) (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 : X → m → R}
{B : X → Matrix 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 : X → Matrix l n R}
(hA : Continuous A)
(e₁ : m → l)
(e₂ : p → n)
:
Continuous fun (x : X) => Matrix.submatrix (A x) 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 : X → Matrix 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 : X → Matrix n n R}
(hA : Continuous A)
:
Continuous fun (x : X) => Matrix.diag (A x)
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 : X → Matrix n n R}
(hA : Continuous A)
:
Continuous fun (x : X) => Matrix.trace (A x)
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 : X → Matrix n n R}
(hA : Continuous A)
:
Continuous fun (x : X) => Matrix.det (A x)
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 : X → Matrix m n R}
{B : X → m → R}
(hA : Continuous A)
(hB : Continuous B)
:
Continuous fun (x : X) => Matrix.updateColumn (A x) 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 : X → Matrix m n R}
{B : X → n → R}
(hA : Continuous A)
(hB : Continuous B)
:
Continuous fun (x : X) => Matrix.updateRow (A x) 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 : X → Matrix n n R}
{B : X → n → R}
(hA : Continuous A)
(hB : Continuous B)
:
Continuous fun (x : X) => (Matrix.cramer (A x)) (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 : X → Matrix n n R}
(hA : Continuous A)
:
Continuous fun (x : X) => Matrix.adjugate (A x)
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 (Matrix.det A))
:
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 : 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 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 : X → p → Matrix 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 : X → Matrix (m × p) (n × p) R}
(hA : Continuous A)
:
Continuous fun (x : X) => Matrix.blockDiag (A x)
theorem
Continuous.matrix_blockDiagonal'
{X : Type u_1}
{l : Type u_3}
{R : Type u_8}
{m' : l → Type u_9}
{n' : l → Type 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' : l → Type u_9}
{n' : l → Type u_10}
[TopologicalSpace X]
[TopologicalSpace R]
{A : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R}
(hA : Continuous A)
:
Continuous fun (x : X) => Matrix.blockDiag' (A x)
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 : X → Matrix m n R}
{a : Matrix m n R}
(hf : HasSum f a)
:
HasSum (fun (x : X) => Matrix.transpose (f x)) (Matrix.transpose a)
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 : X → Matrix m n R}
(hf : Summable f)
:
Summable fun (x : X) => Matrix.transpose (f x)
@[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 : X → Matrix m n R}
:
(Summable fun (x : X) => Matrix.transpose (f x)) ↔ 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 : X → Matrix m n R}
:
Matrix.transpose (∑' (x : X), f x) = ∑' (x : X), Matrix.transpose (f x)
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 : X → Matrix m n R}
{a : Matrix m n R}
(hf : HasSum f a)
:
HasSum (fun (x : X) => Matrix.conjTranspose (f x)) (Matrix.conjTranspose a)
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 : X → Matrix m n R}
(hf : Summable f)
:
Summable fun (x : X) => Matrix.conjTranspose (f x)
@[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 : X → Matrix m n R}
:
(Summable fun (x : X) => Matrix.conjTranspose (f x)) ↔ 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 : X → Matrix m n R}
:
Matrix.conjTranspose (∑' (x : X), f x) = ∑' (x : X), Matrix.conjTranspose (f x)
theorem
HasSum.matrix_diagonal
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[AddCommMonoid R]
[TopologicalSpace R]
[DecidableEq n]
{f : X → n → R}
{a : n → R}
(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 : X → n → R}
(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 : X → n → R}
:
(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 : X → n → R}
:
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 : X → Matrix n n R}
{a : Matrix n n R}
(hf : HasSum f a)
:
HasSum (fun (x : X) => Matrix.diag (f x)) (Matrix.diag a)
theorem
Summable.matrix_diag
{X : Type u_1}
{n : Type u_5}
{R : Type u_8}
[AddCommMonoid R]
[TopologicalSpace R]
{f : X → Matrix n n R}
(hf : Summable f)
:
Summable fun (x : X) => Matrix.diag (f x)
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 : X → p → Matrix m n R}
{a : p → Matrix m n R}
(hf : HasSum f a)
:
HasSum (fun (x : X) => Matrix.blockDiagonal (f x)) (Matrix.blockDiagonal 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 : X → p → Matrix 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 : X → p → Matrix 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 : X → p → Matrix 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 : X → Matrix (m × p) (n × p) R}
{a : Matrix (m × p) (n × p) R}
(hf : HasSum f a)
:
HasSum (fun (x : X) => Matrix.blockDiag (f x)) (Matrix.blockDiag a)
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 : X → Matrix (m × p) (n × p) R}
(hf : Summable f)
:
Summable fun (x : X) => Matrix.blockDiag (f x)
theorem
HasSum.matrix_blockDiagonal'
{X : Type u_1}
{l : Type u_3}
{R : Type u_8}
{m' : l → Type u_9}
{n' : l → Type 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)
:
HasSum (fun (x : X) => Matrix.blockDiagonal' (f x)) (Matrix.blockDiagonal' a)
theorem
Summable.matrix_blockDiagonal'
{X : Type u_1}
{l : Type u_3}
{R : Type u_8}
{m' : l → Type u_9}
{n' : l → Type 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' : l → Type u_9}
{n' : l → Type 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' : l → Type u_9}
{n' : l → Type 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' : l → Type u_9}
{n' : l → Type u_10}
[AddCommMonoid R]
[TopologicalSpace 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 : HasSum f a)
:
HasSum (fun (x : X) => Matrix.blockDiag' (f x)) (Matrix.blockDiag' a)
theorem
Summable.matrix_blockDiag'
{X : Type u_1}
{l : Type u_3}
{R : Type u_8}
{m' : l → Type u_9}
{n' : l → Type u_10}
[AddCommMonoid R]
[TopologicalSpace R]
{f : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R}
(hf : Summable f)
:
Summable fun (x : X) => Matrix.blockDiag' (f x)