Documentation

Mathlib.Analysis.SpecialFunctions.Gamma.Basic

The Gamma function #

This file defines the Γ function (of a real or complex variable s). We define this by Euler's integral Γ(s) = ∫ x in Ioi 0, exp (-x) * x ^ (s - 1) in the range where this integral converges (i.e., for 0 < s in the real case, and 0 < re s in the complex case).

We show that this integral satisfies Γ(1) = 1 and Γ(s + 1) = s * Γ(s); hence we can define Γ(s) for all s as the unique function satisfying this recurrence and agreeing with Euler's integral in the convergence range. (If s = -n for n ∈ ℕ, then the function is undefined, and we set it to be 0 by convention.)

Gamma function: main statements (complex case) #

Gamma function: main statements (real case) #

Tags #

Gamma

theorem Real.Gamma_integrand_isLittleO (s : ) :
(fun (x : ) => Real.exp (-x) * x ^ s) =o[Filter.atTop] fun (x : ) => Real.exp (-(1 / 2) * x)

Asymptotic bound for the Γ function integrand.

theorem Real.GammaIntegral_convergent {s : } (h : 0 < s) :
MeasureTheory.IntegrableOn (fun (x : ) => Real.exp (-x) * x ^ (s - 1)) (Set.Ioi 0) MeasureTheory.volume

The Euler integral for the Γ function converges for positive real s.

theorem Complex.GammaIntegral_convergent {s : } (hs : 0 < s.re) :
MeasureTheory.IntegrableOn (fun (x : ) => (Real.exp (-x)) * x ^ (s - 1)) (Set.Ioi 0) MeasureTheory.volume

The integral defining the Γ function converges for complex s with 0 < re s.

This is proved by reduction to the real case.

Euler's integral for the Γ function (of a complex variable s), defined as ∫ x in Ioi 0, exp (-x) * x ^ (s - 1).

See Complex.GammaIntegral_convergent for a proof of the convergence of the integral for 0 < re s.

