OAI/NumberTheory/CubicMoment/Decomposition/StoppedCommonTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The nonunit common-factor weight has a genuine roughness saving. Its small-power cost is charged to the common factor itself, never to an ambient coefficient length.

  1. theorem OAI.CubicFirstMoment.rough_common_factor_weight_tail line 12