OAI/NumberTheory/DirichletL/Moments/SuccessorPaidParameters.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentSuccessorPaidParameters.edge line 11
2. def OAI.SevenEighths.CenteredMomentSuccessorPaidParameters.exceptional line 14
3. def OAI.SevenEighths.CenteredMomentSuccessorPaidParameters.diagonal line 17
4. lemma OAI.SevenEighths.CenteredMomentSuccessorPaidParameters.paid_normalization line 20
5. lemma OAI.SevenEighths.CenteredMomentSuccessorPaidParameters.paid_normalization_with_ratio line 26
6. theorem OAI.SevenEighths.CenteredMomentSuccessorPaidParameters.actual_paid_error_reference line 32
7. lemma OAI.SevenEighths.CenteredMomentSuccessorPaidParameters.declared_parent_deficit line 52
8. lemma OAI.SevenEighths.CenteredMomentSuccessorPaidParameters.paired_declared_parent line 55
9. lemma OAI.SevenEighths.CenteredMomentSuccessorPaidParameters.mesh_cost line 61
10. theorem OAI.SevenEighths.CenteredMomentSuccessorPaidParameters.simultaneous_parameters line 67