OAI/NumberTheory/DirichletL/Moments/FiniteProfileExceptionalNormalize.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.sourceControl line 11
2. def OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.normalizedProfile line 14
3. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.sourceControl_nonneg line 17
4. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.sourceControl_zero line 19
5. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.normalizedProfile_control line 27
6. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.normalizedProfile_support line 36
7. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.normalizedProfile_reconstruct line 42
8. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.twistedIdealSum_profile_smul line 49
9. theorem OAI.SevenEighths.CenteredMomentFiniteProfileExceptional.twistedIdealSum_normalized line 58