OAI/NumberTheory/CubicMoment/Transform/MetaplecticRadialResidue.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The radial model and the short inverse residue differ only by the proved squarefree lattice error and an absolutely convergent Euler tail.

  1. lemma OAI.CubicFirstMoment.UniformLogWeights.radial_main_bound line 12
  2. theorem OAI.CubicFirstMoment.UniformLogWeights.radial_short_model_error line 41
  3. theorem OAI.CubicFirstMoment.LogarithmicWeightFamily.radial_short_model_error line 80