OAI/NumberTheory/DirichletL/Moments/FiniteProfileExceptionalStability.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.sourcePlain line 15
2. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.sourcePlain_support line 19
3. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.plain_profile_source_control line 29
4. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.scale_source_control line 49
5. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.scale_source_support line 54
6. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.fourier_source_control line 63
7. def OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.logWindowMultiply line 68
8. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.logWindowMultiply_apply line 72
9. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.logWindow_source_control line 80
10. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.window_fourier_twist_source_control line 85
11. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.scaled_plain_profile_source_control line 98