OAI/NumberTheory/DirichletL/Moments/DescentLedger.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentDescentLedger.firstSaving line 11
2. theorem OAI.SevenEighths.CenteredMomentDescentLedger.firstSaving_lower line 14
3. theorem OAI.SevenEighths.CenteredMomentDescentLedger.common_log_ge_unit line 40
4. theorem OAI.SevenEighths.CenteredMomentDescentLedger.half_product_log_ge_radical line 61
5. theorem OAI.SevenEighths.CenteredMomentDescentLedger.declared_width_drop line 79
6. theorem OAI.SevenEighths.CenteredMomentDescentLedger.child_allowance_lower line 86
7. theorem OAI.SevenEighths.CenteredMomentDescentLedger.exceptional_excess_identity line 90
8. theorem OAI.SevenEighths.CenteredMomentDescentLedger.inner_allowance_identity line 102
9. theorem OAI.SevenEighths.CenteredMomentDescentLedger.exceptional_excess_bound line 107
10. theorem OAI.SevenEighths.CenteredMomentDescentLedger.uncentered_exceptional_bound line 113