OAI/NumberTheory/CubicMoment/Transform/MetaplecticSmoothScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Elementary scale regularity of the actual completed smooth sums. Compact support makes every scale neighborhood a common finite sum.

  1. lemma OAI.CubicFirstMoment.metaplectic_completed_scale_finite line 14
  2. lemma OAI.CubicFirstMoment.continuousOn_metaplecticCompleted_scale line 23
  3. lemma OAI.CubicFirstMoment.metaplecticCompleted_scale_small line 53