Skip to content

Commit 18f94b2

Browse files
sjh227Steven Herbertdupuisf
committed
feat(LinearAlgebra): define row- and column-stochastic matrices (leanprover-community#28708)
This PR defines row- and column-stochastic matrices, and relates them to doubly stochastic matrices (which are already in mathlib). Co-authored-by: Steven Herbert <stevenherbert@Stevens-MacBook-Pro.local> Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca>
1 parent 54aa5b5 commit 18f94b2

4 files changed

Lines changed: 255 additions & 6 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4755,6 +4755,7 @@ public import Mathlib.LinearAlgebra.Matrix.SemiringInverse
47554755
public import Mathlib.LinearAlgebra.Matrix.SesquilinearForm
47564756
public import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
47574757
public import Mathlib.LinearAlgebra.Matrix.StdBasis
4758+
public import Mathlib.LinearAlgebra.Matrix.Stochastic
47584759
public import Mathlib.LinearAlgebra.Matrix.Swap
47594760
public import Mathlib.LinearAlgebra.Matrix.Symmetric
47604761
public import Mathlib.LinearAlgebra.Matrix.ToLin

‎Mathlib/Algebra/Group/Submonoid/Defs.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -271,7 +271,7 @@ instance : Min (Submonoid M) :=
271271
theorem coe_inf (p p' : Submonoid M) : ((p ⊓ p' : Submonoid M) : Set M) = (p : Set M) ∩ p' :=
272272
rfl
273273

