OAI/NumberTheory/CubicMoment/Estimates/SinglePrimeTransition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The cube bound at the transition keeps the coefficient l¹ mass, and the full prime variance keeps its diagonal l² mass.

  1. theorem OAI.CubicFirstMoment.prime_variance_transition_bound line 12