Documentation

Mathlib.Probability.Distributions.Exponential

Exponential distributions over ℝ #

Define the Exponential measure over the reals.

Main definitions #

Main results #

noncomputable def ProbabilityTheory.exponentialPDFReal (r x : ) :

The pdf of the exponential distribution depending on its rate

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

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

    Equations
    Instances For

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

      The exponential pdf is measurable.

      The exponential pdf is positive for all positive reals

      The exponential pdf is nonnegative

      @[simp]

      The pdf of the exponential distribution integrates to 1

      Measure defined by the exponential distribution

      Equations
      Instances For

        A negative exponential function is integrable on intervals in R≥0

        The CDF of the exponential distribution equals 1 - exp (-(r * x))