Poisson–Gamma duality

DefinitionPoisson distribution function as a function of the mean#✓fully proved

The Poisson distribution function F_k(x) = ∑_{j ≤ k} e^{-x} x^j / (j!) as a function of the mean x (defined for every real x; it is a probability only for 0 ≤ x).

noncomputable def poissonCDF (x : ℝ) (k : ℕ) : ℝ :=
  ∑ j ∈ range (k + 1), exp (-x) * x ^ j / (j ! : ℝ)

Used by 21

Used byThe flat-prior posterior quantile is Garwood's bound · Continuity of the Poisson distribution function in the mean · Poisson–Gamma duality · Garwood's exact upper confidence bound · Exact coverage of Garwood's bound · Positivity of the Garwood upper bound · Garwood upper bound is strictly increasing in the count · Garwood upper bound after observing zero · Derivative of the Poisson distribution function in the mean · Means below the Garwood upper bound are exactly the non-rejected ones · Garwood upper bound solves the distribution function equation · Poisson distribution function is strictly increasing in the count · Poisson distribution function is monotone in the count · Positivity of the Poisson distribution function · Poisson distribution function is strictly decreasing in the mean · Poisson distribution function at mean zero · Poisson distribution function at count zero · Poisson distribution function agrees with the Poisson law · Super-uniformity of the distribution-function transform · Poisson distribution function vanishes as the mean grows · Poisson distribution function tends to one as the count grows

TheoremPoisson distribution function agrees with the Poisson law#✓fully proved

poissonCDF r k is the distribution function of Mathlib's poissonMeasure r at k.

theorem poissonMeasure_real_Iic (r : ℝ≥0) (k : ℕ) :
    (poissonMeasure r).real (Set.Iic k) = poissonCDF r k

Uses 1

Statement usesPoisson distribution function as a function of the mean

TheoremPoisson distribution function at mean zero#✓fully proved

At mean 0 the Poisson law is the point mass at 0: F_k(0) = 1.

theorem poissonCDF_zero_left (k : ℕ) : poissonCDF 0 k = 1

Uses 1 · Used by 2

Statement usesPoisson distribution function as a function of the mean

Used byPositivity of the Garwood upper bound · Garwood upper bound solves the distribution function equation

TheoremPoisson distribution function at count zero#✓fully proved

F_0(x) = e^{-x}.

theorem poissonCDF_zero_right (x : ℝ) : poissonCDF x 0 = exp (-x)

Uses 1 · Used by 2

Statement usesPoisson distribution function as a function of the mean

Used byGarwood upper bound after observing zero · Derivative of the Poisson distribution function in the mean

TheoremPositivity of the Poisson distribution function#✓fully proved

The distribution function is positive at every nonnegative real mean.

theorem poissonCDF_pos {x : ℝ} (hx : 0 ≤ x) (k : ℕ) : 0 < poissonCDF x k

Uses 1

Statement usesPoisson distribution function as a function of the mean

TheoremDerivative of the Poisson distribution function in the mean#✓fully proved

The derivative in the mean telescopes: ∂_x F_k(x) = -e^{-x} x^k / (k!).

theorem hasDerivAt_poissonCDF (k : ℕ) (x : ℝ) :
    HasDerivAt (fun y => poissonCDF y k) (-(exp (-x) * x ^ k / (k ! : ℝ))) x

Uses 2 · Used by 2

Statement usesPoisson distribution function as a function of the mean

Proof usesPoisson distribution function at count zero

Used byContinuity of the Poisson distribution function in the mean · Poisson distribution function is strictly decreasing in the mean

TheoremContinuity of the Poisson distribution function in the mean#✓fully proved

The distribution function is continuous in the mean.

theorem continuous_poissonCDF (k : ℕ) : Continuous fun x => poissonCDF x k

Uses 2 · Used by 3

Statement usesPoisson distribution function as a function of the mean

Proof usesDerivative of the Poisson distribution function in the mean

Used byPositivity of the Garwood upper bound · Garwood upper bound solves the distribution function equation · Poisson distribution function is strictly decreasing in the mean

TheoremPoisson–Gamma duality#✓fully proved

