OAI/NumberTheory/DirichletL/Moments/ExceptionalAmplitudePair.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SevenEighths.CenteredMomentExceptionalAmplitudePair.Tests line 16
2. def OAI.SevenEighths.CenteredMomentExceptionalAmplitudePair.Tests.profile line 24
3. def OAI.SevenEighths.CenteredMomentExceptionalAmplitudePair.Tests.heightWeight line 27
4. def OAI.SevenEighths.CenteredMomentExceptionalAmplitudePair.volume line 29
5. lemma OAI.SevenEighths.CenteredMomentExceptionalAmplitudePair.volume_pos line 31
6. def OAI.SevenEighths.CenteredMomentExceptionalAmplitudePair.Admissible line 34
7. lemma OAI.SevenEighths.CenteredMomentExceptionalAmplitudePair.norm_le_of_squared line 42
8. lemma OAI.SevenEighths.CenteredMomentExceptionalAmplitudePair.reduction_cap_identity line 49
9. theorem OAI.SevenEighths.CenteredMomentExceptionalAmplitudePair.actual_paired_amplitude line 66