Stochastic

📁 Source: Mathlib/LinearAlgebra/Matrix/Stochastic.lean

Statistics

Metric	Count
Definitions colStochastic, rowStochastic	2
Theorems convex_colStochastic, convex_rowStochastic, le_one_of_mem_colStochastic, le_one_of_mem_rowStochastic, mem_colStochastic, mem_colStochastic_iff_sum, mem_rowStochastic, mem_rowStochastic_iff_sum, mulVec_dotProduct_one_eq_one_colStochastic, nonneg_mulVec_of_mem_colStochastic, nonneg_mulVec_of_mem_rowStochastic, nonneg_of_mem_colStochastic, nonneg_of_mem_rowStochastic, nonneg_vecMul_of_mem_colStochastic, nonneg_vecMul_of_mem_rowStochastic, one_vecMul_of_mem_colStochastic, one_vecMul_of_mem_rowStochastic, permMatrix_mem_colStochastic, permMatrix_mem_rowStochastic, reindex_mem_colStochastic, reindex_mem_colStochastic_iff, reindex_mem_rowStochastic, reindex_mem_rowStochastic_iff, sum_col_of_mem_colStochastic, sum_mulVec_of_mem_colStochastic, sum_row_of_mem_rowStochastic, transpose_mem_colStochastic_iff_mem_rowStochastic, transpose_mem_rowStochastic_iff_mem_colStochastic, vecMul_dotProduct_one_eq_one_rowStochastic	29
Total	31

Matrix

Definitions

Name	Category	Theorems
colStochastic 📖	CompOp	9 math math: reindex_mem_colStochastic_iff, doublyStochastic_eq_rowStochastic_inf_colStochastic, convex_colStochastic, transpose_mem_rowStochastic_iff_mem_colStochastic, mem_doublyStochastic_iff_mem_rowStochastic_and_mem_colStochastic, mem_colStochastic, mem_colStochastic_iff_sum, permMatrix_mem_colStochastic, transpose_mem_colStochastic_iff_mem_rowStochastic
rowStochastic 📖	CompOp	9 math math: permMatrix_mem_rowStochastic, reindex_mem_rowStochastic_iff, doublyStochastic_eq_rowStochastic_inf_colStochastic, transpose_mem_rowStochastic_iff_mem_colStochastic, mem_rowStochastic_iff_sum, mem_doublyStochastic_iff_mem_rowStochastic_and_mem_colStochastic, convex_rowStochastic, mem_rowStochastic, transpose_mem_colStochastic_iff_mem_rowStochastic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convex_colStochastic 📖	mathematical	—	Convex Matrix addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Submonoid.instSetLike colStochastic	—	IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toPosMulMono Finset.sum_congr Finset.sum_add_distrib mul_one
convex_rowStochastic 📖	mathematical	—	Convex Matrix addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Submonoid.instSetLike rowStochastic	—	IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toPosMulMono Finset.sum_congr Finset.sum_add_distrib mul_one
le_one_of_mem_colStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike colStochastic	Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	sum_col_of_mem_colStochastic Finset.single_le_sum IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid Finset.mem_univ
le_one_of_mem_rowStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike rowStochastic	Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	sum_row_of_mem_rowStochastic Finset.single_le_sum IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid Finset.mem_univ
mem_colStochastic 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike colStochastic Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring vecMul Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
mem_colStochastic_iff_sum 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike colStochastic Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Finset.sum_congr one_mul
mem_rowStochastic 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike rowStochastic Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring mulVec Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
mem_rowStochastic_iff_sum 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike rowStochastic Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Finset.sum_congr mul_one
mulVec_dotProduct_one_eq_one_colStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike colStochastic dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	mulVec	—	dotProduct_mulVec
nonneg_mulVec_of_mem_colStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike colStochastic Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	mulVec	—	Finset.sum_congr Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid Left.mul_nonneg IsOrderedRing.toPosMulMono nonneg_of_mem_colStochastic
nonneg_mulVec_of_mem_rowStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike rowStochastic Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	mulVec	—	Finset.sum_congr Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid Left.mul_nonneg IsOrderedRing.toPosMulMono nonneg_of_mem_rowStochastic
nonneg_of_mem_colStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike colStochastic	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	—
nonneg_of_mem_rowStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike rowStochastic	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	—
nonneg_vecMul_of_mem_colStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike colStochastic Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	vecMul	—	Finset.sum_congr Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid Left.mul_nonneg IsOrderedRing.toPosMulMono nonneg_of_mem_colStochastic
nonneg_vecMul_of_mem_rowStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike rowStochastic Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	vecMul	—	Finset.sum_congr Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono nonneg_of_mem_rowStochastic
one_vecMul_of_mem_colStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike colStochastic	vecMul NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mem_colStochastic
one_vecMul_of_mem_rowStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike rowStochastic	mulVec NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mem_rowStochastic
permMatrix_mem_colStochastic 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike colStochastic Equiv.Perm.permMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mem_colStochastic_iff_sum IsOrderedRing.toZeroLEOneClass Finset.sum_congr Finset.sum_ite_eq'
permMatrix_mem_rowStochastic 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike rowStochastic Equiv.Perm.permMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mem_rowStochastic_iff_sum IsOrderedRing.toZeroLEOneClass Finset.sum_congr Finset.sum_ite_eq
reindex_mem_colStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike colStochastic	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reindex	—	reindex_mem_colStochastic_iff
reindex_mem_colStochastic_iff 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike colStochastic DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reindex	—	transpose_transpose transpose_reindex transpose_mem_colStochastic_iff_mem_rowStochastic reindex_mem_rowStochastic_iff
reindex_mem_rowStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike rowStochastic	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reindex	—	nonneg_of_mem_rowStochastic submatrix_mulVec_equiv
reindex_mem_rowStochastic_iff 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike rowStochastic DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike reindex	—	submatrix_submatrix Equiv.symm_comp_self submatrix_id_id reindex_mem_rowStochastic
sum_col_of_mem_colStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike colStochastic	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.univ AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mem_colStochastic_iff_sum
sum_mulVec_of_mem_colStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike colStochastic	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.univ mulVec	—	Finset.sum_congr Finset.sum_comm sum_col_of_mem_colStochastic one_mul
sum_row_of_mem_rowStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike rowStochastic	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.univ AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mem_rowStochastic_iff_sum
transpose_mem_colStochastic_iff_mem_rowStochastic 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike colStochastic transpose rowStochastic	—	Finset.sum_congr forall_swap
transpose_mem_rowStochastic_iff_mem_colStochastic 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike rowStochastic transpose colStochastic	—	Finset.sum_congr forall_swap
vecMul_dotProduct_one_eq_one_rowStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike rowStochastic dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	vecMul	—	dotProduct_mulVec

---

← Back to Index