OAI/NumberTheory/CubicMoment/Estimates/PrimeGroupTailBilinear.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary logarithmic saving for the original small-B Gauss bilinear form, with an explicit outer-length logarithmic cutoff.

  1. theorem OAI.CubicFirstMoment.primeGroupTail_bilinear_log_saving line 12