OAI/Combinatorics/UniformKServer/RawBlockCharge.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniformKServer.RawBlockCharge.paid_or_covered line 8
2. theorem OAI.UniformKServer.RawBlockCharge.one_block line 34
3. theorem OAI.UniformKServer.RawBlockCharge.cost_append line 51
4. theorem OAI.UniformKServer.RawBlockCharge.split_history line 58
5. theorem OAI.UniformKServer.RawBlockCharge.tail_blocks line 65
6. theorem OAI.UniformKServer.RawBlockCharge.word_blocks line 82
7. theorem OAI.UniformKServer.RawBlockCharge.offline_blocks line 94