OAI/NumberTheory/CubicMoment/Estimates/SmallBNonzeroVariance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Nonzero arbitrary-coefficient variance in the small-B range. All common factors are retained; the exact zero mode is subtracted.

  1. theorem OAI.CubicFirstMoment.smallB_nonzero_variance_height_power line 14