OAI/NumberTheory/CubicMoment/Estimates/DivisorFrequency.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The effective frequency after a square-divisor restriction is d*h. This identity retains vanishing when the divisor meets a conductor.

  1. lemma OAI.CubicFirstMoment.cubicSymbol_square_eq_star line 10
  2. lemma OAI.CubicFirstMoment.divisor_mixed_frequency line 30
  3. lemma OAI.CubicFirstMoment.divisor_gram_radial line 38