OAI/NumberTheory/CubicMoment/Transform/MetaplecticLocalSeries.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The local absolute series in the level Voronoi formula. The two terms at each cube exponent are exactly the squarefree exponent 0 or 1. Their product over the level costs only an arbitrary norm power.

  1. def OAI.CubicFirstMoment.metaplecticLocalRatio line 13
  2. def OAI.CubicFirstMoment.metaplecticLocalTerms line 15
  3. def OAI.CubicFirstMoment.metaplecticLocalEuler line 19
  4. lemma OAI.CubicFirstMoment.metaplecticLocalRatio_bounds line 22
  5. theorem OAI.CubicFirstMoment.metaplecticLocalTerms_hasSum line 45
  6. lemma OAI.CubicFirstMoment.metaplecticLocalEuler_nonneg line 62
  7. lemma OAI.CubicFirstMoment.metaplecticLocalEuler_le_three line 70
  8. lemma OAI.CubicFirstMoment.primaryPrime_norm_two line 83
  9. theorem OAI.CubicFirstMoment.metaplectic_local_product_small_power line 94