Documentation

Mathlib.Probability.Distributions.Gamma

Gamma distributions over ℝ #

Define the gamma measure over the reals.

Main definitions #

theorem lintegral_Iic_eq_lintegral_Iio_add_Icc {y : } {z : } (f : ENNReal) (hzy : z y) :
∫⁻ (x : ) in Set.Iic y, f x = (∫⁻ (x : ) in Set.Iio z, f x) + ∫⁻ (x : ) in Set.Icc z y, f x

A Lebesgue Integral from -∞ to y can be expressed as the sum of one from -∞ to 0 and 0 to x

noncomputable def ProbabilityTheory.gammaPDFReal (a : ) (r : ) (x : ) :

The pdf of the gamma distribution depending on its scale and rate

Equations
Instances For
    noncomputable def ProbabilityTheory.gammaPDF (a : ) (r : ) (x : ) :

    The pdf of the gamma distribution, as a function valued in ℝ≥0∞

    Equations
    Instances For
      theorem ProbabilityTheory.gammaPDF_eq (a : ) (r : ) (x : ) :
      ProbabilityTheory.gammaPDF a r x = ENNReal.ofReal (if 0 x then r ^ a / Real.Gamma a * x ^ (a - 1) * Real.exp (-(r * x)) else 0)
      theorem ProbabilityTheory.gammaPDF_of_neg {a : } {r : } {x : } (hx : x < 0) :
      theorem ProbabilityTheory.gammaPDF_of_nonneg {a : } {r : } {x : } (hx : 0 x) :
      theorem ProbabilityTheory.lintegral_gammaPDF_of_nonpos {x : } {a : } {r : } (hx : x 0) :
      ∫⁻ (y : ) in Set.Iio x, ProbabilityTheory.gammaPDF a r y = 0

      The Lebesgue integral of the gamma pdf over nonpositive reals equals 0

      theorem ProbabilityTheory.gammaPDFReal_pos {x : } {a : } {r : } (ha : 0 < a) (hr : 0 < r) (hx : 0 < x) :

      The gamma pdf is positive for all positive reals

      theorem ProbabilityTheory.gammaPDFReal_nonneg {a : } {r : } (ha : 0 < a) (hr : 0 < r) (x : ) :

      The gamma pdf is nonnegative

      @[simp]
      theorem ProbabilityTheory.lintegral_gammaPDF_eq_one {a : } {r : } (ha : 0 < a) (hr : 0 < r) :
      ∫⁻ (x : ), ProbabilityTheory.gammaPDF a r x = 1

      The pdf of the gamma distribution integrates to 1

      Measure defined by the gamma distribution

      Equations
      Instances For

        CDF of the gamma distribution

        Equations
        Instances For
          theorem ProbabilityTheory.gammaCDFReal_eq_integral {a : } {r : } (ha : 0 < a) (hr : 0 < r) (x : ) :
          theorem ProbabilityTheory.gammaCDFReal_eq_lintegral {a : } {r : } (ha : 0 < a) (hr : 0 < r) (x : ) :
          (ProbabilityTheory.gammaCDFReal a r) x = (∫⁻ (x : ) in Set.Iic x, ProbabilityTheory.gammaPDF a r x).toReal