OAI/NumberTheory/CubicMoment/Estimates/LowCommonScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The residual norm factor is summable; it is retained through the common-divisor decomposition instead of discarded by monotonicity.

  1. lemma OAI.CubicFirstMoment.low_common_residual_scale line 10
  2. lemma OAI.CubicFirstMoment.low_common_floor_large line 40