Mathlib.Topology.Instances.Matrix

instTopologicalSpaceMatrix instance

[TopologicalSpace R] : TopologicalSpace (Matrix m n R)

Full source

instance [TopologicalSpace R] : TopologicalSpace (Matrix m n R) :=
  Pi.topologicalSpace

Topology on Matrices Induced by Componentwise Topology

Informal description

For any topological space $R$ and index types $m$, $n$, the space of matrices $\text{Matrix}\, m\, n\, R$ is equipped with the product topology induced by $R$.

instT2SpaceMatrix instance

[TopologicalSpace R] [T2Space R] : T2Space (Matrix m n R)

Full source

instance [TopologicalSpace R] [T2Space R] : T2Space (Matrix m n R) :=
  Pi.t2Space

Hausdorff Property of Matrix Spaces

Informal description

For any topological space $R$ that is a Hausdorff space and index types $m$, $n$, the space of matrices $\text{Matrix}\, m\, n\, R$ is also a Hausdorff space.

instContinuousConstSMulMatrix instance

[SMul α R] [ContinuousConstSMul α R] : ContinuousConstSMul α (Matrix m n R)

Full source

instance [SMul α R] [ContinuousConstSMul α R] : ContinuousConstSMul α (Matrix m n R) :=
  inferInstanceAs (ContinuousConstSMul α (m → n → R))

Continuous Scalar Multiplication on Matrices in the Second Variable

Informal description

For any type $\alpha$ with a scalar multiplication action on $R$ that is continuous in the second variable, the componentwise scalar multiplication on matrices $\text{Matrix}\, m\, n\, R$ is also continuous in the second variable.

instContinuousSMulMatrix instance

[TopologicalSpace α] [SMul α R] [ContinuousSMul α R] : ContinuousSMul α (Matrix m n R)

Full source

instance [TopologicalSpace α] [SMul α R] [ContinuousSMul α R] : ContinuousSMul α (Matrix m n R) :=
  inferInstanceAs (ContinuousSMul α (m → n → R))

Continuous Scalar Multiplication on Matrices

Informal description

For any topological space $\alpha$ with a scalar multiplication action on $R$ that is jointly continuous, the componentwise scalar multiplication on matrices $\text{Matrix}\, m\, n\, R$ is also jointly continuous.

instContinuousAddMatrix instance

[Add R] [ContinuousAdd R] : ContinuousAdd (Matrix m n R)

Full source

instance [Add R] [ContinuousAdd R] : ContinuousAdd (Matrix m n R) :=
  Pi.continuousAdd

Continuous Addition on Matrices

Informal description

For any type $R$ with an addition operation and a topology where addition is continuous, the space of matrices $\text{Matrix}\, m\, n\, R$ also has a continuous addition operation, defined componentwise.

instContinuousNegMatrix instance

[Neg R] [ContinuousNeg R] : ContinuousNeg (Matrix m n R)

Full source

instance [Neg R] [ContinuousNeg R] : ContinuousNeg (Matrix m n R) :=
  Pi.continuousNeg

Continuous Negation on Matrices

Informal description

For any type $R$ with a negation operation and a topology where negation is continuous, the space of matrices $\text{Matrix}\, m\, n\, R$ also has a continuous negation operation, defined componentwise.

instIsTopologicalAddGroupMatrix instance

[AddGroup R] [IsTopologicalAddGroup R] : IsTopologicalAddGroup (Matrix m n R)

Full source

instance [AddGroup R] [IsTopologicalAddGroup R] : IsTopologicalAddGroup (Matrix m n R) :=
  Pi.topologicalAddGroup

Topological Additive Group Structure on Matrices

Informal description

For any additive group $R$ with a topological additive group structure, the space of matrices $\text{Matrix}\, m\, n\, R$ is also a topological additive group, where the topology is induced componentwise from $R$.

continuous_matrix theorem

[TopologicalSpace α] {f : α → Matrix m n R} (h : ∀ i j, Continuous fun a => f a i j) : Continuous f

Full source

/-- To show a function into matrices is continuous it suffices to show the coefficients of the
resulting matrix are continuous -/
@[continuity]
theorem continuous_matrix [TopologicalSpace α] {f : α → Matrix m n R}
    (h : ∀ i j, Continuous fun a => f a i j) : Continuous f :=
  continuous_pi fun _ => continuous_pi fun _ => h _ _

Componentwise Continuity Criterion for Matrix-Valued Functions

Informal description

Let $X$ be a topological space and $R$ be a topological space. A function $f : X \to \text{Matrix}\, m\, n\, R$ is continuous if for every index $i \in m$ and $j \in n$, the component function $x \mapsto f(x)_{i,j}$ is continuous.

Continuous.matrix_elem theorem

{A : X → Matrix m n R} (hA : Continuous A) (i : m) (j : n) : Continuous fun x => A x i j

Full source

theorem Continuous.matrix_elem {A : X → Matrix m n R} (hA : Continuous A) (i : m) (j : n) :
    Continuous fun x => A x i j :=
  (continuous_apply_apply i j).comp hA

Continuity of Matrix Components

Informal description

Let $X$ be a topological space and $A \colon X \to \text{Matrix}\, m\, n\, R$ be a continuous matrix-valued function. Then for any indices $i \in m$ and $j \in n$, the component function $x \mapsto A(x)_{i,j}$ is continuous.

Continuous.matrix_map theorem

 [TopologicalSpace S] {A : X → Matrix m n S} {f : S → R} (hA : Continuous A) (hf : Continuous f) :
  Continuous fun x => (A x).map f

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_map [TopologicalSpace S] {A : X → Matrix m n S} {f : S → R}
    (hA : Continuous A) (hf : Continuous f) : Continuous fun x => (A x).map f :=
  continuous_matrix fun _ _ => hf.comp <| hA.matrix_elem _ _

Continuity of Entrywise Map Operation on Matrices

Informal description

Let $X$ and $S$ be topological spaces, and $R$ be a topological space. Given a continuous matrix-valued function $A \colon X \to \text{Matrix}\, m\, n\, S$ and a continuous function $f \colon S \to R$, the function $x \mapsto \text{map}\, f\, (A(x))$ (where $\text{map}$ applies $f$ to each entry of the matrix) is continuous.

Continuous.matrix_transpose theorem

{A : X → Matrix m n R} (hA : Continuous A) : Continuous fun x => (A x)ᵀ

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_transpose {A : X → Matrix m n R} (hA : Continuous A) :
    Continuous fun x => (A x)ᵀ :=
  continuous_matrix fun i j => hA.matrix_elem j i

Continuity of Matrix Transpose Operation

Informal description

Let $X$ be a topological space and $R$ be a topological space. Given a continuous matrix-valued function $A \colon X \to \text{Matrix}\, m\, n\, R$, the function $x \mapsto (A(x))^\top$ (where $\top$ denotes matrix transpose) is continuous.

Continuous.matrix_conjTranspose theorem

[Star R] [ContinuousStar R] {A : X → Matrix m n R} (hA : Continuous A) : Continuous fun x => (A x)ᴴ

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_conjTranspose [Star R] [ContinuousStar R] {A : X → Matrix m n R}
    (hA : Continuous A) : Continuous fun x => (A x)ᴴ :=
  hA.matrix_transpose.matrix_map continuous_star

