OAI/NumberTheory/CubicMoment/Theta/CubicThetaCompletedShort.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite primal estimate covers the fixed transition range in the actual theta normalization by an exact dilation of its smooth weight.

  1. def OAI.CubicFirstMoment.cubicThetaDilatedWeight line 10
  2. lemma OAI.CubicFirstMoment.cubicThetaDilatedWeight_compact line 12
  3. lemma OAI.CubicFirstMoment.cubicThetaDilatedWeight_continuous line 18
  4. lemma OAI.CubicFirstMoment.cubicThetaHeight_dilated line 21
  5. theorem OAI.CubicFirstMoment.cubicTheta_completed_short_mean line 30