OAI/NumberTheory/CubicMoment/Decomposition/StoppedCommonPointwise.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Pointwise control of the actual shortened common-factor row. The bounded coefficient, not an assumed quotient cancellation property, is used after the exact normalized Gauss reparametrization.

  1. lemma OAI.CubicFirstMoment.bounded_common_residual_scale line 14
  2. theorem OAI.CubicFirstMoment.bounded_common_coprime_row_at_scale line 34
  3. theorem OAI.CubicFirstMoment.bounded_common_coprime_row line 78