Blackwell–MacQueen urn

TheoremMeasurability of the Pólya urn predictive law#✓fully proved

The predictive law depends measurably on the previous draws.

theorem measurable_polyaUrnPredictive (α : ℝ) (H : Measure X) (n : ℕ) :
    Measurable fun xs : Fin n → X ↦ polyaUrnPredictive α H xs

Uses 1 · Used by 2

Statement usesBlackwell–MacQueen urn predictive law

Used byMoments of the Dirichlet process for at most two draws · Exchangeability of the Blackwell–MacQueen urn

DefinitionBlackwell–MacQueen urn#✓fully proved

The Blackwell–MacQueen urn with parameter α and base measure H: the joint law of the first n draws, where draw n has law polyaUrnPredictive α H xs given the previous draws xs (Blackwell–MacQueen 1973).

noncomputable def blackwellMacQueen (α : ℝ) (H : Measure X) : (n : ℕ) → Measure (Fin n → X)
  | 0 => Measure.dirac fun i ↦ i.elim0
  | n + 1 => (blackwellMacQueen α H n).bind fun xs ↦
      (polyaUrnPredictive α H xs).map fun x ↦ Fin.snoc (α := fun _ ↦ X) xs x

Uses 1 · Used by 7

Statement usesBlackwell–MacQueen urn predictive law

Used byThe predictive rule of the urn · The ties of the Blackwell–MacQueen urn follow the Chinese restaurant process · Blackwell–MacQueen urn law is a probability measure · Moments of the Dirichlet process for at most two draws · Exchangeability of the Blackwell–MacQueen urn · The moments of the Dirichlet process are the Blackwell–MacQueen urn · Ferguson's conjugacy

TheoremBlackwell–MacQueen urn law is a probability measure#✓fully proved

The urn law is a probability measure.

theorem isProbabilityMeasure_blackwellMacQueen {α : ℝ} (hα : 0 < α) (H : Measure X)
    [IsProbabilityMeasure H] (n : ℕ) : IsProbabilityMeasure (blackwellMacQueen α H n)

Uses 3 · Used by 1

Statement usesBlackwell–MacQueen urn

Proof usesBlackwell–MacQueen predictive law is a probability measure · Blackwell–MacQueen urn predictive law

Used byExchangeability of the Blackwell–MacQueen urn

TheoremThe predictive rule of the urn#✓fully proved

