OAI/NumberTheory/DirichletL/Moments/CanonicalRetainedSource.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentCanonicalRetainedSource.positiveChildren line 24
2. theorem OAI.SevenEighths.CenteredMomentCanonicalRetainedSource.positiveChildren_nonneg line 38
3. def OAI.SevenEighths.CenteredMomentCanonicalRetainedSource.SmoothedBound line 56
4. theorem OAI.SevenEighths.CenteredMomentCanonicalRetainedSource.uniform_smoothed_bound line 77
5. theorem OAI.SevenEighths.CenteredMomentCanonicalRetainedSource.live_residual_pool line 101
6. theorem OAI.SevenEighths.CenteredMomentCanonicalRetainedSource.liveBox_original_pools line 108
7. def OAI.SevenEighths.CenteredMomentCanonicalRetainedSource.commonPositiveChildren line 116
8. theorem OAI.SevenEighths.CenteredMomentCanonicalRetainedSource.canonical_source_to_positive line 127
9. def OAI.SevenEighths.CenteredMomentCanonicalRetainedSource.CanonicalBound line 204
10. theorem OAI.SevenEighths.CenteredMomentCanonicalRetainedSource.uniform_canonical_source_to_positive line 234