OAI/NumberTheory/DirichletL/Moments/FirstExceptionalPaidScales.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SevenEighths.CenteredMomentFirstExceptionalPaidScales.Branch line 15
2. def OAI.SevenEighths.CenteredMomentFirstExceptionalPaidScales.removedWidth line 48
3. def OAI.SevenEighths.CenteredMomentFirstExceptionalPaidScales.saving line 51
4. def OAI.SevenEighths.CenteredMomentFirstExceptionalPaidScales.loss line 62
5. def OAI.SevenEighths.CenteredMomentFirstExceptionalPaidScales.rawCap line 64
6. lemma OAI.SevenEighths.CenteredMomentFirstExceptionalPaidScales.actual_saving line 67
7. lemma OAI.SevenEighths.CenteredMomentFirstExceptionalPaidScales.raw_cap_lower line 74
8. theorem OAI.SevenEighths.CenteredMomentFirstExceptionalPaidScales.actual_branch_stage line 87
9. theorem OAI.SevenEighths.CenteredMomentFirstExceptionalPaidScales.actual_paired_stage line 96