Documentation

Mathlib.Data.Matrix.ColumnRowPartitioned

Block Matrices from Rows and Columns #

This file provides the basic definitions of matrices composed from columns and rows. The concatenation of two matrices with the same row indices can be expressed as A = fromColumns A₁ A₂ the concatenation of two matrices with the same column indices can be expressed as B = fromRows B₁ B₂.

We then provide a few lemmas that deal with the products of these with each other and with block matrices

Tags #

column matrices, row matrices, column row block matrices

source
def Matrix.fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
Matrix (m₁ ⊕ m₂) n R

Concatenate together two matrices A₁[m₁ × N] and A₂[m₂ × N] with the same columns (N) to get a bigger matrix indexed by [(m₁ ⊕ m₂) × N]

Equations
  • A₁.fromRows A₂ = Matrix.of (Sum.elim A₁ A₂)
Instances For
    source
    def Matrix.fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) :
    Matrix m (n₁ ⊕ n₂) R

    Concatenate together two matrices B₁[m × n₁] and B₂[m × n₂] with the same rows (M) to get a bigger matrix indexed by [m × (n₁ ⊕ n₂)]

    Equations
    • B₁.fromColumns B₂ = Matrix.of fun (i : m) => Sum.elim (B₁ i) (B₂ i)
    Instances For
      source
      def Matrix.toColumns₁ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) :
      Matrix m n₁ R

      Given a column partitioned matrix extract the first column

      Equations
      • A.toColumns₁ = Matrix.of fun (i : m) (j : n₁) => A i (Sum.inl j)
      Instances For
        source
        def Matrix.toColumns₂ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) :
        Matrix m n₂ R

        Given a column partitioned matrix extract the second column

        Equations
        • A.toColumns₂ = Matrix.of fun (i : m) (j : n₂) => A i (Sum.inr j)
        Instances For
          source
          def Matrix.toRows₁ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) :
          Matrix m₁ n R

          Given a row partitioned matrix extract the first row

          Equations
          • A.toRows₁ = Matrix.of fun (i : m₁) (j : n) => A (Sum.inl i) j
          Instances For
            source
            def Matrix.toRows₂ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) :
            Matrix m₂ n R

            Given a row partitioned matrix extract the second row

            Equations
            • A.toRows₂ = Matrix.of fun (i : m₂) (j : n) => A (Sum.inr i) j
            Instances For
              source
              @[simp]
              theorem Matrix.fromRows_apply_inl {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (i : m₁) (j : n) :
              A₁.fromRows A₂ (Sum.inl i) j = A₁ i j
              source
              @[simp]
              theorem Matrix.fromRows_apply_inr {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (i : m₂) (j : n) :
              A₁.fromRows A₂ (Sum.inr i) j = A₂ i j
              source
              @[simp]
              theorem Matrix.fromColumns_apply_inl {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₁) :
              A₁.fromColumns A₂ i (Sum.inl j) = A₁ i j
              source
              @[simp]
              theorem Matrix.fromColumns_apply_inr {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₂) :
              A₁.fromColumns A₂ i (Sum.inr j) = A₂ i j
              source
              @[simp]
              theorem Matrix.toRows₁_apply {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) (i : m₁) (j : n) :
              A.toRows₁ i j = A (Sum.inl i) j
              source
              @[simp]
              theorem Matrix.toRows₂_apply {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) (i : m₂) (j : n) :
              A.toRows₂ i j = A (Sum.inr i) j
              source
              @[simp]
              theorem Matrix.toRows₁_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
              (A₁.fromRows A₂).toRows₁ = A₁
              source
              @[simp]
              theorem Matrix.toRows₂_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
              (A₁.fromRows A₂).toRows₂ = A₂
              source
              @[simp]
              theorem Matrix.toColumns₁_apply {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₁) :
              A.toColumns₁ i j = A i (Sum.inl j)
              source
              @[simp]
              theorem Matrix.toColumns₂_apply {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₂) :
              A.toColumns₂ i j = A i (Sum.inr j)
              source
              @[simp]
              theorem Matrix.toColumns₁_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
              (A₁.fromColumns A₂).toColumns₁ = A₁
              source
              @[simp]
              theorem Matrix.toColumns₂_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
              (A₁.fromColumns A₂).toColumns₂ = A₂
              source
              @[simp]
              theorem Matrix.fromColumns_toColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) :
              A.toColumns₁.fromColumns A.toColumns₂ = A
              source
              @[simp]
              theorem Matrix.fromRows_toRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) :
              A.toRows₁.fromRows A.toRows₂ = A
              source
              theorem Matrix.fromRows_inj {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} :
              Function.Injective2 Matrix.fromRows
              source
              theorem Matrix.fromColumns_inj {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} :
              Function.Injective2 Matrix.fromColumns
              source
              theorem Matrix.fromColumns_ext_iff {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) :
              A₁.fromColumns A₂ = B₁.fromColumns B₂ ↔ A₁ = B₁ ∧ A₂ = B₂
              source
              theorem Matrix.fromRows_ext_iff {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) :
              A₁.fromRows A₂ = B₁.fromRows B₂ ↔ A₁ = B₁ ∧ A₂ = B₂
              source
              theorem Matrix.transpose_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
              (A₁.fromColumns A₂).transpose = A₁.transpose.fromRows A₂.transpose

              A column partitioned matrix when transposed gives a row partitioned matrix with columns of the initial matrix transposed to become rows.

              source
              theorem Matrix.transpose_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
              (A₁.fromRows A₂).transpose = A₁.transpose.fromColumns A₂.transpose

              A row partitioned matrix when transposed gives a column partitioned matrix with rows of the initial matrix transposed to become columns.

              source
              @[simp]
              theorem Matrix.fromRows_neg {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Neg R] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
              -A₁.fromRows A₂ = (-A₁).fromRows (-A₂)

              Negating a matrix partitioned by rows is equivalent to negating each of the rows.

              source
              @[simp]
              theorem Matrix.fromColumns_neg {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Neg R] (A₁ : Matrix n m₁ R) (A₂ : Matrix n m₂ R) :
              -A₁.fromColumns A₂ = (-A₁).fromColumns (-A₂)

              Negating a matrix partitioned by columns is equivalent to negating each of the columns.

              source
              @[simp]
              theorem Matrix.fromColumns_fromRows_eq_fromBlocks {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
              (B₁₁.fromRows B₂₁).fromColumns (B₁₂.fromRows B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
              source
              @[simp]
              theorem Matrix.fromRows_fromColumn_eq_fromBlocks {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
              (B₁₁.fromColumns B₁₂).fromRows (B₂₁.fromColumns B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
              source
              @[simp]
              theorem Matrix.fromRows_mulVec {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (v : n → R) :
              (A₁.fromRows A₂).mulVec v = Sum.elim (A₁.mulVec v) (A₂.mulVec v)
              source
              @[simp]
              theorem Matrix.vecMul_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype m] (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) (v : m → R) :
              Matrix.vecMul v (B₁.fromColumns B₂) = Sum.elim (Matrix.vecMul v B₁) (Matrix.vecMul v B₂)
              source
              @[simp]
              theorem Matrix.sum_elim_vecMul_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] [Fintype m₁] [Fintype m₂] (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) (v₁ : m₁ → R) (v₂ : m₂ → R) :
              Matrix.vecMul (Sum.elim v₁ v₂) (B₁.fromRows B₂) = Matrix.vecMul v₁ B₁ + Matrix.vecMul v₂ B₂
              source
              @[simp]
              theorem Matrix.fromColumns_mulVec_sum_elim {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (v₁ : n₁ → R) (v₂ : n₂ → R) :
              (A₁.fromColumns A₂).mulVec (Sum.elim v₁ v₂) = A₁.mulVec v₁ + A₂.mulVec v₂
              source
              @[simp]
              theorem Matrix.fromRows_mul {R : Type u_1} {m : Type u_2} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B : Matrix n m R) :
              A₁.fromRows A₂ * B = (A₁ * B).fromRows (A₂ * B)
              source
              @[simp]
              theorem Matrix.mul_fromColumns {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n] (A : Matrix m n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
              A * B₁.fromColumns B₂ = (A * B₁).fromColumns (A * B₂)
              source
              @[simp]
              theorem Matrix.fromRows_zero {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] :
              Matrix.fromRows 0 0 = 0
              source
              @[simp]
              theorem Matrix.fromColumns_zero {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] :
              Matrix.fromColumns 0 0 = 0
              source
              theorem Matrix.fromRows_mul_fromColumns {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
              A₁.fromRows A₂ * B₁.fromColumns B₂ = Matrix.fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)

              A row partitioned matrix multiplied by a column partitioned matrix gives a 2 by 2 block matrix.

              source
              theorem Matrix.fromColumns_mul_fromRows {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :
              A₁.fromColumns A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂

              A column partitioned matrix multiplied by a row partitioned matrix gives the sum of the "outer" products of the block matrices.

              source
              theorem Matrix.fromColumns_mul_fromBlocks {R : Type u_1} {m : Type u_2} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype m₁] [Fintype m₂] (A₁ : Matrix m m₁ R) (A₂ : Matrix m m₂ R) (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
              A₁.fromColumns A₂ * Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromColumns (A₁ * B₁₂ + A₂ * B₂₂)

              A column partitioned matrix multipiled by a block matrix results in a column partitioned matrix.

              source
              theorem Matrix.fromBlocks_mul_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix n₁ n R) (A₂ : Matrix n₂ n R) (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
              Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)

              A block matrix multiplied by a row partitioned matrix gives a row partitioned matrix.

              source
              theorem Matrix.fromColumns_mul_fromRows_eq_one_comm {R : Type u_1} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [CommRing R] [Fintype n₁] [Fintype n₂] [Fintype n] [DecidableEq n] [DecidableEq n₁] [DecidableEq n₂] (e : n ≃ n₁ ⊕ n₂) (A₁ : Matrix n n₁ R) (A₂ : Matrix n n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :
              A₁.fromColumns A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromColumns A₂ = 1

              Multiplication of a matrix by its inverse is commutative. This is the column and row partitioned matrix form of Matrix.mul_eq_one_comm.

              The condition e : n ≃ n₁ ⊕ n₂ states that fromColumns A₁ A₂ and fromRows B₁ B₂ are "square".

              source
              theorem Matrix.equiv_compl_fromColumns_mul_fromRows_eq_one_comm {R : Type u_1} {n : Type u_5} [CommRing R] [Fintype n] [DecidableEq n] (p : n → Prop) [DecidablePred p] (A₁ : Matrix n { i : n // p i } R) (A₂ : Matrix n { i : n // ¬p i } R) (B₁ : Matrix { i : n // p i } n R) (B₂ : Matrix { i : n // ¬p i } n R) :
              A₁.fromColumns A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromColumns A₂ = 1

              The lemma fromColumns_mul_fromRows_eq_one_comm specialized to the case where the index sets n₁ and n₂, are the result of subtyping by a predicate and its complement.

              source
              theorem Matrix.conjTranspose_fromColumns_eq_fromRows_conjTranspose {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Star R] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
              (A₁.fromColumns A₂).conjTranspose = A₁.conjTranspose.fromRows A₂.conjTranspose

              A column partitioned matrix in a Star ring when conjugate transposed gives a row partitioned matrix with the columns of the initial matrix conjugate transposed to become rows.

              source
              theorem Matrix.conjTranspose_fromRows_eq_fromColumns_conjTranspose {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Star R] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
              (A₁.fromRows A₂).conjTranspose = A₁.conjTranspose.fromColumns A₂.conjTranspose

              A row partitioned matrix in a Star ring when conjugate transposed gives a column partitioned matrix with the rows of the initial matrix conjugate transposed to become columns.