OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialLongScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Put the two actual radial remainder means back on the original scale. The fixed factor 729 changes only the uniform constant.

  1. theorem OAI.CubicFirstMoment.UniformLogWeights.cubicTheta_radial_remainder_long_mean line 13
  2. theorem OAI.CubicFirstMoment.UniformLogWeights.cubicTheta_radial_remainder_negative_long_mean line 45