OAI/Combinatorics/BalancedRyser/Selection/SelectionProcessLaw.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Selection.Process.sum_flagsWeight line 16
  2. theorem OAI.Balanced.Selection.Process.sum_drawWeight_vertex line 24
  3. theorem OAI.Balanced.Selection.Process.sum_drawWeight line 40
  4. theorem OAI.Balanced.Selection.Process.sum_noiseWeight line 49
  5. theorem OAI.Balanced.Selection.Process.sum_stepWeight line 56
  6. theorem OAI.Balanced.Selection.Process.sum_transitionWeight line 65
  7. theorem OAI.Balanced.Selection.Process.sum_historyWeight line 72
  8. theorem OAI.Balanced.Selection.Process.hazard_nonnegative line 83
  9. theorem OAI.Balanced.Selection.Process.thinningRate_bounds_of_precheck line 89
  10. theorem OAI.Balanced.Selection.Process.flagsWeight_nonnegative_of_precheck line 100
  11. theorem OAI.Balanced.Selection.Process.drawWeight_nonnegative line 110
  12. theorem OAI.Balanced.Selection.Process.noiseWeight_nonnegative_of_precheck line 118
  13. theorem OAI.Balanced.Selection.Process.stepWeight_nonnegative line 124
  14. theorem OAI.Balanced.Selection.Process.transitionWeight_nonnegative line 136
  15. theorem OAI.Balanced.Selection.Process.historyWeight_nonnegative line 142
  16. theorem OAI.Balanced.Selection.Process.sum_drawStepWeight line 151
  17. theorem OAI.Balanced.Selection.Process.drawStepWeight_nonnegative line 163
  18. theorem OAI.Balanced.Selection.Process.transitionWeight_eq_draw_pushforward line 176
  19. theorem OAI.Balanced.Selection.Process.snapshotWeight_nonnegative line 190
  20. theorem OAI.Balanced.Selection.Process.sum_snapshotWeight line 197
  21. def OAI.Balanced.Selection.Process.snapshotPMF line 204
  22. theorem OAI.Balanced.Selection.Process.snapshotPMF_apply_real line 212
  23. def OAI.Balanced.Selection.Process.historyPMF line 217
  24. theorem OAI.Balanced.Selection.Process.historyPMF_apply_real line 225