OAI/Dynamics/EntropyCounterexample/CylinderAttraction.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.clockMainCylinder line 16
  2. def OAI.Problem340.sphereVectorCylinder line 19
  3. lemma OAI.Problem340.infDist_clockMainCylinder_le line 22
  4. lemma OAI.Problem340.infDist_sphereVectorCylinder_le line 38
  5. lemma OAI.Problem340.clockMainCylinder_nonempty line 45
  6. lemma OAI.Problem340.sphereVectorCylinder_nonempty line 50
  7. theorem OAI.Problem340.tendsto_infDist_clockMainCylinder line 53
  8. theorem OAI.Problem340.tendsto_infDist_sphereVectorCylinder line 68
  9. theorem OAI.Problem340.tendsto_infDist_attractor_union_of_coordinates line 79
  10. theorem OAI.Problem340.tendsto_sphereVector_of_main_and_eventual_reset line 98
  11. lemma OAI.Problem340.isClosed_clockMainCylinder line 114
  12. lemma OAI.Problem340.isClosed_sphereVectorCylinder line 120
  13. lemma OAI.Problem340.isCompact_attractor_union line 125
  14. theorem OAI.Problem340.eventually_mem_of_tendsto_infDist_zero line 134
  15. theorem OAI.Problem340.counterexample_attraction_of_coordinate_alternatives line 145
  16. lemma OAI.Problem340.counterexample_attractor_isCompact line 163
  17. theorem OAI.Problem340.counterexample_eventually_mem_attractor_neighborhood line 170