OAI/NumberTheory/DirichletL/Moments/DyadicCount.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentDyadicCount.indices line 13
2. lemma OAI.SevenEighths.CenteredMomentDyadicCount.logb_dyadicScale line 16
3. lemma OAI.SevenEighths.CenteredMomentDyadicCount.mem_indices_iff_scale line 19
4. lemma OAI.SevenEighths.CenteredMomentDyadicCount.mem_indices_iff_whole_support line 31
5. lemma OAI.SevenEighths.CenteredMomentDyadicCount.support_indices line 43
6. lemma OAI.SevenEighths.CenteredMomentDyadicCount.finite_active_indices line 48
7. lemma OAI.SevenEighths.CenteredMomentDyadicCount.logb_four_mul line 54
8. theorem OAI.SevenEighths.CenteredMomentDyadicCount.indices_card_bound line 61
9. theorem OAI.SevenEighths.CenteredMomentDyadicCount.scaled_indices_card_bound line 77
10. lemma OAI.SevenEighths.CenteredMomentDyadicCount.dyadic_partition_on_interval line 84
11. theorem OAI.SevenEighths.CenteredMomentDyadicCount.four_indices_card_bound line 93
12. lemma OAI.SevenEighths.CenteredMomentDyadicCount.retained_integral_mem line 105
13. theorem OAI.SevenEighths.CenteredMomentDyadicCount.indices_card_log_bound line 112
14. theorem OAI.SevenEighths.CenteredMomentDyadicCount.four_indices_subpower line 131