OAI/NumberTheory/DirichletL/Moments/ExceptionalCappedAmplitude.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentExceptionalCappedAmplitude.rowTwistedSum_absolute line 20
2. theorem OAI.SevenEighths.CenteredMomentExceptionalCappedAmplitude.normalized_rectangle_absolute line 40
3. theorem OAI.SevenEighths.CenteredMomentExceptionalCappedAmplitude.capped_rectangle_uniform_degree line 73
4. theorem OAI.SevenEighths.CenteredMomentExceptionalCappedAmplitude.actual_capped_slots line 129
5. theorem OAI.SevenEighths.CenteredMomentExceptionalCappedAmplitude.actual_canonical_capped_energy line 165
6. theorem OAI.SevenEighths.CenteredMomentExceptionalCappedAmplitude.max_raw_reduction line 213
7. theorem OAI.SevenEighths.CenteredMomentExceptionalCappedAmplitude.reciprocal_max_raw_reduction line 224
8. theorem OAI.SevenEighths.CenteredMomentExceptionalCappedAmplitude.allocation_reciprocal_max line 228