OAI/Analysis/MarkovType/TriangularTransport.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MarkovSuperreflexivity.TriangularSystem.scaleParameterline 22 - def
OAI.MarkovSuperreflexivity.TriangularSystem.mapEquivOfBoundsline 45 - def
OAI.MarkovSuperreflexivity.TriangularSystem.toDualline 83 - def
OAI.MarkovSuperreflexivity.TriangularSystem.ofDualline 94 - theorem
OAI.MarkovSuperreflexivity.finiteTriangularObstruction_of_equiv_boundsline 129 - theorem
OAI.MarkovSuperreflexivity.finiteTriangularObstruction_of_equivline 145 - theorem
OAI.MarkovSuperreflexivity.finiteTriangularObstruction_equiv_iffline 175 - theorem
OAI.MarkovSuperreflexivity.finiteTriangularObstruction_dual_iffline 180