OAI/NumberTheory/CubicMoment/Estimates/SparseLateGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The late-stop norm range in the manuscript supplies all length hypotheses of the sparse cubic and model bounds, including fixed dyadic dilations.

  1. lemma OAI.CubicFirstMoment.late_stop_rectangle_bounds line 12
  2. lemma OAI.CubicFirstMoment.eventually_late_stop_rectangle_bounds line 39