OAI/NumberTheory/CubicMoment/Theta/CubicThetaBaseScalarReal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual base scalar is real. This uses exact conjugation of the arithmetic series and its proved inversion law; it does not set the scalar or its absolute value equal to one.

  1. lemma OAI.CubicFirstMoment.cubicThetaArithmetic_axis_term_star line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaArithmeticAxis_star line 27
  3. lemma OAI.CubicFirstMoment.cubicThetaSeriesConstant_star line 37
  4. theorem OAI.CubicFirstMoment.cubicThetaArithmeticBaseScalar_star line 54