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

Equations

• ProbabilityTheory.exponentialPDFReal r x = ProbabilityTheory.gammaPDFReal 1 r x

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

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

Equations

• ProbabilityTheory.exponentialPDF r x = ENNReal.ofReal (ProbabilityTheory.exponentialPDFReal r x)

theorem ProbabilityTheory.exponentialPDF_eq (r x : ℝ) : ProbabilityTheory.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) : ProbabilityTheory.exponentialPDF r x = 0

theorem ProbabilityTheory.exponentialPDF_of_nonneg {r x : ℝ} (hx : 0 ≤ x) : ProbabilityTheory.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, ProbabilityTheory.exponentialPDF r y = 0

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

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

The exponential pdf is measurable.

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

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

The exponential pdf is positive for all positive reals

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

The exponential pdf is nonnegative

@[simp]

theorem ProbabilityTheory.lintegral_exponentialPDF_eq_one {r : ℝ} (hr : 0 < r) : ∫⁻ (x : ℝ), ProbabilityTheory.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

Equations

• ProbabilityTheory.expMeasure r = ProbabilityTheory.gammaMeasure 1 r

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

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

CDF of the exponential distribution

Equations

• ProbabilityTheory.exponentialCDFReal r = ProbabilityTheory.cdf (ProbabilityTheory.expMeasure r)

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

theorem ProbabilityTheory.exponentialCDFReal_eq_lintegral {r : ℝ} (hr : 0 < r) (x : ℝ) : ↑(ProbabilityTheory.exponentialCDFReal r) x = (∫⁻ (x : ℝ) in Set.Iic x, ProbabilityTheory.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, ProbabilityTheory.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 : ℝ) : ↑(ProbabilityTheory.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))