OAI/Combinatorics/BalancedRyser/Selection/SelectionProcessScales.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.Selection.Process.Parameters.Pstar_pos line 13
2. theorem OAI.Balanced.Selection.Process.Parameters.a_bounds line 19
3. theorem OAI.Balanced.Selection.Process.Parameters.tailSlots_le_order line 22
4. theorem OAI.Balanced.Selection.Process.Parameters.remaining_ge line 28
5. theorem OAI.Balanced.Selection.Process.Parameters.source_scale_bounds line 36
6. theorem OAI.Balanced.Selection.Process.Parameters.source_relative_changes line 52
7. theorem OAI.Balanced.Selection.Process.Parameters.source_size_increment_le line 66
8. theorem OAI.Balanced.Selection.Process.Parameters.source_degree_increment_le line 80
9. theorem OAI.Balanced.Selection.Process.Parameters.exists_admissible line 98
10. theorem OAI.Balanced.Selection.Process.Parameters.eventually_scale_regime line 112
11. theorem OAI.Balanced.Selection.Process.Parameters.Bstar_pos line 122
12. theorem OAI.Balanced.Selection.Process.Parameters.rho_pos line 125
13. theorem OAI.Balanced.Selection.Process.Parameters.occupancy_scale_bounds line 128
14. theorem OAI.Balanced.Selection.Process.Parameters.occupancy_rescaled_increment_le line 134
15. theorem OAI.Balanced.Selection.Process.Parameters.tailSlots_le_rho_mul line 147
16. theorem OAI.Balanced.Selection.Process.Parameters.occupancy_after_tail line 156
17. theorem OAI.Balanced.Selection.Process.Parameters.eventually_occupancy_regime line 162