OAI/NumberTheory/CubicMoment/Transform/MetaplecticLogTail.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The long-tail cubic estimate for the original logarithmically varying weights, obtained by exact scalar normalization.

  1. lemma OAI.CubicFirstMoment.metaplecticAngularSmoothSum_const_mul line 12
  2. lemma OAI.CubicFirstMoment.logarithmic_tail_energy line 22
  3. theorem OAI.CubicFirstMoment.LogarithmicWeightFamily.metaplectic_tail_dyad_sieve line 43