OAI/NumberTheory/CubicMoment/Theta/CubicThetaRadialRegularization.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Explicit removal of the actual radial pole. The residue is retained as the computed cusp constant; no normalization of that constant is assumed.

  1. def OAI.CubicFirstMoment.cubicThetaSelectedRadialTail line 12
  2. lemma OAI.CubicFirstMoment.cubicThetaSelectedRadialTail_differentiable line 17
  3. def OAI.CubicFirstMoment.cubicThetaSelectedRadialResidue line 23
  4. def OAI.CubicFirstMoment.cubicThetaSelectedRadialRegularized line 27
  5. lemma OAI.CubicFirstMoment.cubicThetaSelectedRadialRegularized_differentiable line 32
  6. lemma OAI.CubicFirstMoment.cubicThetaSelectedRadialRegularized_eq line 38
  7. lemma OAI.CubicFirstMoment.cubicThetaSelectedRadialRegularized_at_pole line 50
  8. def OAI.CubicFirstMoment.cubicThetaSelectedRadialHolomorphicPart line 57
  9. lemma OAI.CubicFirstMoment.cubicThetaSelectedRadialHolomorphicPart_differentiable line 63
  10. lemma OAI.CubicFirstMoment.cubicThetaSelectedRadialDirichlet_pole_decomposition line 71