OAI/NumberTheory/CubicMoment/Estimates/MixedPrimitiveData.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Chosen arithmetic data for the actual primitive mixed character. All fields are proved from the original squarefree coprime pair.

  1. structure OAI.CubicFirstMoment.MixedPrimitiveData line 11
  2. def OAI.CubicFirstMoment.mixedPrimitiveData line 23
  3. lemma OAI.CubicFirstMoment.MixedPrimitiveData.norm_le line 38
  4. lemma OAI.CubicFirstMoment.residueHeckeScale_sq line 47
  5. lemma OAI.CubicFirstMoment.MixedPrimitiveData.scale_sq_le line 52