The negative-binomial distribution

This file defines the negative-binomial family. The law counts failures before the rth success, with real shape r and success probability p. Its native mass is the Gamma-expression Γ(k + r) / (k! Γ(r)) * p^r * (1 - p)^k.

The definition is totalized explicitly: the positive family is used for 0 < r and 0 < p ≤ 1, the boundary r = 0 is a Dirac mass at zero, and every other parameter value gives the zero measure. The file supplies the normalized measure, its native singleton and support interfaces, the exact integrability domain and closed form of its probability-generating function, and the additivity of the shape parameter under convolution.

Main results

• negativeBinomialMeasure_singleton and negativeBinomialMeasure_real_singleton compute the native masses;
• negativeBinomialMeasure_singleton_ne_zero_iff characterizes their exact support, including the shape-zero and success-probability-one boundary laws;
• pgf_negativeBinomialMeasure computes the probability-generating function on its exact domain;
• negativeBinomialMeasure_conv_negativeBinomialMeasure proves that convolution adds shapes.

The normalization uses Mathlib's real binomial power series, after identifying its coefficients with the Gamma quotient. The distributional convention follows Johnson, Kemp, and Kotz, Univariate Discrete Distributions, 3rd ed., Chapter 5.

noncomputable def TauCeti.Probability.negativeBinomialWeightReal (r p : ℝ) (k : ℕ) : ℝ

The real coefficient in the negative-binomial mass at k.

Equations

• TauCeti.Probability.negativeBinomialWeightReal r p k = if r = 0 then if k = 0 then 1 else 0 else Real.Gamma (↑k + r) / (↑k.factorial * Real.Gamma r) * p.rpow r * (1 - p) ^ k

noncomputable def TauCeti.Probability.negativeBinomialWeight (r p : ℝ) (k : ℕ) : ENNReal

The ℝ≥0∞-valued negative-binomial mass at k.

Equations

• TauCeti.Probability.negativeBinomialWeight r p k = ENNReal.ofReal (TauCeti.Probability.negativeBinomialWeightReal r p k)

noncomputable def TauCeti.Probability.negativeBinomialMeasure (r p : ℝ) : MeasureTheory.Measure ℕ

The negative-binomial law with real shape r and success probability p.

For 0 < r and 0 < p ≤ 1 this is the weighted Dirac sum with the usual Gamma masses. The boundary shape r = 0 is the Dirac law at zero; all remaining parameters are totalized to zero.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.Probability.negativeBinomialMeasure_eq_sum_dirac {r p : ℝ} (hr : 0 ≤ r) (hp : 0 < p) (hp1 : p ≤ 1) : negativeBinomialMeasure r p = MeasureTheory.Measure.sum fun (k : ℕ) => negativeBinomialWeight r p k • MeasureTheory.Measure.dirac k

In the valid parameter range, the measure is its weighted Dirac sum, including r = 0.

@[simp]

theorem TauCeti.Probability.negativeBinomialMeasure_eq_zero_of_invalid {r p : ℝ} (h : ¬(0 ≤ r ∧ 0 < p ∧ p ≤ 1)) : negativeBinomialMeasure r p = 0

Outside the probability parameter range, the measure is explicitly totalized to zero.

@[simp]

theorem TauCeti.Probability.negativeBinomialMeasure_zero {p : ℝ} (hp : 0 < p) (hp1 : p ≤ 1) : negativeBinomialMeasure 0 p = MeasureTheory.Measure.dirac 0

The boundary shape r = 0 is the Dirac law at zero in the valid probability range.

@[simp]

theorem TauCeti.Probability.negativeBinomialWeightReal_eq_gamma {r p : ℝ} (hr : r ≠ 0) (k : ℕ) : negativeBinomialWeightReal r p k = Real.Gamma (↑k + r) / (↑k.factorial * Real.Gamma r) * p.rpow r * (1 - p) ^ k

At nonzero shape, the real negative-binomial weight has its defining Gamma-quotient form.

theorem TauCeti.Probability.negativeBinomialWeightReal_eq_coeff {r p : ℝ} (hr : 0 < r) (k : ℕ) : negativeBinomialWeightReal r p k = Ring.multichoose r k * p.rpow r * (1 - p) ^ k

The real negative-binomial mass in its multichoose coefficient form.

theorem TauCeti.Probability.negativeBinomialWeight_toReal {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) (hp1 : p ≤ 1) (k : ℕ) : (negativeBinomialWeight r p k).toReal = negativeBinomialWeightReal r p k

The real-valued mass agrees with the toReal of the nonnegative mass, including boundaries.

