OAI/NumberTheory/CubicMoment/Transform/MetaplecticSmallLow.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The counting bound at the source small-level cutoff X^(13/100), including the actual finite dyads and original logarithmic weights.

  1. theorem OAI.CubicFirstMoment.LogarithmicWeightFamily.metaplectic_long_small_power line 13