DoublyStochasticMatrix

📁 Source: Mathlib/Analysis/Convex/DoublyStochasticMatrix.lean

Statistics

Metric	Count
Definitions doublyStochastic	1
Theorems convex_doublyStochastic, doublyStochastic_eq_rowStochastic_inf_colStochastic, exists_mem_doublyStochastic_eq_smul_iff, le_one_of_mem_doublyStochastic, mem_doublyStochastic, mem_doublyStochastic_iff_mem_rowStochastic_and_mem_colStochastic, mem_doublyStochastic_iff_sum, mulVec_one_of_mem_doublyStochastic, nonneg_of_mem_doublyStochastic, one_vecMul_of_mem_doublyStochastic, permMatrix_mem_doublyStochastic, reindex_mem_doublyStochastic, reindex_mem_doublyStochastic_iff, sum_col_of_mem_doublyStochastic, sum_mulVec_of_mem_doublyStochastic, sum_row_of_mem_doublyStochastic, transpose_mem_doublyStochastic_iff	17
Total	18

(root)

Definitions

Name	Category	Theorems
doublyStochastic 📖	CompOp	12 math math: reindex_mem_doublyStochastic, reindex_mem_doublyStochastic_iff, mem_doublyStochastic_iff_sum, doublyStochastic_eq_rowStochastic_inf_colStochastic, mem_doublyStochastic_iff_mem_rowStochastic_and_mem_colStochastic, doublyStochastic_eq_convexHull_permMatrix, extremePoints_doublyStochastic, mem_doublyStochastic, convex_doublyStochastic, transpose_mem_doublyStochastic_iff, permMatrix_mem_doublyStochastic, exists_mem_doublyStochastic_eq_smul_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convex_doublyStochastic 📖	mathematical	—	Convex Matrix Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Matrix.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 Matrix.nonAssocSemiring Submonoid.instSetLike doublyStochastic	—	IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toPosMulMono Finset.sum_congr Finset.sum_add_distrib mul_one
doublyStochastic_eq_rowStochastic_inf_colStochastic 📖	mathematical	—	doublyStochastic Submonoid Matrix MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring Submonoid.instMin Matrix.rowStochastic Matrix.colStochastic	—	Submonoid.ext
exists_mem_doublyStochastic_eq_smul_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing Matrix.smul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ	—	IsStrictOrderedRing.toIsOrderedRing Finset.sum_congr mul_nonneg IsOrderedRing.toPosMulMono mem_doublyStochastic_iff_sum mul_one eq_or_lt_of_le zero_smul Submonoid.one_mem Matrix.ext Finset.sum_eq_zero_iff_of_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toPosMulStrictMono PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE inv_mul_cancel₀ LT.lt.ne' smul_inv_smul₀
le_one_of_mem_doublyStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic	Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	sum_row_of_mem_doublyStochastic Finset.single_le_sum IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid Finset.mem_univ
mem_doublyStochastic 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Matrix.mulVec Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Matrix.vecMul	—	—
mem_doublyStochastic_iff_mem_rowStochastic_and_mem_colStochastic 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic Matrix.rowStochastic Matrix.colStochastic	—	doublyStochastic_eq_rowStochastic_inf_colStochastic Submonoid.mem_inf
mem_doublyStochastic_iff_sum 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic 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 one_mul
mulVec_one_of_mem_doublyStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic	Matrix.mulVec NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mem_doublyStochastic
nonneg_of_mem_doublyStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	—
one_vecMul_of_mem_doublyStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic	Matrix.vecMul NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mem_doublyStochastic
permMatrix_mem_doublyStochastic 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic Equiv.Perm.permMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
reindex_mem_doublyStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.reindex	—	—
reindex_mem_doublyStochastic_iff 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.reindex	—	—
sum_col_of_mem_doublyStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.univ AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mem_doublyStochastic_iff_sum
sum_mulVec_of_mem_doublyStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.univ Matrix.mulVec	—	Matrix.sum_mulVec_of_mem_colStochastic
sum_row_of_mem_doublyStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.univ AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	mem_doublyStochastic_iff_sum
transpose_mem_doublyStochastic_iff 📖	mathematical	—	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike doublyStochastic Matrix.transpose	—	—

---

← Back to Index