OAI/NumberTheory/CubicMoment/Transform/MetaplecticRadialModel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual radial model has the same finite residue density as the short inverse completion, up to the proved squarefree lattice error.

  1. lemma OAI.CubicFirstMoment.angularSmoothModel_const_mul line 14
  2. lemma OAI.CubicFirstMoment.radial_squarefree_main_scaled line 26
  3. theorem OAI.CubicFirstMoment.UniformLogWeights.radial_model_finite_error line 44
  4. theorem OAI.CubicFirstMoment.LogarithmicWeightFamily.radial_model_finite_error line 69