theorem TauCeti.Probability.isProbabilityMeasure_negativeBinomialMeasure {r p : ℝ} (hr : 0 ≤ r) (hp : 0 < p) (hp1 : p ≤ 1) : MeasureTheory.IsProbabilityMeasure (negativeBinomialMeasure r p)

The negative-binomial measure is a probability measure in its classical parameter range.

@[simp]

theorem TauCeti.Probability.negativeBinomialMeasure_singleton {r p : ℝ} (hr : 0 ≤ r) (hp : 0 < p) (hp1 : p ≤ 1) (k : ℕ) : (negativeBinomialMeasure r p) {k} = negativeBinomialWeight r p k

The singleton mass of the negative-binomial law in its valid parameter range.

theorem TauCeti.Probability.negativeBinomialMeasure_real_singleton {r p : ℝ} (hr : 0 ≤ r) (hp : 0 < p) (hp1 : p ≤ 1) (k : ℕ) : (negativeBinomialMeasure r p).real {k} = negativeBinomialWeightReal r p k

The real singleton mass of the negative-binomial law in its valid parameter range.

theorem TauCeti.Probability.geometricMeasure_eq_negativeBinomialMeasure_one (p : ↑unitInterval) (hp : p ≠ 0) : ProbabilityTheory.geometricMeasure p = negativeBinomialMeasure 1 ↑p

For nonzero success probability, the geometric law is the negative-binomial law of shape one.

Support

@[simp]

theorem TauCeti.Probability.negativeBinomialWeightReal_pos_iff {r p : ℝ} (hr : 0 ≤ r) (hp : 0 < p) (hp1 : p ≤ 1) (k : ℕ) : 0 < negativeBinomialWeightReal r p k ↔ k = 0 ∨ 0 < r ∧ p < 1

A real negative-binomial weight is positive exactly at zero or in the nondegenerate family.

Thus the shape-zero and success-probability-one laws are supported only at zero, while positive shape and success probability strictly below one give positive mass to every natural number.

@[simp]

theorem TauCeti.Probability.negativeBinomialWeight_ne_zero_iff {r p : ℝ} (hr : 0 ≤ r) (hp : 0 < p) (hp1 : p ≤ 1) (k : ℕ) : negativeBinomialWeight r p k ≠ 0 ↔ k = 0 ∨ 0 < r ∧ p < 1

A negative-binomial weight is nonzero exactly at zero or in the nondegenerate family.

theorem TauCeti.Probability.negativeBinomialMeasure_singleton_ne_zero_iff {r p : ℝ} (hr : 0 ≤ r) (hp : 0 < p) (hp1 : p ≤ 1) (k : ℕ) : (negativeBinomialMeasure r p) {k} ≠ 0 ↔ k = 0 ∨ 0 < r ∧ p < 1

The singleton mass of a valid negative-binomial law is nonzero exactly at zero or in the nondegenerate family.

theorem TauCeti.Probability.integrable_pow_negativeBinomialMeasure_iff {r p : ℝ} (hr : 0 < r) (hp : 0 < p) (hp1 : p ≤ 1) (t : ℝ) : MeasureTheory.Integrable (fun (k : ℕ) => t ^ k) (negativeBinomialMeasure r p) ↔ |(1 - p) * t| < 1

For positive shape and valid success probability, the negative-binomial probability-generating-function integrand is integrable exactly inside its disk of convergence. Thus it is non-integrable both on and beyond the boundary.

theorem TauCeti.Probability.pgf_negativeBinomialMeasure {r p : ℝ} (hr : 0 < r) (hp : 0 < p) (hp1 : p ≤ 1) {t : ℝ} (ht : |(1 - p) * t| < 1) : pgf id (negativeBinomialMeasure r p) t = (p / (1 - (1 - p) * t)).rpow r

The probability-generating function of a negative-binomial law with positive shape, on its exact integrability domain.

@[simp]

theorem TauCeti.Probability.pgf_negativeBinomialMeasure_zero (p t : ℝ) : pgf id (negativeBinomialMeasure 0 p) t = if 0 < p ∧ p ≤ 1 then 1 else 0

At shape zero, the negative-binomial PGF is one in the valid probability range and zero outside it, in accordance with the totalization of negativeBinomialMeasure.

Convolution

@[simp]

theorem TauCeti.Probability.negativeBinomialMeasure_conv_negativeBinomialMeasure {r s p : ℝ} (hr : 0 ≤ r) (hs : 0 ≤ s) : (negativeBinomialMeasure r p).conv (negativeBinomialMeasure s p) = negativeBinomialMeasure (r + s) p

The convolution of two negative-binomial laws with the same success probability is negative-binomial, with the shape parameters added. This includes either shape-zero boundary and the success-probability-one Dirac family; outside the valid probability range all three measures vanish.