OAI/Dynamics/EntropyCounterexample/Clock.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.Clock.profileCutoff line 9
  2. def OAI.Problem340.Clock.cutoff line 15
  3. lemma OAI.Problem340.Clock.cutoff_nonneg line 17
  4. lemma OAI.Problem340.Clock.cutoff_le_one line 19
  5. lemma OAI.Problem340.Clock.cutoff_neg line 21
  6. lemma OAI.Problem340.Clock.contDiff_cutoff line 23
  7. def OAI.Problem340.Clock.profile line 26
  8. lemma OAI.Problem340.Clock.contDiff_profile line 28
  9. def OAI.Problem340.Clock.localBarrier line 33
  10. lemma OAI.Problem340.Clock.localBarrier_eq_profile line 35
  11. lemma OAI.Problem340.Clock.cutoff_one line 37
  12. lemma OAI.Problem340.Clock.cutoff_zero line 42
  13. lemma OAI.Problem340.Clock.localBarrier_of_abs_le_one line 47
  14. lemma OAI.Problem340.Clock.localBarrier_of_abs_ge line 51
  15. lemma OAI.Problem340.Clock.localBarrier_nonneg line 55
  16. lemma OAI.Problem340.Clock.localBarrier_le_one line 62
  17. lemma OAI.Problem340.Clock.localBarrier_eq_zero_iff line 75
  18. lemma OAI.Problem340.Clock.localBarrier_neg line 90
  19. lemma OAI.Problem340.Clock.contDiff_localBarrier line 93
  20. lemma OAI.Problem340.Clock.profile_nonneg line 98
  21. lemma OAI.Problem340.Clock.profile_le_one line 102
  22. lemma OAI.Problem340.Clock.profile_eq_zero_iff line 106
  23. def OAI.Problem340.Clock.coordinate line 111
  24. lemma OAI.Problem340.Clock.contDiff_coordinate line 113
  25. lemma OAI.Problem340.Clock.coordinate_add_period line 117
  26. lemma OAI.Problem340.Clock.abs_coordinate_le line 124
  27. def OAI.Problem340.Clock.barrier line 135
  28. lemma OAI.Problem340.Clock.contDiff_barrier line 137
  29. lemma OAI.Problem340.Clock.barrier_periodic line 140
  30. lemma OAI.Problem340.Clock.barrier_nonneg line 144
  31. lemma OAI.Problem340.Clock.barrier_le_one line 146
  32. lemma OAI.Problem340.Clock.barrier_stops line 148
  33. lemma OAI.Problem340.Clock.barrier_eq_zero_iff line 164
  34. lemma OAI.Problem340.Clock.abs_coordinate_lower line 180
  35. lemma OAI.Problem340.Clock.barrier_plateau line 200
  36. lemma OAI.Problem340.Clock.coordinate_sq line 209
  37. def OAI.Problem340.Clock.ambientBarrier line 219
  38. lemma OAI.Problem340.Clock.contDiff_ambientBarrier line 221
  39. lemma OAI.Problem340.Clock.ambientBarrier_on_circle line 225
  40. lemma OAI.Problem340.Clock.ambientBarrier_mem_Icc line 230
  41. lemma OAI.Problem340.Clock.ambientBarrier_eq_zero_iff line 238
  42. def OAI.Problem340.Clock.increment line 247
  43. lemma OAI.Problem340.Clock.increment_nonneg line 249
  44. lemma OAI.Problem340.Clock.barrier_le_increment line 256
  45. lemma OAI.Problem340.Clock.increment_le_one line 262
  46. lemma OAI.Problem340.Clock.increment_zero line 267
  47. lemma OAI.Problem340.Clock.increment_one line 270
  48. lemma OAI.Problem340.Clock.increment_eq_one_of_barrier_eq_one line 273
  49. lemma OAI.Problem340.Clock.increment_periodic line 277
  50. lemma OAI.Problem340.Clock.contDiff_increment line 281