OAI/NumberTheory/CubicMoment/Decomposition/StoppedVarianceRemainder.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact restoration of the noncoprime part of a square-divisor variance. The bound uses active roughness of the original coefficient, which is preserved by the actual cubic divisor twist.

  1. theorem OAI.CubicFirstMoment.bounded_rough_divisor_variance_remainder line 12