274-
@[to_additive (attr := simp)]
274+
@[to_additive (attr := simp, grind =)]
275275
theorem mem_inf {p p' : Submonoid M} {x : M} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p' :=
276276
Iff.rfl
277277

‎Mathlib/Analysis/Convex/DoublyStochasticMatrix.lean‎

Lines changed: 24 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ module
77

88
public import Mathlib.Analysis.Convex.Basic
99
public import Mathlib.LinearAlgebra.Matrix.Permutation
10+
public import Mathlib.LinearAlgebra.Matrix.Stochastic
1011

1112
/-!
1213
# Doubly stochastic matrices
@@ -64,6 +65,20 @@ lemma mem_doublyStochastic_iff_sum :
6465
(∀ i j, 0 ≤ M i j) ∧ (∀ i, ∑ j, M i j = 1) ∧ ∀ j, ∑ i, M i j = 1 := by
6566
simp [funext_iff, doublyStochastic, mulVec, vecMul, dotProduct]
6667

68+
/-- A matrix is doubly stochastic if and only if it is both row and
69+
column stochastic. -/
70+
@[grind =]
71+
lemma doublyStochastic_eq_rowStochastic_inf_colStochastic :
72+
doublyStochastic R n = rowStochastic R n ⊓ colStochastic R n := by
73+
ext M
74+
simp only [rowStochastic, colStochastic, Submonoid.mem_inf, Submonoid.mem_mk, Subsemigroup.mem_mk,
75+
Set.mem_setOf_eq, doublyStochastic]
76+
grind
77+
78+
lemma mem_doublyStochastic_iff_mem_rowStochastic_and_mem_colStochastic {M : Matrix n n R} :
79+
M ∈ doublyStochastic R n ↔ M ∈ rowStochastic R n ∧ M ∈ colStochastic R n := by
80+
rw [doublyStochastic_eq_rowStochastic_inf_colStochastic, Submonoid.mem_inf]
81+
6782
/-- Every entry of a doubly stochastic matrix is nonnegative. -/
6883
lemma nonneg_of_mem_doublyStochastic (hM : M ∈ doublyStochastic R n) {i j : n} : 0 ≤ M i j :=
6984
hM.1 _ _
@@ -99,11 +114,15 @@ lemma convex_doublyStochastic : Convex R (doublyStochastic R n : Set (Matrix n n
99114
/-- Any permutation matrix is doubly stochastic. -/
100115
lemma permMatrix_mem_doublyStochastic {σ : Equiv.Perm n} :
101116
σ.permMatrix R ∈ doublyStochastic R n := by
102-
rw [mem_doublyStochastic_iff_sum]
103-
refine ⟨fun i j => ?g1, ?g2, ?g3⟩
104-
case g1 => aesop
105-
case g2 => simp [Equiv.toPEquiv_apply]
106-
case g3 => simp [Equiv.toPEquiv_apply, ← Equiv.eq_symm_apply]
117+
grind only [= doublyStochastic_eq_rowStochastic_inf_colStochastic, = Submonoid.mem_inf,
118+
← permMatrix_mem_rowStochastic, ← permMatrix_mem_colStochastic]
119+
120+
/-- A matrix is doubly stochastic iff its transpose is doubly stochastic -/
121+
lemma transpose_mem_doublyStochastif_iff :
122+
M.transpose ∈ doublyStochastic R n ↔ M ∈ doublyStochastic R n := by
123+
grind only [= doublyStochastic_eq_rowStochastic_inf_colStochastic, = Submonoid.mem_inf,
124+
= transpose_mem_rowStochastic_iff_mem_colStochastic, = mem_rowStochastic,
125+
= transpose_mem_colStochastic_iff_mem_rowStochastic, = mem_colStochastic]
107126

108127
end OrderedSemiring
109128

‎Mathlib/LinearAlgebra/Matrix/Stochastic.lean‎

Lines changed: 229 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,229 @@
1+
/-
2+
Copyright (c) 2025 Steven Herbert. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Steven Herbert
5+
-/
6+
module
7+
8+
public import Mathlib.Data.Matrix.Basic
9+
public import Mathlib.Data.Matrix.Mul
10+
public import Mathlib.Analysis.Convex.Basic
11+
public import Mathlib.LinearAlgebra.Matrix.Permutation
12+
13+
/-!
14+
# Row- and Column-stochastic matrices
15+
16+
A square matrix `M` is *row-stochastic* if all its entries are non-negative and `M *ᵥ 1 = 1`.
17+
Likewise, `M` is *column-stochastic* if all its entries are non-negative and `1 ᵥ* M = 1`. This
18+
file defines these concepts and provides basic API for them.
19+
20+
Note that *doubly stochastic* matrices (i.e. matrices that are both row- and column-stochastic)
21+
are defined in `Analysis.Convex.DoublyStochasticMatrix`.
22+
23+
## Main definitions
24+
25+
* `rowStochastic`: row-stochastic matrices indexed by `n` with entries in `R`, as a submonoid
26+
of `Matrix n n R`.
27+
* `colStochastic R n`: column-stochastic matrices indexed by `n` with entries in `R`, as a
28+
submonoid of `Matrix n n R`.
29+
30+
-/
31+
32+
@[expose] public section
33+
34+
open Finset
35+
36+
namespace Matrix
37+
38+
variable {R n : Type*} [Fintype n] [DecidableEq n]
39+
variable [Semiring R] [PartialOrder R] [IsOrderedRing R] {M : Matrix n n R}
40+
variable {x : n → R}
41+
42+
/- ## Row-stochastic matrices -/
43+
44+
/-- A square matrix is row stochastic iff all entries are nonnegative, and right
45+
multiplication by the vector of all 1s gives the vector of all 1s. -/
46+
def rowStochastic (R n : Type*) [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R]
47+
[IsOrderedRing R] : Submonoid (Matrix n n R) where
48+
carrier := {M | (∀ i j, 0 ≤ M i j) ∧ M *ᵥ 1 = 1 }
49+
mul_mem' {M N} hM hN := by
50+
refine ⟨fun i j => sum_nonneg fun i _ => mul_nonneg (hM.1 _ _) (hN.1 _ _), ?_⟩
51+
next => rw [← mulVec_mulVec, hN.2, hM.2]
52+
one_mem' := by
53+
simp [zero_le_one_elem]
54+
55+
@[grind =]
56+
lemma mem_rowStochastic :
57+
M ∈ rowStochastic R n ↔ (∀ i j, 0 ≤ M i j) ∧ M *ᵥ 1 = 1 :=
58+
Iff.rfl
59+
60+
/-- A square matrix is row stochastic if each element is non-negative and row sums to one. -/
61+
lemma mem_rowStochastic_iff_sum :
62+
M ∈ rowStochastic R n ↔ (∀ i j, 0 ≤ M i j) ∧ (∀ i, ∑ j, M i j = 1) := by
63+
simp [funext_iff, rowStochastic, mulVec, dotProduct]
64+
65+
/-- Every entry of a row stochastic matrix is nonnegative. -/
66+
lemma nonneg_of_mem_rowStochastic (hM : M ∈ rowStochastic R n) {i j : n} : 0 ≤ M i j :=
67+
hM.1 _ _
68+
69+
/-- Each row sum of a row stochastic matrix is 1. -/
70+
lemma sum_row_of_mem_rowStochastic (hM : M ∈ rowStochastic R n) (i : n) : ∑ j, M i j = 1 :=
71+
(mem_rowStochastic_iff_sum.1 hM).2 _
72+
73+
/-- The all-ones column vector multiplied with a row stochastic matrix is 1. -/
74+
lemma one_vecMul_of_mem_rowStochastic (hM : M ∈ rowStochastic R n) : M *ᵥ 1 = 1 :=
75+
(mem_rowStochastic.1 hM).2
76+
77+
/-- Every entry of a row stochastic matrix is less than or equal to 1. -/
78+
lemma le_one_of_mem_rowStochastic (hM : M ∈ rowStochastic R n) {i j : n} :
79+
M i j ≤ 1 := by
80+
rw [← sum_row_of_mem_rowStochastic hM i]
81+
exact single_le_sum (fun k _ => hM.1 _ k) (mem_univ j)
82+
83+
/-- Left multiplication of a row stochastic matrix by a non-negative vector
84+
gives a non-negative vector -/
85+
lemma nonneg_vecMul_of_mem_rowStochastic (hM : M ∈ rowStochastic R n)
86+
(hx : ∀ i : n, 0 ≤ x i) : ∀ j : n, 0 ≤ (x ᵥ* M) j := by
87+
intro j
88+
simp only [Matrix.vecMul, dotProduct]
89+
apply Finset.sum_nonneg
90+
intro k _
91+
apply mul_nonneg (hx k)
92+
exact nonneg_of_mem_rowStochastic hM
93+
94+
/-- Right multiplication of a row stochastic matrix by a non-negative vector
95+
gives a non-negative vector -/
96+
lemma nonneg_mulVec_of_mem_rowStochastic (hM : M ∈ rowStochastic R n)
97+
(hx : ∀ i : n, 0 ≤ x i) : ∀ j : n, 0 ≤ (M *ᵥ x) j := by
98+
intro j
99+
simp only [Matrix.mulVec, dotProduct]
100+
apply Finset.sum_nonneg
101+
intro k _
102+
refine Left.mul_nonneg ?_ (hx k)
103+
exact nonneg_of_mem_rowStochastic hM
104+
105+
/-- Left left-multiplication by row stochastic preserves `ℓ₁ norm` -/
106+
lemma vecMul_dotProduct_one_eq_one_rowStochastic (hM : M ∈ rowStochastic R n)
107+
(hx : x ⬝ᵥ 1 = 1) : (x ᵥ* M) ⬝ᵥ 1 = 1 := by
108+
rw [← dotProduct_mulVec, hM.2, hx]
109+
110+
/-- The set of row stochastic matrices is convex. -/
111+
lemma convex_rowStochastic : Convex R (rowStochastic R n : Set (Matrix n n R)) := by
112+
intro x hx y hy a b ha hb h
113+
simp only [SetLike.mem_coe, mem_rowStochastic_iff_sum] at hx hy ⊢
114+
simp [add_nonneg, ha, hb, mul_nonneg, hx, hy, sum_add_distrib, ← mul_sum, h]
115+
116+
/-- Any permutation matrix is row stochastic. -/
117+
@[simp, grind ←]
118+
lemma permMatrix_mem_rowStochastic {σ : Equiv.Perm n} :
119+
σ.permMatrix R ∈ rowStochastic R n := by
120+
rw [mem_rowStochastic_iff_sum]
121+
refine ⟨fun i j => ?g1, ?g2⟩
122+
case g1 => aesop
123+
case g2 => simp [Equiv.toPEquiv_apply]
124+
125+
126+
/- ## Column-stochastic matrices -/
127+
128+
/-- A square matrix is column stochastic iff all entries are nonnegative, and left
129+
multiplication by the vector of all 1s gives the vector of all 1s. -/
130+
def colStochastic (R n : Type*) [Fintype n] [DecidableEq n] [Semiring R] [PartialOrder R]
131+
[IsOrderedRing R] : Submonoid (Matrix n n R) where
132+
carrier := {M | (∀ i j, 0 ≤ M i j) ∧ 1 ᵥ* M = 1 }
133+
mul_mem' {M N} hM hN := by
134+
refine Set.mem_sep ?_ ?_
135+
· intro i j
136+
apply Finset.sum_nonneg
137+
grind [mul_nonneg]
138+
· rw [← vecMul_vecMul, hM.2, hN.2]
139+
one_mem' := by
140+
simp [zero_le_one_elem]
141+
142+
@[grind =]
143+
lemma mem_colStochastic :
144+
M ∈ colStochastic R n ↔ (∀ i j, 0 ≤ M i j) ∧ 1 ᵥ* M = 1 :=
145+
Iff.rfl
146+
147+
/-- A matrix is column stochastic if each column sums to one. -/
148+
lemma mem_colStochastic_iff_sum :
149+
M ∈ colStochastic R n ↔
150+
(∀ i j, 0 ≤ M i j) ∧ (∀ j, ∑ i, M i j = 1) := by
151+
simp [funext_iff, colStochastic, vecMul, dotProduct]
152+
153+
/-- Every entry of a column stochastic matrix is nonnegative. -/
154+
lemma nonneg_of_mem_colStochastic (hM : M ∈ colStochastic R n) {i j : n} : 0 ≤ M i j :=
155+
hM.1 _ _
156+
157+
/-- Each column sum of a column stochastic matrix is 1. -/
158+
lemma sum_col_of_mem_colStochastic (hM : M ∈ colStochastic R n) (i : n) : ∑ j, M j i = 1 :=
159+
(mem_colStochastic_iff_sum.1 hM).2 _
160+
161+
/-- The all-ones column vector multiplied with a column stochastic matrix is 1. -/
162+
lemma one_vecMul_of_mem_colStochastic (hM : M ∈ colStochastic R n) : 1 ᵥ* M = 1 :=
163+
(mem_colStochastic.1 hM).2
164+
165+
/-- Every entry of a column stochastic matrix is less than or equal to 1. -/
166+
lemma le_one_of_mem_colStochastic (hM : M ∈ colStochastic R n) {i j : n} :
167+
M j i ≤ 1 := by
168+
rw [← sum_col_of_mem_colStochastic hM i]
169+
exact single_le_sum (fun k _ => hM.1 k _) (mem_univ j)
170+
171+
/-- Right multiplication of a column stochastic matrix by a non-negative vector
172+
gives a non-negative vector. -/
173+
lemma nonneg_mulVec_of_mem_colStochastic (hM : M ∈ colStochastic R n)
174+
(hx : ∀ i : n, 0 ≤ x i) : ∀ j : n, 0 ≤ (M *ᵥ x) j := by
175+
intro j
176+
simp only [Matrix.mulVec, dotProduct]
177+
apply Finset.sum_nonneg
178+
intro k _
179+
refine Left.mul_nonneg ?_ (hx k)
180+
exact nonneg_of_mem_colStochastic hM
181+
182+
/-- Left multiplication of a column stochastic matrix by a non-negative vector
183+
gives a non-negative vector. -/
184+
lemma nonneg_vecMul_of_mem_colStochastic (hM : M ∈ colStochastic R n)
185+
(hx : ∀ i : n, 0 ≤ x i) : ∀ j : n, 0 ≤ (x ᵥ* M) j := by
186+
intro j
187+
simp only [Matrix.vecMul, dotProduct]
188+
apply Finset.sum_nonneg
189+
intro k _
190+
refine Left.mul_nonneg (hx k) ?_
191+
exact nonneg_of_mem_colStochastic hM
192+
193+
/-- Left left-multiplication by column stochastic preserves `ℓ₁ norm` -/
194+
lemma mulVec_dotProduct_one_eq_one_colStochastic (hM : M ∈ colStochastic R n)
195+
(hx : 1 ⬝ᵥ x = 1) : 1 ⬝ᵥ (M *ᵥ x) = 1 := by
196+
rw [dotProduct_mulVec, hM.2, hx]
197+
198+
/-- The set of column stochastic matrices is convex. -/
199+
lemma convex_colStochastic : Convex R (colStochastic R n : Set (Matrix n n R)) := by
200+
intro x hx y hy a b ha hb h
201+
simp only [SetLike.mem_coe, mem_colStochastic_iff_sum] at hx hy ⊢
202+
simp [add_nonneg, ha, hb, mul_nonneg, hx, hy, sum_add_distrib, ← mul_sum, h]
203+
204+
/-- Any permutation matrix is column stochastic. -/
205+
@[simp, grind ←]
206+
lemma permMatrix_mem_colStochastic {σ : Equiv.Perm n} :
207+
σ.permMatrix R ∈ colStochastic R n := by
208+
rw [mem_colStochastic_iff_sum]
209+
refine ⟨fun i j => ?g1, ?g2⟩
210+
case g1 => aesop
211+
case g2 => simp [Equiv.toPEquiv_apply, ← Equiv.eq_symm_apply]
212+
213+
/-- The transpose of a matrix is row stochastic matrix if it is column stochastic. -/
214+
@[grind =]
215+
lemma transpose_mem_rowStochastic_iff_mem_colStochastic :
216+
Mᵀ ∈ rowStochastic R n ↔ M ∈ colStochastic R n := by
217+
simp only [mem_colStochastic_iff_sum, mem_rowStochastic_iff_sum, transpose_apply,
218+
and_congr_left_iff]
219+
exact fun _ ↦ forall_swap
220+
221+
/-- The transpose of a matrix is column stochastic matrix if it is row stochastic. -/
222+
@[grind =]
223+
lemma transpose_mem_colStochastic_iff_mem_rowStochastic :
224+
Mᵀ ∈ colStochastic R n ↔ M ∈ rowStochastic R n := by
225+
simp only [mem_colStochastic_iff_sum, mem_rowStochastic_iff_sum, transpose_apply,
226+
and_congr_left_iff]
227+
exact fun _ ↦ forall_swap
228+
229+
end Matrix

0 commit comments

Comments
 (0)