OAI/NumberTheory/DirichletL/Moments/ActiveCanonicalSource.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentActiveCanonicalSource.positiveChildren line 26
2. theorem OAI.SevenEighths.CenteredMomentActiveCanonicalSource.positiveChildren_nonneg line 42
3. def OAI.SevenEighths.CenteredMomentActiveCanonicalSource.SmoothedBound line 60
4. theorem OAI.SevenEighths.CenteredMomentActiveCanonicalSource.uniform_smoothed_bound line 81
5. def OAI.SevenEighths.CenteredMomentActiveCanonicalSource.commonPositiveChildren line 105
6. theorem OAI.SevenEighths.CenteredMomentActiveCanonicalSource.canonical_source_to_positive line 116
7. def OAI.SevenEighths.CenteredMomentActiveCanonicalSource.CanonicalBound line 193
8. theorem OAI.SevenEighths.CenteredMomentActiveCanonicalSource.uniform_canonical_source_to_positive line 223