P(X₀ ∈ A₀, …, X_n ∈ A_n) is the integral over A₀ × ⋯ × A_{n-1} of the predictive probability (α H(A_n) + #{i < n | xᵢ ∈ A_n}) / (α + n).

theorem blackwellMacQueen_succ_pi (α : ℝ) (H : Measure X) [SFinite H] {n : ℕ}
    (A : Fin (n + 1) → Set X) (hA : ∀ i, MeasurableSet (A i)) :
    blackwellMacQueen α H (n + 1) (Set.univ.pi A) =
      ∫⁻ xs in Set.univ.pi fun i ↦ A (Fin.castSucc i),
        polyaUrnPredictive α H xs (A (Fin.last n)) ∂blackwellMacQueen α H n

Uses 2 · Used by 2

Statement usesBlackwell–MacQueen urn · Blackwell–MacQueen urn predictive law

Used byMoments of the Dirichlet process for at most two draws · Exchangeability of the Blackwell–MacQueen urn

TheoremPólya urn predictive law is invariant under reordering#✓fully proved

The predictive law does not depend on the order of the previous draws.

theorem polyaUrnPredictive_comp_perm (α : ℝ) (H : Measure X) {n : ℕ} (xs : Fin n → X)
    (σ : Equiv.Perm (Fin n)) : polyaUrnPredictive α H (xs ∘ σ) = polyaUrnPredictive α H xs

Uses 1 · Used by 1

Statement usesBlackwell–MacQueen urn predictive law

Used byExchangeability of the Blackwell–MacQueen urn

TheoremExchangeability of the Blackwell–MacQueen urn#✓fully proved

Exchangeability of the Blackwell–MacQueen urn (Blackwell–MacQueen 1973): relabeling the draws by a permutation does not change their joint law.

theorem map_perm_blackwellMacQueen (α : ℝ) (hα : 0 < α) (H : Measure X)
    [IsProbabilityMeasure H] {n : ℕ} (σ : Equiv.Perm (Fin n)) :
    (blackwellMacQueen α H n).map (fun xs ↦ xs ∘ σ) = blackwellMacQueen α H n

Uses 6

Statement usesBlackwell–MacQueen urn

Proof usesThe predictive rule of the urn · Blackwell–MacQueen urn law is a probability measure · Measurability of the Pólya urn predictive law · Blackwell–MacQueen urn predictive law · Pólya urn predictive law is invariant under reordering

DefinitionTie partition of a sequence of draws#✓fully proved

The partition of the indices {0, …, n-1} into groups of equal entries of xs.

noncomputable def tiePartition {n : ℕ} (xs : Fin n → X) : Finpartition (univ : Finset (Fin n)) :=
  haveI := Classical.decRel (Setoid.ker xs).r
  Finpartition.ofSetoid (Setoid.ker xs)

Used by 7

Used byThe ties of the Blackwell–MacQueen urn follow the Chinese restaurant process · Tie partition after forgetting the last draw · Measurability of the tie partition event · Blocks of the tie partition are classes of equal entries · Characterization of the tie partition · Last draw opens a new block iff it is new · Last draw joins a block iff it matches that block

TheoremBlocks of the tie partition are classes of equal entries#✓fully proved

Two indices lie in the same block of tiePartition xs iff the entries agree.

theorem mem_part_tiePartition {n : ℕ} (xs : Fin n → X) (i j : Fin n) :
    j ∈ (tiePartition xs).part i ↔ xs i = xs j

Uses 1 · Used by 5

Statement usesTie partition of a sequence of draws

Used byThe ties of the Blackwell–MacQueen urn follow the Chinese restaurant process · Tie partition after forgetting the last draw · Characterization of the tie partition · Last draw opens a new block iff it is new · Last draw joins a block iff it matches that block

TheoremCharacterization of the tie partition#✓fully proved

tiePartition xs = π iff equal entries are exactly the pairs in a common block of π.

theorem tiePartition_eq_iff {n : ℕ} (xs : Fin n → X) (π : Finpartition (univ : Finset (Fin n))) :
    tiePartition xs = π ↔ ∀ i j, (xs i = xs j ↔ j ∈ π.part i)

Uses 2 · Used by 1

Statement usesTie partition of a sequence of draws

Proof usesBlocks of the tie partition are classes of equal entries

Used byMeasurability of the tie partition event

TheoremTie partition after forgetting the last draw#✓fully proved

Forgetting the last draw restricts the tie partition to the earlier draws.

theorem comap_castSucc_tiePartition_snoc {n : ℕ} (xs : Fin n → X) (x : X) :
    (tiePartition (Fin.snoc (α := fun _ ↦ X) xs x)).comap Fin.castSucc = tiePartition xs

Uses 4 · Used by 3

Statement usesPull-back of a finite partition along a map · Tie partition of a sequence of draws

Proof usesBlocks of a pulled-back partition · Blocks of the tie partition are classes of equal entries

Used byThe ties of the Blackwell–MacQueen urn follow the Chinese restaurant process · Last draw opens a new block iff it is new · Last draw joins a block iff it matches that block

TheoremLast draw opens a new block iff it is new#✓fully proved

Where the last draw sits: a new table iff it differs from all earlier draws.

theorem tiePartition_snoc_eq_seat_none_iff {n : ℕ} (xs : Fin n → X) (x : X) :
    tiePartition (Fin.snoc (α := fun _ ↦ X) xs x) = seat (tiePartition xs) none ↔
      x ∉ Set.range xs

Uses 8 · Used by 1

Statement usesSeating a customer by a seating choice · Tie partition of a sequence of draws

Proof usesPull-back of a finite partition along a map · Every partition arises from seating the last customer · Seating a customer at an occupied table · Seating a customer at a new table · Tie partition after forgetting the last draw · Blocks of the tie partition are classes of equal entries

Used byThe ties of the Blackwell–MacQueen urn follow the Chinese restaurant process

TheoremLast draw joins a block iff it matches that block#✓fully proved

Where the last draw sits: at the table B iff it equals the earlier draws in B.

theorem tiePartition_snoc_eq_seat_some_iff {n : ℕ} (xs : Fin n → X) (x : X)
    (B : (tiePartition xs).parts) {i : Fin n} (hi : i ∈ B.1) :
    tiePartition (Fin.snoc (α := fun _ ↦ X) xs x) = seat (tiePartition xs) (some B) ↔
      x = xs i

Uses 8 · Used by 1

Statement usesSeating a customer by a seating choice · Tie partition of a sequence of draws

Proof usesPull-back of a finite partition along a map · Every partition arises from seating the last customer · Seating a customer at an occupied table · Seating a customer at a new table · Tie partition after forgetting the last draw · Blocks of the tie partition are classes of equal entries

Used byThe ties of the Blackwell–MacQueen urn follow the Chinese restaurant process

TheoremMeasurability of the tie partition event#✓fully proved

The event that the draws have a given tie partition is measurable.

theorem measurableSet_tiePartition_eq [MeasurableSingletonClass X]
    [MeasurableSpace.CountablySeparated X] {n : ℕ} (π : Finpartition (univ : Finset (Fin n))) :
    MeasurableSet {xs : Fin n → X | tiePartition xs = π}

Uses 2 · Used by 1

Statement usesTie partition of a sequence of draws

Proof usesCharacterization of the tie partition

Used byThe ties of the Blackwell–MacQueen urn follow the Chinese restaurant process

TheoremThe ties of the Blackwell–MacQueen urn follow the Chinese restaurant process#✓fully proved

The ties of the Blackwell–MacQueen urn follow the Chinese restaurant process (Pitman 2006, §3.1): for an atomless base measure, the partition of the first n draws into groups of equal values has the law α^{|π|} ∏_{B ∈ π} (|B| - 1)! / α^{(n)}.

theorem blackwellMacQueen_tiePartition [MeasurableSingletonClass X]
    [MeasurableSpace.CountablySeparated X] (α : ℝ) (hα : 0 < α) (H : Measure X)
    [IsProbabilityMeasure H] (hH : ∀ x, H {x} = 0) {n : ℕ}
    (π : Finpartition (univ : Finset (Fin n))) :
    blackwellMacQueen α H n {xs | tiePartition xs = π} =
      ENNReal.ofReal (MathlibExt.Biology.PopulationGenetics.ChineseRestaurant.crpProb α π)

Uses 19

Statement usesClosed-form law of the Chinese restaurant process · Blackwell–MacQueen urn · Tie partition of a sequence of draws

Proof usesProduct over block sizes · Pull-back of a finite partition along a map · Removing the last customer undoes a seating · Chinese restaurant process · Seating multiplies the closed-form law by the seating probability · Chinese restaurant process law as a real number · Every partition arises from seating the last customer · Seating a customer by a seating choice · Seating probabilities in the Chinese restaurant process · Tie partition after forgetting the last draw · Measurability of the tie partition event · Blocks of the tie partition are classes of equal entries · Blackwell–MacQueen urn predictive law · Predictive probability of a set in the Blackwell–MacQueen urn · Last draw opens a new block iff it is new · Last draw joins a block iff it matches that block

TheoremMoments of the Dirichlet process for at most two draws#✓fully proved

For n ≤ 2, E[∏_{i<n} G(Aᵢ)] = P(X₀ ∈ A₀, …, X_{n-1} ∈ A_{n-1}) for the Blackwell–MacQueen urn. The case n ≥ 3 is the wanted lintegral_dirichletProcess_prod.

theorem lintegral_dirichletProcess_prod_of_le_two (α : ℝ) (hα : 0 < α) (H : Measure X)
    [IsProbabilityMeasure H] {n : ℕ} (hn : n ≤ 2) (A : Fin n → Set X)
    (hA : ∀ i, MeasurableSet (A i)) :
    ∫⁻ ν, ∏ i, ν (A i) ∂dirichletProcess α hα H = blackwellMacQueen α H n (Set.univ.pi A)

Uses 15

Statement usesBlackwell–MacQueen urn · Dirichlet process

Proof usesStick-breaking process · Random measure of a stick-breaking process · The Blackwell–MacQueen urn for two draws · Sethuraman's canonical model is a Dirichlet process · The predictive rule of the urn · Mean of the Dirichlet process · Measurability of the Pólya urn predictive law · Measurability of the stick-breaking measure in its parameters · Blackwell–MacQueen urn predictive law · Predictive probability of a set in the Blackwell–MacQueen urn · Sethuraman's construction · Sethuraman's canonical probability space · Stick-breaking measure

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.