Documentation Verification Report

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	11 math math: `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` `SetLike.instMembership` `Submonoid.instSetLike` `doublyStochastic` `IsStrictOrderedRing.toIsOrderedRing` `Matrix.smul` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `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`	—	`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` `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`	—	—
`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` `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`	`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` `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` `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` `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