OAI/NumberTheory/CubicMoment/Transform/MetaplecticRadialDensity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Identification of the radial lattice density with the literal metaplectic residue constant.

  1. lemma OAI.CubicFirstMoment.integral_radial_model_weight line 14
  2. lemma OAI.CubicFirstMoment.primaryCoprimeRadialMain_eq line 23
  3. lemma OAI.CubicFirstMoment.cStar_primary_area_constant line 43
  4. lemma OAI.CubicFirstMoment.metaplectic_radial_density_scale line 57