OAI/NumberTheory/CubicMoment/Estimates/CubicNumeratorNonprincipal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Nontrivial cubic numerator characters in the squarefree primary case, using the mixed-character Fourier witness and reciprocity.

  1. lemma OAI.CubicFirstMoment.cubicNumeratorChar_squarefree_nonprincipal line 11
  2. lemma OAI.CubicFirstMoment.cubicNumeratorChar_squarefree_nonreal line 27