OAI/NumberTheory/CubicMoment/Theta/CubicThetaProjectedConstant.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The actual radial constant in the adapted primary cusp. The arithmetic base scalar is retained, including after finite character averaging.

  1. lemma OAI.CubicFirstMoment.cubicThetaActualCuspConstant_adapted line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaNineGaussMatrix_constant line 33
  3. lemma OAI.CubicFirstMoment.cubicThetaResidueCuspMatrix_weighted_constant line 48
  4. def OAI.CubicFirstMoment.cubicThetaResidueConstant line 66
  5. lemma OAI.CubicFirstMoment.cubicThetaResidueConstant_units line 71