OAI/NumberTheory/DirichletL/Moments/FirstSecondCapacityDefect.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentFirstSecondCapacityLedger.width_defect_cost line 16
2. theorem OAI.SevenEighths.CenteredMomentFirstSecondCapacityLedger.live_allocated_excess_defect line 22
3. theorem OAI.SevenEighths.CenteredMomentFirstSecondCapacityLedger.live_removal_width_cost line 43
4. theorem OAI.SevenEighths.CenteredMomentFirstSecondCapacityLedger.source_removal_width_cost line 72
5. theorem OAI.SevenEighths.CenteredMomentFirstSecondCapacityLedger.paired_width_defect_cost line 102