OAI/NumberTheory/CubicMoment/Transform/MetaplecticNegativeTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact completed tail split on the negative height dyad. The original Voronoi identity is evaluated at the reflected height.

  1. theorem OAI.CubicFirstMoment.metaplectic_completed_negative_tail_mean line 13