OAI/NumberTheory/CubicMoment/Estimates/TypeILowHeightTwist.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The low-height Type-I estimate with its actual Mellin phase. The original height-dependent squarefree model is retained.

  1. lemma OAI.CubicFirstMoment.metaplecticAngularSmoothSum_phase line 13
  2. def OAI.CubicFirstMoment.lowTwistedTypeIRow line 29
  3. theorem OAI.CubicFirstMoment.typeI_low_height_twist line 33