OAI/NumberTheory/CubicMoment/Transform/MetaplecticLongCompletion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual long inverse-completion sum, collected by e=cd. The resulting weight is the proved tail coefficient, not an arbitrary divisor-bounded replacement.

  1. def OAI.CubicFirstMoment.metaplecticLongCompletion line 14
  2. theorem OAI.CubicFirstMoment.metaplectic_long_completion_collect line 20