OAI/NumberTheory/CubicMoment/Estimates/GammaInverseGrowth.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal Gamma has the coarse strip growth needed for the completed Hecke functions. This uses Euler's integral, reflection and recurrence.

  1. lemma OAI.CubicFirstMoment.gamma_inverse_reflection line 11
  2. lemma OAI.CubicFirstMoment.gamma_inverse_large_height_bound line 38
  3. theorem OAI.CubicFirstMoment.gammaInverseFiniteOrder line 65

    Source documentation

    The exact reciprocal-Gamma strip input is an elementary theorem.

    theorem gammaInverseFiniteOrder (a b : ℝ) : GammaInverseFiniteOrder a b := by
…

    Mentions: OAI.CubicFirstMoment.GammaInverseFiniteOrder