Tail-Sum Identities for PMF

This file records discrete tail-sum formulas for nonnegative ℕ-valued random variables.

The core identity is the standard discrete expectation formula

E[X] = ∑ i, Pr[i < X]

for ℕ-valued random variables with values in ℝ≥0∞.

We first prove the corresponding summation identity for arbitrary nonnegative sequences, and then specialize it to probability mass functions.

theorem ENNReal.tsum_mul_nat_eq_tsum_tail (f : ℕ → ENNReal) : ∑' (n : ℕ), f n * ↑n = ∑' (i : ℕ) (n : ℕ), if i < n then f n else 0

Tail-sum identity for a nonnegative sequence on ℕ:

∑' n, f n * n = ∑' i, ∑' n, if i < n then f n else 0.

This is the discrete nonnegative analogue of writing n = ∑_{i < n} 1 and exchanging the order of summation.

theorem PMF.tsum_coe_mul_nat_eq_tsum_measure_Ioi (p : PMF ℕ) : ∑' (n : ℕ), p n * ↑n = ∑' (i : ℕ), p.toMeasure (Set.Ioi i)

Tail-sum identity for the ℝ≥0∞-valued expectation of a PMF ℕ:

∑' n, p n * n = ∑' i, p.toMeasure {n | i < n}.

This is the discrete formula E[X] = ∑ i, Pr[i < X] for ℕ-valued random variables.

theorem PMF.tsum_coe_mul_nat_le_tsum_of_measure_Ioi_le (p : PMF ℕ) {a : ℕ → ENNReal} (h : ∀ (i : ℕ), p.toMeasure (Set.Ioi i) ≤ a i) : ∑' (n : ℕ), p n * ↑n ≤ ∑' (i : ℕ), a i

Tail domination bounds the ℝ≥0∞-valued expectation of a PMF ℕ.

If each tail probability Pr[i < X] is bounded above by a i, then E[X] ≤ ∑ i, a i. This is the generic discrete upper-bound principle used to turn tail estimates into expectation bounds.