OAI/NumberTheory/CubicMoment/Theta/CubicThetaCentralTypeILowHeightTwist.lean

GitHub source file

1 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. theorem OAI.CubicFirstMoment.typeI_low_height_twist_actual line 14