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.

      theorem ProbabilityTheory.exponentialPDFReal_pos {x r : } (hr : 0 < r) (hx : 0 < x) :

      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
        @[deprecated ProbabilityTheory.isProbabilityMeasure_expMeasure (since := "2025-08-29")]

        Alias of ProbabilityTheory.isProbabilityMeasure_expMeasure.

        @[deprecated "Use `cdf (expMeasure r)` instead." (since := "2025-08-28")]

        CDF of the exponential distribution

        Equations
        Instances For
          @[deprecated ProbabilityTheory.cdf_expMeasure_eq_integral (since := "2025-08-28")]

          Alias of ProbabilityTheory.cdf_expMeasure_eq_integral.

          @[deprecated ProbabilityTheory.cdf_expMeasure_eq_lintegral (since := "2025-08-28")]

          Alias of ProbabilityTheory.cdf_expMeasure_eq_lintegral.

          theorem ProbabilityTheory.hasDerivAt_neg_exp_mul_exp {r x : } :
          HasDerivAt (fun (a : ) => -Real.exp (-(r * a))) (r * Real.exp (-(r * x))) x

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

          theorem ProbabilityTheory.cdf_expMeasure_eq {r : } (hr : 0 < r) (x : ) :
          (cdf (expMeasure r)) x = if 0 x then 1 - Real.exp (-(r * x)) else 0

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

          @[deprecated ProbabilityTheory.cdf_expMeasure_eq (since := "2025-08-28")]
          theorem ProbabilityTheory.exponentialCDFReal_eq {r : } (hr : 0 < r) (x : ) :
          (cdf (expMeasure r)) x = if 0 x then 1 - Real.exp (-(r * x)) else 0

          Alias of ProbabilityTheory.cdf_expMeasure_eq.


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