OAI/NumberTheory/CubicMoment/Transform/MetaplecticLargeLow.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual long inverse tail in the large-level branch of low Type I. The source cutoff is X^(1/50); the completion cutoff is the harmless X^2.

  1. theorem OAI.CubicFirstMoment.LogarithmicWeightFamily.metaplectic_long_large_power line 14