OAI/NumberTheory/CubicMoment/Estimates/OuterCoreBlock.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The outer cubic sieve on one actual frequency core block. This is valid for arbitrary squarefree coefficients, hence for the shortened common-divisor rows.

  1. theorem OAI.CubicFirstMoment.outer_core_block_sieve line 13