OAI/NumberTheory/CubicMoment/Transform/MetaplecticCompletedShort.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The short angular completed mean, with the fixed smooth weight's actual support and size bounds constructed, including the empty range.

  1. lemma OAI.CubicFirstMoment.metaplecticHeightCompleted_zero_of_small_support line 12
  2. lemma OAI.CubicFirstMoment.short_square_root_factor line 30
  3. theorem OAI.CubicFirstMoment.metaplectic_completed_short_mean line 45