feat: add lemmas about doubly stochastic matrices (#33394)

This PR adds a few basic lemmas about doubly stochastic matrices.

Author: dupuisf

Mathlib/Analysis/Convex/DoublyStochasticMatrix.lean

@@ -5,8 +5,6 @@ Authors: Bhavik Mehta
 -/
 module
 
-public import Mathlib.Analysis.Convex.Basic
-public import Mathlib.LinearAlgebra.Matrix.Permutation
 public import Mathlib.LinearAlgebra.Matrix.Stochastic
 
 /-!
@@ -23,11 +21,6 @@ public import Mathlib.LinearAlgebra.Matrix.Stochastic
 * `convex_doublyStochastic`: The set of doubly stochastic matrices is convex.
 * `permMatrix_mem_doublyStochastic`: Any permutation matrix is doubly stochastic.
 
-## TODO
-
-Define the submonoids of row-stochastic and column-stochastic matrices.
-Show that the submonoid of doubly stochastic matrices is the meet of them, or redefine it as such.
-
 ## Tags
 
 Doubly stochastic, Birkhoff's theorem, Birkhoff-von Neumann theorem
@@ -67,7 +60,7 @@ lemma mem_doublyStochastic_iff_sum :
 
 /-- A matrix is doubly stochastic if and only if it is both row and
 column stochastic. -/
-@[grind =]
+@[local grind =]
 lemma doublyStochastic_eq_rowStochastic_inf_colStochastic :
     doublyStochastic R n = rowStochastic R n ⊓ colStochastic R n := by
   ext M
@@ -112,17 +105,32 @@ lemma convex_doublyStochastic : Convex R (doublyStochastic R n : Set (Matrix n n
   simp [add_nonneg, ha, hb, mul_nonneg, hx, hy, sum_add_distrib, ← mul_sum, h]
 
 /-- Any permutation matrix is doubly stochastic. -/
+@[simp, grind ←]
 lemma permMatrix_mem_doublyStochastic {σ : Equiv.Perm n} :
-    σ.permMatrix R ∈ doublyStochastic R n := by
-  grind only [= doublyStochastic_eq_rowStochastic_inf_colStochastic, = Submonoid.mem_inf,
-    ← permMatrix_mem_rowStochastic, ← permMatrix_mem_colStochastic]
+    σ.permMatrix R ∈ doublyStochastic R n := by grind
 
 /-- A matrix is doubly stochastic iff its transpose is doubly stochastic -/
+@[grind =]
 lemma transpose_mem_doublyStochastic_iff :
-    M.transpose ∈ doublyStochastic R n ↔ M ∈ doublyStochastic R n := by
-  grind only [= doublyStochastic_eq_rowStochastic_inf_colStochastic, = Submonoid.mem_inf,
-    = transpose_mem_rowStochastic_iff_mem_colStochastic, = mem_rowStochastic,
-    = transpose_mem_colStochastic_iff_mem_rowStochastic, = mem_colStochastic]
+    Mᵀ ∈ doublyStochastic R n ↔ M ∈ doublyStochastic R n := by grind
+
+/-- Reindexing a matrix preserves double stochasticity. -/
+@[aesop safe apply]
+lemma reindex_mem_doublyStochastic {m : Type*} [Fintype m] [DecidableEq m] {M : Matrix n n R}
+    {e₁ e₂ : n ≃ m} (hM : M ∈ doublyStochastic R n) : M.reindex e₁ e₂ ∈ doublyStochastic R m := by
+  grind
+
+/-- Reindexing a matrix preserves double stochasticity. -/
+@[grind =]
+lemma reindex_mem_doublyStochastic_iff {m : Type*} [Fintype m] [DecidableEq m] {M : Matrix n n R}
+    {e₁ e₂ : n ≃ m} : M.reindex e₁ e₂ ∈ doublyStochastic R m ↔ M ∈ doublyStochastic R n := by
+  grind
+
+/-- Applying a doubly stochastic matrix to a vector preserves its sum. -/
+lemma sum_mulVec_of_mem_doublyStochastic {M : Matrix n n R} {x : n → R}
+    (hA : M ∈ doublyStochastic R n) : ∑ i, (M *ᵥ x) i = ∑ i, x i := by
+  apply sum_mulVec_of_mem_colStochastic
+  grind
 
 end OrderedSemiring
 

Mathlib/LinearAlgebra/Matrix/Stochastic.lean

@@ -52,7 +52,6 @@ def rowStochastic (R n : Type*) [Fintype n] [DecidableEq n] [Semiring R] [Partia
   one_mem' := by
     simp [zero_le_one_elem]
 
-@[grind =]
 lemma mem_rowStochastic :
     M ∈ rowStochastic R n ↔ (∀ i j, 0 ≤ M i j) ∧  M *ᵥ 1 = 1 :=
   Iff.rfl
@@ -139,7 +138,6 @@ def colStochastic (R n : Type*) [Fintype n] [DecidableEq n] [Semiring R] [Partia
   one_mem' := by
     simp [zero_le_one_elem]
 
-@[grind =]
 lemma mem_colStochastic :
     M ∈ colStochastic R n ↔ (∀ i j, 0 ≤ M i j) ∧ 1 ᵥ* M = 1 :=
   Iff.rfl
@@ -195,6 +193,13 @@ lemma mulVec_dotProduct_one_eq_one_colStochastic (hM : M ∈ colStochastic R n)
     (hx : 1 ⬝ᵥ x = 1) : 1 ⬝ᵥ (M *ᵥ x) = 1 := by
   rw [dotProduct_mulVec, hM.2, hx]
 
+/-- Applying a column-stochastic matrix to a vector preserves its sum. -/
+lemma sum_mulVec_of_mem_colStochastic {M : Matrix n n R} {x : n → R}
+    (hA : M ∈ colStochastic R n) : ∑ i, (M *ᵥ x) i = ∑ i, x i := by
+  simp only [Matrix.mulVec, dotProduct]
+  rw [Finset.sum_comm]
+  simp [sum_col_of_mem_colStochastic hA, ← Finset.sum_mul]
+
 /-- The set of column stochastic matrices is convex. -/
 lemma convex_colStochastic : Convex R (colStochastic R n : Set (Matrix n n R)) := by
   intro x hx y hy a b ha hb h
@@ -226,4 +231,31 @@ lemma transpose_mem_colStochastic_iff_mem_rowStochastic :
     and_congr_left_iff]
   exact fun _ ↦ forall_swap
 
+/-- Reindexing a matrix preserves row-stochasticity. -/
+@[aesop safe apply]
+lemma reindex_mem_rowStochastic {m : Type*} [Fintype m] [DecidableEq m] {M : Matrix n n R}
+    {e₁ e₂ : n ≃ m} (hM : M ∈ rowStochastic R n) : M.reindex e₁ e₂ ∈ rowStochastic R m :=
+  ⟨fun _ _ ↦ by simpa using nonneg_of_mem_rowStochastic hM, by simp [submatrix_mulVec_equiv, hM.2]⟩
+
+/-- Reindexing a matrix preserves row-stochasticity. -/
+@[grind =]
+lemma reindex_mem_rowStochastic_iff {m : Type*} [Fintype m] [DecidableEq m] {M : Matrix n n R}
+    {e₁ e₂ : n ≃ m} : M.reindex e₁ e₂ ∈ rowStochastic R m ↔ M ∈ rowStochastic R n := by
+  refine ⟨fun h => ?_, reindex_mem_rowStochastic⟩
+  have : M = (M.reindex e₁ e₂).reindex e₁.symm e₂.symm := by simp
+  rw [this]
+  exact reindex_mem_rowStochastic h
+
+/-- Reindexing a matrix preserves column-stochasticity. -/
+@[grind =]
+lemma reindex_mem_colStochastic_iff {m : Type*} [Fintype m] [DecidableEq m] {M : Matrix n n R}
+    {e₁ e₂ : n ≃ m} : M.reindex e₁ e₂ ∈ colStochastic R m ↔ M ∈ colStochastic R n := by
+  rw [← transpose_transpose (reindex e₁ e₂ M), transpose_reindex,
+    transpose_mem_colStochastic_iff_mem_rowStochastic, reindex_mem_rowStochastic_iff,
+    ← transpose_mem_colStochastic_iff_mem_rowStochastic, transpose_transpose]
+
+/-- Reindexing a matrix preserves column-stochasticity. -/
+@[aesop safe apply]
+alias ⟨_, reindex_mem_colStochastic⟩ := reindex_mem_colStochastic_iff
+
 end Matrix