Equations
Instances For
    theorem Complex.GammaIntegral_conj (s : ) :
    ((starRingEnd ) s).GammaIntegral = (starRingEnd ) s.GammaIntegral
    theorem Complex.GammaIntegral_ofReal (s : ) :
    (s).GammaIntegral = (∫ (x : ) in Set.Ioi 0, Real.exp (-x) * x ^ (s - 1))

    Now we establish the recurrence relation Γ(s + 1) = s * Γ(s) using integration by parts.

    def Complex.partialGamma (s : ) (X : ) :

    The indefinite version of the Γ function, Γ(s, X) = ∫ x ∈ 0..X, exp(-x) x ^ (s - 1).

    Equations
    Instances For
      theorem Complex.tendsto_partialGamma {s : } (hs : 0 < s.re) :
      Filter.Tendsto (fun (X : ) => s.partialGamma X) Filter.atTop (nhds s.GammaIntegral)
      theorem Complex.partialGamma_add_one {s : } (hs : 0 < s.re) {X : } (hX : 0 X) :
      (s + 1).partialGamma X = s * s.partialGamma X - (Real.exp (-X)) * X ^ s

      The recurrence relation for the indefinite version of the Γ function.

      theorem Complex.GammaIntegral_add_one {s : } (hs : 0 < s.re) :
      (s + 1).GammaIntegral = s * s.GammaIntegral

      The recurrence relation for the Γ integral.

      Now we define Γ(s) on the whole complex plane, by recursion.

      noncomputable def Complex.GammaAux :

      The nth function in this family is Γ(s) if -n < s.re, and junk otherwise.

      Equations
      Instances For
        theorem Complex.GammaAux_recurrence1 (s : ) (n : ) (h1 : -s.re < n) :
        theorem Complex.GammaAux_recurrence2 (s : ) (n : ) (h1 : -s.re < n) :
        @[irreducible]
        def Complex.Gamma (s : ) :

        The Γ function (of a complex variable s).

        Equations
        Instances For
          theorem Complex.Gamma_eq_GammaAux (s : ) (n : ) (h1 : -s.re < n) :
          theorem Complex.Gamma_add_one (s : ) (h2 : s 0) :

          The recurrence relation for the Γ function.

          theorem Complex.Gamma_eq_integral {s : } (hs : 0 < s.re) :
          Complex.Gamma s = s.GammaIntegral
          theorem Complex.Gamma_nat_eq_factorial (n : ) :
          Complex.Gamma (n + 1) = n.factorial
          @[simp]
          theorem Complex.Gamma_ofNat_eq_factorial (n : ) [(n + 1).AtLeastTwo] :
          Complex.Gamma (OfNat.ofNat (n + 1)) = n.factorial
          @[simp]

          At 0 the Gamma function is undefined; by convention we assign it the value 0.

          At -n for n ∈ ℕ, the Gamma function is undefined; by convention we assign it the value 0.

          theorem Complex.integral_cpow_mul_exp_neg_mul_Ioi {a : } {r : } (ha : 0 < a.re) (hr : 0 < r) :
          ∫ (t : ) in Set.Ioi 0, t ^ (a - 1) * Complex.exp (-(r * t)) = (1 / r) ^ a * Complex.Gamma a

          Expresses the integral over Ioi 0 of t ^ (a - 1) * exp (-(r * t)) in terms of the Gamma function, for complex a.

          Now check that the Γ function is differentiable, wherever this makes sense.

          Rewrite the Gamma integral as an example of a Mellin transform.

          theorem Complex.hasDerivAt_GammaIntegral {s : } (hs : 0 < s.re) :
          HasDerivAt Complex.GammaIntegral (∫ (t : ) in Set.Ioi 0, t ^ (s - 1) * ((Real.log t) * (Real.exp (-t)))) s

          The derivative of the Γ integral, at any s ∈ ℂ with 1 < re s, is given by the Mellin transform of log t * exp (-t).

          theorem Complex.differentiableAt_GammaAux (s : ) (n : ) (h1 : 1 - s.re < n) (h2 : ∀ (m : ), s -m) :

          At s = 0, the Gamma function has a simple pole with residue 1.

          def Real.Gamma (s : ) :

          The Γ function (of a real variable s).

          Equations
          Instances For
            theorem Real.Gamma_eq_integral {s : } (hs : 0 < s) :
            Real.Gamma s = ∫ (x : ) in Set.Ioi 0, Real.exp (-x) * x ^ (s - 1)
            theorem Real.Gamma_add_one {s : } (hs : s 0) :
            @[simp]
            theorem Real.Gamma_nat_eq_factorial (n : ) :
            Real.Gamma (n + 1) = n.factorial
            @[simp]
            theorem Real.Gamma_ofNat_eq_factorial (n : ) [(n + 1).AtLeastTwo] :
            Real.Gamma (OfNat.ofNat (n + 1)) = n.factorial
            @[simp]

            At 0 the Gamma function is undefined; by convention we assign it the value 0.

            At -n for n ∈ ℕ, the Gamma function is undefined; by convention we assign it the value 0.

            theorem Real.Gamma_pos_of_pos {s : } (hs : 0 < s) :
            theorem Real.integral_rpow_mul_exp_neg_mul_Ioi {a : } {r : } (ha : 0 < a) (hr : 0 < r) :
            ∫ (t : ) in Set.Ioi 0, t ^ (a - 1) * Real.exp (-(r * t)) = (1 / r) ^ a * Real.Gamma a

            Expresses the integral over Ioi 0 of t ^ (a - 1) * exp (-(r * t)), for positive real r, in terms of the Gamma function.

            The positivity extension which identifies expressions of the form Gamma a.

            Instances For
              theorem Real.Gamma_ne_zero {s : } (hs : ∀ (m : ), s -m) :

              The Gamma function does not vanish on (except at non-positive integers, where the function is mathematically undefined and we set it to 0 by convention).

              theorem Real.Gamma_eq_zero_iff (s : ) :
              Real.Gamma s = 0 ∃ (m : ), s = -m
              theorem Real.differentiableAt_Gamma {s : } (hs : ∀ (m : ), s -m) :