The Pólya urn

An urn holds balls of the colours in α with positive weights θ c. Draws are made one at a time; after n draws in which colour c came up x c times, the next draw is colour c with probability

(θ c + x c) / (∑ θ + n),

the prediction rule of [Pit06] Exercise 2.2.2, polyaUrnPredictive. Multiplying these probabilities along a sequence gives the probability of the sequence, which depends only on its count vector x:

polyaUrnProb θ x = ∏ c, (θ c)_{x c} / (∑ θ)_{∑ x}

in rising factorials (a)_m = a (a + 1) ⋯ (a + m - 1) (ascPochhammer). The drawn sequence is exchangeable, with Dirichlet-distributed limiting frequencies ([Pit06] Exercise 2.2.2).

This file is measure-free: the law of the sequence and its exchangeability are in Linglib.Core.Probability.Distributions.PolyaUrn.

Main definitions

• ProbabilityTheory.countVec s: how often each colour occurs in the sequence s.
• ProbabilityTheory.polyaUrnPredictive θ x c: the probability of drawing c next.
• ProbabilityTheory.polyaUrnProb θ x: the probability of a sequence with count vector x.

Main results

• ProbabilityTheory.polyaUrnProb_update_succ, ProbabilityTheory.polyaUrnProb_countVec_snoc: drawing colour c multiplies the probability by the probability of drawing c.
• ProbabilityTheory.polyaUrnProb_add: conjugacy; after the counts x, the urn with weights θ + x gives the probability of the further counts y.
• ProbabilityTheory.sum_polyaUrnPredictive: the prediction rule is a probability.

Implementation notes

The weights are a plain function θ : α → ℝ, positivity being a hypothesis of the results that need it, and updating them by observed counts is the sum θ + x. The identities between polyaUrnProb and polyaUrnPredictive hold without hypotheses.

The partition of the draws generated by the symmetric urn with m colours of weight κ is the Pitman–Yor partition with discount -κ and concentration m κ ([Pit06] Exercise 2.2.5 and p. 61); as κ → 0 with m κ tending to a concentration c > 0 it tends to the discount-0 partition, generated by the Blackwell–MacQueen urn ([Pit06] Exercise 2.2.6 and p. 61). Neither is formalized here.

References

• [Pit06]

Count vectors

def ProbabilityTheory.countVec {α : Type u_1} [DecidableEq α] {n : ℕ} (s : Fin n → α) (c : α) : ℕ

The count vector of a sequence: how often each colour occurs in it.

Equations

• ProbabilityTheory.countVec s c = {i : Fin n | s i = c}.card

@[simp]

theorem ProbabilityTheory.countVec_zero {α : Type u_1} [DecidableEq α] (s : Fin 0 → α) : countVec s = 0

theorem ProbabilityTheory.countVec_cons {α : Type u_1} [DecidableEq α] {n : ℕ} (c : α) (s : Fin n → α) : countVec (Fin.cons c s) = Function.update (countVec s) c (countVec s c + 1)

Prepending a draw increments its colour's count.

theorem ProbabilityTheory.countVec_snoc {α : Type u_1} [DecidableEq α] {n : ℕ} (c : α) (s : Fin n → α) : countVec (Fin.snoc s c) = Function.update (countVec s) c (countVec s c + 1)

Appending a draw increments its colour's count.

theorem ProbabilityTheory.countVec_comp_perm {α : Type u_1} [DecidableEq α] {n : ℕ} (s : Fin n → α) (σ : Equiv.Perm (Fin n)) : countVec (s ∘ ⇑σ) = countVec s

Permuting a sequence does not change its counts.

theorem ProbabilityTheory.sum_countVec {α : Type u_1} [DecidableEq α] {n : ℕ} [Fintype α] (s : Fin n → α) : ∑ c : α, countVec s c = n

The counts of a sequence of n draws add up to n.

The prediction rule and the probability of a sequence

noncomputable def ProbabilityTheory.polyaUrnPredictive {α : Type u_1} [Fintype α] (θ : α → ℝ) (x : α → ℕ) (c : α) : ℝ

