OAI/Probability/FreeIsing/Estimates/RoundedStoppingTimes.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.RoundedStoppingTimes.round line 14
  2. theorem OAI.Problem367.RoundedStoppingTimes.mesh_pos line 17
  3. theorem OAI.Problem367.RoundedStoppingTimes.le_round line 19
  4. theorem OAI.Problem367.RoundedStoppingTimes.round_le_add line 23
  5. theorem OAI.Problem367.RoundedStoppingTimes.round_le_iff line 29
  6. theorem OAI.Problem367.RoundedStoppingTimes.floor_div_le line 34
  7. theorem OAI.Problem367.RoundedStoppingTimes.tendsto_round line 39
  8. def OAI.Problem367.RoundedStoppingTimes.roundTop line 46
  9. theorem OAI.Problem367.RoundedStoppingTimes.roundTop_top line 48
  10. theorem OAI.Problem367.RoundedStoppingTimes.roundTop_coe line 50
  11. theorem OAI.Problem367.RoundedStoppingTimes.le_roundTop line 53
  12. theorem OAI.Problem367.RoundedStoppingTimes.roundTop_le_iff line 58
  13. theorem OAI.Problem367.RoundedStoppingTimes.countable_range_roundTop line 65
  14. theorem OAI.Problem367.RoundedStoppingTimes.isStoppingTime_roundTop line 76
  15. theorem OAI.Problem367.RoundedStoppingTimes.countable_range_roundTop_comp line 82
  16. theorem OAI.Problem367.RoundedStoppingTimes.tendsto_min_roundTop_untopA line 86
  17. theorem OAI.Problem367.RoundedStoppingTimes.exists_countable_range_approximation line 96