OAI/NumberTheory/CubicMoment/Transform/MetaplecticInverseSplit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact short/long splitting of the original finite inverse completion. The short residue sum remains explicit, and vanishes at nonzero angular index.

  1. lemma OAI.CubicFirstMoment.primaryElementBall_filter_norm line 13
  2. theorem OAI.CubicFirstMoment.metaplectic_inverse_split line 23
  3. theorem OAI.CubicFirstMoment.metaplectic_angular_inverse_split line 53