OAI/Combinatorics/BalancedRyser/Selection/SelectionOccupancyAgreement.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.Selection.Process.positive_snapshot_survival_before line 17
2. theorem OAI.Balanced.Selection.Process.occupancyPrefix_succ_of_draw line 35
3. theorem OAI.Balanced.Selection.Process.occupancyTrack_eq_on_surviving_path line 59
4. theorem OAI.Balanced.Selection.Process.ae_occupancyTrack_eq line 91
5. theorem OAI.Balanced.Selection.Process.surviving_occupancy_lower_tail line 102