OAI/NumberTheory/CubicMoment/Estimates/TypeILowKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Identify the estimated Type-I row with the literal finite sum of the corrected Gauss kernel. The squarefree model and every phase are retained.

  1. lemma OAI.CubicFirstMoment.angularSmoothModel_finite line 13
  2. theorem OAI.CubicFirstMoment.lowTwistedTypeIRow_finite line 32