OAI/Combinatorics/EditApproximation/Refinement/PhysicalSeedSchedule.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The actual finite adaptive sequence of median seed passes. Every chosen incoming table uses its own fresh product of full-table copy streams.

  1. theorem OAI.EditApproximation.scheduledSeedMultiplier_spec line 19
  2. theorem OAI.EditApproximation.scheduledSeedFactor_succ line 26
  3. theorem OAI.EditApproximation.scheduledSeedFactor_zero line 40
  4. theorem OAI.EditApproximation.scheduledSeedFactor_terminal line 44
  5. theorem OAI.EditApproximation.scheduledSeedFactor_terminal_refinement line 48
  6. abbrev OAI.EditApproximation.ScheduledSeedDraw line 66
  7. instance OAI.EditApproximation.scheduledSeedDrawFintype line 70
  8. def OAI.EditApproximation.scheduledSeedDrawLaw line 75
  9. instance OAI.EditApproximation.scheduledSeedDrawLaw_probability line 80
  10. def OAI.EditApproximation.scheduledSeedNext line 85
  11. def OAI.EditApproximation.scheduledSeedLaw line 92
  12. instance OAI.EditApproximation.scheduledSeedLaw_probability line 97
  13. theorem OAI.EditApproximation.scheduledSeedNext_failure line 113
  14. theorem OAI.EditApproximation.scheduledSeedLaw_failure line 154
  15. theorem OAI.EditApproximation.scheduledSeedLaw_failure_lt line 170