OAI/NumberTheory/DirichletL/CubicDyadicDecay.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CubicDyadicDecay.decayConstant line 16
2. lemma OAI.SevenEighths.CubicDyadicDecay.dyadic_rpow line 19
3. lemma OAI.SevenEighths.CubicDyadicDecay.decay_le_low line 24
4. lemma OAI.SevenEighths.CubicDyadicDecay.decay_le_high line 31
5. lemma OAI.SevenEighths.CubicDyadicDecay.decay_summable line 44
6. lemma OAI.SevenEighths.CubicDyadicDecay.decayConstant_pos line 51
7. lemma OAI.SevenEighths.CubicDyadicDecay.geometric_prefix_le line 59
8. lemma OAI.SevenEighths.CubicDyadicDecay.decay_tail_le line 64
9. theorem OAI.SevenEighths.CubicDyadicDecay.dyadic_decay_bound line 81
10. theorem OAI.SevenEighths.CubicDyadicDecay.two_power_majorant line 138
11. theorem OAI.SevenEighths.CubicDyadicDecay.sieve_growth_majorant line 169
12. lemma OAI.SevenEighths.CubicDyadicDecay.poisson_scale_identity line 189
13. lemma OAI.SevenEighths.CubicDyadicDecay.poisson_small_power_identity line 198
14. theorem OAI.SevenEighths.CubicDyadicDecay.sieve_poisson_bound line 209
15. lemma OAI.SevenEighths.CubicDyadicDecay.descent_factor_le_one line 248
16. lemma OAI.SevenEighths.CubicDyadicDecay.monomial_descendant_le line 261
17. lemma OAI.SevenEighths.CubicDyadicDecay.mixed_monomial_identity line 275
18. lemma OAI.SevenEighths.CubicDyadicDecay.secondary_monomial_identity line 285
19. lemma OAI.SevenEighths.CubicDyadicDecay.mixed_descendant_le line 294
20. lemma OAI.SevenEighths.CubicDyadicDecay.secondary_descendant_le line 305
21. theorem OAI.SevenEighths.CubicDyadicDecay.poisson_envelope_descendant_le line 316