OAI/NumberTheory/DirichletL/Energy/AllocatedClipped.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentEnergyAllocatedClipped.pair line 22
2. def OAI.SevenEighths.CenteredMomentEnergyAllocatedClipped.scale line 28
3. lemma OAI.SevenEighths.CenteredMomentEnergyAllocatedClipped.scale_pos line 32
4. lemma OAI.SevenEighths.CenteredMomentEnergyAllocatedClipped.scale_cap line 38
5. lemma OAI.SevenEighths.CenteredMomentEnergyAllocatedClipped.allocated_pair line 43
6. theorem OAI.SevenEighths.CenteredMomentEnergyAllocatedClipped.actual_clipped_paid_bands line 65