OAI/NumberTheory/CubicMoment/Theta/CubicThetaProjectedRadialPoles.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual primary-projected radial continuation has one pole in each half-plane. Its residue retains the genuine arithmetic scalar.

  1. lemma OAI.CubicFirstMoment.cubicThetaSelectedRadialTail_entire line 13
  2. lemma OAI.CubicFirstMoment.cubicThetaProjectedRadialTail_entire line 19
  3. lemma OAI.CubicFirstMoment.cubicThetaSelectedRadialCompleted_meromorphic line 25
  4. lemma OAI.CubicFirstMoment.cubicThetaProjectedRadialCompleted_meromorphic line 33
  5. lemma OAI.CubicFirstMoment.radial_pole_limit line 41
  6. lemma OAI.CubicFirstMoment.cubicThetaSelectedRadialCompleted_residue line 55
  7. lemma OAI.CubicFirstMoment.cubicThetaProjectedRadialCompleted_residue line 63
  8. lemma OAI.CubicFirstMoment.cubicThetaSelectedRadialCompleted_initial line 74
  9. lemma OAI.CubicFirstMoment.cubicThetaProjectedRadialCompleted_initial line 91