OAI/Analysis/MarkovType/LatticeLift.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MarkovSuperreflexivity.LiftCube line 16
  2. def OAI.MarkovSuperreflexivity.liftAccept line 19
  3. def OAI.MarkovSuperreflexivity.liftMove line 24
  4. theorem OAI.MarkovSuperreflexivity.latticeCubeVal_liftMove line 28
  5. theorem OAI.MarkovSuperreflexivity.liftAccept_reverse line 33
  6. theorem OAI.MarkovSuperreflexivity.liftMove_reverse line 41
  7. def OAI.MarkovSuperreflexivity.liftSource line 48
  8. def OAI.MarkovSuperreflexivity.liftTarget line 51
  9. def OAI.MarkovSuperreflexivity.liftReverse line 57
  10. theorem OAI.MarkovSuperreflexivity.liftReverse_involutive line 63
  11. theorem OAI.MarkovSuperreflexivity.liftSource_reverse line 76
  12. theorem OAI.MarkovSuperreflexivity.liftTarget_reverse line 85
  13. def OAI.MarkovSuperreflexivity.liftMass line 90
  14. theorem OAI.MarkovSuperreflexivity.liftMass_nonneg line 94
  15. theorem OAI.MarkovSuperreflexivity.sum_liftMass line 98
  16. theorem OAI.MarkovSuperreflexivity.sum_liftOutgoing line 110
  17. theorem OAI.MarkovSuperreflexivity.lift_edge_balance line 121
  18. def OAI.MarkovSuperreflexivity.latticeLift line 139
  19. def OAI.MarkovSuperreflexivity.latticeTransition line 159
  20. theorem OAI.MarkovSuperreflexivity.latticeTransition_formula line 165
  21. def OAI.MarkovSuperreflexivity.liftPotential line 190
  22. theorem OAI.MarkovSuperreflexivity.liftPotential_increment_accepted line 193
  23. theorem OAI.MarkovSuperreflexivity.liftPotential_increment_rejected line 204
  24. theorem OAI.MarkovSuperreflexivity.liftPotential_increment line 212