OAI/NumberTheory/CubicMoment/Estimates/GammaQuotientGrowth.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The bounded-strip Gamma quotient follows from the Beta integral and integer recurrence, with the fixed angular shift retained.

  1. lemma OAI.CubicFirstMoment.pochhammer_norm_bound line 12
  2. lemma OAI.CubicFirstMoment.gamma_positive_ratio_compact line 28
  3. theorem OAI.CubicFirstMoment.angularGammaQuotientStripBound_proved line 65

    Source documentation

    The exact fixed-angular quotient input used by the conditional proof.

    theorem angularGammaQuotientStripBound_proved (k a : ℝ) (hk : -(1/2:ℝ) < k) :
    AngularGammaQuotientStripBound k a := by
…

    Mentions: OAI.CubicFirstMoment.AngularGammaQuotientStripBound