OAI/NumberTheory/CubicMoment/Estimates/PrimeGroupTailHeightBlocks.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Combining the actual small-core height mean and the uniform remaining core estimate. Sharp coefficient supports and arbitrary height shifts remain.

  1. theorem OAI.CubicFirstMoment.primeGroupTail_noncube_height_blocks line 12