OAI/NumberTheory/CubicMoment/Transform/MetaplecticLongSieve.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The canonical finite dyads sum to the actual long inverse completion. The squared estimate keeps the square of the number of active dyads.

  1. lemma OAI.CubicFirstMoment.metaplecticLongDyad_scale line 12
  2. lemma OAI.CubicFirstMoment.metaplectic_long_outer_partition line 18
  3. lemma OAI.CubicFirstMoment.metaplectic_long_cutoff_ratio line 41
  4. lemma OAI.CubicFirstMoment.metaplectic_long_dyad_power line 51
  5. theorem OAI.CubicFirstMoment.LogarithmicWeightFamily.metaplectic_long_sieve line 61