OAI/NumberTheory/CubicMoment/Transform/MetaplecticTailDyad.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual long-completion dyad obeys the cubic-sieve estimate. This theorem retains the original outer coefficients and all e-dependent coprimality restrictions instead of bounding them by an abstract family.

  1. theorem OAI.CubicFirstMoment.UniformLogWeights.metaplectic_tail_dyad_sieve line 12