OAI/Combinatorics/BalancedRyser/Selection/SelectionOccupancyBound.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.Selection.Process.Parameters.occupancyDecay line 17
2. theorem OAI.Balanced.Selection.Process.Parameters.occupancyDecay_pos line 20
3. theorem OAI.Balanced.Selection.Process.surviving_source_occupancy_bound line 28
4. theorem OAI.Balanced.Selection.Process.source_plane_line_card line 75
5. theorem OAI.Balanced.Selection.Process.surviving_all_line_occupancy_bound line 84
6. theorem OAI.Balanced.Selection.Process.source_occupancy_error_tendsto line 120