OAI/NumberTheory/CubicMoment/Transform/MetaplecticActualBlockMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The complete retained norm-block mean for the original coefficients. The supported parametrization and every free coefficient estimate are constructed from the precisely stated published Voronoi coefficient bound.

  1. theorem OAI.CubicFirstMoment.metaplectic_actual_norm_block_mean line 14