OAI/NumberTheory/CubicMoment/Estimates/TypeIHeightRanges.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The two actual height ranges in the prime decomposition. The constants remain uniform in the selected smooth weight and the pole term has an arbitrary prescribed logarithmic saving.

  1. theorem OAI.CubicFirstMoment.typeI_selected_height_ranges line 14
  2. theorem OAI.CubicFirstMoment.angular_typeI_selected_height_ranges line 60