OAI/NumberTheory/CubicMoment/Estimates/ArithmeticTwist.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Twisting actual ideal arithmetic functions by a residue character and norm phase commutes with convolution. Different original factors may therefore retain different Mellin heights throughout short inversion.

  1. def OAI.CubicFirstMoment.residueNormTwist line 15
  2. lemma OAI.CubicFirstMoment.residueNormTwist_add line 19
  3. def OAI.CubicFirstMoment.twistArithmetic line 27
  4. lemma OAI.CubicFirstMoment.twistArithmetic_mul line 31
  5. lemma OAI.CubicFirstMoment.twistArithmetic_add line 48
  6. lemma OAI.CubicFirstMoment.twistArithmetic_sub line 57
  7. lemma OAI.CubicFirstMoment.twistArithmetic_coeff_primary line 66