OAI/NumberTheory/CubicMoment/Theta/CubicThetaGramPrimeMismatch.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Mismatched prime divisibility removes every higher prime-power denominator from the actual off-diagonal Gram kernel.

  1. lemma OAI.CubicFirstMoment.inverse_square_representative line 11
  2. theorem OAI.CubicFirstMoment.cubicThetaKloostermanSum_prime_mismatch_zero line 28
  3. theorem OAI.CubicFirstMoment.cubicThetaKloostermanSum_prime_mismatch_zero_symm line 50
  4. theorem OAI.CubicFirstMoment.cubicThetaKloostermanSum_primeFree_power_zero line 60