OAI/NumberTheory/CubicMoment/Estimates/TypeIMixedLow.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Type I with the precise radial factor in the mixed term of the corrected square. The squarefree product model, including common zeros, is preserved on the right.

  1. theorem OAI.CubicFirstMoment.typeI_mixed_low_of_published line 12