OAI/NumberTheory/CubicMoment/Estimates/SmallBCoreOrdinary.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Retain the conductor, rather than length, loss of the ordinary sieve. This gives logarithmic savings for moderately small noncube cores.

  1. theorem OAI.CubicFirstMoment.smallB_core_ordinary_sieve line 11