Exponential distributions over ℝ

Define the Exponential measure over the reals.

Main definitions

• exponentialPDFReal: the function r x ↦ r * exp (-(r * x) for 0 ≤ x or 0 else, which is the probability density function of a exponential distribution with rate r (when hr : 0 < r).
• exponentialPDF: ℝ≥0∞-valued pdf, exponentialPDF r = ENNReal.ofReal (exponentialPDFReal r).
• expMeasure: an exponential measure on ℝ, parametrized by its rate r.
• exponentialCDFReal: the CDF given by the definition of CDF in ProbabilityTheory.CDF applied to the exponential measure.

Main results

• exponentialCDFReal_eq: Proof that the exponentialCDFReal given by the definition equals the known function given as r x ↦ 1 - exp (- (r * x)) for 0 ≤ x or 0 else.

noncomputable def ProbabilityTheory.exponentialPDFReal (r x : ℝ) : ℝ

The pdf of the exponential distribution depending on its rate

noncomputable def ProbabilityTheory.exponentialPDF (r x : ℝ) : ENNReal

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

theorem ProbabilityTheory.exponentialPDF_eq (r x : ℝ) : exponentialPDF r x = ENNReal.ofReal (if 0 ≤ x then r * Real.exp (-(r * x)) else 0)

theorem ProbabilityTheory.exponentialPDF_of_neg {r x : ℝ} (hx : x < 0) : exponentialPDF r x = 0

theorem ProbabilityTheory.exponentialPDF_of_nonneg {r x : ℝ} (hx : 0 ≤ x) : exponentialPDF r x = ENNReal.ofReal (r * Real.exp (-(r * x)))

theorem ProbabilityTheory.lintegral_exponentialPDF_of_nonpos {x r : ℝ} (hx : x ≤ 0) : ∫⁻ (y : ℝ) in Set.Iio x, exponentialPDF r y = 0

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

theorem ProbabilityTheory.measurable_exponentialPDFReal (r : ℝ) : Measurable (exponentialPDFReal r)

The exponential pdf is measurable.

theorem ProbabilityTheory.stronglyMeasurable_exponentialPDFReal (r : ℝ) : MeasureTheory.StronglyMeasurable (exponentialPDFReal r)

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

The exponential pdf is positive for all positive reals

theorem ProbabilityTheory.exponentialPDFReal_nonneg {r : ℝ} (hr : 0 < r) (x : ℝ) : 0 ≤ exponentialPDFReal r x

The exponential pdf is nonnegative

@[simp]

theorem ProbabilityTheory.lintegral_exponentialPDF_eq_one {r : ℝ} (hr : 0 < r) : ∫⁻ (x : ℝ), exponentialPDF r x = 1

The pdf of the exponential distribution integrates to 1

noncomputable def ProbabilityTheory.expMeasure (r : ℝ) : MeasureTheory.Measure ℝ

Measure defined by the exponential distribution

theorem ProbabilityTheory.isProbabilityMeasureExponential {r : ℝ} (hr : 0 < r) : MeasureTheory.IsProbabilityMeasure (expMeasure r)

noncomputable def ProbabilityTheory.exponentialCDFReal (r : ℝ) : StieltjesFunction

CDF of the exponential distribution

theorem ProbabilityTheory.exponentialCDFReal_eq_integral {r : ℝ} (hr : 0 < r) (x : ℝ) : ↑(exponentialCDFReal r) x = ∫ (x : ℝ) in Set.Iic x, exponentialPDFReal r x

theorem ProbabilityTheory.exponentialCDFReal_eq_lintegral {r : ℝ} (hr : 0 < r) (x : ℝ) : ↑(exponentialCDFReal r) x = (∫⁻ (x : ℝ) in Set.Iic x, exponentialPDF r x).toReal

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

theorem ProbabilityTheory.exp_neg_integrableOn_Ioc {b x : ℝ} (hb : 0 < b) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Real.exp (-(b * x))) (Set.Ioc 0 x) MeasureTheory.volume

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

theorem ProbabilityTheory.lintegral_exponentialPDF_eq_antiDeriv {r : ℝ} (hr : 0 < r) (x : ℝ) : ∫⁻ (y : ℝ) in Set.Iic x, exponentialPDF r y = ENNReal.ofReal (if 0 ≤ x then 1 - Real.exp (-(r * x)) else 0)

theorem ProbabilityTheory.exponentialCDFReal_eq {r : ℝ} (hr : 0 < r) (x : ℝ) : ↑(exponentialCDFReal r) x = if 0 ≤ x then 1 - Real.exp (-(r * x)) else 0

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