OAI/NumberTheory/CubicMoment/Estimates/LowNearHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The near-cell diagonal is summed with the degree-five incidence bound. Only the logarithmically small remainder pays the cell-count cost.

  1. theorem OAI.CubicFirstMoment.low_near_logCell_height_bound line 14