OAI/NumberTheory/DirichletL/Moments/HeckeHeight.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.CenteredMomentHeckeHeight.volumeControl_polynomial_height line 13
2. theorem OAI.SevenEighths.CenteredMomentHeckeHeight.normalized_actual_rectangle_estimate line 52
3. def OAI.SevenEighths.CenteredMomentHeckeHeight.rowTwistedSum line 125
4. theorem OAI.SevenEighths.CenteredMomentHeckeHeight.rowTwistedSum_eq line 129
5. theorem OAI.SevenEighths.CenteredMomentHeckeHeight.exceptional_rectangle_estimate line 140