OAI/NumberTheory/CubicMoment/Decomposition/StoppedBoundedDivisor.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Pointwise bounds for all rows in the actual coprimality expansion. The small-core estimate sums inverse-square quotient lengths, while the hybrid core estimate sums the proved logarithmic divisor energy.

  1. lemma OAI.CubicFirstMoment.bounded_filtered_character_row line 15
  2. lemma OAI.CubicFirstMoment.bounded_divisor_character_row line 48
  3. theorem OAI.CubicFirstMoment.bounded_divisor_all_frequency_mass line 67