OAI/NumberTheory/CubicMoment/Transform/MetaplecticUniformTruncation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform arbitrary-power truncation for the original weight family. The far-left line and the constant are chosen before the weight index.

  1. theorem OAI.CubicFirstMoment.UniformLogWeights.metaplectic_twisted_tail_natural_cutoff line 12
  2. theorem OAI.CubicFirstMoment.UniformLogWeights.metaplectic_twisted_tail_arbitrary_power line 38