OAI/NumberTheory/DirichletL/Moments/FirstSecondCapacityLedger.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentFirstSecondCapacityLedger.formal_reduction_pays_slots line 16
2. theorem OAI.SevenEighths.CenteredMomentFirstSecondCapacityLedger.affine_reduction_le_parent line 35
3. theorem OAI.SevenEighths.CenteredMomentFirstSecondCapacityLedger.allocated_excess_from_parent line 44
4. theorem OAI.SevenEighths.CenteredMomentFirstSecondCapacityLedger.live_allocated_excess line 66
5. theorem OAI.SevenEighths.CenteredMomentFirstSecondCapacityLedger.live_whole_removal line 84
6. theorem OAI.SevenEighths.CenteredMomentFirstSecondCapacityLedger.paired_edge_cost line 109
7. theorem OAI.SevenEighths.CenteredMomentFirstSecondCapacityLedger.edge_loss_budget line 116