OAI/NumberTheory/CubicMoment/Estimates/SquarefreeNormFiber.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Squarefree norm fibers have a divisor weight attached to each actual member. Summing this weight retains logarithmic rather than small-power loss.

  1. lemma OAI.CubicFirstMoment.squarefree_primeFactors_norm_subset line 14
  2. lemma OAI.CubicFirstMoment.squarefree_norm_fiber_card line 38
  3. lemma OAI.CubicFirstMoment.normCollectedCoeff_squarefree_energy line 66