OAI/NumberTheory/CubicMoment/Estimates/PrimeTransitionScale.lean
2 declarations, 0 contain sorry, 0 declared as axioms
The diagonal and cube terms both give the required three-prime logarithmic saving after Cauchy--Schwarz.
- lemma
OAI.CubicFirstMoment.transition_diagonal_scaleline 10 - lemma
OAI.CubicFirstMoment.prime_transition_cauchy_scaleline 26