OAI/NumberTheory/DirichletL/Moments/AmplificationSourceDomain.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentAmplificationSourceDomain.residualIdeal line 15
2. theorem OAI.SevenEighths.CenteredMomentAmplificationSourceDomain.residualIdeal_supported line 19
3. theorem OAI.SevenEighths.CenteredMomentAmplificationSourceDomain.residualIdeal_generator line 25
4. theorem OAI.SevenEighths.CenteredMomentAmplificationSourceDomain.residualIdeal_reconstruct line 37
5. def OAI.SevenEighths.CenteredMomentAmplificationSourceDomain.valuationColumns line 44
6. def OAI.SevenEighths.CenteredMomentAmplificationSourceDomain.residualColumns line 47
7. theorem OAI.SevenEighths.CenteredMomentAmplificationSourceDomain.valuationColumns_supported line 50
8. theorem OAI.SevenEighths.CenteredMomentAmplificationSourceDomain.residualIdeal_injOn line 54
9. theorem OAI.SevenEighths.CenteredMomentAmplificationSourceDomain.residualColumns_supported line 63
10. theorem OAI.SevenEighths.CenteredMomentAmplificationSourceDomain.residual_column_sum line 68