OAI/NumberTheory/CubicMoment/Angular/AngularTruncatedDual.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact retained-plus-tail decomposition for a fixed angular Hecke series. The possible poles of the totalized Gamma denominator are handled using the entire completion, before any integration is performed.

  1. lemma OAI.CubicFirstMoment.angular_left_uncompleted line 14
  2. lemma OAI.CubicFirstMoment.angular_left_integrand_split line 45
  3. lemma OAI.CubicFirstMoment.angular_finite_dual_mellin_integrable line 67
  4. theorem OAI.CubicFirstMoment.angular_smooth_truncated_identity line 86