OAI/Analysis/MarkovType/OrbitDisplacement.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.OrbitRep line 17
  2. instance OAI.MarkovSuperreflexivity.(instance at line 20) line 20
  3. theorem OAI.MarkovSuperreflexivity.orbitRep_rev_ne line 25
  4. theorem OAI.MarkovSuperreflexivity.orbitRep_rev_ne_rep line 32
  5. def OAI.MarkovSuperreflexivity.orbitDisplacement line 39
  6. theorem OAI.MarkovSuperreflexivity.orbitDisplacement_rev line 45
  7. theorem OAI.MarkovSuperreflexivity.orbitDisplacement_bounds line 55
  8. theorem OAI.MarkovSuperreflexivity.orbitDisplacement_fixed line 62
  9. theorem OAI.MarkovSuperreflexivity.orbitDisplacement_rep_self line 68
  10. theorem OAI.MarkovSuperreflexivity.orbitDisplacement_rep_other line 73
  11. def OAI.MarkovSuperreflexivity.labelLinear line 82
  12. theorem OAI.MarkovSuperreflexivity.labelLinear_zero line 86
  13. theorem OAI.MarkovSuperreflexivity.labelLinear_add line 90
  14. theorem OAI.MarkovSuperreflexivity.labelLinear_neg line 95
  15. theorem OAI.MarkovSuperreflexivity.oddLabel_eq_zero_of_fixed line 100
  16. theorem OAI.MarkovSuperreflexivity.labelLinear_displacement_rep line 111
  17. theorem OAI.MarkovSuperreflexivity.labelLinear_displacement line 123
  18. theorem OAI.MarkovSuperreflexivity.oddLabel_zero_of_no_orbits line 140