OAI/NumberTheory/CubicMoment/Estimates/TypeILow.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The low-height Type-I estimate for every fixed angular mode. The zero mode uses the radial residue, and every nonzero mode uses angular lattice cancellation.

  1. theorem OAI.CubicFirstMoment.typeI_low_of_published line 13