OAI/NumberTheory/CubicMoment/Estimates/RadialTypeILow.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The radial low-height Type-I estimate, including the literal finite residue density. The short and long inverse sums are actual finite sums, and the coefficient masses are deduced from the literal primary-divisor bound.

  1. theorem OAI.CubicFirstMoment.radial_typeI_low_squarefree_of_published line 20
  2. theorem OAI.CubicFirstMoment.radial_typeI_low_of_published line 131