feat(data/matrix/block): add matrix.block_diag and `matrix.block_di…

…ag'` (#13918)

`matrix.block_diag` is to `matrix.block_diagonal` as `matrix.diag` is to `matrix.diagonal`.

As well as the basic arithmetic lemmas and bundling, this also adds continuity lemmas.

These definitions are primarily an auxiliary construction to prove `matrix.tsum_block_diagonal`, and `matrix.tsum_block_diagonal'`, which are really the main goal of this PR.

src/data/matrix/block.lean

@@ -15,8 +15,10 @@ import data.matrix.basic
   extract each of the four blocks from `matrix.from_blocks`.
 * `matrix.block_diagonal`: block diagonal of equally sized blocks. On square blocks, this is a
   ring homomorphisms, `matrix.block_diagonal_ring_hom`.
+* `matrix.block_diag`: extract the blocks from the diagonal of a block diagonal matrix.
 * `matrix.block_diagonal'`: block diagonal of unequally sized blocks. On square blocks, this is a
   ring homomorphisms, `matrix.block_diagonal'_ring_hom`.
+* `matrix.block_diag'`: extract the blocks from the diagonal of a block diagonal matrix.
 -/
 
 variables {l m n o p q : Type*} {m' n' p' : o → Type*}
@@ -334,12 +336,87 @@ by { ext, simp only [block_diagonal_apply, pi.smul_apply], split_ifs; simp }
 
 end block_diagonal
 
+section block_diag
+
+
+/-- Extract a block from the diagonal of a block diagonal matrix.
+
+This is the block form of `matrix.diag`, and the left-inverse of `matrix.block_diagonal`. -/
+def block_diag (M : matrix (m × o) (n × o) α) (k : o) : matrix m n α
+| i j := M (i, k) (j, k)
+
+lemma block_diag_map (M : matrix (m × o) (n × o) α) (f : α → β) :
+  block_diag (M.map f) = λ k, (block_diag M k).map f :=
+rfl
+
+@[simp] lemma block_diag_transpose (M : matrix (m × o) (n × o) α) (k : o) :
+  block_diag Mᵀ k = (block_diag M k)ᵀ :=
+ext $ λ i j, rfl
+
+@[simp] lemma block_diag_conj_transpose
+  {α : Type*} [add_monoid α] [star_add_monoid α] (M : matrix (m × o) (n × o) α) (k : o) :
+  block_diag Mᴴ k = (block_diag M k)ᴴ :=
+ext $ λ i j, rfl
+
+section has_zero
+variables [has_zero α] [has_zero β]
+
+@[simp] lemma block_diag_zero :
+  block_diag (0 : matrix (m × o) (n × o) α) = 0 :=
+rfl
+
+@[simp] lemma block_diag_diagonal [decidable_eq o] [decidable_eq m] (d : (m × o) → α) (k : o) :
+  block_diag (diagonal d) k = diagonal (λ i, d (i, k)) :=
+ext $ λ i j, begin
+  obtain rfl | hij := decidable.eq_or_ne i j,
+  { rw [block_diag, diagonal_apply_eq, diagonal_apply_eq] },
+  { rw [block_diag, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt _ hij)],
+    exact prod.fst_eq_iff.mpr },
+end
+
+@[simp] lemma block_diag_block_diagonal [decidable_eq o] (M : o → matrix m n α) :
+  block_diag (block_diagonal M) = M :=
+funext $ λ k, ext $ λ i j, block_diagonal_apply_eq _ _ _ _
+
+@[simp] lemma block_diag_one [decidable_eq o] [decidable_eq m] [has_one α] :
+  block_diag (1 : matrix (m × o) (m × o) α) = 1 :=
+funext $ block_diag_diagonal _
+
+end has_zero
+
+@[simp] lemma block_diag_add [add_zero_class α] (M N : matrix (m × o) (n × o) α) :
+  block_diag (M + N) = block_diag M + block_diag N :=
+rfl
+
+section
+variables (o m n α)
+/-- `matrix.block_diag` as an `add_monoid_hom`. -/
+@[simps] def block_diag_add_monoid_hom [add_zero_class α] :
+  matrix (m × o) (n × o) α →+ (o → matrix m n α) :=
+{ to_fun := block_diag,
+  map_zero' := block_diag_zero,
+  map_add' := block_diag_add }
+end
+
+@[simp] lemma block_diag_neg [add_group α] (M : matrix (m × o) (n × o) α) :
+  block_diag (-M) = - block_diag M :=
+map_neg (block_diag_add_monoid_hom m n o α) M
+
+@[simp] lemma block_diag_sub [add_group α] (M N : matrix (m × o) (n × o) α) :
+  block_diag (M - N) = block_diag M - block_diag N :=
+map_sub (block_diag_add_monoid_hom m n o α) M N
+
+@[simp] lemma block_diag_smul {R : Type*} [monoid R] [add_monoid α] [distrib_mul_action R α]
+  (x : R) (M : matrix (m × o) (n × o) α) : block_diag (x • M) = x • block_diag M :=
+rfl
+
+end block_diag
+
 section block_diagonal'
 
 variables [decidable_eq o]
 
 section has_zero
-
 variables [has_zero α] [has_zero β]
 
 /-- `matrix.block_diagonal' M` turns `M : Π i, matrix (m i) (n i) α` into a
@@ -481,4 +558,80 @@ by { ext, simp only [block_diagonal'_apply, pi.smul_apply], split_ifs; simp }
 
 end block_diagonal'
 
+section block_diag'
+
+/-- Extract a block from the diagonal of a block diagonal matrix.
+
+This is the block form of `matrix.diag`, and the left-inverse of `matrix.block_diagonal'`. -/
+def block_diag' (M : matrix (Σ i, m' i) (Σ i, n' i) α) (k : o) : matrix (m' k) (n' k) α
+| i j := M ⟨k, i⟩ ⟨k, j⟩
+
+lemma block_diag'_map (M : matrix (Σ i, m' i) (Σ i, n' i) α) (f : α → β) :
+  block_diag' (M.map f) = λ k, (block_diag' M k).map f :=
+rfl
+
+@[simp] lemma block_diag'_transpose (M : matrix (Σ i, m' i) (Σ i, n' i) α) (k : o) :
+  block_diag' Mᵀ k = (block_diag' M k)ᵀ :=
+ext $ λ i j, rfl
+
+@[simp] lemma block_diag'_conj_transpose
+  {α : Type*} [add_monoid α] [star_add_monoid α] (M : matrix (Σ i, m' i) (Σ i, n' i) α) (k : o) :
+  block_diag' Mᴴ k = (block_diag' M k)ᴴ :=
+ext $ λ i j, rfl
+
+section has_zero
+variables [has_zero α] [has_zero β]
+
+@[simp] lemma block_diag'_zero :
+  block_diag' (0 : matrix (Σ i, m' i) (Σ i, n' i) α) = 0 :=
+rfl
+
+@[simp] lemma block_diag'_diagonal [decidable_eq o] [Π i, decidable_eq (m' i)]
+  (d : (Σ i, m' i) → α) (k : o) :
+  block_diag' (diagonal d) k = diagonal (λ i, d ⟨k, i⟩) :=
+ext $ λ i j, begin
+  obtain rfl | hij := decidable.eq_or_ne i j,
+  { rw [block_diag', diagonal_apply_eq, diagonal_apply_eq] },
+  { rw [block_diag', diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt (λ h, _) hij)],
+    cases h, refl },
+end
+
+@[simp] lemma block_diag'_block_diagonal' [decidable_eq o] (M : Π i, matrix (m' i) (n' i) α) :
+  block_diag' (block_diagonal' M) = M :=
+funext $ λ k, ext $ λ i j, block_diagonal'_apply_eq _ _ _ _
+
+@[simp] lemma block_diag'_one [decidable_eq o] [Π i, decidable_eq (m' i)] [has_one α] :
+  block_diag' (1 : matrix (Σ i, m' i) (Σ i, m' i) α) = 1 :=
+funext $ block_diag'_diagonal _
+
+end has_zero
+
+@[simp] lemma block_diag'_add [add_zero_class α] (M N : matrix (Σ i, m' i) (Σ i, n' i) α) :
+  block_diag' (M + N) = block_diag' M + block_diag' N :=
+rfl
+
+section
+variables (m' n' α)
+/-- `matrix.block_diag'` as an `add_monoid_hom`. -/
+@[simps] def block_diag'_add_monoid_hom [add_zero_class α] :
+  matrix (Σ i, m' i) (Σ i, n' i) α →+ Π i, matrix (m' i) (n' i) α :=
+{ to_fun := block_diag',
+  map_zero' := block_diag'_zero,
+  map_add' := block_diag'_add }
+end
+
+@[simp] lemma block_diag'_neg [add_group α] (M : matrix (Σ i, m' i) (Σ i, n' i) α) :
+  block_diag' (-M) = - block_diag' M :=
+map_neg (block_diag'_add_monoid_hom m' n' α) M
+
+@[simp] lemma block_diag'_sub [add_group α] (M N : matrix (Σ i, m' i) (Σ i, n' i) α) :
+  block_diag' (M - N) = block_diag' M - block_diag' N :=
+map_sub (block_diag'_add_monoid_hom m' n' α) M N
+
+@[simp] lemma block_diag'_smul {R : Type*} [monoid R] [add_monoid α] [distrib_mul_action R α]
+  (x : R) (M : matrix (Σ i, m' i) (Σ i, n' i) α) : block_diag' (x • M) = x • block_diag' M :=
+rfl
+
+end block_diag'
+
 end matrix

src/topology/instances/matrix.lean

@@ -25,6 +25,8 @@ This file is a place to collect topological results about matrices.
 * Infinite sums
   * `matrix.transpose_tsum`: transpose commutes with infinite sums
   * `matrix.diagonal_tsum`: diagonal commutes with infinite sums
+  * `matrix.block_diagonal_tsum`: block diagonal commutes with infinite sums
+  * `matrix.block_diagonal'_tsum`: non-uniform block diagonal commutes with infinite sums
 -/
 
 open matrix
@@ -224,6 +226,11 @@ lemma continuous.matrix_block_diagonal [has_zero R] [decidable_eq p] {A : X →
 continuous_matrix $ λ ⟨i₁, i₂⟩ ⟨j₁, j₂⟩,
   (((continuous_apply i₂).comp hA).matrix_elem i₁ j₁).if_const _ continuous_zero
 
+@[continuity]
+lemma continuous.matrix_block_diag {A : X → matrix (m × p) (n × p) R} (hA : continuous A) :
+  continuous (λ x, block_diag (A x)) :=
+continuous_pi $ λ i, continuous_matrix $ λ j k, hA.matrix_elem _ _
+
 @[continuity]
 lemma continuous.matrix_block_diagonal' [has_zero R] [decidable_eq l]
   {A : X → Π i, matrix (m' i) (n' i) R} (hA : continuous A) :
@@ -236,6 +243,11 @@ continuous_matrix $ λ ⟨i₁, i₂⟩ ⟨j₁, j₂⟩, begin
   { exact continuous_const },
 end
 
+@[continuity]
+lemma continuous.matrix_block_diag' {A : X → matrix (Σ i, m' i) (Σ i, n' i) R} (hA : continuous A) :
+  continuous (λ x, block_diag' (A x)) :=
+continuous_pi $ λ i, continuous_matrix $ λ j k, hA.matrix_elem _ _
+
 end block_matrices
 
 end continuity
@@ -335,17 +347,72 @@ lemma summable.matrix_block_diagonal [decidable_eq p] {f : X → p → matrix m
   summable (λ x, block_diagonal (f x)) :=
 hf.has_sum.matrix_block_diagonal.summable
 
+lemma summable_matrix_block_diagonal [decidable_eq p] {f : X → p → matrix m n R} :
+  summable (λ x, block_diagonal (f x)) ↔ summable f :=
+(summable.map_iff_of_left_inverse
+  (matrix.block_diagonal_add_monoid_hom m n p R) (matrix.block_diag_add_monoid_hom m n p R)
+  (by exact continuous.matrix_block_diagonal continuous_id)
+  (by exact continuous.matrix_block_diag continuous_id)
+  (λ A, block_diag_block_diagonal A) : _)
+
+lemma matrix.block_diagonal_tsum [decidable_eq p] [t2_space R] {f : X → p → matrix m n R} :
+  block_diagonal (∑' x, f x) = ∑' x, block_diagonal (f x) :=
+begin
+  by_cases hf : summable f,
+  { exact hf.has_sum.matrix_block_diagonal.tsum_eq.symm },
+  { have hft := summable_matrix_block_diagonal.not.mpr hf,
+    rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft],
+    exact block_diagonal_zero },
+end
+
+lemma has_sum.matrix_block_diag {f : X → matrix (m × p) (n × p) R}
+  {a : matrix (m × p) (n × p) R} (hf : has_sum f a) :
+  has_sum (λ x, block_diag (f x)) (block_diag a) :=
+(hf.map (block_diag_add_monoid_hom m n p R) $ continuous.matrix_block_diag continuous_id : _)
+
+lemma summable.matrix_block_diag {f : X → matrix (m × p) (n × p) R} (hf : summable f) :
+  summable (λ x, block_diag (f x)) :=
+hf.has_sum.matrix_block_diag.summable
+
 lemma has_sum.matrix_block_diagonal' [decidable_eq l]
   {f : X → Π i, matrix (m' i) (n' i) R} {a : Π i, matrix (m' i) (n' i) R} (hf : has_sum f a) :
   has_sum (λ x, block_diagonal' (f x)) (block_diagonal' a) :=
 (hf.map (block_diagonal'_add_monoid_hom m' n' R) $
   continuous.matrix_block_diagonal' $ by exact continuous_id : _)
 
-lemma summable.matrix_block_diagonal' [decidable_eq l]  {f : X → Π i, matrix (m' i) (n' i) R}
-  (hf : summable f) :
+lemma summable.matrix_block_diagonal' [decidable_eq l]
+  {f : X → Π i, matrix (m' i) (n' i) R} (hf : summable f) :
   summable (λ x, block_diagonal' (f x)) :=
 hf.has_sum.matrix_block_diagonal'.summable
 
+lemma summable_matrix_block_diagonal' [decidable_eq l] {f : X → Π i, matrix (m' i) (n' i) R} :
+  summable (λ x, block_diagonal' (f x)) ↔ summable f :=
+(summable.map_iff_of_left_inverse
+  (matrix.block_diagonal'_add_monoid_hom m' n' R) (matrix.block_diag'_add_monoid_hom m' n' R)
+  (by exact continuous.matrix_block_diagonal' continuous_id)
+  (by exact continuous.matrix_block_diag' continuous_id)
+  (λ A, block_diag'_block_diagonal' A) : _)
+
+lemma matrix.block_diagonal'_tsum [decidable_eq l] [t2_space R]
+  {f : X → Π i, matrix (m' i) (n' i) R} :
+  block_diagonal' (∑' x, f x) = ∑' x, block_diagonal' (f x) :=
+begin
+  by_cases hf : summable f,
+  { exact hf.has_sum.matrix_block_diagonal'.tsum_eq.symm },
+  { have hft := summable_matrix_block_diagonal'.not.mpr hf,
+    rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft],
+    exact block_diagonal'_zero },
+end
+
+lemma has_sum.matrix_block_diag' {f : X → matrix (Σ i, m' i) (Σ i, n' i) R}
+  {a : matrix (Σ i, m' i) (Σ i, n' i) R} (hf : has_sum f a) :
+  has_sum (λ x, block_diag' (f x)) (block_diag' a) :=
+(hf.map (block_diag'_add_monoid_hom m' n' R) $ continuous.matrix_block_diag' continuous_id : _)
+
+lemma summable.matrix_block_diag' {f : X → matrix (Σ i, m' i) (Σ i, n' i) R} (hf : summable f) :
+  summable (λ x, block_diag' (f x)) :=
+hf.has_sum.matrix_block_diag'.summable
+
 end block_matrices
 
 end tsum