The probability that the urn with weights θ draws colour c after draws with counts x: (θ c + x c) / (∑ θ + ∑ x) ([Pit06] Exercise 2.2.2).

Equations

• ProbabilityTheory.polyaUrnPredictive θ x c = (θ c + ↑(x c)) / (∑ i : α, θ i + ∑ i : α, ↑(x i))

noncomputable def ProbabilityTheory.polyaUrnProb {α : Type u_1} [Fintype α] (θ : α → ℝ) (x : α → ℕ) : ℝ

The probability that the urn with weights θ draws a given sequence with counts x.

Equations

• ProbabilityTheory.polyaUrnProb θ x = (∏ c : α, Polynomial.eval (θ c) (ascPochhammer ℝ (x c))) / Polynomial.eval (∑ c : α, θ c) (ascPochhammer ℝ (∑ c : α, x c))

@[simp]

theorem ProbabilityTheory.polyaUrnProb_zero {α : Type u_1} [Fintype α] (θ : α → ℝ) : polyaUrnProb θ 0 = 1

theorem ProbabilityTheory.polyaUrnPredictive_zero {α : Type u_1} [Fintype α] (θ : α → ℝ) (c : α) : polyaUrnPredictive θ 0 c = θ c / ∑ i : α, θ i

The first draw is proportional to the weights.

theorem ProbabilityTheory.polyaUrnProb_update_succ {α : Type u_1} [Fintype α] (θ : α → ℝ) [DecidableEq α] (x : α → ℕ) (c : α) : polyaUrnProb θ (Function.update x c (x c + 1)) = polyaUrnProb θ x * polyaUrnPredictive θ x c

Drawing colour c multiplies the probability of the sequence by the probability of drawing c: the rising-factorial recursion (a)_{m + 1} = (a)_m (a + m) at c and at the total.

theorem ProbabilityTheory.polyaUrnProb_countVec_snoc {α : Type u_1} [Fintype α] (θ : α → ℝ) [DecidableEq α] (c : α) {n : ℕ} (s : Fin n → α) : polyaUrnProb θ (countVec (Fin.snoc s c)) = polyaUrnProb θ (countVec s) * polyaUrnPredictive θ (countVec s) c

Appending colour c to a sequence multiplies its probability by the probability of drawing c.

theorem ProbabilityTheory.polyaUrnProb_countVec_cons {α : Type u_1} [Fintype α] (θ : α → ℝ) [DecidableEq α] (c : α) {n : ℕ} (s : Fin n → α) : polyaUrnProb θ (countVec (Fin.cons c s)) = polyaUrnProb θ (countVec s) * polyaUrnPredictive θ (countVec s) c

Prepending colour c to a sequence multiplies its probability by the probability of drawing c first given the rest; the counts do not see the order.

theorem ProbabilityTheory.polyaUrnProb_add {α : Type u_1} [Fintype α] (θ : α → ℝ) (x y : α → ℕ) : polyaUrnProb θ (x + y) = polyaUrnProb θ x * polyaUrnProb (θ + fun (c : α) => ↑(x c)) y

Conjugacy. The probability of counts x + y is the probability of x times the probability of y under the urn whose weights are raised by x.

theorem ProbabilityTheory.polyaUrnPredictive_nonneg {α : Type u_1} [Fintype α] {θ : α → ℝ} (hθ : ∀ (i : α), 0 ≤ θ i) (x : α → ℕ) (c : α) : 0 ≤ polyaUrnPredictive θ x c

theorem ProbabilityTheory.sum_polyaUrnPredictive {α : Type u_1} [Fintype α] {θ : α → ℝ} [Nonempty α] (hθ : ∀ (i : α), 0 < θ i) (x : α → ℕ) : ∑ c : α, polyaUrnPredictive θ x c = 1

The prediction rule is a probability on the colours.

theorem ProbabilityTheory.polyaUrnProb_pos {α : Type u_1} [Fintype α] {θ : α → ℝ} [Nonempty α] (hθ : ∀ (i : α), 0 < θ i) (x : α → ℕ) : 0 < polyaUrnProb θ x