OAI/NumberTheory/CubicMoment/Transform/MetaplecticShortOuter.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual short inverse-completion error after summing the level coefficients. This is the common radial/angular short-error term.

  1. lemma OAI.CubicFirstMoment.short_completion_level_scale line 12
  2. theorem OAI.CubicFirstMoment.LogarithmicWeightFamily.metaplectic_short_outer_error line 19