OAI/Combinatorics/SharpRamsey/Exposure/FreshBlockBudgets.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpLogRamsey.Selection.selected_absorption line 13
2. theorem OAI.SharpLogRamsey.Selection.selected_fixed_observable line 35
3. def OAI.SharpLogRamsey.Selection.maximumCharge line 41
4. lemma OAI.SharpLogRamsey.Selection.maximumCharge_le_sum line 44
5. theorem OAI.SharpLogRamsey.Selection.selected_charge_absorption line 52