Documentation

Mathlib.Analysis.SpecialFunctions.Gamma.Beta

The Beta function, and further properties of the Gamma function #

In this file we define the Beta integral, relate Beta and Gamma functions, and prove some refined properties of the Gamma function using these relations.

Results on the Beta function #

Results on the Gamma function #

The Beta function #

noncomputable def Complex.betaIntegral (u : ) (v : ) :

The Beta function Β (u, v), defined as ∫ x:ℝ in 0..1, x ^ (u - 1) * (1 - x) ^ (v - 1).

Equations
  • u.betaIntegral v = ∫ (x : ) in 0 ..1, x ^ (u - 1) * (1 - x) ^ (v - 1)
Instances For
    theorem Complex.betaIntegral_convergent_left {u : } (hu : 0 < u.re) (v : ) :
    IntervalIntegrable (fun (x : ) => x ^ (u - 1) * (1 - x) ^ (v - 1)) MeasureTheory.volume 0 (1 / 2)

    Auxiliary lemma for betaIntegral_convergent, showing convergence at the left endpoint.

    theorem Complex.betaIntegral_convergent {u : } {v : } (hu : 0 < u.re) (hv : 0 < v.re) :
    IntervalIntegrable (fun (x : ) => x ^ (u - 1) * (1 - x) ^ (v - 1)) MeasureTheory.volume 0 1

    The Beta integral is convergent for all u, v of positive real part.

    theorem Complex.betaIntegral_symm (u : ) (v : ) :
    v.betaIntegral u = u.betaIntegral v
    theorem Complex.betaIntegral_eval_one_right {u : } (hu : 0 < u.re) :
    u.betaIntegral 1 = 1 / u
    theorem Complex.betaIntegral_scaled (s : ) (t : ) {a : } (ha : 0 < a) :
    ∫ (x : ) in 0 ..a, x ^ (s - 1) * (a - x) ^ (t - 1) = a ^ (s + t - 1) * s.betaIntegral t
    theorem Complex.Gamma_mul_Gamma_eq_betaIntegral {s : } {t : } (hs : 0 < s.re) (ht : 0 < t.re) :
    Complex.Gamma s * Complex.Gamma t = Complex.Gamma (s + t) * s.betaIntegral t

    Relation between Beta integral and Gamma function.

    theorem Complex.betaIntegral_recurrence {u : } {v : } (hu : 0 < u.re) (hv : 0 < v.re) :
    u * u.betaIntegral (v + 1) = v * (u + 1).betaIntegral v

    Recurrence formula for the Beta function.

    theorem Complex.betaIntegral_eval_nat_add_one_right {u : } (hu : 0 < u.re) (n : ) :
    u.betaIntegral (n + 1) = n.factorial / jFinset.range (n + 1), (u + j)

    Explicit formula for the Beta function when second argument is a positive integer.

    The Euler limit formula #

    noncomputable def Complex.GammaSeq (s : ) (n : ) :

    The sequence with n-th term n ^ s * n! / (s * (s + 1) * ... * (s + n)), for complex s. We will show that this tends to Γ(s) as n → ∞.

    Equations
    Instances For
      theorem Complex.GammaSeq_eq_betaIntegral_of_re_pos {s : } (hs : 0 < s.re) (n : ) :
      s.GammaSeq n = n ^ s * s.betaIntegral (n + 1)
      theorem Complex.GammaSeq_add_one_left (s : ) {n : } (hn : n 0) :
      (s + 1).GammaSeq n / s = n / (n + 1 + s) * s.GammaSeq n
      theorem Complex.GammaSeq_eq_approx_Gamma_integral {s : } (hs : 0 < s.re) {n : } (hn : n 0) :
      s.GammaSeq n = ∫ (x : ) in 0 ..n, ((1 - x / n) ^ n) * x ^ (s - 1)
      theorem Complex.approx_Gamma_integral_tendsto_Gamma_integral {s : } (hs : 0 < s.re) :
      Filter.Tendsto (fun (n : ) => ∫ (x : ) in 0 ..n, ((1 - x / n) ^ n) * x ^ (s - 1)) Filter.atTop (nhds (Complex.Gamma s))

      The main technical lemma for GammaSeq_tendsto_Gamma, expressing the integral defining the Gamma function for 0 < re s as the limit of a sequence of integrals over finite intervals.

      theorem Complex.GammaSeq_tendsto_Gamma (s : ) :
      Filter.Tendsto s.GammaSeq Filter.atTop (nhds (Complex.Gamma s))

      Euler's limit formula for the complex Gamma function.

      The reflection formula #

      theorem Complex.GammaSeq_mul (z : ) {n : } (hn : n 0) :
      z.GammaSeq n * (1 - z).GammaSeq n = n / (n + 1 - z) * (1 / (z * jFinset.range n, (1 - z ^ 2 / (j + 1) ^ 2)))

      Euler's reflection formula for the complex Gamma function.

      theorem Complex.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 Complex.Gamma_eq_zero_iff (s : ) :
      Complex.Gamma s = 0 ∃ (m : ), s = -m
      theorem Complex.Gamma_ne_zero_of_re_pos {s : } (hs : 0 < s.re) :

      A weaker, but easier-to-apply, version of Complex.Gamma_ne_zero.

      noncomputable def Real.GammaSeq (s : ) (n : ) :

      The sequence with n-th term n ^ s * n! / (s * (s + 1) * ... * (s + n)), for real s. We will show that this tends to Γ(s) as n → ∞.

      Equations
      Instances For
        theorem Real.GammaSeq_tendsto_Gamma (s : ) :
        Filter.Tendsto s.GammaSeq Filter.atTop (nhds (Real.Gamma s))

        Euler's limit formula for the real Gamma function.

        Euler's reflection formula for the real Gamma function.

        The reciprocal Gamma function #

        We show that the reciprocal Gamma function 1 / Γ(s) is entire. These lemmas show that (in this case at least) mathlib's conventions for division by zero do actually give a mathematically useful answer! (These results are useful in the theory of zeta and L-functions.)

        A reformulation of the Gamma recurrence relation which is true for s = 0 as well.

        The reciprocal of the Gamma function is differentiable everywhere (including the points where Gamma itself is not).

        The doubling formula for Gamma #

        We prove the doubling formula for arbitrary real or complex arguments, by analytic continuation from the positive real case. (Knowing that Γ⁻¹ is analytic everywhere makes this much simpler, since we do not have to do any special-case handling for the poles of Γ.)