OAI/NumberTheory/DirichletL/Moments/CommonWindowColumn.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentCommonWindowColumn.columns line 22
2. def OAI.SevenEighths.CenteredMomentCommonWindowColumn.coefficient line 25
3. def OAI.SevenEighths.CenteredMomentCommonWindowColumn.windowColumn line 32
4. theorem OAI.SevenEighths.CenteredMomentCommonWindowColumn.coefficient_polynomial line 39
5. theorem OAI.SevenEighths.CenteredMomentCommonWindowColumn.sourceGenerator_span line 49
6. theorem OAI.SevenEighths.CenteredMomentCommonWindowColumn.whole_window_pair line 54