The law of the Pólya urn

polyaUrn θ n is the law of the first n draws from the Pólya urn with weights θ: the sequence drawn, by seqLaw, from the prediction rule polyaUrnPredictive. Each sequence has probability polyaUrnProb θ (countVec s) (polyaUrn_real_singleton), which depends only on the counts, so the sequence is exchangeable (exchangeable_polyaUrn).

Main definitions

• ProbabilityTheory.polyaUrnRule θ n: the prediction rule as a kernel.
• ProbabilityTheory.polyaUrn θ n: the law of the first n draws.

Main results

• ProbabilityTheory.polyaUrn_real_singleton: the probability of a sequence.
• ProbabilityTheory.exchangeable_polyaUrn: the drawn sequence is exchangeable.

References

• [Pit06]

noncomputable def ProbabilityTheory.polyaUrnRule {α : Type u_1} [DecidableEq α] [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (θ : α → ℝ) (n : ℕ) : Kernel (Fin n → α) α

The Pólya urn prediction rule as a kernel: after the draws s, colour c is drawn with probability polyaUrnPredictive θ (countVec s) c.

Equations

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

noncomputable def ProbabilityTheory.polyaUrn {α : Type u_1} [DecidableEq α] [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (θ : α → ℝ) (n : ℕ) : MeasureTheory.Measure (Fin n → α)

The Pólya urn: the law of the first n draws from the urn with weights θ.

Equations

• ProbabilityTheory.polyaUrn θ n = ProbabilityTheory.seqLaw (ProbabilityTheory.polyaUrnRule θ) n

theorem ProbabilityTheory.polyaUrnRule_apply_singleton {α : Type u_1} [DecidableEq α] [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] (θ : α → ℝ) {n : ℕ} (s : Fin n → α) (c : α) : ((polyaUrnRule θ n) s) {c} = ENNReal.ofReal (polyaUrnPredictive θ (countVec s) c)

theorem ProbabilityTheory.isMarkovKernel_polyaUrnRule {α : Type u_1} [DecidableEq α] [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {θ : α → ℝ} [Nonempty α] (hθ : ∀ (i : α), 0 < θ i) (n : ℕ) : IsMarkovKernel (polyaUrnRule θ n)

theorem ProbabilityTheory.isProbabilityMeasure_polyaUrn {α : Type u_1} [DecidableEq α] [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {θ : α → ℝ} [Nonempty α] (hθ : ∀ (i : α), 0 < θ i) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (polyaUrn θ n)

theorem ProbabilityTheory.polyaUrn_singleton {α : Type u_1} [DecidableEq α] [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {θ : α → ℝ} [Nonempty α] (hθ : ∀ (i : α), 0 < θ i) {n : ℕ} (s : Fin n → α) : (polyaUrn θ n) {s} = ENNReal.ofReal (polyaUrnProb θ (countVec s))

The probability that the urn draws the sequence s is polyaUrnProb θ (countVec s).

theorem ProbabilityTheory.polyaUrn_real_singleton {α : Type u_1} [DecidableEq α] [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {θ : α → ℝ} [Nonempty α] (hθ : ∀ (i : α), 0 < θ i) {n : ℕ} (s : Fin n → α) : (polyaUrn θ n).real {s} = polyaUrnProb θ (countVec s)

theorem ProbabilityTheory.exchangeable_polyaUrn {α : Type u_1} [DecidableEq α] [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {θ : α → ℝ} [Nonempty α] (hθ : ∀ (i : α), 0 < θ i) (n : ℕ) : Exchangeable (polyaUrn θ n)

The sequence drawn from a Pólya urn is exchangeable ([Pit06] Exercise 2.2.2).