Negative binomial and beta-binomial distributions

DefinitionNegative binomial mass function with real shape#✓fully proved

Negative binomial mass P(X = k) = r^{(k)} / k! · p ^ r · (1 - p) ^ k with real shape r (rising factorial r^{(k)} = (ascPochhammer ℝ k).eval r) and success probability p, using the real power p ^ r. A probability mass function for r > 0 and p ∈ (0, 1].

noncomputable def negBinomialPMF (r p : ℝ) (k : ℕ) : ℝ :=
  (ascPochhammer ℝ k).eval r / k ! * p ^ r * (1 - p) ^ k

Used by 6

Used byNegative binomial masses sum to one · Normalization · Negative binomial splitting for random variables · Negative binomial splitting · Mean parametrization is the canonical p-parametrization · Convolution of negative binomial laws with a common p

DefinitionBeta-binomial mass function#✓fully proved

Beta-binomial mass C(n, k) α^{(k)} β^{(n - k)} / (α + β)^{(n)} (zero for k > n, since C(n, k) = 0). A probability mass function for α, β > 0.

noncomputable def betaBinomialPMF (n : ℕ) (α β : ℝ) (k : ℕ) : ℝ :=
  (n.choose k : ℝ) * (ascPochhammer ℝ k).eval α * (ascPochhammer ℝ (n - k)).eval β /
    (ascPochhammer ℝ n).eval (α + β)

Used by 6

Used byNegative binomial splitting for random variables · Negative binomial splitting · Beta-binomial masses sum to one · Mean · Second factorial moment · Variance

TheoremChu–Vandermonde identity for rising factorials#✓fully proved

(α + β)^{(n)} = ∑_{k ≤ n} C(n, k) α^{(k)} β^{(n - k)}, for all real α, β.

theorem ascPochhammer_eval_add_eq_sum (α β : ℝ) (n : ℕ) :
    (ascPochhammer ℝ n).eval (α + β) =
      ∑ k ∈ range (n + 1),
        (n.choose k : ℝ) * (ascPochhammer ℝ k).eval α * (ascPochhammer ℝ (n - k)).eval β

Used by 4

Used byBeta-binomial masses sum to one · Mean · Second factorial moment · Convolution of negative binomial laws with a common p

TheoremBeta-binomial masses sum to one#✓fully proved

The beta-binomial masses sum to one for α, β > 0.

theorem sum_betaBinomialPMF (n : ℕ) {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) :
    ∑ k ∈ range (n + 1), betaBinomialPMF n α β k = 1

Uses 2

Statement usesBeta-binomial mass function

Proof usesChu–Vandermonde identity for rising factorials

TheoremNegative binomial masses sum to one#✓fully proved

The negative binomial masses sum to one for r > 0 and p ∈ (0, 1] (the binomial series ∑ₖ r^{(k)} xᵏ / k! = (1 - x)^{-r} at x = 1 - p).

theorem hasSum_negBinomialPMF {r p : ℝ} (hr : 0 < r) (hp : 0 < p) (hp1 : p ≤ 1) :
    HasSum (negBinomialPMF r p) 1

Uses 1 · Used by 1

Statement usesNegative binomial mass function with real shape

Used byNormalization

TheoremConvolution of negative binomial laws with a common p#✓fully proved

∑_{k ≤ n} NB(r₁, p)(k) NB(r₂, p)(n - k) = NB(r₁ + r₂, p)(n) for p > 0 and all real shapes.

theorem sum_negBinomialPMF_mul (r₁ r₂ : ℝ) {p : ℝ} (hp : 0 < p) (n : ℕ) :
    ∑ k ∈ range (n + 1), negBinomialPMF r₁ p k * negBinomialPMF r₂ p (n - k) =
      negBinomialPMF (r₁ + r₂) p n

Uses 2 · Used by 1

Statement usesNegative binomial mass function with real shape

Proof usesChu–Vandermonde identity for rising factorials

Used byNegative binomial splitting for random variables

TheoremNegative binomial splitting#✓fully proved

For r₁, r₂ > 0, 0 < p < 1 and k ≤ n, NB(r₁, p)(k) NB(r₂, p)(n - k) / NB(r₁ + r₂, p)(n) = BB(n; r₁, r₂)(k); the conditional law of one component given the total is beta-binomial and does not depend on p.

