OAI/NumberTheory/CubicGram/NormRecurrence.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Divisor-completed energies and the coprime Poisson norm recurrence.

  1. lemma OAI.CubicFirstMoment.divisorCompleted_energy_le line 16
  2. lemma OAI.CubicFirstMoment.coprimeNormMajorant_le_divisorEnergy line 38
  3. def OAI.CubicFirstMoment.sievePrimeSet line 62
  4. lemma OAI.CubicFirstMoment.sievePrimeSet_primary line 65
  5. lemma OAI.CubicFirstMoment.factors_subset_sievePrimeSet line 71
  6. def OAI.CubicFirstMoment.gaussRowCoefficient line 80
  7. lemma OAI.CubicFirstMoment.gaussRowCoefficient_norm_sq line 83
  8. def OAI.CubicFirstMoment.coprimePoissonDyad line 90
  9. lemma OAI.CubicFirstMoment.gramDyadTerm_separated line 96
  10. lemma OAI.CubicFirstMoment.coprimePoissonDyad_separated line 117
  11. lemma OAI.CubicFirstMoment.gaussRowCoefficient_divisor_energy line 143
  12. theorem OAI.CubicFirstMoment.coprimePoissonDyad_norm_recurrence line 154