OAI/NumberTheory/CubicMoment/Transform/MetaplecticUniformShort.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The primal short-range estimate with a single constant before the weight index, obtained from common log support and derivative bounds.

  1. lemma OAI.CubicFirstMoment.uniform_short_square_root_factor line 13

    Also declared: OAI/NumberTheory/CubicMoment/Theta/CubicThetaUniformShort.lean:13 (same declaration text).

  2. theorem OAI.CubicFirstMoment.UniformLogWeights.metaplectic_completed_short_mean line 28