OAI/NumberTheory/DirichletL/Moments/DetectorPlainSource.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentDetectorPlainSource.completePool line 23
2. lemma OAI.SevenEighths.CenteredMomentDetectorPlainSource.support_zero line 27
3. lemma OAI.SevenEighths.CenteredMomentDetectorPlainSource.comparison_row_zero line 33
4. theorem OAI.SevenEighths.CenteredMomentDetectorPlainSource.complete_source_polynomial line 45
5. theorem OAI.SevenEighths.CenteredMomentDetectorPlainSource.positiveSlotRow_eq_complete_source line 84
6. theorem OAI.SevenEighths.CenteredMomentDetectorPlainSource.positive_energy_eq_complete_source line 103