OAI/NumberTheory/CubicMoment/Theta/CubicThetaUniformShort.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform finite primal bound on the enlarged transition range required by the actual fixed theta dilation.

  1. lemma OAI.CubicFirstMoment.uniform_short_square_root_factor line 13

    Also declared: OAI/NumberTheory/CubicMoment/Transform/MetaplecticUniformShort.lean:13 (same declaration text).

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