OAI/NumberTheory/CubicMoment/Estimates/SmallBLowHeightBlocks.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The low-height noncube moment with an explicit core cutoff. The small cores use a summed divisor moment; no length-to-a-small-power loss remains.

  1. theorem OAI.CubicFirstMoment.smallB_noncube_bounded_blocks line 12