Continuity of Matrix Conjugate Transpose Operation

Informal description

Let $X$ be a topological space and $R$ be a topological space equipped with a continuous star operation $\star \colon R \to R$. Given a continuous matrix-valued function $A \colon X \to \text{Matrix}\, m\, n\, R$, the function $x \mapsto (A(x))^\mathsf{H}$ (where $\mathsf{H}$ denotes the conjugate transpose) is continuous.

instContinuousStarMatrix instance

[Star R] [ContinuousStar R] : ContinuousStar (Matrix m m R)

Full source

instance [Star R] [ContinuousStar R] : ContinuousStar (Matrix m m R) :=
  ⟨continuous_id.matrix_conjTranspose⟩

Continuous Star Operation on Square Matrices

Informal description

For any topological space $R$ with a continuous star operation $\star \colon R \to R$ and any index type $m$, the space of square matrices $\text{Matrix}\, m\, m\, R$ is equipped with a continuous star operation, where the star operation is applied componentwise.

Continuous.matrix_replicateCol theorem

{ι : Type*} {A : X → n → R} (hA : Continuous A) : Continuous fun x => replicateCol ι (A x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_replicateCol {ι : Type*} {A : X → n → R} (hA : Continuous A) :
    Continuous fun x => replicateCol ι (A x) :=
  continuous_matrix fun i _ => (continuous_apply i).comp hA

Continuity of Matrix Column Replication

Informal description

Let $X$ be a topological space and $R$ be a topological space. For any index type $\iota$ and continuous function $A : X \to n \to R$, the function $x \mapsto \text{replicateCol}\, \iota\, (A x)$ is continuous, where $\text{replicateCol}$ creates a matrix by replicating the vector $A x$ across $\iota$ columns.

Continuous.matrix_replicateRow theorem

{ι : Type*} {A : X → n → R} (hA : Continuous A) : Continuous fun x => replicateRow ι (A x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_replicateRow {ι : Type*} {A : X → n → R} (hA : Continuous A) :
    Continuous fun x => replicateRow ι (A x) :=
  continuous_matrix fun _ _ => (continuous_apply _).comp hA

Continuity of Matrix Row Replication

Informal description

Let $X$ be a topological space and $R$ be a topological space. For any index type $\iota$ and continuous function $A : X \to n \to R$, the function $x \mapsto \text{replicateRow}\, \iota\, (A x)$ is continuous, where $\text{replicateRow}$ creates a matrix by replicating the vector $A x$ across $\iota$ rows.

Continuous.matrix_diagonal theorem

[Zero R] [DecidableEq n] {A : X → n → R} (hA : Continuous A) : Continuous fun x => diagonal (A x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_diagonal [Zero R] [DecidableEq n] {A : X → n → R} (hA : Continuous A) :
    Continuous fun x => diagonal (A x) :=
  continuous_matrix fun i _ => ((continuous_apply i).comp hA).if_const _ continuous_zero

Continuity of Diagonal Matrix Construction

Informal description

Let $X$ be a topological space and $R$ be a topological space with a zero element and decidable equality on the index type $n$. If $A : X \to n \to R$ is a continuous function, then the function $x \mapsto \text{diagonal}(A x)$ is continuous, where $\text{diagonal}(A x)$ constructs a diagonal matrix from the vector $A x$.

Continuous.matrix_dotProduct theorem

 [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 => dotProduct (A x) (B x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_dotProduct [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 => dotProduct (A x) (B x) :=
  continuous_finset_sum _ fun i _ =>
    ((continuous_apply i).comp hA).mul ((continuous_apply i).comp hB)

Continuity of the Dot Product of Continuous Vector-Valued Functions

Informal description

Let $X$ be a topological space and $R$ be a topological space equipped with a multiplication operation, an addition operation that forms a commutative monoid, and continuous addition and multiplication operations. For any finite index type $n$, if $A \colon X \to n \to R$ and $B \colon X \to n \to R$ are continuous functions, then the function $x \mapsto \text{dotProduct}(A x, B x)$ is continuous, where $\text{dotProduct}$ denotes the standard dot product of vectors.

Continuous.matrix_mul theorem

 [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 => A x * B x

Full source

/-- For square matrices the usual `continuous_mul` can be used. -/
@[continuity, fun_prop]
theorem Continuous.matrix_mul [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 => A x * B x :=
  continuous_matrix fun _ _ =>
    continuous_finset_sum _ fun _ _ => (hA.matrix_elem _ _).mul (hB.matrix_elem _ _)

Continuity of Matrix Multiplication

Informal description

Let $X$ be a topological space and $R$ be a topological ring with continuous addition and multiplication. Given two continuous matrix-valued functions $A \colon X \to \text{Matrix}\, m\, n\, R$ and $B \colon X \to \text{Matrix}\, n\, p\, R$, the function $x \mapsto A(x) \cdot B(x)$ is continuous, where $\cdot$ denotes matrix multiplication.

instContinuousMulMatrixOfContinuousAdd instance

[Fintype n] [Mul R] [AddCommMonoid R] [ContinuousAdd R] [ContinuousMul R] : ContinuousMul (Matrix n n R)

Full source

instance [Fintype n] [Mul R] [AddCommMonoid R] [ContinuousAdd R] [ContinuousMul R] :
    ContinuousMul (Matrix n n R) :=
  ⟨continuous_fst.matrix_mul continuous_snd⟩

Continuous Multiplication on Square Matrices over a Topological Ring

Informal description

For any finite index type $n$ and topological ring $R$ with continuous addition and multiplication, the space of square matrices $\text{Matrix}\, n\, n\, R$ has a continuous multiplication operation.

instIsTopologicalSemiringMatrix instance

[Fintype n] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] : IsTopologicalSemiring (Matrix n n R)

Full source

instance [Fintype n] [NonUnitalNonAssocSemiring R] [IsTopologicalSemiring R] :
    IsTopologicalSemiring (Matrix n n R) where

Square Matrices Form a Topological Semiring

Informal description

For any finite index type $n$ and any topological semiring $R$, the space of square matrices $\text{Matrix}\, n\, n\, R$ forms a topological semiring, where both addition and multiplication are continuous operations.

Matrix.topologicalRing instance

[Fintype n] [NonUnitalNonAssocRing R] [IsTopologicalRing R] : IsTopologicalRing (Matrix n n R)

Full source

instance Matrix.topologicalRing [Fintype n] [NonUnitalNonAssocRing R] [IsTopologicalRing R] :
    IsTopologicalRing (Matrix n n R) where

Square Matrices Form a Topological Ring

Informal description

For any finite index type $n$ and any topological ring $R$, the space of square matrices $\text{Matrix}\, n\, n\, R$ forms a topological ring, where addition, negation, and multiplication are continuous operations.

Continuous.matrix_vecMulVec theorem

 [Mul R] [ContinuousMul R] {A : X → m → R} {B : X → n → R} (hA : Continuous A) (hB : Continuous B) :
  Continuous fun x => vecMulVec (A x) (B x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_vecMulVec [Mul R] [ContinuousMul R] {A : X → m → R} {B : X → n → R}
    (hA : Continuous A) (hB : Continuous B) : Continuous fun x => vecMulVec (A x) (B x) :=
  continuous_matrix fun _ _ => ((continuous_apply _).comp hA).mul ((continuous_apply _).comp hB)

Continuity of Vector Outer Product for Matrix-Valued Functions

Informal description

Let $X$ be a topological space and $R$ be a topological space with a continuous multiplication operation. Given two continuous functions $A : X \to m \to R$ and $B : X \to n \to R$, the function $x \mapsto \text{vecMulVec}(A(x), B(x))$ is continuous, where $\text{vecMulVec}$ denotes the vector outer product operation on matrices.

Continuous.matrix_mulVec theorem

 [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 => A x *ᵥ B x

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_mulVec [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 => A x *ᵥ B x :=
  continuous_pi fun i => ((continuous_apply i).comp hA).matrix_dotProduct hB

Continuity of Matrix-Vector Multiplication for Continuous Matrix-Valued and Vector-Valued Functions

Informal description

Let $X$ be a topological space and $R$ be a topological semiring with continuous addition and multiplication operations. For any finite index type $n$, if $A \colon X \to \text{Matrix}\, m\, n\, R$ and $B \colon X \to n \to R$ are continuous functions, then the function $x \mapsto A(x) \cdot B(x)$ is continuous, where $\cdot$ denotes the matrix-vector multiplication operation.

Continuous.matrix_vecMul theorem

 [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 => A x ᵥ* B x

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_vecMul [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 => A x ᵥ* B x :=
  continuous_pi fun _i => hA.matrix_dotProduct <| continuous_pi fun _j => hB.matrix_elem _ _

Continuity of Vector-Matrix Multiplication for Continuous Vector-Valued and Matrix-Valued Functions

Informal description

Let $X$ be a topological space and $R$ be a topological semiring with continuous addition and multiplication operations. For any finite index type $m$, if $A \colon X \to m \to R$ is a continuous vector-valued function and $B \colon X \to \text{Matrix}\, m\, n\, R$ is a continuous matrix-valued function, then the function $x \mapsto A(x) \cdot B(x)$ is continuous, where $\cdot$ denotes the vector-matrix multiplication operation.

Continuous.matrix_submatrix theorem

 {A : X → Matrix l n R} (hA : Continuous A) (e₁ : m → l) (e₂ : p → n) : Continuous fun x => (A x).submatrix e₁ e₂

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_submatrix {A : X → Matrix l n R} (hA : Continuous A) (e₁ : m → l)
    (e₂ : p → n) : Continuous fun x => (A x).submatrix e₁ e₂ :=
  continuous_matrix fun _i _j => hA.matrix_elem _ _

Continuity of Matrix Submatrix Operation

Informal description

Let $X$ be a topological space and $A \colon X \to \text{Matrix}\, l\, n\, R$ be a continuous matrix-valued function. Given functions $e_1 \colon m \to l$ and $e_2 \colon p \to n$, the function $x \mapsto \text{submatrix}(A(x), e_1, e_2)$ is continuous, where $\text{submatrix}(A(x), e_1, e_2)$ denotes the submatrix of $A(x)$ formed by selecting rows according to $e_1$ and columns according to $e_2$.

Continuous.matrix_reindex theorem

 {A : X → Matrix l n R} (hA : Continuous A) (e₁ : l ≃ m) (e₂ : n ≃ p) : Continuous fun x => reindex e₁ e₂ (A x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_reindex {A : X → Matrix l n R} (hA : Continuous A) (e₁ : l ≃ m)
    (e₂ : n ≃ p) : Continuous fun x => reindex e₁ e₂ (A x) :=
  hA.matrix_submatrix _ _

Continuity of Matrix Reindexing Operation

Informal description

Let $X$ be a topological space and $A \colon X \to \text{Matrix}\, l\, n\, R$ be a continuous matrix-valued function. Given bijections $e_1 \colon l \to m$ and $e_2 \colon n \to p$, the function $x \mapsto \text{reindex}(A(x), e_1, e_2)$ is continuous, where $\text{reindex}(A(x), e_1, e_2)$ denotes the matrix obtained by reindexing the rows and columns of $A(x)$ according to $e_1$ and $e_2$ respectively.

Continuous.matrix_diag theorem

{A : X → Matrix n n R} (hA : Continuous A) : Continuous fun x => Matrix.diag (A x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_diag {A : X → Matrix n n R} (hA : Continuous A) :
    Continuous fun x => Matrix.diag (A x) :=
  continuous_pi fun _ => hA.matrix_elem _ _

Continuity of Matrix Diagonal Extraction

Informal description

Let $X$ be a topological space and $A \colon X \to \text{Matrix}\, n\, n\, R$ be a continuous matrix-valued function. Then the function $x \mapsto \text{diag}(A(x))$, which extracts the diagonal of the matrix $A(x)$, is continuous.

continuous_matrix_diag theorem

: Continuous (Matrix.diag : Matrix n n R → n → R)

Full source

theorem continuous_matrix_diag : Continuous (Matrix.diag : Matrix n n R → n → R) :=
  show Continuous fun x : Matrix n n R => Matrix.diag x from continuous_id.matrix_diag

Continuity of Matrix Diagonal Function

Informal description

The function $\text{diag} \colon \text{Matrix}\, n\, n\, R \to n \to R$ that extracts the diagonal of a square matrix is continuous, where the space of matrices is equipped with the product topology induced by $R$.

Continuous.matrix_trace theorem

 [Fintype n] [AddCommMonoid R] [ContinuousAdd R] {A : X → Matrix n n R} (hA : Continuous A) :
  Continuous fun x => trace (A x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_trace [Fintype n] [AddCommMonoid R] [ContinuousAdd R]
    {A : X → Matrix n n R} (hA : Continuous A) : Continuous fun x => trace (A x) :=
  continuous_finset_sum _ fun _ _ => hA.matrix_elem _ _

Continuity of Matrix Trace Function

Informal description

Let $X$ be a topological space, $R$ an additive commutative monoid with a continuous addition operation, and $n$ a finite type. For any continuous matrix-valued function $A \colon X \to \text{Matrix}\, n\, n\, R$, the trace function $x \mapsto \text{trace}(A(x))$ is continuous.

Continuous.matrix_det theorem

 [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R] {A : X → Matrix n n R} (hA : Continuous A) :
  Continuous fun x => (A x).det

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_det [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R]
    {A : X → Matrix n n R} (hA : Continuous A) : Continuous fun x => (A x).det := by
  simp_rw [Matrix.det_apply]
  refine continuous_finset_sum _ fun l _ => Continuous.const_smul ?_ _
  exact continuous_finset_prod _ fun l _ => hA.matrix_elem _ _

Continuity of Determinant for Continuous Matrix-Valued Functions

Informal description

Let $X$ be a topological space, $R$ a topological commutative ring, and $n$ a finite type with decidable equality. For any continuous matrix-valued function $A \colon X \to \text{Matrix}\, n\, n\, R$, the determinant function $x \mapsto \det(A(x))$ is continuous on $X$.

Continuous.matrix_updateCol theorem

 [DecidableEq n] (i : n) {A : X → Matrix m n R} {B : X → m → R} (hA : Continuous A) (hB : Continuous B) :
  Continuous fun x => (A x).updateCol i (B x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_updateCol [DecidableEq n] (i : n) {A : X → Matrix m n R}
    {B : X → m → R} (hA : Continuous A) (hB : Continuous B) :
    Continuous fun x => (A x).updateCol i (B x) :=
  continuous_matrix fun _j k =>
    (continuous_apply k).comp <|
      ((continuous_apply _).comp hA).update i ((continuous_apply _).comp hB)

Continuity of Matrix Column Update Operation

Informal description

Let $X$ be a topological space, $R$ a topological ring, and $m$, $n$ index types with decidable equality on $n$. Given a continuous matrix-valued function $A \colon X \to \text{Matrix}\, m\, n\, R$ and a continuous vector-valued function $B \colon X \to m \to R$, the function $x \mapsto (A(x)).\text{updateCol}\, i\, (B(x))$ is continuous for any fixed column index $i \in n$. Here, $\text{updateCol}$ modifies the $i$-th column of the matrix $A(x)$ with the vector $B(x)$.

Continuous.matrix_updateRow theorem

 [DecidableEq m] (i : m) {A : X → Matrix m n R} {B : X → n → R} (hA : Continuous A) (hB : Continuous B) :
  Continuous fun x => (A x).updateRow i (B x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_updateRow [DecidableEq m] (i : m) {A : X → Matrix m n R} {B : X → n → R}
    (hA : Continuous A) (hB : Continuous B) : Continuous fun x => (A x).updateRow i (B x) :=
  hA.update i hB

Continuity of Matrix Row Update Operation

Informal description

Let $X$ be a topological space, $R$ a topological ring, and $m$, $n$ index types with decidable equality on $m$. Given a continuous matrix-valued function $A \colon X \to \text{Matrix}\, m\, n\, R$ and a continuous vector-valued function $B \colon X \to n \to R$, the function $x \mapsto (A(x)).\text{updateRow}\, i\, (B(x))$ is continuous for any fixed row index $i \in m$. Here, $\text{updateRow}$ modifies the $i$-th row of the matrix $A(x)$ with the vector $B(x)$.

Continuous.matrix_cramer theorem

 [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R] {A : X → Matrix n n R} {B : X → n → R}
  (hA : Continuous A) (hB : Continuous B) : Continuous fun x => cramer (A x) (B x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_cramer [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R]
    {A : X → Matrix n n R} {B : X → n → R} (hA : Continuous A) (hB : Continuous B) :
    Continuous fun x => cramer (A x) (B x) :=
  continuous_pi fun _ => (hA.matrix_updateCol _ hB).matrix_det

Continuity of Cramer's Rule Solution for Continuous Matrix and Vector Functions

Informal description

Let $X$ be a topological space, $R$ a topological commutative ring, and $n$ a finite type with decidable equality. Given a continuous matrix-valued function $A \colon X \to \text{Matrix}\, n\, n\, R$ and a continuous vector-valued function $B \colon X \to n \to R$, the function $x \mapsto \text{cramer}(A(x), B(x))$ is continuous on $X$, where $\text{cramer}(A, B)$ denotes the Cramer's rule solution vector for the system $A \cdot y = B$.

Continuous.matrix_adjugate theorem

 [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R] {A : X → Matrix n n R} (hA : Continuous A) :
  Continuous fun x => (A x).adjugate

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_adjugate [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R]
    {A : X → Matrix n n R} (hA : Continuous A) : Continuous fun x => (A x).adjugate :=
  continuous_matrix fun _j k =>
    (hA.matrix_transpose.matrix_updateCol k continuous_const).matrix_det

Continuity of Adjugate for Continuous Matrix-Valued Functions

Informal description

Let $X$ be a topological space, $R$ a topological commutative ring, and $n$ a finite type with decidable equality. For any continuous matrix-valued function $A \colon X \to \text{Matrix}\, n\, n\, R$, the adjugate matrix function $x \mapsto \text{adj}(A(x))$ is continuous on $X$.

continuousAt_matrix_inv theorem

 [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R] (A : Matrix n n R)
  (h : ContinuousAt Ring.inverse A.det) : ContinuousAt Inv.inv A

Full source

/-- When `Ring.inverse` is continuous at the determinant (such as in a `NormedRing`, or a
topological field), so is `Matrix.inv`. -/
theorem continuousAt_matrix_inv [Fintype n] [DecidableEq n] [CommRing R] [IsTopologicalRing R]
    (A : Matrix n n R) (h : ContinuousAt Ring.inverse A.det) : ContinuousAt Inv.inv A :=
  (h.comp continuous_id.matrix_det.continuousAt).smul continuous_id.matrix_adjugate.continuousAt

Continuity of Matrix Inversion at a Point with Continuous Determinant Inversion

Informal description

Let $R$ be a topological commutative ring and $n$ a finite type with decidable equality. For any matrix $A \in \text{Matrix}\, n\, n\, R$, if the ring inversion operation is continuous at $\det(A)$, then the matrix inversion operation is continuous at $A$.

Continuous.matrix_fromBlocks theorem

 {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 => Matrix.fromBlocks (A x) (B x) (C x) (D x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_fromBlocks {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 => Matrix.fromBlocks (A x) (B x) (C x) (D x) :=
  continuous_matrix <| by
    rintro (i | i) (j | j) <;> refine Continuous.matrix_elem ?_ i j <;> assumption

Continuity of Block Matrix Construction from Continuous Components

Informal description

Let $X$ be a topological space and $R$ be a topological space. Given continuous matrix-valued functions $A \colon X \to \text{Matrix}\, n\, l\, R$, $B \colon X \to \text{Matrix}\, n\, m\, R$, $C \colon X \to \text{Matrix}\, p\, l\, R$, and $D \colon X \to \text{Matrix}\, p\, m\, R$, the function $x \mapsto \text{fromBlocks}\, (A(x))\, (B(x))\, (C(x))\, (D(x))$ is continuous, where $\text{fromBlocks}$ constructs a block matrix from the four given submatrices.

Continuous.matrix_blockDiagonal theorem

[Zero R] [DecidableEq p] {A : X → p → Matrix m n R} (hA : Continuous A) : Continuous fun x => blockDiagonal (A x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_blockDiagonal [Zero R] [DecidableEq p] {A : X → p → Matrix m n R}
    (hA : Continuous A) : Continuous fun x => blockDiagonal (A x) :=
  continuous_matrix fun ⟨i₁, i₂⟩ ⟨j₁, _j₂⟩ =>
    (((continuous_apply i₂).comp hA).matrix_elem i₁ j₁).if_const _ continuous_zero

Continuity of Block Diagonal Matrix Construction from Continuous Family of Matrices

Informal description

Let $X$ be a topological space and $R$ be a topological space with a zero element. Given a continuous function $A \colon X \to p \to \text{Matrix}\, m\, n\, R$ (where $p$ is a decidable equality type), the function $x \mapsto \text{blockDiagonal}\, (A(x))$ is continuous, where $\text{blockDiagonal}$ constructs a block diagonal matrix from a family of matrices indexed by $p$.

Continuous.matrix_blockDiag theorem

{A : X → Matrix (m × p) (n × p) R} (hA : Continuous A) : Continuous fun x => blockDiag (A x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_blockDiag {A : X → Matrix (m × p) (n × p) R} (hA : Continuous A) :
    Continuous fun x => blockDiag (A x) :=
  continuous_pi fun _i => continuous_matrix fun _j _k => hA.matrix_elem _ _

Continuity of Block Diagonal Extraction from Matrices

Informal description

Let $X$ be a topological space and $R$ be a topological space. Given a continuous matrix-valued function $A \colon X \to \text{Matrix}\, (m \times p)\, (n \times p)\, R$, the function $x \mapsto \text{blockDiag}\, (A(x))$ is continuous, where $\text{blockDiag}$ extracts the block diagonal from a matrix.

Continuous.matrix_blockDiagonal' theorem

 [Zero R] [DecidableEq l] {A : X → ∀ i, Matrix (m' i) (n' i) R} (hA : Continuous A) :
  Continuous fun x => blockDiagonal' (A x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_blockDiagonal' [Zero R] [DecidableEq l]
    {A : X → ∀ i, Matrix (m' i) (n' i) R} (hA : Continuous A) :
    Continuous fun x => blockDiagonal' (A x) :=
  continuous_matrix fun ⟨i₁, i₂⟩ ⟨j₁, j₂⟩ => by
    dsimp only [blockDiagonal'_apply']
    split_ifs with h
    · subst h
      exact ((continuous_apply i₁).comp hA).matrix_elem i₂ j₂
    · exact continuous_const

Continuity of Non-Uniform Block Diagonal Matrix Construction from Continuous Family of Matrices

Informal description

Let $X$ be a topological space and $R$ be a topological space with a zero element. Given a continuous function $A \colon X \to \prod_{i \in l} \text{Matrix}\, (m'_i)\, (n'_i)\, R$ (where $l$ has decidable equality), the function $x \mapsto \text{blockDiagonal'}\, (A(x))$ is continuous, where $\text{blockDiagonal'}$ constructs a block diagonal matrix from a family of matrices with varying block sizes indexed by $i \in l$.

Continuous.matrix_blockDiag' theorem

{A : X → Matrix (Σ i, m' i) (Σ i, n' i) R} (hA : Continuous A) : Continuous fun x => blockDiag' (A x)

Full source

@[continuity, fun_prop]
theorem Continuous.matrix_blockDiag'
    {A : X → Matrix (Σ i, m' i) (Σ i, n' i) R} (hA : Continuous A) :
    Continuous fun x => blockDiag' (A x) :=
  continuous_pi fun _i => continuous_matrix fun _j _k => hA.matrix_elem _ _

Continuity of Block Diagonal Extraction for Matrices with Dependent Indices

Informal description

Let $X$ be a topological space and $R$ be a topological space. Given a continuous matrix-valued function $A \colon X \to \text{Matrix}\, (\Sigma i, m'_i)\, (\Sigma i, n'_i)\, R$, the function $x \mapsto \text{blockDiag'}\, (A(x))$ is continuous, where $\text{blockDiag'}$ extracts the block diagonal from a matrix with dependent type indices.

HasSum.matrix_transpose theorem

{f : X → Matrix m n R} {a : Matrix m n R} (hf : HasSum f a) : HasSum (fun x => (f x)ᵀ) aᵀ

Full source

theorem HasSum.matrix_transpose {f : X → Matrix m n R} {a : Matrix m n R} (hf : HasSum f a) :
    HasSum (fun x => (f x)ᵀ) aᵀ :=
  (hf.map (Matrix.transposeAddEquiv m n R) continuous_id.matrix_transpose :)

Transpose Commutes with Infinite Sums of Matrices

Informal description

Let $X$ be a topological space and $R$ be a topological ring. Given a function $f \colon X \to \text{Matrix}\, m\, n\, R$ that has a sum $a \in \text{Matrix}\, m\, n\, R$, the function $x \mapsto (f(x))^\top$ has sum $a^\top$, where $\top$ denotes the matrix transpose operation.

Summable.matrix_transpose theorem

{f : X → Matrix m n R} (hf : Summable f) : Summable fun x => (f x)ᵀ

Full source

theorem Summable.matrix_transpose {f : X → Matrix m n R} (hf : Summable f) :
    Summable fun x => (f x)ᵀ :=
  hf.hasSum.matrix_transpose.summable

Summability of Matrix Transpose

Informal description

For any function $f \colon X \to \text{Matrix}\, m\, n\, R$ from a topological space $X$ to the space of $m \times n$ matrices over a topological ring $R$, if $f$ is summable, then the function $x \mapsto (f(x))^\top$ is also summable, where $\top$ denotes the matrix transpose operation.

summable_matrix_transpose theorem

{f : X → Matrix m n R} : (Summable fun x => (f x)ᵀ) ↔ Summable f

Full source

@[simp]
theorem summable_matrix_transpose {f : X → Matrix m n R} :
    (Summable fun x => (f x)ᵀ) ↔ Summable f :=
  Summable.map_iff_of_equiv (Matrix.transposeAddEquiv m n R)
    continuous_id.matrix_transpose continuous_id.matrix_transpose

Summability of Matrix Transpose Equivalence

Informal description

For a function $f \colon X \to \text{Matrix}\, m\, n\, R$ from a topological space $X$ to the space of $m \times n$ matrices over a topological ring $R$, the function $x \mapsto (f(x))^\top$ is summable if and only if $f$ is summable.

Matrix.transpose_tsum theorem

[T2Space R] {f : X → Matrix m n R} : (∑' x, f x)ᵀ = ∑' x, (f x)ᵀ

Full source

theorem Matrix.transpose_tsum [T2Space R] {f : X → Matrix m n R} : (∑' x, f x)ᵀ = ∑' x, (f x)ᵀ := by
  by_cases hf : Summable f
  · exact hf.hasSum.matrix_transpose.tsum_eq.symm
  · have hft := summable_matrix_transpose.not.mpr hf
    rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft, transpose_zero]

Transpose Commutes with Infinite Sum: $(\sum f)^\top = \sum f^\top$

Informal description

Let $R$ be a Hausdorff topological space and $X$ be a topological space. For any function $f \colon X \to \text{Matrix}\, m\, n\, R$, the transpose of the infinite sum of $f$ equals the infinite sum of the transposes of $f$, i.e., $$ \left(\sum_{x} f(x)\right)^\top = \sum_{x} (f(x))^\top. $$

HasSum.matrix_conjTranspose theorem

 [StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R} {a : Matrix m n R} (hf : HasSum f a) :
  HasSum (fun x => (f x)ᴴ) aᴴ

Full source

theorem HasSum.matrix_conjTranspose [StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R}
    {a : Matrix m n R} (hf : HasSum f a) : HasSum (fun x => (f x)ᴴ) aᴴ :=
  (hf.map (Matrix.conjTransposeAddEquiv m n R) continuous_id.matrix_conjTranspose :)

Conjugate Transpose Preserves Summability: $\sum_{x} (f(x))^\mathsf{H} = (\sum_{x} f(x))^\mathsf{H}$

Informal description

Let $R$ be a topological space equipped with a star operation $\star \colon R \to R$ that is continuous, and let $X$ be a topological space. Given a matrix-valued function $f \colon X \to \text{Matrix}\, m\, n\, R$ and a matrix $a \in \text{Matrix}\, m\, n\, R$, if $f$ has sum $a$ (i.e., $\sum_{x} f(x) = a$), then the conjugate transpose function $x \mapsto (f(x))^\mathsf{H}$ has sum $a^\mathsf{H}$ (i.e., $\sum_{x} (f(x))^\mathsf{H} = a^\mathsf{H}$).

Summable.matrix_conjTranspose theorem

[StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R} (hf : Summable f) : Summable fun x => (f x)ᴴ

Full source

theorem Summable.matrix_conjTranspose [StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R}
    (hf : Summable f) : Summable fun x => (f x)ᴴ :=
  hf.hasSum.matrix_conjTranspose.summable

Summability of Matrix Conjugate Transpose: $\sum_{x} (f(x))^\mathsf{H}$ is summable when $\sum_{x} f(x)$ is summable

Informal description

Let $R$ be a topological space equipped with a continuous star operation $\star \colon R \to R$ and let $X$ be a topological space. For any summable matrix-valued function $f \colon X \to \text{Matrix}\, m\, n\, R$, the function $x \mapsto (f(x))^\mathsf{H}$ is also summable.

summable_matrix_conjTranspose theorem

[StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R} : (Summable fun x => (f x)ᴴ) ↔ Summable f

Full source

@[simp]
theorem summable_matrix_conjTranspose [StarAddMonoid R] [ContinuousStar R] {f : X → Matrix m n R} :
    (Summable fun x => (f x)ᴴ) ↔ Summable f :=
  Summable.map_iff_of_equiv (Matrix.conjTransposeAddEquiv m n R)
    continuous_id.matrix_conjTranspose continuous_id.matrix_conjTranspose

Summability Equivalence for Matrix Conjugate Transpose: $\sum_{x} (f(x))^\mathsf{H}$ exists iff $\sum_{x} f(x)$ exists

Informal description

Let $R$ be a topological space equipped with a star operation $\star \colon R \to R$ that is continuous, and let $X$ be a topological space. For a matrix-valued function $f \colon X \to \text{Matrix}\, m\, n\, R$, the function $x \mapsto (f(x))^\mathsf{H}$ is summable if and only if $f$ is summable.

Matrix.conjTranspose_tsum theorem

[StarAddMonoid R] [ContinuousStar R] [T2Space R] {f : X → Matrix m n R} : (∑' x, f x)ᴴ = ∑' x, (f x)ᴴ

Full source

theorem Matrix.conjTranspose_tsum [StarAddMonoid R] [ContinuousStar R] [T2Space R]
    {f : X → Matrix m n R} : (∑' x, f x)ᴴ = ∑' x, (f x)ᴴ := by
  by_cases hf : Summable f
  · exact hf.hasSum.matrix_conjTranspose.tsum_eq.symm
  · have hft := summable_matrix_conjTranspose.not.mpr hf
    rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft, conjTranspose_zero]

Conjugate Transpose Commutes with Infinite Sum: $\left( \sum_{x} f(x) \right)^\mathsf{H} = \sum_{x} (f(x))^\mathsf{H}$

Informal description

Let $R$ be a topological space equipped with a continuous star operation $\star \colon R \to R$ and Hausdorff topology, and let $X$ be a topological space. For any matrix-valued function $f \colon X \to \text{Matrix}\, m\, n\, R$, the conjugate transpose of the infinite sum of $f$ equals the infinite sum of the conjugate transposes: $$ \left( \sum_{x} f(x) \right)^\mathsf{H} = \sum_{x} (f(x))^\mathsf{H}. $$

HasSum.matrix_diagonal theorem

[DecidableEq n] {f : X → n → R} {a : n → R} (hf : HasSum f a) : HasSum (fun x => diagonal (f x)) (diagonal a)

Full source

theorem HasSum.matrix_diagonal [DecidableEq n] {f : X → n → R} {a : n → R} (hf : HasSum f a) :
    HasSum (fun x => diagonal (f x)) (diagonal a) :=
  hf.map (diagonalAddMonoidHom n R) continuous_id.matrix_diagonal

Sum of Diagonal Matrices Equals Diagonal of Sums

Informal description

Let $X$ be a topological space, $R$ a topological space with decidable equality on the index type $n$, and $f : X \to n \to R$ a function. If $f$ has sum $a$ (i.e., $\sum_{x} f(x) = a$), then the diagonal matrix construction $\text{diagonal}(f(x))$ has sum $\text{diagonal}(a)$ (i.e., $\sum_{x} \text{diagonal}(f(x)) = \text{diagonal}(a)$).

Summable.matrix_diagonal theorem

[DecidableEq n] {f : X → n → R} (hf : Summable f) : Summable fun x => diagonal (f x)

Full source

theorem Summable.matrix_diagonal [DecidableEq n] {f : X → n → R} (hf : Summable f) :
    Summable fun x => diagonal (f x) :=
  hf.hasSum.matrix_diagonal.summable

Summability of Diagonal Matrix Construction

Informal description

Let $X$ be a topological space, $R$ a topological space with decidable equality on the index type $n$, and $f : X \to n \to R$ a function. If $f$ is summable, then the function $x \mapsto \text{diagonal}(f(x))$ is also summable.

summable_matrix_diagonal theorem

[DecidableEq n] {f : X → n → R} : (Summable fun x => diagonal (f x)) ↔ Summable f

Full source

@[simp]
theorem summable_matrix_diagonal [DecidableEq n] {f : X → n → R} :
    (Summable fun x => diagonal (f x)) ↔ Summable f :=
  Summable.map_iff_of_leftInverse (Matrix.diagonalAddMonoidHom n R) (Matrix.diagAddMonoidHom n R)
    continuous_id.matrix_diagonal continuous_matrix_diag fun A => diag_diagonal A

Summability of Diagonal Matrix Construction vs. Summability of Vector Components

Informal description

For a topological space $X$, a topological space $R$ with decidable equality on the index type $n$, and a function $f \colon X \to n \to R$, the function $x \mapsto \text{diagonal}(f(x))$ is summable if and only if $f$ is summable.

Matrix.diagonal_tsum theorem

[DecidableEq n] [T2Space R] {f : X → n → R} : diagonal (∑' x, f x) = ∑' x, diagonal (f x)

Full source

theorem Matrix.diagonal_tsum [DecidableEq n] [T2Space R] {f : X → n → R} :
    diagonal (∑' x, f x) = ∑' x, diagonal (f x) := by
  by_cases hf : Summable f
  · exact hf.hasSum.matrix_diagonal.tsum_eq.symm
  · have hft := summable_matrix_diagonal.not.mpr hf
    rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft]
    exact diagonal_zero

Diagonal Construction Commutes with Infinite Sums in Matrix Spaces

Informal description

For a topological space $X$, a Hausdorff topological space $R$ with decidable equality on the index type $n$, and a function $f \colon X \to n \to R$, the diagonal matrix constructed from the infinite sum of $f$ equals the infinite sum of the diagonal matrices constructed from $f$. That is, \[ \text{diagonal}\left(\sum_{x} f(x)\right) = \sum_{x} \text{diagonal}(f(x)). \]

HasSum.matrix_diag theorem

{f : X → Matrix n n R} {a : Matrix n n R} (hf : HasSum f a) : HasSum (fun x => diag (f x)) (diag a)

Full source

theorem HasSum.matrix_diag {f : X → Matrix n n R} {a : Matrix n n R} (hf : HasSum f a) :
    HasSum (fun x => diag (f x)) (diag a) :=
  hf.map (diagAddMonoidHom n R) continuous_matrix_diag

Diagonal Extraction Preserves Infinite Sums

Informal description

Let $X$ be a topological space, $R$ a topological ring, and $n$ an index type. Given a function $f \colon X \to \text{Matrix}\, n\, n\, R$ and a matrix $a \in \text{Matrix}\, n\, n\, R$, if $f$ has sum $a$ (i.e., $\sum_{x} f(x) = a$), then the diagonal extraction preserves the sum: $\sum_{x} \text{diag}\, (f(x)) = \text{diag}\, a$.

Summable.matrix_diag theorem

{f : X → Matrix n n R} (hf : Summable f) : Summable fun x => diag (f x)

Full source

theorem Summable.matrix_diag {f : X → Matrix n n R} (hf : Summable f) :
    Summable fun x => diag (f x) :=
  hf.hasSum.matrix_diag.summable

Summability of Matrix Diagonals

Informal description

Let $X$ be a topological space, $R$ a topological ring, and $n$ an index type. If a function $f \colon X \to \text{Matrix}\, n\, n\, R$ is summable, then the function $x \mapsto \text{diag}(f(x))$ is also summable.

HasSum.matrix_blockDiagonal theorem

 [DecidableEq p] {f : X → p → Matrix m n R} {a : p → Matrix m n R} (hf : HasSum f a) :
  HasSum (fun x => blockDiagonal (f x)) (blockDiagonal a)

Full source

theorem HasSum.matrix_blockDiagonal [DecidableEq p] {f : X → p → Matrix m n R}
    {a : p → Matrix m n R} (hf : HasSum f a) :
    HasSum (fun x => blockDiagonal (f x)) (blockDiagonal a) :=
  hf.map (blockDiagonalAddMonoidHom m n p R) continuous_id.matrix_blockDiagonal

Block Diagonal Construction Preserves Infinite Sums

Informal description

Let $X$ be a topological space, $R$ a topological ring, and $p$ an index type with decidable equality. Given a function $f \colon X \to p \to \text{Matrix}\, m\, n\, R$ and a family of matrices $a \colon p \to \text{Matrix}\, m\, n\, R$, if $f$ has sum $a$ (i.e., $\sum_{x} f(x) = a$), then the block diagonal construction preserves the sum: $\sum_{x} \text{blockDiagonal}\, (f(x)) = \text{blockDiagonal}\, a$.

Summable.matrix_blockDiagonal theorem

[DecidableEq p] {f : X → p → Matrix m n R} (hf : Summable f) : Summable fun x => blockDiagonal (f x)

Full source

theorem Summable.matrix_blockDiagonal [DecidableEq p] {f : X → p → Matrix m n R} (hf : Summable f) :
    Summable fun x => blockDiagonal (f x) :=
  hf.hasSum.matrix_blockDiagonal.summable

Summability of Block Diagonal Matrices

Informal description

Let $X$ be a topological space, $R$ a topological ring, and $p$ an index type with decidable equality. If a function $f \colon X \to p \to \text{Matrix}\, m\, n\, R$ is summable, then the function $x \mapsto \text{blockDiagonal}(f(x))$ is also summable.

summable_matrix_blockDiagonal theorem

[DecidableEq p] {f : X → p → Matrix m n R} : (Summable fun x => blockDiagonal (f x)) ↔ Summable f

Full source

theorem summable_matrix_blockDiagonal [DecidableEq p] {f : X → p → Matrix m n R} :
    (Summable fun x => blockDiagonal (f x)) ↔ Summable f :=
  Summable.map_iff_of_leftInverse (blockDiagonalAddMonoidHom m n p R)
    (blockDiagAddMonoidHom m n p R) continuous_id.matrix_blockDiagonal
    continuous_id.matrix_blockDiag fun A => blockDiag_blockDiagonal A

Summability Equivalence for Block Diagonal Matrices: $\sum \text{blockDiagonal}\, f \leftrightarrow \sum f$

Informal description

Let $X$ be a topological space and $R$ be a topological ring with decidable equality on the index type $p$. For a function $f \colon X \to p \to \text{Matrix}\, m\, n\, R$, the sum $\sum_{x} \text{blockDiagonal}\, (f(x))$ converges if and only if the sum $\sum_{x} f(x)$ converges.

Matrix.blockDiagonal_tsum theorem

[DecidableEq p] [T2Space R] {f : X → p → Matrix m n R} : blockDiagonal (∑' x, f x) = ∑' x, blockDiagonal (f x)

Full source

theorem Matrix.blockDiagonal_tsum [DecidableEq p] [T2Space R] {f : X → p → Matrix m n R} :
    blockDiagonal (∑' x, f x) = ∑' x, blockDiagonal (f x) := by
  by_cases hf : Summable f
  · exact hf.hasSum.matrix_blockDiagonal.tsum_eq.symm
  · have hft := summable_matrix_blockDiagonal.not.mpr hf
    rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft]
    exact blockDiagonal_zero

Block Diagonal Commutes with Infinite Sum: $\text{blockDiagonal}(\sum f) = \sum \text{blockDiagonal}\, f$

Informal description

Let $X$ be a topological space, $R$ a Hausdorff topological ring, and $p$ an index type with decidable equality. For any function $f \colon X \to p \to \text{Matrix}\, m\, n\, R$, the block diagonal construction commutes with infinite sums: \[ \text{blockDiagonal}\left(\sum_{x} f(x)\right) = \sum_{x} \text{blockDiagonal}(f(x)). \]

HasSum.matrix_blockDiag theorem

 {f : X → Matrix (m × p) (n × p) R} {a : Matrix (m × p) (n × p) R} (hf : HasSum f a) :
  HasSum (fun x => blockDiag (f x)) (blockDiag a)

Full source

theorem HasSum.matrix_blockDiag {f : X → Matrix (m × p) (n × p) R} {a : Matrix (m × p) (n × p) R}
    (hf : HasSum f a) : HasSum (fun x => blockDiag (f x)) (blockDiag a) :=
  (hf.map (blockDiagAddMonoidHom m n p R) <| Continuous.matrix_blockDiag continuous_id :)

Convergence of Block Diagonal Extraction from Matrix-Valued Sums

Informal description

Let $X$ be a topological space and $R$ be a topological ring. Given a function $f \colon X \to \text{Matrix}\,(m \times p)\,(n \times p)\,R$ with a sum converging to $a \in \text{Matrix}\,(m \times p)\,(n \times p)\,R$, the function $x \mapsto \text{blockDiag}\,(f(x))$ has a sum converging to $\text{blockDiag}\,(a)$, where $\text{blockDiag}$ extracts the block diagonal from a matrix.

Summable.matrix_blockDiag theorem

{f : X → Matrix (m × p) (n × p) R} (hf : Summable f) : Summable fun x => blockDiag (f x)

Full source

theorem Summable.matrix_blockDiag {f : X → Matrix (m × p) (n × p) R} (hf : Summable f) :
    Summable fun x => blockDiag (f x) :=
  hf.hasSum.matrix_blockDiag.summable

Summability of Block Diagonal Extraction from Matrix-Valued Functions

Informal description

Let $X$ be a topological space and $R$ be a topological ring. For any summable function $f \colon X \to \text{Matrix}\,(m \times p)\,(n \times p)\,R$, the function $x \mapsto \text{blockDiag}\,(f(x))$ is also summable, where $\text{blockDiag}$ extracts the block diagonal from a matrix.

HasSum.matrix_blockDiagonal' theorem

 [DecidableEq l] {f : X → ∀ i, Matrix (m' i) (n' i) R} {a : ∀ i, Matrix (m' i) (n' i) R} (hf : HasSum f a) :
  HasSum (fun x => blockDiagonal' (f x)) (blockDiagonal' a)

Full source

theorem HasSum.matrix_blockDiagonal' [DecidableEq l] {f : X → ∀ i, Matrix (m' i) (n' i) R}
    {a : ∀ i, Matrix (m' i) (n' i) R} (hf : HasSum f a) :
    HasSum (fun x => blockDiagonal' (f x)) (blockDiagonal' a) :=
  hf.map (blockDiagonal'AddMonoidHom m' n' R) continuous_id.matrix_blockDiagonal'

Convergence of Block Diagonal Matrix Construction from Summable Family of Matrices

Informal description

Let $X$ be a topological space, $l$ be a type with decidable equality, and $R$ be a topological space. Given a function $f \colon X \to \prod_{i \in l} \text{Matrix}\,(m'_i)\,(n'_i)\,R$ that has a sum converging to $a \in \prod_{i \in l} \text{Matrix}\,(m'_i)\,(n'_i)\,R$, the function $x \mapsto \text{blockDiagonal'}\,(f(x))$ has a sum converging to $\text{blockDiagonal'}\,(a)$, where $\text{blockDiagonal'}$ constructs a block diagonal matrix from a family of matrices with varying block sizes indexed by $i \in l$.

Summable.matrix_blockDiagonal' theorem

[DecidableEq l] {f : X → ∀ i, Matrix (m' i) (n' i) R} (hf : Summable f) : Summable fun x => blockDiagonal' (f x)

Full source

theorem Summable.matrix_blockDiagonal' [DecidableEq l] {f : X → ∀ i, Matrix (m' i) (n' i) R}
    (hf : Summable f) : Summable fun x => blockDiagonal' (f x) :=
  hf.hasSum.matrix_blockDiagonal'.summable

Summability of Block Diagonal Matrix Construction from Summable Family of Matrices

Informal description

Let $X$ be a type, $l$ be a type with decidable equality, and $R$ be a topological space. Given a summable function $f \colon X \to \prod_{i \in l} \text{Matrix}\,(m'_i)\,(n'_i)\,R$, the function $x \mapsto \text{blockDiagonal'}\,(f(x))$ is also summable, where $\text{blockDiagonal'}$ constructs a block diagonal matrix from a family of matrices with varying block sizes indexed by $i \in l$.

summable_matrix_blockDiagonal' theorem

[DecidableEq l] {f : X → ∀ i, Matrix (m' i) (n' i) R} : (Summable fun x => blockDiagonal' (f x)) ↔ Summable f

Full source

theorem summable_matrix_blockDiagonal' [DecidableEq l] {f : X → ∀ i, Matrix (m' i) (n' i) R} :
    (Summable fun x => blockDiagonal' (f x)) ↔ Summable f :=
  Summable.map_iff_of_leftInverse (blockDiagonal'AddMonoidHom m' n' R)
    (blockDiag'AddMonoidHom m' n' R) continuous_id.matrix_blockDiagonal'
    continuous_id.matrix_blockDiag' fun A => blockDiag'_blockDiagonal' A

Summability of Block Diagonal Matrices vs. Componentwise Summability

Informal description

Let $X$ be a type, $l$ be a type with decidable equality, and $R$ be a topological space. For a function $f \colon X \to \prod_{i \in l} \text{Matrix}\, (m'_i)\, (n'_i)\, R$, the sum $\sum_{x} \text{blockDiagonal'}\, (f(x))$ exists if and only if the sum $\sum_{x} f(x)$ exists.

Matrix.blockDiagonal'_tsum theorem

 [DecidableEq l] [T2Space R] {f : X → ∀ i, Matrix (m' i) (n' i) R} :
  blockDiagonal' (∑' x, f x) = ∑' x, blockDiagonal' (f x)

Full source

theorem Matrix.blockDiagonal'_tsum [DecidableEq l] [T2Space R]
    {f : X → ∀ i, Matrix (m' i) (n' i) R} :
    blockDiagonal' (∑' x, f x) = ∑' x, blockDiagonal' (f x) := by
  by_cases hf : Summable f
  · exact hf.hasSum.matrix_blockDiagonal'.tsum_eq.symm
  · have hft := summable_matrix_blockDiagonal'.not.mpr hf
    rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft]
    exact blockDiagonal'_zero

Block Diagonal Construction Commutes with Infinite Summation

Informal description

Let $X$ be a type, $l$ be a type with decidable equality, and $R$ be a Hausdorff topological space. For any function $f \colon X \to \prod_{i \in l} \text{Matrix}\,(m'_i)\,(n'_i)\,R$, the block diagonal matrix constructed from the infinite sum $\sum_{x} f(x)$ is equal to the infinite sum of the block diagonal matrices constructed from $f(x)$ for each $x \in X$. In other words, the following equality holds: \[ \text{blockDiagonal'}\left(\sum_{x} f(x)\right) = \sum_{x} \text{blockDiagonal'}(f(x)). \]

HasSum.matrix_blockDiag' theorem

 {f : X → Matrix (Σ i, m' i) (Σ i, n' i) R} {a : Matrix (Σ i, m' i) (Σ i, n' i) R} (hf : HasSum f a) :
  HasSum (fun x => blockDiag' (f x)) (blockDiag' a)

Full source

theorem HasSum.matrix_blockDiag' {f : X → Matrix (Σ i, m' i) (Σ i, n' i) R}
    {a : Matrix (Σ i, m' i) (Σ i, n' i) R} (hf : HasSum f a) :
    HasSum (fun x => blockDiag' (f x)) (blockDiag' a) :=
  hf.map (blockDiag'AddMonoidHom m' n' R) continuous_id.matrix_blockDiag'

Block Diagonal Extraction Preserves Summability

Informal description

Let $X$ be a topological space and $R$ be a topological space. Given a function $f \colon X \to \text{Matrix}\, (\Sigma i, m'_i)\, (\Sigma i, n'_i)\, R$ and a matrix $a$ of the same type, if $f$ has sum $a$ (i.e., $\sum_{x} f(x) = a$), then the function $x \mapsto \text{blockDiag'}\, (f(x))$ has sum $\text{blockDiag'}\, a$.

Summable.matrix_blockDiag' theorem

{f : X → Matrix (Σ i, m' i) (Σ i, n' i) R} (hf : Summable f) : Summable fun x => blockDiag' (f x)

Full source

theorem Summable.matrix_blockDiag' {f : X → Matrix (Σ i, m' i) (Σ i, n' i) R} (hf : Summable f) :
    Summable fun x => blockDiag' (f x) :=
  hf.hasSum.matrix_blockDiag'.summable

Summability of Block Diagonal Extraction

Informal description

Let $X$ be a topological space and $R$ be a topological space. Given a summable function $f \colon X \to \text{Matrix}\, (\Sigma i, m'_i)\, (\Sigma i, n'_i)\, R$, the function $x \mapsto \text{blockDiag'}\, (f(x))$ is also summable.

Mathlib.Topology.Instances.Matrix

Main definitions:

Main results