Birkhoff

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

Statistics

Metric	Count
Definitions	0
Theorems l2_opNorm_le_one_of_mem_doublyStochastic, doublyStochastic_eq_convexHull_permMatrix, exists_eq_sum_perm_of_mem_doublyStochastic, extremePoints_doublyStochastic	4
Total	4

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
l2_opNorm_le_one_of_mem_doublyStochastic 📖	mathematical	Matrix Real Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass nonAssocSemiring Semiring.toNonAssocSemiring Real.semiring SetLike.instMembership Submonoid.instSetLike doublyStochastic Real.partialOrder Real.instIsOrderedRing	Real.instLE Norm.norm NormedRing.toNorm instL2OpNormedRing Real.instRCLike Real.instOne	—	Real.instIsOrderedRing ConvexOn.exists_ge_of_mem_convexHull Real.instIsStrictOrderedRing Real.instIsOrderedAddMonoid IsStrictOrderedRing.toIsStrictOrderedModule convexOn_univ_norm IsStrictOrderedRing.toIsOrderedRing doublyStochastic_eq_convexHull_permMatrix SetLike.mem_coe LE.le.trans permMatrix_l2_opNorm_le

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
doublyStochastic_eq_convexHull_permMatrix 📖	mathematical	—	SetLike.coe Submonoid Matrix MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Submonoid.instSetLike doublyStochastic SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix.module Semiring.toModule setOf Equiv.Perm Equiv.Perm.permMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	HasSubset.Subset.antisymm' IsStrictOrderedRing.toIsOrderedRing Set.instAntisymmSubset convexHull_min permMatrix_mem_doublyStochastic convex_doublyStochastic exists_eq_sum_perm_of_mem_doublyStochastic mem_convexHull_of_exists_fintype
exists_eq_sum_perm_of_mem_doublyStochastic 📖	mathematical	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SetLike.instMembership Submonoid.instSetLike doublyStochastic SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedRing	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Finset.sum Equiv.Perm NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ Equiv.instFintype AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.addCommMonoid Matrix.smul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id Equiv.Perm.permMatrix	—	IsStrictOrderedRing.toIsOrderedRing isEmpty_or_nonempty IsStrictOrderedRing.toZeroLEOneClass Finset.sum_congr Finset.univ_unique IsEmpty.instSubsingleton Finset.sum_const Finset.card_singleton one_smul Matrix.subsingleton_of_empty_right Matrix.smul_apply sum_row_of_mem_doublyStochastic mul_ite mul_one MulZeroClass.mul_zero Finset.sum_comm Finset.sum_ite_eq
extremePoints_doublyStochastic 📖	mathematical	—	Set.extremePoints Matrix DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Matrix.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix.smul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring Submonoid.instSetLike doublyStochastic IsStrictOrderedRing.toIsOrderedRing setOf Equiv.Perm Equiv.Perm.permMatrix MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	subset_antisymm IsStrictOrderedRing.toIsOrderedRing Set.instAntisymmSubset doublyStochastic_eq_convexHull_permMatrix extremePoints_convexHull_subset LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors instIsDomain GroupWithZero.toNoZeroSMulDivisors permMatrix_mem_doublyStochastic image_openSegment covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid openSegment_eq_Ioo' Set.Ioo_subset_Ioo openSegment_same IsStrictOrderedRing.toZeroLEOneClass IsLocalRing.toNontrivial Field.instIsLocalRing

---

← Back to Index