OAI/Analysis/BoundedHochschild/RareScales.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Rare-event probabilities, time scales and label counts.

  1. def OAI.HochschildRare.q line 25
  2. def OAI.HochschildRare.p line 26
  3. def OAI.HochschildRare.time line 27
  4. def OAI.HochschildRare.slots line 28
  5. def OAI.HochschildRare.labels line 29
  6. lemma OAI.HochschildRare.q_pos line 31
  7. lemma OAI.HochschildRare.q_le line 32
  8. lemma OAI.HochschildRare.p_pos line 35
  9. lemma OAI.HochschildRare.p_le line 36
  10. lemma OAI.HochschildRare.q_succ line 41
  11. lemma OAI.HochschildRare.p_succ line 44
  12. lemma OAI.HochschildRare.p_succ_le line 45
  13. lemma OAI.HochschildRare.p_antitone line 50
  14. lemma OAI.HochschildRare.tail_bound line 56
  15. lemma OAI.HochschildRare.geometric_bound line 67
  16. lemma OAI.HochschildRare.summable_p line 74
  17. lemma OAI.HochschildRare.sum_p_le line 79
  18. lemma OAI.HochschildRare.sum_tail_le line 89
  19. lemma OAI.HochschildRare.time_pos line 99
  20. lemma OAI.HochschildRare.slots_pos line 100
  21. lemma OAI.HochschildRare.labels_pos line 101
  22. lemma OAI.HochschildRare.successor_le_two_pow line 103
  23. lemma OAI.HochschildRare.q_geometric_bound line 111
  24. lemma OAI.HochschildRare.tendsto_stage_q line 114
  25. lemma OAI.HochschildRare.time_mul_p_mul_q line 121
  26. lemma OAI.HochschildRare.slots_mul_p_sq line 127
  27. lemma OAI.HochschildRare.geometric_miss_bound line 135
  28. lemma OAI.HochschildRare.miss_le_q line 149
  29. lemma OAI.HochschildRare.slots_ge_stage line 157
  30. lemma OAI.HochschildRare.slots_tendsto line 160
  31. lemma OAI.HochschildRare.slots_real_tendsto line 163
  32. lemma OAI.HochschildRare.bad_bound_tendsto line 166