The Gamma law of shape k + 1 and rate r (Mathlib's gammaMeasure) has upper tail P(Gamma(k + 1, r) > x) = F_k(r x). This is the Erlang tail gammaMeasure_real_Ioi_natCast_add_one in GammaMoments, rewritten with the definition of poissonCDF.

theorem gammaMeasure_real_Ioi_poissonCDF (k : ℕ) {r x : ℝ} (hr : 0 < r) (hx : 0 ≤ x) :
    (gammaMeasure (k + 1) r).real (Ioi x) = poissonCDF (r * x) k

Uses 2 · Used by 1

Statement usesPoisson distribution function as a function of the mean

Proof usesErlang tail formula

Used byThe flat-prior posterior quantile is Garwood's bound

TheoremPoisson distribution function is strictly decreasing in the mean#✓fully proved

The distribution function is strictly decreasing in the mean on [0, ∞).

theorem poissonCDF_strictAntiOn (k : ℕ) : StrictAntiOn (fun x => poissonCDF x k) (Ici 0)

Uses 3 · Used by 3

Statement usesPoisson distribution function as a function of the mean

Proof usesContinuity of the Poisson distribution function in the mean · Derivative of the Poisson distribution function in the mean

Used byPositivity of the Garwood upper bound · Means below the Garwood upper bound are exactly the non-rejected ones · Garwood upper bound solves the distribution function equation

TheoremPoisson distribution function is strictly increasing in the count#✓fully proved

The distribution function is strictly increasing in k at every positive mean.

theorem poissonCDF_lt_poissonCDF_succ {x : ℝ} (hx : 0 < x) (k : ℕ) :
    poissonCDF x k < poissonCDF x (k + 1)

Uses 1 · Used by 1

Statement usesPoisson distribution function as a function of the mean

Used byGarwood upper bound is strictly increasing in the count

TheoremPoisson distribution function is monotone in the count#✓fully proved

The distribution function is monotone in k at every nonnegative mean.

theorem poissonCDF_mono {x : ℝ} (hx : 0 ≤ x) : Monotone fun k => poissonCDF x k

Uses 1 · Used by 1

Statement usesPoisson distribution function as a function of the mean

Used bySuper-uniformity of the distribution-function transform

TheoremPoisson distribution function vanishes as the mean grows#✓fully proved

For fixed k, F_k(x) → 0 as the mean x → ∞.

theorem tendsto_poissonCDF_atTop (k : ℕ) :
    Tendsto (fun x => poissonCDF x k) atTop (𝓝 0)

Uses 1 · Used by 2

Statement usesPoisson distribution function as a function of the mean

Used byPositivity of the Garwood upper bound · Garwood upper bound solves the distribution function equation

TheoremPoisson distribution function tends to one as the count grows#✓fully proved

For a fixed nonnegative mean, F_k(x) → 1 as k → ∞.

theorem tendsto_poissonCDF_nat {x : ℝ} (hx : 0 ≤ x) :
    Tendsto (fun k => poissonCDF x k) atTop (𝓝 1)

Uses 1 · Used by 1

Statement usesPoisson distribution function as a function of the mean

Used bySuper-uniformity of the distribution-function transform

DefinitionGarwood's exact upper confidence bound#✓fully proved

Garwood's exact upper confidence bound for a Poisson mean after observing k, at level α: u_α(k) = sup {x ≥ 0 | α ≤ F_k(x)}. For 0 < α < 1 it is the root of F_k(u) = α (poissonCDF_garwoodUpper).

noncomputable def garwoodUpper (α : ℝ) (k : ℕ) : ℝ :=
  sSup {x : ℝ | 0 ≤ x ∧ α ≤ poissonCDF x k}

Uses 1 · Used by 12

Statement usesPoisson distribution function as a function of the mean

Used byThe flat-prior posterior quantile is Garwood's bound · Upper confidence bound for the observed/expected ratio · Exact coverage · Observed/expected upper bound decreases with the expected count · Observed/expected upper bound increases with the observed count · Observed/expected upper bound with no observed variants · Exact coverage of Garwood's bound · Positivity of the Garwood upper bound · Garwood upper bound is strictly increasing in the count · Garwood upper bound after observing zero · Means below the Garwood upper bound are exactly the non-rejected ones · Garwood upper bound solves the distribution function equation

TheoremPositivity of the Garwood upper bound#✓fully proved

The bound is positive for 0 < α < 1.

theorem garwoodUpper_pos {α : ℝ} (hα0 : 0 < α) (hα1 : α < 1) (k : ℕ) :
    0 < garwoodUpper α k

Uses 6 · Used by 4

Statement usesGarwood's exact upper confidence bound

Proof usesContinuity of the Poisson distribution function in the mean · Poisson distribution function as a function of the mean · Poisson distribution function is strictly decreasing in the mean · Poisson distribution function at mean zero · Poisson distribution function vanishes as the mean grows

Used byThe flat-prior posterior quantile is Garwood's bound · Observed/expected upper bound decreases with the expected count · Garwood upper bound is strictly increasing in the count · Means below the Garwood upper bound are exactly the non-rejected ones

TheoremGarwood upper bound solves the distribution function equation#✓fully proved

The bound solves F_k(u_α(k)) = α.

theorem poissonCDF_garwoodUpper {α : ℝ} (hα0 : 0 < α) (hα1 : α < 1) (k : ℕ) :
    poissonCDF (garwoodUpper α k) k = α

Uses 6 · Used by 4

Statement usesGarwood's exact upper confidence bound · Poisson distribution function as a function of the mean

Proof usesContinuity of the Poisson distribution function in the mean · Poisson distribution function is strictly decreasing in the mean · Poisson distribution function at mean zero · Poisson distribution function vanishes as the mean grows

Used byThe flat-prior posterior quantile is Garwood's bound · Garwood upper bound is strictly increasing in the count · Garwood upper bound after observing zero · Means below the Garwood upper bound are exactly the non-rejected ones

TheoremMeans below the Garwood upper bound are exactly the non-rejected ones#✓fully proved

A nonnegative mean lies below the bound iff it is not rejected: x ≤ u_α(k) ↔ α ≤ F_k(x).

theorem le_garwoodUpper_iff {α : ℝ} (hα0 : 0 < α) (hα1 : α < 1) (k : ℕ) {x : ℝ}
    (hx : 0 ≤ x) : x ≤ garwoodUpper α k ↔ α ≤ poissonCDF x k

Uses 5 · Used by 2

Statement usesGarwood's exact upper confidence bound · Poisson distribution function as a function of the mean

Proof usesPositivity of the Garwood upper bound · Garwood upper bound solves the distribution function equation · Poisson distribution function is strictly decreasing in the mean

Used byExact coverage of Garwood's bound · Garwood upper bound is strictly increasing in the count

TheoremGarwood upper bound is strictly increasing in the count#✓fully proved

The bound is strictly increasing in the observed count.

theorem garwoodUpper_strictMono {α : ℝ} (hα0 : 0 < α) (hα1 : α < 1) :
    StrictMono (garwoodUpper α)

Uses 6 · Used by 1

Statement usesGarwood's exact upper confidence bound

Proof usesPositivity of the Garwood upper bound · Means below the Garwood upper bound are exactly the non-rejected ones · Poisson distribution function as a function of the mean · Garwood upper bound solves the distribution function equation · Poisson distribution function is strictly increasing in the count

Used byObserved/expected upper bound increases with the observed count

TheoremGarwood upper bound after observing zero#✓fully proved

After observing 0 the bound is u_α(0) = log (1 / α) (e^{-u} = α).

theorem garwoodUpper_zero {α : ℝ} (hα0 : 0 < α) (hα1 : α < 1) :
    garwoodUpper α 0 = log (1 / α)

Uses 4 · Used by 1

Statement usesGarwood's exact upper confidence bound

Proof usesPoisson distribution function as a function of the mean · Garwood upper bound solves the distribution function equation · Poisson distribution function at count zero

Used byObserved/expected upper bound with no observed variants

TheoremSuper-uniformity of the distribution-function transform#✓fully proved

For K ~ Poisson(r) and every α ≥ 0, P(F_r(K) ≤ α) ≤ α. (For α < 0 the event is empty.)

theorem poissonMeasure_real_poissonCDF_le (r : ℝ≥0) {α : ℝ} (hα : 0 ≤ α) :
    (poissonMeasure r).real {k | poissonCDF r k ≤ α} ≤ α

Uses 3 · Used by 1

Statement usesPoisson distribution function as a function of the mean

Proof usesPoisson distribution function is monotone in the count · Poisson distribution function tends to one as the count grows

Used byExact coverage of Garwood's bound

TheoremExact coverage of Garwood's bound#✓fully proved

For every mean r ≥ 0 and 0 < α < 1, P_r(r ≤ u_α(K)) ≥ 1 - α when K ~ Poisson(r).

theorem garwoodUpper_coverage (r : ℝ≥0) {α : ℝ} (hα0 : 0 < α) (hα1 : α < 1) :
    1 - α ≤ (poissonMeasure r).real {k | (r : ℝ) ≤ garwoodUpper α k}

Uses 4 · Used by 1

Statement usesGarwood's exact upper confidence bound

Proof usesMeans below the Garwood upper bound are exactly the non-rejected ones · Poisson distribution function as a function of the mean · Super-uniformity of the distribution-function transform

Used byExact coverage

21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.