OAI/NumberTheory/CubicMoment/Estimates/LargeCommonSaving.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every large common factor is controlled after its exact zero mode has been removed. The divisor-energy loss leaves a fixed power saving.

  1. theorem OAI.CubicFirstMoment.large_common_nonzero_power line 12