OAI/NumberTheory/DirichletL/Moments/SecondBlockCount.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentSecondBlockCount.ideal_norm_ge_one line 23
2. lemma OAI.SevenEighths.CenteredMomentSecondBlockCount.sourceLower_le_upper line 26
3. lemma OAI.SevenEighths.CenteredMomentSecondBlockCount.source_ratio_bound line 33
4. theorem OAI.SevenEighths.CenteredMomentSecondBlockCount.sourceBlocks_subpower line 68
5. abbrev OAI.SevenEighths.CenteredMomentSecondBlockCount.CommonSubsets line 87
6. lemma OAI.SevenEighths.CenteredMomentSecondBlockCount.commonSubset_support line 90
7. def OAI.SevenEighths.CenteredMomentSecondBlockCount.commonSubsetLabel line 97
8. lemma OAI.SevenEighths.CenteredMomentSecondBlockCount.commonSubsetLabel_injective line 102
9. lemma OAI.SevenEighths.CenteredMomentSecondBlockCount.commonSubsets_card_le line 111
10. abbrev OAI.SevenEighths.CenteredMomentSecondBlockCount.BlockLabels line 116
11. lemma OAI.SevenEighths.CenteredMomentSecondBlockCount.blockLabels_card_eq line 119
12. theorem OAI.SevenEighths.CenteredMomentSecondBlockCount.actual_block_count line 130