OAI/Computability/StarHeight/LateSchedule.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.GeneralizedStarHeight.SourceSchedule.Late line 13
  2. lemma OAI.GeneralizedStarHeight.SourceSchedule.exists_late line 25
  3. lemma OAI.GeneralizedStarHeight.SourceSchedule.Late.radius_nonneg line 70
  4. lemma OAI.GeneralizedStarHeight.SourceSchedule.Late.overlap line 73
  5. lemma OAI.GeneralizedStarHeight.SourceSchedule.Late.complete_lower line 82
  6. lemma OAI.GeneralizedStarHeight.SourceSchedule.Late.visible line 90
  7. def OAI.GeneralizedStarHeight.SourceSchedule.finiteBound line 126
  8. lemma OAI.GeneralizedStarHeight.SourceSchedule.abs_le_finiteBound line 128
  9. def OAI.GeneralizedStarHeight.SourceSchedule.Early.period line 142
  10. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.period_pos line 144
  11. def OAI.GeneralizedStarHeight.SourceSchedule.Early.cuts line 146
  12. def OAI.GeneralizedStarHeight.SourceSchedule.Early.diameter line 155
  13. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.diameter_pos line 157
  14. def OAI.GeneralizedStarHeight.SourceSchedule.Early.sweepWidth line 159
  15. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.sweepWidth_large line 162
  16. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.sweepWidth_pos line 165
  17. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.offsets_difference line 168
  18. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.stencil_difference line 177
  19. def OAI.GeneralizedStarHeight.SourceSchedule.Early.envelope line 184
  20. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.envelope_pos line 191
  21. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.inner_left line 195
  22. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.inner_right line 211
  23. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.exists_full_late line 231
  24. def OAI.GeneralizedStarHeight.SourceSchedule.Early.parameters line 237
  25. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.geometry line 253
  26. lemma OAI.GeneralizedStarHeight.SourceSchedule.Early.actual_visible line 306
  27. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.not_failed_clock line 322
  28. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.not_failed_inner line 325
  29. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.not_failed_absent line 334
  30. lemma OAI.GeneralizedStarHeight.ExceptionalOrigins.Parameters.not_failed_end line 341