OAI/NumberTheory/CubicMoment/Theta/CubicThetaGramIntegralDecomposition.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Legitimate finite splitting of the full Gram integral. Each summand is absolutely integrable with its original positive cutoffs.

  1. def OAI.CubicFirstMoment.cubicThetaGramIdentityPart line 14
  2. def OAI.CubicFirstMoment.cubicThetaGramPrimeFreePart line 18
  3. lemma OAI.CubicFirstMoment.cubicThetaGramIdentity_integrable line 23
  4. lemma OAI.CubicFirstMoment.cubicThetaGram_sum_integrable line 44
  5. theorem OAI.CubicFirstMoment.cubicThetaKloostermanGram_finite_integrals line 51
  6. theorem OAI.CubicFirstMoment.cubicThetaGramPrimePart_finite_integrals line 62
  7. theorem OAI.CubicFirstMoment.cubicThetaGramPrimeFreePart_finite_integrals line 71
  8. theorem OAI.CubicFirstMoment.cubicThetaKloostermanGram_prime_split line 80