OAI/NumberTheory/CubicMoment/Theta/CubicThetaConstantContinuation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Continuation of the actual zero-frequency scattering coefficient. This does not assert continuation of the nonzero Fourier coefficients.

  1. def OAI.CubicFirstMoment.cubicThetaConstantContinuation line 12
  2. theorem OAI.CubicFirstMoment.cubicThetaConstantContinuation_right line 16
  3. lemma OAI.CubicFirstMoment.cubicTheta_principalZeta_analyticAt line 27
  4. lemma OAI.CubicFirstMoment.cubicTheta_principalZeta_two_ne_zero line 39
  5. def OAI.CubicFirstMoment.cubicThetaConstantRegular line 43
  6. lemma OAI.CubicFirstMoment.cubicThetaConstantRegular_analyticAt line 47
  7. lemma OAI.CubicFirstMoment.cubicThetaConstantRegular_eq line 82
  8. lemma OAI.CubicFirstMoment.cubicThetaConstantRegular_value line 88
  9. theorem OAI.CubicFirstMoment.cubicThetaConstantContinuation_residue line 95