OAI/NumberTheory/CubicMoment/Estimates/PrincipalZetaPole.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

An analytic, nonzero numerator for the simple pole at one of the actual principal ideal zeta function.

  1. def OAI.CubicFirstMoment.principalZetaPrefactor line 12
  2. lemma OAI.CubicFirstMoment.principalZetaPrefactor_differentiable line 15
  3. def OAI.CubicFirstMoment.principalZetaRegularFactor line 21
  4. lemma OAI.CubicFirstMoment.principalZetaRegularFactor_analyticAt_one line 25
  5. lemma OAI.CubicFirstMoment.principalZetaRegularFactor_one line 34
  6. lemma OAI.CubicFirstMoment.principalZetaRegularFactor_one_ne_zero line 39
  7. lemma OAI.CubicFirstMoment.principalZetaRegularFactor_eq line 44
  8. theorem OAI.CubicFirstMoment.principalIdealZeta_residue_one line 54