theorem negBinomialPMF_mul_div_eq_betaBinomialPMF {r₁ r₂ p : ℝ} (hr₁ : 0 < r₁) (hr₂ : 0 < r₂)
    (hp : 0 < p) (hp1 : p < 1) {n k : ℕ} (hk : k ≤ n) :
    negBinomialPMF r₁ p k * negBinomialPMF r₂ p (n - k) / negBinomialPMF (r₁ + r₂) p n =
      betaBinomialPMF n r₁ r₂ k

Uses 2 · Used by 1

Statement usesBeta-binomial mass function · Negative binomial mass function with real shape

Used byNegative binomial splitting for random variables

TheoremNegative binomial splitting for random variables#✓fully proved

If X and Y are independent with P(X = j) = NB(r₁, p)(j) and P(Y = j) = NB(r₂, p)(j) for all j, where r₁, r₂ > 0 and 0 < p < 1, then P(X = k ∣ X + Y = n) = BB(n; r₁, r₂)(k) for k ≤ n.

theorem measure_cond_eq_betaBinomialPMF {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
    [IsProbabilityMeasure μ] {X Y : Ω → ℕ} (hX : Measurable X) (hY : Measurable Y)
    (hXY : IndepFun X Y μ) {r₁ r₂ p : ℝ} (hr₁ : 0 < r₁) (hr₂ : 0 < r₂) (hp : 0 < p)
    (hp1 : p < 1) (hlawX : ∀ j, μ.real (X ⁻¹' {j}) = negBinomialPMF r₁ p j)
    (hlawY : ∀ j, μ.real (Y ⁻¹' {j}) = negBinomialPMF r₂ p j) {n k : ℕ} (hk : k ≤ n) :
    μ.real ({ω | X ω = k} ∩ {ω | X ω + Y ω = n}) / μ.real {ω | X ω + Y ω = n} =
      betaBinomialPMF n r₁ r₂ k

Uses 4

Statement usesBeta-binomial mass function · Negative binomial mass function with real shape

Proof usesNegative binomial splitting · Convolution of negative binomial laws with a common p

TheoremMean#✓fully proved

For α, β > 0, E M = n α / (α + β) = n π.

theorem sum_mul_betaBinomialPMF {n : ℕ} {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) :
    ∑ k ∈ range (n + 1), (k : ℝ) * betaBinomialPMF n α β k = n * α / (α + β)

Uses 2 · Used by 1

Statement usesBeta-binomial mass function

Proof usesChu–Vandermonde identity for rising factorials

Used byVariance

TheoremSecond factorial moment#✓fully proved

For α, β > 0, E[M (M - 1)] = n (n - 1) α (α + 1) / ((α + β) (α + β + 1)).

theorem sum_mul_sub_one_betaBinomialPMF {n : ℕ} {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) :
    ∑ k ∈ range (n + 1), (k : ℝ) * ((k : ℝ) - 1) * betaBinomialPMF n α β k =
      n * (n - 1) * α * (α + 1) / ((α + β) * (α + β + 1))

Uses 2 · Used by 1

Statement usesBeta-binomial mass function

Proof usesChu–Vandermonde identity for rising factorials

Used byVariance

TheoremVariance#✓fully proved

Variance (Dolzhenko–Smith parametrization). For α, β > 0, with π = α / (α + β) and γ = 1 / (α + β + 1), Var M = E M² - (E M)² = n π (1 - π) (1 + (n - 1) γ).

theorem variance_betaBinomial {n : ℕ} {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) :
    ∑ k ∈ range (n + 1), (k : ℝ) ^ 2 * betaBinomialPMF n α β k -
        (∑ k ∈ range (n + 1), (k : ℝ) * betaBinomialPMF n α β k) ^ 2 =
      n * (α / (α + β)) * (1 - α / (α + β)) * (1 + (n - 1) * (1 / (α + β + 1)))

Uses 3

Statement usesBeta-binomial mass function

Proof usesMean · Second factorial moment

DefinitionMixed Poisson mass function#✓fully proved

The mixed Poisson mass function p(k) = ∫ e^{-λ} λ^k / k! dν(λ) for a mixing law ν of the rate. It is a probability mass function when ν is a probability measure concentrated on [0, ∞), which the theorems below assume; for such ν the integrand lies in [0, 1], so the integral is never a junk value.

noncomputable def poissonMixtureReal (ν : Measure ℝ) (k : ℕ) : ℝ :=
  ∫ r, exp (-r) * r ^ k / (k ! : ℝ) ∂ν

Used by 17

Used bySquared coefficient of variation · Zero inflation by mixing · Fano factor of the Poisson law · Gamma–Poisson conjugacy, posterior · Mean · Mean · Second factorial moment · Normalization · Second moment · Second moment · Poisson mixture over a point mass is Poisson · Greenwood–Yule · Greenwood–Yule, mean form · Nonnegativity of the mixed Poisson mass function · Zero class of a mixed Poisson law · Gamma–Poisson conjugacy, posterior predictive · Variance decomposition

TheoremZero class of a mixed Poisson law#✓fully proved

The zero class of a mixed Poisson law is E e^{-Λ}.

theorem poissonMixtureReal_zero (ν : Measure ℝ) :
    poissonMixtureReal ν 0 = ∫ r, exp (-r) ∂ν

Uses 1 · Used by 1

Statement usesMixed Poisson mass function

Used byZero inflation by mixing

TheoremNonnegativity of the mixed Poisson mass function#✓fully proved

The mixed Poisson mass function is nonnegative when ν is concentrated on [0, ∞).

theorem poissonMixtureReal_nonneg (h0 : ∀ᵐ r ∂ν, 0 ≤ r) (k : ℕ) :
    0 ≤ poissonMixtureReal ν k

Uses 1

Statement usesMixed Poisson mass function

TheoremPoisson mixture over a point mass is Poisson#✓fully proved

The Poisson mixture over a point mass δ_m is the Poisson law with mean m.

theorem poissonMixtureReal_dirac (m : ℝ) (k : ℕ) :
    poissonMixtureReal (Measure.dirac m) k = exp (-m) * m ^ k / k !

Uses 1 · Used by 1

Statement usesMixed Poisson mass function

Used byFano factor of the Poisson law

TheoremNormalization#✓fully proved

For a probability measure ν concentrated on [0, ∞), the mixed Poisson masses sum to one.

theorem hasSum_poissonMixtureReal [IsProbabilityMeasure ν] (h0 : ∀ᵐ r ∂ν, 0 ≤ r) :
    HasSum (poissonMixtureReal ν) 1

Uses 1

Statement usesMixed Poisson mass function

TheoremZero inflation by mixing#✓fully proved

Zero inflation by mixing (Jensen's inequality for λ ↦ e^{-λ}). For a probability measure ν with integrable rate, P(N = 0) = E e^{-Λ} ≥ e^{-E Λ}, the zero class of the Poisson law with the same mean.

theorem exp_neg_integral_le_poissonMixtureReal_zero [IsProbabilityMeasure ν]
    (h0 : ∀ᵐ r ∂ν, 0 ≤ r) (hint : Integrable id ν) :
    exp (-∫ r, r ∂ν) ≤ poissonMixtureReal ν 0

Uses 2

Statement usesMixed Poisson mass function

Proof usesZero class of a mixed Poisson law

TheoremMean#✓fully proved

For a mixing measure ν on [0, ∞) with integrable rate, E N = E Λ (finiteness of ν is not needed for this identity).

theorem hasSum_mul_poissonMixtureReal (h0 : ∀ᵐ r ∂ν, 0 ≤ r)
    (hint : Integrable id ν) :
    HasSum (fun k : ℕ => (k : ℝ) * poissonMixtureReal ν k) (∫ r, r ∂ν)

Uses 1 · Used by 5

Statement usesMixed Poisson mass function

Used bySquared coefficient of variation · Fano factor of the Poisson law · Mean · Second moment · Variance decomposition

TheoremSecond factorial moment#✓fully proved

For a mixing measure ν on [0, ∞) with square-integrable rate, E[N (N - 1)] = E Λ² (finiteness of ν is not needed for this identity).

theorem hasSum_mul_sub_one_poissonMixtureReal (h0 : ∀ᵐ r ∂ν, 0 ≤ r)
    (hint₂ : Integrable (fun r => r ^ 2) ν) :
    HasSum (fun k : ℕ => (k : ℝ) * ((k : ℝ) - 1) * poissonMixtureReal ν k) (∫ r, r ^ 2 ∂ν)

Uses 1 · Used by 1

Statement usesMixed Poisson mass function

Used bySecond moment

TheoremSecond moment#✓fully proved

For a finite mixing measure ν on [0, ∞) with square-integrable rate, E N² = E Λ² + E Λ.

theorem hasSum_sq_poissonMixtureReal [IsFiniteMeasure ν] (h0 : ∀ᵐ r ∂ν, 0 ≤ r)
    (hint₂ : Integrable (fun r => r ^ 2) ν) :
    HasSum (fun k : ℕ => (k : ℝ) ^ 2 * poissonMixtureReal ν k)
      (∫ r, r ^ 2 ∂ν + ∫ r, r ∂ν)

Uses 3 · Used by 2

Statement usesMixed Poisson mass function

Proof usesMean · Second factorial moment

Used bySecond moment · Variance decomposition

TheoremVariance decomposition#✓fully proved

For a probability measure ν on [0, ∞) with square-integrable rate, Var N = E N² - (E N)² = E Λ + Var Λ: Poisson noise plus the variance of the rate.

theorem variance_poissonMixture [IsProbabilityMeasure ν] (h0 : ∀ᵐ r ∂ν, 0 ≤ r)
    (hmem : MemLp id 2 ν) :
    ∑' k : ℕ, (k : ℝ) ^ 2 * poissonMixtureReal ν k -
        (∑' k : ℕ, (k : ℝ) * poissonMixtureReal ν k) ^ 2 =
      ∫ r, r ∂ν + Var[id; ν]

Uses 3 · Used by 2

Statement usesMixed Poisson mass function

Proof usesMean · Second moment

Used bySquared coefficient of variation · Fano factor of the Poisson law

TheoremSquared coefficient of variation#✓fully proved

Squared coefficient of variation (Brennecke et al. 2013; Svensson 2020). For a probability measure ν on [0, ∞) with square-integrable rate and E Λ > 0, CV²(N) = Var N / (E N)² = 1 / E Λ + Var Λ / (E Λ)² = 1 / E Λ + CV²(Λ).

theorem cv_sq_poissonMixture [IsProbabilityMeasure ν] (h0 : ∀ᵐ r ∂ν, 0 ≤ r)
    (hmem : MemLp id 2 ν) (hpos : 0 < ∫ r, r ∂ν) :
    (∑' k : ℕ, (k : ℝ) ^ 2 * poissonMixtureReal ν k -
        (∑' k : ℕ, (k : ℝ) * poissonMixtureReal ν k) ^ 2) /
        (∑' k : ℕ, (k : ℝ) * poissonMixtureReal ν k) ^ 2 =
      1 / ∫ r, r ∂ν + Var[id; ν] / (∫ r, r ∂ν) ^ 2

Uses 3

Statement usesMixed Poisson mass function

Proof usesMean · Variance decomposition

DefinitionNegative binomial mass function with size and mean#✓fully proved

The negative binomial mass function with size θ and mean μ: NB(k; θ, μ) = θ⁽ᵏ⁾ / k! · (θ / (θ + μ)) ^ θ · (μ / (θ + μ)) ^ k, with the rising factorial θ⁽ᵏ⁾ = Γ(θ + k) / Γ(θ) and a real power (θ / (θ + μ)) ^ θ. The parameter domain is θ > 0, μ ≥ 0; at μ = 0 it is the point mass at 0. Outside the domain the formula is not a probability mass function.

noncomputable def negBinomialReal (θ μ : ℝ) (k : ℕ) : ℝ :=
  (ascPochhammer ℝ k).eval θ / k ! * (θ / (θ + μ)) ^ θ * (μ / (θ + μ)) ^ k

Used by 14

Used byBursty expression stationary law · Zero class versus the Poisson law · Fano factor of bursty expression · Mean · Normalization · Second moment · Mean parametrization is the canonical p-parametrization · Negative binomial law with mean zero is a point mass · Nonnegativity of the negative binomial mass function · Zero class of the negative binomial law · Greenwood–Yule · Greenwood–Yule, mean form · Gamma–Poisson conjugacy, posterior predictive · Variance

TheoremMean parametrization is the canonical p-parametrization#✓fully proved

For θ > 0 and μ ≥ 0, negBinomialReal θ μ is negBinomialPMF θ p at p = θ / (θ + μ), since 1 - p = μ / (θ + μ). The two APIs are the same law; reuse the splitting and conditioning results proved for negBinomialPMF through this equivalence.

theorem negBinomialReal_eq_negBinomialPMF {θ μ : ℝ} (hθ : 0 < θ) (hμ : 0 ≤ μ) (k : ℕ) :
    negBinomialReal θ μ k = negBinomialPMF θ (θ / (θ + μ)) k

Uses 2 · Used by 1

Statement usesNegative binomial mass function with real shape · Negative binomial mass function with size and mean

Used byNormalization

TheoremNonnegativity of the negative binomial mass function#✓fully proved

The negative binomial mass function is nonnegative on the parameter domain.

theorem negBinomialReal_nonneg {θ μ : ℝ} (hθ : 0 < θ) (hμ : 0 ≤ μ) (k : ℕ) :
    0 ≤ negBinomialReal θ μ k

Uses 1

Statement usesNegative binomial mass function with size and mean

TheoremZero class of the negative binomial law#✓fully proved

The zero class of the negative binomial law is (θ / (θ + μ)) ^ θ.

theorem negBinomialReal_zero (θ μ : ℝ) : negBinomialReal θ μ 0 = (θ / (θ + μ)) ^ θ

Uses 1 · Used by 1

Statement usesNegative binomial mass function with size and mean

Used byZero class versus the Poisson law

TheoremNegative binomial law with mean zero is a point mass#✓fully proved

With mean 0 the negative binomial law is the point mass at 0.

theorem negBinomialReal_mean_zero {θ : ℝ} (hθ : 0 < θ) (k : ℕ) :
    negBinomialReal θ 0 k = if k = 0 then 1 else 0

Uses 1 · Used by 3

Statement usesNegative binomial mass function with size and mean

Used byMean · Normalization · Second moment

TheoremZero class versus the Poisson law#✓fully proved

For θ > 0 and μ ≥ 0, P(0) = (θ / (θ + μ)) ^ θ ≥ e^{-μ}: a negative binomial law puts at least as much mass at zero as the Poisson law with the same mean.

theorem exp_neg_le_negBinomialReal_zero {θ μ : ℝ} (hθ : 0 < θ) (hμ : 0 ≤ μ) :
    exp (-μ) ≤ negBinomialReal θ μ 0

Uses 2

Statement usesNegative binomial mass function with size and mean

Proof usesZero class of the negative binomial law

TheoremGreenwood–Yule#✓fully proved

The Poisson mixture over a Gamma rate of shape a > 0 and rate b > 0 is negative binomial with size a and mean a / b.

theorem poissonMixtureReal_gammaMeasure {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (k : ℕ) :
    poissonMixtureReal (gammaMeasure a b) k = negBinomialReal a (a / b) k

Uses 3 · Used by 1

Statement usesNegative binomial mass function with size and mean · Mixed Poisson mass function

Proof usesGamma integrals

Used byGreenwood–Yule, mean form

TheoremGreenwood–Yule, mean form#✓fully proved

For θ, μ > 0, the Poisson mixture over Gamma(θ, θ / μ) (mean μ, variance μ² / θ) is NB(θ, μ).

theorem poissonMixtureReal_gammaMeasure_mean {θ μ : ℝ} (hθ : 0 < θ) (hμ : 0 < μ) (k : ℕ) :
    poissonMixtureReal (gammaMeasure θ (θ / μ)) k = negBinomialReal θ μ k

Uses 3 · Used by 2

Statement usesNegative binomial mass function with size and mean · Mixed Poisson mass function

Proof usesGreenwood–Yule

Used byMean · Second moment

TheoremNormalization#✓fully proved

For θ > 0 and μ ≥ 0 the negative binomial masses sum to one. For μ > 0 this is hasSum_negBinomialPMF transported along negBinomialReal_eq_negBinomialPMF, so the mean parametrization shares the canonical law's normalization instead of re-proving it.

theorem hasSum_negBinomialReal {θ μ : ℝ} (hθ : 0 < θ) (hμ : 0 ≤ μ) :
    HasSum (negBinomialReal θ μ) 1

Uses 5

Statement usesNegative binomial mass function with size and mean

Proof usesNegative binomial masses sum to one · Negative binomial mass function with real shape · Mean parametrization is the canonical p-parametrization · Negative binomial law with mean zero is a point mass

TheoremMean#✓fully proved

For θ > 0 and μ ≥ 0 the negative binomial law has mean μ.

theorem hasSum_mul_negBinomialReal {θ μ : ℝ} (hθ : 0 < θ) (hμ : 0 ≤ μ) :
    HasSum (fun k : ℕ => (k : ℝ) * negBinomialReal θ μ k) μ

Uses 8 · Used by 2

Statement usesNegative binomial mass function with size and mean

Proof usesGamma law is concentrated on the nonnegative reals · Mean · Gamma law has finite first moment · Mean of the gamma law · Negative binomial law with mean zero is a point mass · Mixed Poisson mass function · Greenwood–Yule, mean form

Used byFano factor of bursty expression · Variance

TheoremSecond moment#✓fully proved

For θ > 0 and μ ≥ 0, E N² = μ + μ² / θ + μ².

theorem hasSum_sq_negBinomialReal {θ μ : ℝ} (hθ : 0 < θ) (hμ : 0 ≤ μ) :
    HasSum (fun k : ℕ => (k : ℝ) ^ 2 * negBinomialReal θ μ k) (μ + μ ^ 2 / θ + μ ^ 2)

Uses 9 · Used by 1

Statement usesNegative binomial mass function with size and mean

Proof usesGamma law is concentrated on the nonnegative reals · Second moment · Gamma law has finite second moment · Mean of the gamma law · Second moment of the gamma law · Negative binomial law with mean zero is a point mass · Mixed Poisson mass function · Greenwood–Yule, mean form

Used byVariance

TheoremVariance#✓fully proved

For θ > 0 and μ ≥ 0 the negative binomial law has variance μ + μ² / θ.

theorem variance_negBinomial {θ μ : ℝ} (hθ : 0 < θ) (hμ : 0 ≤ μ) :
    ∑' k : ℕ, (k : ℝ) ^ 2 * negBinomialReal θ μ k -
        (∑' k : ℕ, (k : ℝ) * negBinomialReal θ μ k) ^ 2 = μ + μ ^ 2 / θ

Uses 3 · Used by 1

Statement usesNegative binomial mass function with size and mean

Proof usesMean · Second moment

Used byFano factor of bursty expression

TheoremGamma–Poisson conjugacy, posterior#✓fully proved

With prior Λ ~ Gamma(a, b) (a, b > 0) and one observation N = k from Po(Λ), the posterior density (likelihood times prior over the marginal NB(k; a, a / b)) is the Gamma(a + k, b + 1) density.

theorem gammaPDFReal_posterior {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (k : ℕ) (r : ℝ) :
    exp (-r) * r ^ k / k ! * gammaPDFReal a b r / poissonMixtureReal (gammaMeasure a b) k =
      gammaPDFReal (a + k) (b + 1) r

Uses 4

Statement usesMixed Poisson mass function

Proof usesGamma function at \(a + k\) via the rising factorial · Gamma integrals · \(r^k r^{a-1} = r^{a+k-1}\) for nonnegative \(r\)

TheoremGamma–Poisson conjugacy, posterior predictive#✓fully proved

With prior Λ ~ Gamma(a, b) (a, b > 0) and counts N, N' that are independent Po(Λ) given Λ, P(N' = j | N = k) = P(N = k, N' = j) / P(N = k) = NB(j; a + k, (a + k) / (b + 1)).

theorem posterior_predictive_gammaPoisson {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (k j : ℕ) :
    (∫ r, exp (-r) * r ^ k / k ! * (exp (-r) * r ^ j / j !) ∂gammaMeasure a b) /
        poissonMixtureReal (gammaMeasure a b) k =
      negBinomialReal (a + k) ((a + k) / (b + 1)) j

Uses 3

Statement usesNegative binomial mass function with size and mean · Mixed Poisson mass function

Proof usesGamma integrals

DefinitionNet probability flow of the immigration–death chain#✓fully proved

The net probability flow into state n of the immigration–death chain on ℕ, in which molecules are made at rate κ (n → n + 1) and each decays at rate γ (n → n - 1 at rate γ n): (κ p(n - 1) + γ (n + 1) p(n + 1)) - (κ + γ n) p(n), with no inflow from below at n = 0. A law p is stationary (global balance) iff this flow vanishes for every n.

noncomputable def immigrationDeathFlow (κ γ : ℝ) (p : ℕ → ℝ) : ℕ → ℝ
  | 0 => γ * p 1 - κ * p 0
  | n + 1 => κ * p n + γ * (n + 2) * p (n + 2) - (κ + γ * (n + 1)) * p (n + 1)

Used by 1

Used byImmigration–death stationary law

TheoremImmigration–death stationary law#✓fully proved

For γ ≠ 0 the Poisson law with mean κ / γ satisfies global balance for the immigration–death chain. The identity holds for all real κ; the chain is meaningful for κ ≥ 0, γ > 0.

theorem immigrationDeathFlow_poisson {κ γ : ℝ} (hγ : γ ≠ 0) (n : ℕ) :
    immigrationDeathFlow κ γ (fun m => exp (-(κ / γ)) * (κ / γ) ^ m / m !) n = 0

Uses 1

Statement usesNet probability flow of the immigration–death chain

TheoremFano factor of the Poisson law#✓fully proved

For mean m > 0, Var N / E N = 1; in particular the stationary law of the immigration–death chain has Fano factor 1.

theorem fano_poisson {m : ℝ} (hm : 0 < m) :
    (∑' k : ℕ, (k : ℝ) ^ 2 * (exp (-m) * m ^ k / k !) -
        (∑' k : ℕ, (k : ℝ) * (exp (-m) * m ^ k / k !)) ^ 2) /
        ∑' k : ℕ, (k : ℝ) * (exp (-m) * m ^ k / k !) = 1

Uses 4

Proof usesMean · Mixed Poisson mass function · Poisson mixture over a point mass is Poisson · Variance decomposition

DefinitionNet probability flow of the bursty production–degradation chain#✓fully proved

The net probability flow into state n of the bursty production–degradation chain: bursts arrive at rate κ and add B molecules, B geometric with mean b, P(B = j) = b ^ j / (1 + b) ^ (j + 1) for j ≥ 0; each molecule decays at rate γ. A burst of size 0 changes nothing, so state n is left by a burst at rate κ P(B ≥ 1) = κ b / (1 + b). The flow is κ ∑_{m < n} p(m) P(B = n - m) + γ (n + 1) p(n + 1) - (κ b / (1 + b) + γ n) p(n).

noncomputable def burstDeathFlow (κ γ b : ℝ) (p : ℕ → ℝ) (n : ℕ) : ℝ :=
  κ * ∑ m ∈ range n, p m * (b ^ (n - m) / (1 + b) ^ (n - m + 1)) + γ * (n + 1) * p (n + 1) -
    (κ * (b / (1 + b)) + γ * n) * p n

Used by 1

Used byBursty expression stationary law

TheoremBursty expression stationary law#✓fully proved

Bursty expression stationary law (Shahrezaei–Swain). For burst rate κ > 0, decay rate γ > 0 and mean burst size b ≥ 0, the negative binomial law with size a = κ / γ (bursts per lifetime) and mean a b satisfies global balance for the bursty production–degradation chain.

theorem burstDeathFlow_negBinomial {κ γ b : ℝ} (hκ : 0 < κ) (hγ : 0 < γ) (hb : 0 ≤ b) (n : ℕ) :
    burstDeathFlow κ γ b (negBinomialReal (κ / γ) (κ / γ * b)) n = 0

Uses 2

Statement usesNet probability flow of the bursty production–degradation chain · Negative binomial mass function with size and mean

TheoremFano factor of bursty expression#✓fully proved

For a > 0 and b > 0, the negative binomial law with size a and mean a b has Var N / E N = 1 + b.

theorem fano_negBinomial {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
    (∑' k : ℕ, (k : ℝ) ^ 2 * negBinomialReal a (a * b) k -
        (∑' k : ℕ, (k : ℝ) * negBinomialReal a (a * b) k) ^ 2) /
        ∑' k : ℕ, (k : ℝ) * negBinomialReal a (a * b) k = 1 + b

Uses 3

Statement usesNegative binomial mass function with size and mean

Proof usesMean · Variance

42 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.