OAI/NumberTheory/CubicMoment/Decomposition/StoppedRoughRows.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Early stopping makes every nonempty small-divisor row identically zero. The cutoff is the actual minimum of the distinguished-prime cutoff and the final permitted stopping-bin endpoint.

  1. lemma OAI.CubicFirstMoment.rough_filtered_row_zero line 14
  2. theorem OAI.CubicFirstMoment.rough_small_divisor_mass line 33
  3. theorem OAI.CubicFirstMoment.stoppedRowCoefficient_early_roughness line 55
  4. theorem OAI.CubicFirstMoment.stopped_early_small_divisor_mass line 72