OAI/NumberTheory/DirichletL/Moments/SecondChildPowerBudget.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentSecondChildPowerBudget.endpoint_product line 18
2. lemma OAI.SevenEighths.CenteredMomentSecondChildPowerBudget.main_cost line 28
3. lemma OAI.SevenEighths.CenteredMomentSecondChildPowerBudget.diagonal_cost line 49
4. lemma OAI.SevenEighths.CenteredMomentSecondChildPowerBudget.tail_cost line 64
5. def OAI.SevenEighths.CenteredMomentSecondChildPowerBudget.powers line 70
6. lemma OAI.SevenEighths.CenteredMomentSecondChildPowerBudget.powers_nonneg line 72
7. def OAI.SevenEighths.CenteredMomentSecondChildPowerBudget.coefficients line 76
8. lemma OAI.SevenEighths.CenteredMomentSecondChildPowerBudget.coefficients_nonneg line 86
9. def OAI.SevenEighths.CenteredMomentSecondChildPowerBudget.sourceCost line 99
10. theorem OAI.SevenEighths.CenteredMomentSecondChildPowerBudget.source_rhs line 110
11. theorem OAI.SevenEighths.CenteredMomentSecondChildPowerBudget.twice_source_rhs line 140