OAI/NumberTheory/CubicMoment/Estimates/LowFarHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The far cells gain two integrations by parts. The diagonal and the logarithmic remainder retain their separate cell-count costs.

  1. theorem OAI.CubicFirstMoment.low_far_logCell_integrated_bound line 13