OAI/Dynamics/EntropyCounterexample/ClockRotation.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.Clock.rotate line 10
  2. lemma OAI.Problem340.Clock.rotate_zero_apply line 14
  3. lemma OAI.Problem340.Clock.rotate_one_apply line 17
  4. lemma OAI.Problem340.Clock.norm_rotate line 20
  5. lemma OAI.Problem340.Clock.contDiff_rotate line 27
  6. def OAI.Problem340.Clock.parametrization line 39
  7. lemma OAI.Problem340.Clock.parametrization_zero line 42
  8. lemma OAI.Problem340.Clock.parametrization_one line 45
  9. lemma OAI.Problem340.Clock.norm_parametrization line 48
  10. lemma OAI.Problem340.Clock.rotate_parametrization line 54
  11. def OAI.Problem340.Clock.advance line 70
  12. def OAI.Problem340.Clock.ambientIncrement line 75
  13. lemma OAI.Problem340.Clock.ambientIncrement_mem_Icc line 78
  14. lemma OAI.Problem340.Clock.ambientBarrier_le_ambientIncrement line 87
  15. lemma OAI.Problem340.Clock.ambientIncrement_one line 94
  16. lemma OAI.Problem340.Clock.ambientIncrement_zero line 97
  17. lemma OAI.Problem340.Clock.contDiff_ambientIncrement line 100
  18. lemma OAI.Problem340.Clock.ambientIncrement_parametrization line 107
  19. def OAI.Problem340.Clock.ambientUpdate line 112
  20. lemma OAI.Problem340.Clock.contDiff_ambientUpdate line 115
  21. lemma OAI.Problem340.Clock.ambientUpdate_parametrization line 122
  22. lemma OAI.Problem340.Clock.norm_ambientUpdate line 126
  23. def OAI.Problem340.Clock.update line 129
  24. lemma OAI.Problem340.Clock.continuous_update line 134
  25. def OAI.Problem340.Clock.clockStep line 140
  26. lemma OAI.Problem340.Clock.isC1SelfMap_clockStep line 144