Exponential distribution

LemmaExponential density as an indicator on the half-line#✓fully proved

The rate-r exponential density times f, as an indicator on Ici 0.

lemma gammaPDFReal_one_eq_indicator {r : ℝ} (f : ℝ → ℝ) :
    (fun x => gammaPDFReal 1 r x * f x)
      = (Ici (0 : ℝ)).indicator (fun x => r * exp (-(r * x)) * f x)

Used by 2

Used byIntegrability criterion for the exponential law · Integrals against the exponential law

TheoremIntegrals against the exponential law#✓fully proved

Integrals against the exponential law of rate r > 0 are integrals of r * exp (-(r * x)) * f x over (0, ∞).

theorem integral_expMeasure_eq_setIntegral {r : ℝ} (hr : 0 < r) (f : ℝ → ℝ) :
    ∫ x, f x ∂(expMeasure r) = ∫ x in Ioi 0, r * exp (-(r * x)) * f x

Uses 1 · Used by 3

Proof usesExponential density as an indicator on the half-line

Used byMoments of the exponential law · Restart law at a fixed time · Kolmogorov

TheoremIntegrability criterion for the exponential law#✓fully proved

A function is integrable against the exponential law of rate r > 0 iff r * exp (-(r * x)) * f x is integrable on (0, ∞).

theorem integrable_expMeasure_iff {r : ℝ} (hr : 0 < r) {f : ℝ → ℝ} :
    Integrable f (expMeasure r)
      ↔ IntegrableOn (fun x => r * exp (-(r * x)) * f x) (Ioi 0)

Uses 1 · Used by 2

Proof usesExponential density as an indicator on the half-line

Used byFiniteness of all moments of the exponential law · Kolmogorov

LemmaPower times exponential density in gamma-integrand form#✓fully proved

Rewriting x ^ n times the exponential density in the gamma-integrand form.

lemma pow_eq_rpow_mul_exp (r x : ℝ) (n : ℕ) :
    r * exp (-(r * x)) * x ^ n = r * (x ^ (((n + 1 : ℕ) : ℝ) - 1) * exp (-(r * x)))

Used by 2

Used byFiniteness of all moments of the exponential law · Moments of the exponential law

TheoremFiniteness of all moments of the exponential law#✓fully proved

All moments of the exponential law are finite.

theorem integrable_pow_expMeasure {r : ℝ} (hr : 0 < r) (n : ℕ) :
    Integrable (fun x => x ^ n) (expMeasure r)

Uses 3 · Used by 9

Proof usesIntegrability of the scaled gamma integrand · Integrability criterion for the exponential law · Power times exponential density in gamma-integrand form

Used byVariance of the time to the most recent common ancestor · Covariance of π and S · Pair coalescence time against the total branch length · Variance of the mean number of pairwise differences · Variance of the total branch length · Integrability of the identity under the exponential law · Variance of the exponential law · Product moment of two hitting times, first-step equation · Minimality of the product moment

TheoremMoments of the exponential law#✓fully proved

The n-th moment of the exponential law of rate r > 0 is n! / r ^ n.

theorem integral_pow_expMeasure {r : ℝ} (hr : 0 < r) (n : ℕ) :
    ∫ x, x ^ n ∂(expMeasure r) = n ! / r ^ n

Uses 2 · Used by 2

Proof usesIntegrals against the exponential law · Power times exponential density in gamma-integrand form

Used byMean of the exponential law · Second moment of the exponential law

TheoremIntegrability of the identity under the exponential law#✓fully proved

The identity is integrable against the exponential law.

theorem integrable_id_expMeasure {r : ℝ} (hr : 0 < r) : Integrable id (expMeasure r)

Uses 1 · Used by 6

Proof usesFiniteness of all moments of the exponential law

Used byExponentially distributed random variables are integrable · Non-explosion · Mean hitting time, first-step equation · Minimality of the mean hitting time · Product moment of two hitting times, first-step equation · Minimality of the product moment

TheoremMean of the exponential law#✓fully proved

The mean of the exponential law of rate r > 0 is r⁻¹.

theorem integral_id_expMeasure {r : ℝ} (hr : 0 < r) : ∫ x, x ∂(expMeasure r) = r⁻¹

Uses 1 · Used by 7

Proof usesMoments of the exponential law

Used byMean of an exponentially distributed random variable · Variance of the exponential law · Non-explosion · Mean hitting time, first-step equation · Minimality of the mean hitting time · Product moment of two hitting times, first-step equation · Minimality of the product moment

TheoremSecond moment of the exponential law#✓fully proved

The second moment of the exponential law of rate r > 0 is 2 / r ^ 2.

theorem integral_sq_expMeasure {r : ℝ} (hr : 0 < r) :
    ∫ x, x ^ 2 ∂(expMeasure r) = 2 / r ^ 2

Uses 1 · Used by 3

Proof usesMoments of the exponential law

Used byVariance of the exponential law · Product moment of two hitting times, first-step equation · Minimality of the product moment

TheoremVariance of the exponential law#✓fully proved

The variance of the exponential law of rate r > 0 is r⁻¹ ^ 2.

theorem variance_id_expMeasure {r : ℝ} (hr : 0 < r) : Var[id; expMeasure r] = r⁻¹ ^ 2

Uses 3 · Used by 1

Proof usesFiniteness of all moments of the exponential law · Mean of the exponential law · Second moment of the exponential law

Used byVariance of an exponentially distributed random variable

TheoremExponentially distributed random variables are integrable#✓fully proved

A random variable with exponential law of rate r > 0 is integrable.

theorem HasLaw.integrable_of_expMeasure (hX : HasLaw X (expMeasure r) μ) (hr : 0 < r) :
    Integrable X μ

Uses 1 · Used by 3

Proof usesIntegrability of the identity under the exponential law

Used byIntegrability of coalescent holding times · Expected divergence · Variance of the divergence

TheoremMean of an exponentially distributed random variable#✓fully proved

A random variable with exponential law of rate r > 0 has mean r⁻¹.

theorem HasLaw.integral_eq_inv_of_expMeasure (hX : HasLaw X (expMeasure r) μ) (hr : 0 < r) :
    μ[X] = r⁻¹

Uses 1 · Used by 7

Proof usesMean of the exponential law

Used byExpected coalescent holding time · Covariance of π and S · Expected pairwise differences · Variance of the mean number of pairwise differences · The skyline estimate is unbiased · Expected divergence · Variance of the divergence

TheoremVariance of an exponentially distributed random variable#✓fully proved

A random variable with exponential law of rate r > 0 has variance r⁻¹ ^ 2.

theorem HasLaw.variance_eq_of_expMeasure (hX : HasLaw X (expMeasure r) μ) (hr : 0 < r) :
    Var[X; μ] = r⁻¹ ^ 2

Uses 1 · Used by 7

Proof usesVariance of the exponential law

Used byVariance of the time to the most recent common ancestor · Covariance of π and S · Pair coalescence time against the total branch length · Variance of the mean number of pairwise differences · Variance of the total branch length · Variance of the skyline estimate · Variance of the divergence

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.