OAI/Probability/Contingency/WeightedSampler.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Weighted Sampler.

  1. def OAI.Contingency.BitModel.StackCode.WeightedSampler.preg line 14
  2. abbrev OAI.Contingency.BitModel.StackCode.WeightedSampler.first line 15
  3. def OAI.Contingency.BitModel.StackCode.WeightedSampler.sreg line 17
  4. abbrev OAI.Contingency.BitModel.StackCode.WeightedSampler.second line 18
  5. def OAI.Contingency.BitModel.StackCode.WeightedSampler.program line 20
  6. theorem OAI.Contingency.BitModel.StackCode.WeightedSampler.preg_injective line 22
  7. theorem OAI.Contingency.BitModel.StackCode.WeightedSampler.sreg_injective line 25
  8. theorem OAI.Contingency.BitModel.StackCode.WeightedSampler.reverse_value line 29
  9. theorem OAI.Contingency.BitModel.StackCode.WeightedSampler.first_safe line 36
  10. def OAI.Contingency.BitModel.StackCode.WeightedSampler.project line 56
  11. theorem OAI.Contingency.BitModel.StackCode.WeightedSampler.select_run line 61
  12. theorem OAI.Contingency.BitModel.StackCode.WeightedSampler.after_first line 111
  13. theorem OAI.Contingency.BitModel.StackCode.WeightedSampler.finishes_after line 145
  14. abbrev OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.draw line 190
  15. abbrev OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.selector line 191
  16. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.padded_select line 193
  17. abbrev OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.post line 231
  18. def OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.program line 232
  19. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.post_run line 234
  20. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.after_first line 291
  21. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.finishes_after line 325
  22. def OAI.Contingency.BitModel.StackCode.WeightedSampler.storedMass line 371
  23. theorem OAI.Contingency.BitModel.StackCode.WeightedSampler.stored_refinement line 375
  24. theorem OAI.Contingency.BitModel.StackCode.WeightedSampler.stored_shifted line 408
  25. theorem OAI.Contingency.BitModel.StackCode.WeightedSampler.stored_summable line 435
  26. theorem OAI.Contingency.BitModel.StackCode.WeightedSampler.stored_uniform line 440
  27. theorem OAI.Contingency.BitModel.StackCode.WeightedSampler.stored_expected line 447
  28. def OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.delay line 486
  29. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.tail_delay line 488
  30. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.stack_summable line 519
  31. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.stack_expected line 526
  32. def OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.machine line 544
  33. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.charged_time line 548
  34. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.live_fold line 573
  35. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.live_left line 590
  36. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.first_returned line 596
  37. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.word_injective line 606
  38. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.completes line 614
  39. theorem OAI.Contingency.BitModel.StackCode.PaddedWeightedSampler.halted_output line 655