OAI/NumberTheory/DirichletL/Moments/Bridge.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentBridge.productCharacter line 13
2. theorem OAI.SevenEighths.CenteredMomentBridge.productCharacter_apply line 28
3. theorem OAI.SevenEighths.CenteredMomentBridge.productCharacter_mk line 37
4. theorem OAI.SevenEighths.CenteredMomentBridge.productCharacter_gauss line 43
5. theorem OAI.SevenEighths.CenteredMomentBridge.triple_pair_gauss line 60
6. theorem OAI.SevenEighths.CenteredMomentBridge.triple_pair_poisson line 80
7. theorem OAI.SevenEighths.CenteredMomentBridge.masked_triple_pair_poisson line 121
8. theorem OAI.SevenEighths.CenteredMomentBridge.normalized_triple_pair_poisson line 170