OAI/NumberTheory/CubicMoment/Estimates/GammaLeftLine.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A far-left bound for the gamma quotient, obtained directly from recurrence at half-integer real parts. No Stirling estimate is assumed.

  1. lemma OAI.CubicFirstMoment.half_sub_nat_regular line 12
  2. lemma OAI.CubicFirstMoment.norm_ascPochhammer_le line 24
  3. theorem OAI.CubicFirstMoment.norm_gamma_left_ratio_le line 44

    Source documentation

    The quotient on Re s = 1/2-m is a polynomial in norm of degree 2m, because the gamma arguments differ by the integer 2m after complex conjugation.

    theorem norm_gamma_left_ratio_le (m : ℕ) (u : ℝ) :
    ‖Complex.Gamma ((1/2:ℂ)+(m:ℂ)-(u:ℂ)*Complex.I) /
      Complex.Gamma ((1/2:ℂ)-(m:ℂ)+(u:ℂ)*Complex.I)‖ ≤
        (3*(m:ℝ)+1)^(2*m)*(1+|u|)^(2*m) := by
…