OAI/Dynamics/EntropyCounterexample/CircleDoublingChains.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem340.CircleDoublingChains.Circle line 12
  2. abbrev OAI.Problem340.CircleDoublingChains.singularSet line 13
  3. abbrev OAI.Problem340.CircleDoublingChains.coefficients line 14
  4. abbrev OAI.Problem340.CircleDoublingChains.chains line 15
  5. def OAI.Problem340.CircleDoublingChains.loopMap line 17
  6. def OAI.Problem340.CircleDoublingChains.triangleMap line 22
  7. def OAI.Problem340.CircleDoublingChains.doubling line 28
  8. lemma OAI.Problem340.CircleDoublingChains.continuous_doubling line 30
  9. def OAI.Problem340.CircleDoublingChains.doublingMap line 33
  10. def OAI.Problem340.CircleDoublingChains.loopSimplex line 35
  11. def OAI.Problem340.CircleDoublingChains.triangleSimplex line 38
  12. def OAI.Problem340.CircleDoublingChains.doubledLoopSimplex line 41
  13. lemma OAI.Problem340.CircleDoublingChains.triangle_face_zero line 44
  14. lemma OAI.Problem340.CircleDoublingChains.triangle_face_one line 64
  15. lemma OAI.Problem340.CircleDoublingChains.triangle_face_two line 80
  16. lemma OAI.Problem340.CircleDoublingChains.loop_endpoints line 96
  17. def OAI.Problem340.CircleDoublingChains.loopChain line 113
  18. def OAI.Problem340.CircleDoublingChains.triangleChain line 115
  19. def OAI.Problem340.CircleDoublingChains.doubledLoopChain line 117
  20. lemma OAI.Problem340.CircleDoublingChains.loopChain_boundary line 120
  21. lemma OAI.Problem340.CircleDoublingChains.triangleChain_boundary line 128
  22. lemma OAI.Problem340.CircleDoublingChains.doubledLoopSimplex_eq_map line 141
  23. lemma OAI.Problem340.CircleDoublingChains.doubledLoopChain_eq_map line 145
  24. def OAI.Problem340.CircleDoublingChains.loop line 153
  25. def OAI.Problem340.CircleDoublingChains.triangle line 155
  26. lemma OAI.Problem340.CircleDoublingChains.loop_boundary line 157
  27. lemma OAI.Problem340.CircleDoublingChains.triangle_boundary line 160
  28. lemma OAI.Problem340.CircleDoublingChains.doubling_loop_sub_two_is_boundary line 166
  29. lemma OAI.Problem340.CircleDoublingChains.loop_cycle_sc line 173
  30. def OAI.Problem340.CircleDoublingChains.loopClass line 178
  31. lemma OAI.Problem340.CircleDoublingChains.loopClass_eq_zero_iff line 181
  32. theorem OAI.Problem340.CircleDoublingChains.doubling_loopClass line 190
  33. theorem OAI.Problem340.CircleDoublingChains.exists_doubling_eigenvector_of_loop_not_boundary line 226