OAI/Probability/Contingency/IntegerDrawTail.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Integer Draw Tail.

  1. instance OAI.Contingency.BitModel.StackCode.IntegerDraw.(instance at line 17) line 17
  2. def OAI.Contingency.BitModel.StackCode.IntegerDraw.extend line 20
  3. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.trace_extend line 22
  4. def OAI.Contingency.BitModel.StackCode.IntegerDraw.coord line 28
  5. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.coord_injective line 37
  6. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.candidate_coord line 61
  7. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.bound_lt line 76
  8. def OAI.Contingency.BitModel.StackCode.IntegerDraw.badCount line 79
  9. def OAI.Contingency.BitModel.StackCode.IntegerDraw.rejectRate line 81
  10. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.bad_words line 83
  11. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.all_bad line 93
  12. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.bad_probability line 107
  13. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.tail_bound line 124
  14. theorem OAI.Contingency.BitModel.CoordinateLaw.count_snoc line 151
  15. def OAI.Contingency.BitModel.StackCode.IntegerDraw.word line 181
  16. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.word_value line 183
  17. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.word_injective line 187
  18. def OAI.Contingency.BitModel.StackCode.IntegerDraw.hit line 192
  19. instance OAI.Contingency.BitModel.StackCode.IntegerDraw.(instance at line 195) line 195
  20. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.hit_halts line 199
  21. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.hit_disjoint line 207
  22. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.hit_coordinates_count line 216
  23. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.hit_probability line 233
  24. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.rate_nonneg line 278
  25. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.rate_lt_one line 279
  26. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.rate_le_half line 286
  27. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.grouped_geometric line 295
  28. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.tail_nonneg line 313
  29. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.tail_le_one line 317
  30. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.shifted_tail_bound line 325
  31. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.stack_summable line 332
  32. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.stack_expected line 338
  33. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.stack_linear_expected line 354
  34. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.machine_summable line 367
  35. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.machine_halts_ae line 370
  36. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.machine_linear_expected line 373
  37. theorem OAI.Contingency.BitModel.StackCode.run_prefix_halt line 395
  38. theorem OAI.Contingency.BitModel.StackCode.mass_nonneg line 418
  39. theorem OAI.Contingency.BitModel.StackCode.mass_le_one line 422
  40. theorem OAI.Contingency.BitModel.StackCode.mass_mono line 431
  41. theorem OAI.Contingency.BitModel.StackCode.mass_limit_exists line 454
  42. theorem OAI.Contingency.BitModel.StackCode.sum_mass_le_one line 460
  43. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.initial_mass_lower line 497
  44. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.hit_series line 536
  45. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.limit_lower line 550
  46. def OAI.Contingency.BitModel.StackCode.IntegerDraw.validWord line 558
  47. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.validWord_injective line 561
  48. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.stack_uniform line 566
  49. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.machine_uniform line 588
  50. def OAI.Contingency.BitModel.StackCode.IntegerDraw.drawBits line 605
  51. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.candidate_bits line 608
  52. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.wordValue_false line 618
  53. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.extend_accepts line 623
  54. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.validWord_bits line 639
  55. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.halted_trace line 648
  56. theorem OAI.Contingency.BitModel.StackCode.IntegerDraw.stack_safe line 661