OAI/NumberTheory/CubicMoment/Transform/MetaplecticHarmonic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite d-sum in the retained angular estimate costs an arbitrarily small power of its cutoff. The proof uses the already proved convergent Eisenstein norm series.

  1. theorem OAI.CubicFirstMoment.primary_finite_harmonic_power line 12