OAI/NumberTheory/CubicMoment/Transform/MetaplecticShortLogInverse.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The short inverse-completion error for the original logarithmically varying weights, in both the radial and fixed angular modes.

  1. lemma OAI.CubicFirstMoment.metaplecticCompleted_const_mul line 13
  2. lemma OAI.CubicFirstMoment.metaplecticMain_const_mul line 25
  3. lemma OAI.CubicFirstMoment.metaplecticShortCompletionError_const_mul line 36
  4. theorem OAI.CubicFirstMoment.LogarithmicWeightFamily.metaplectic_short_completion_error line 47