OAI/NumberTheory/DirichletL/Moments/SecondUniformSubsetSource.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.CenteredMomentSecondUniformSubsetSource.control_mono line 40
2. lemma OAI.SevenEighths.CenteredMomentSecondUniformSubsetSource.moment_mono line 47
3. lemma OAI.SevenEighths.CenteredMomentSecondUniformSubsetSource.factor_mono line 54
4. theorem OAI.SevenEighths.CenteredMomentSecondUniformSubsetSource.original_subsets_source_descent line 78
5. def OAI.SevenEighths.CenteredMomentSecondUniformSubsetSource.nestedImage line 205
6. lemma OAI.SevenEighths.CenteredMomentSecondUniformSubsetSource.nestedImage_ranges line 213
7. lemma OAI.SevenEighths.CenteredMomentSecondUniformSubsetSource.nestedImage_source line 223
8. lemma OAI.SevenEighths.CenteredMomentSecondUniformSubsetSource.nestedImage_data line 232