OAI/NumberTheory/CubicMoment/Transform/MetaplecticLogCounting.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual long inverse-completion counting estimate for an arbitrary logarithmic weight family, with all outer coefficients kept.

  1. theorem OAI.CubicFirstMoment.LogarithmicWeightFamily.metaplectic_long_counting line 12