OAI/Probability/Ballisticity/Estimates/CellSchedule.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.cellWidth line 11
  2. def OAI.DirectionalTransience.cellOpportunity line 13
  3. lemma OAI.DirectionalTransience.cellWidth_zero line 16
  4. lemma OAI.DirectionalTransience.cellWidth_last line 17
  5. lemma OAI.DirectionalTransience.cellWidth_antitone line 18
  6. lemma OAI.DirectionalTransience.cellWidth_pos line 22
  7. lemma OAI.DirectionalTransience.cellWidth_min line 24
  8. lemma OAI.DirectionalTransience.cellWidth_step line 28
  9. lemma OAI.DirectionalTransience.cellWidth_shift line 34
  10. lemma OAI.DirectionalTransience.cellOpportunity_last line 40
  11. lemma OAI.DirectionalTransience.cellOpportunity_le_end line 42
  12. lemma OAI.DirectionalTransience.cellOpportunity_monotone line 47
  13. lemma OAI.DirectionalTransience.cell_seed_endpoint line 56
  14. lemma OAI.DirectionalTransience.cell_seed_before_next line 62
  15. lemma OAI.DirectionalTransience.cell_step_length line 73
  16. def OAI.DirectionalTransience.cellEarlyHeight line 81
  17. def OAI.DirectionalTransience.cellLateHeight line 84
  18. lemma OAI.DirectionalTransience.cellEarly_endpoint line 88
  19. lemma OAI.DirectionalTransience.cellEarlyHeight_bound line 98
  20. lemma OAI.DirectionalTransience.cellLateHeight_bound line 107
  21. lemma OAI.DirectionalTransience.cellLate_endpoint line 119
  22. def OAI.DirectionalTransience.cellRadius line 145
  23. lemma OAI.DirectionalTransience.cellRadius_pos line 150
  24. def OAI.DirectionalTransience.cellRestart line 153
  25. lemma OAI.DirectionalTransience.cellRestart_measurable line 158
  26. def OAI.DirectionalTransience.scheduledCellFailure line 165
  27. def OAI.DirectionalTransience.cellFiltration line 179
  28. lemma OAI.DirectionalTransience.scheduledCellFailure_measurable line 192