Ewens sampling formula and the Chinese restaurant process

DefinitionEwens sampling formula#✓fully proved

The Ewens sampling formula: the probability, under the neutral infinite-alleles model with scaled mutation rate θ = 4Nu, that a sample of n genes has allelic partition π (π.parts.count j alleles carried by exactly j genes each): n! * (∏ j, (θ / j) ^ (a j) / (a j)!) / θ^{(n)} (Ewens 1972), for θ > 0.

def ewensProb (θ : ℝ) {n : ℕ} (π : n.Partition) : ℝ :=
  (n.factorial : ℝ) / (ascPochhammer ℝ n).eval θ *
    ∏ j ∈ π.parts.toFinset,
      (θ / j) ^ (π.parts.count j) / ((π.parts.count j).factorial : ℝ)
Used by 14
Used byEwens conditional probability given the number of alleles · K is sufficient for θ · Factorization of the Ewens sampling formula · Probability of a given number of alleles under the Ewens formula · Law of the number of alleles · Validity of the Ewens–Watterson test · Cauchy's count by number of cycles · The allelic partition of the Chinese restaurant process follows the Ewens sampling formula · Nonnegativity of the Ewens sampling formula · Hoppe's urn generates the Ewens sampling formula · Nonnegativity of the Hoppe urn law · Expected number of tables · The Ewens sampling formula is a probability distribution · Expected number of alleles

TheoremThe Ewens sampling formula is a probability distribution#✓fully proved

The Ewens sampling formula is a probability distribution on the partitions of n (Ewens 1972; equivalently, Cauchy's cycle-type formula ∑_{σ ∈ S_n} θ^{#cycles σ} = θ^{(n)}).

theorem sum_ewensProb (θ : ℝ) (hθ : 0 < θ) (n : ℕ) :
    ∑ π : n.Partition, ewensProb θ π = 1
Uses 1 · Used by 2
Statement usesEwens sampling formula
Used byValidity of the Ewens–Watterson test · Cauchy's count by number of cycles

TheoremNonnegativity of the Ewens sampling formula#✓fully proved

The Ewens sampling formula is nonnegative for θ > 0; with sum_ewensProb it is a probability distribution on the partitions of n.

theorem ewensProb_nonneg {θ : ℝ} (hθ : 0 < θ) {n : ℕ} (π : n.Partition) :
    0 ≤ ewensProb θ π
Uses 1 · Used by 2
Statement usesEwens sampling formula
Used byNonnegativity of the Hoppe urn law · Expected number of tables

TheoremExpected number of alleles#✓fully proved

Expected number of alleles in a sample of n genes under the Ewens sampling formula: E[K_n] = ∑_{i < n} θ / (θ + i) (Ewens 1972).

theorem sum_ewensProb_mul_card_parts (θ : ℝ) (hθ : 0 < θ) (n : ℕ) :
    ∑ π : n.Partition, ewensProb θ π * (π.parts.card : ℝ) =
      ∑ i ∈ range n, θ / (θ + i)
Uses 1 · Used by 1
Statement usesEwens sampling formula
Used byExpected number of tables

DefinitionOne step of Hoppe's urn#✓fully proved

One step of Hoppe's urn on allelic partitions (Hoppe 1984): from a partition π of k, the next gene carries a new allele with probability θ / (θ + k) (target parts 1 ::ₘ π.parts), and copies an allele carried by j genes with probability j * a j / (θ + k), where a j = π.parts.count j (target parts (j + 1) ::ₘ π.parts.erase j). The value is the transition probability from π to π'.

def hoppeStep (θ : ℝ) {k : ℕ} (π : k.Partition) (π' : (k + 1).Partition) : ℝ :=
  (if π'.parts = 1 ::ₘ π.parts then θ / (θ + k) else 0) +
    ∑ j ∈ π.parts.toFinset,
      if π'.parts = (j + 1) ::ₘ π.parts.erase j then
        (j * π.parts.count j : ℝ) / (θ + k) else 0
Used by 5
Used byThe block sizes follow Hoppe's urn · Law of the allelic partition from Hoppe's urn · Hoppe's urn generates the Ewens sampling formula · Hoppe urn transition probabilities are nonnegative · Hoppe urn transition is stochastic

DefinitionLaw of the allelic partition from Hoppe's urn#✓fully proved

The law of the allelic partition after n draws from Hoppe's urn, started from the empty sample: hoppeLaw θ (n + 1) π' = ∑ π, hoppeLaw θ n π * hoppeStep θ π π'.

def hoppeLaw (θ : ℝ) : (n : ℕ) → n.Partition → ℝ
  | 0, _ => 1
  | n + 1, π' => ∑ π : n.Partition, hoppeLaw θ n π * hoppeStep θ π π'
Uses 1 · Used by 4
Statement usesOne step of Hoppe's urn
Used byThe allelic partition of the Chinese restaurant process follows the Ewens sampling formula · The block sizes follow Hoppe's urn · Hoppe's urn generates the Ewens sampling formula · Nonnegativity of the Hoppe urn law

TheoremHoppe urn transition probabilities are nonnegative#✓fully proved

Hoppe-urn transition probabilities are nonnegative.

theorem hoppeStep_nonneg {θ : ℝ} (hθ : 0 < θ) {k : ℕ} (π : k.Partition)
    (π' : (k + 1).Partition) : 0 ≤ hoppeStep θ π π'
Uses 1 · Used by 1
Statement usesOne step of Hoppe's urn
Used byThe block sizes follow Hoppe's urn

TheoremHoppe urn transition is stochastic#✓fully proved

The Hoppe-urn transition is stochastic: from every partition of k the probabilities of the partitions of k + 1 sum to one.

theorem sum_hoppeStep {θ : ℝ} (hθ : 0 < θ) {k : ℕ} (π : k.Partition) :
    ∑ π' : (k + 1).Partition, hoppeStep θ π π' = 1
Uses 1
Statement usesOne step of Hoppe's urn

TheoremHoppe's urn generates the Ewens sampling formula#✓fully proved

Hoppe's urn generates the Ewens sampling formula (Hoppe 1984): after n draws, the allelic partition has law ewensProb θ.

theorem hoppeLaw_eq_ewensProb {θ : ℝ} (hθ : 0 < θ) {n : ℕ} (π : n.Partition) :
    hoppeLaw θ n π = ewensProb θ π
Uses 3 · Used by 2
Statement usesEwens sampling formula · Law of the allelic partition from Hoppe's urn
Proof usesOne step of Hoppe's urn
Used byThe allelic partition of the Chinese restaurant process follows the Ewens sampling formula · Nonnegativity of the Hoppe urn law

TheoremNonnegativity of the Hoppe urn law#✓fully proved

The law of Hoppe's urn after n draws is nonnegative for θ > 0.

theorem hoppeLaw_nonneg {θ : ℝ} (hθ : 0 < θ) {n : ℕ} (π : n.Partition) :
    0 ≤ hoppeLaw θ n π
Uses 4 · Used by 1
Statement usesLaw of the allelic partition from Hoppe's urn
Proof usesEwens sampling formula · Nonnegativity of the Ewens sampling formula · Hoppe's urn generates the Ewens sampling formula
Used byThe block sizes follow Hoppe's urn

DefinitionSeating a customer at a new table#✓fully proved

Seat customer n at a new table: the partition of Fin (n + 1) whose blocks are the blocks of π (relabeled into Fin (n + 1)) together with the singleton {n}.

MathlibExt.Biology.PopulationGenetics.ChineseRestaurant.newTable · 30 lines 
def newTable {n : ℕ} (π : Finpartition (univ : Finset (Fin n))) :
    Finpartition (univ : Finset (Fin (n + 1))) :=
  Finpartition.ofExistsUnique
    (insert {Fin.last n} (π.parts.map (mapEmbedding Fin.castSuccEmb).toEmbedding))
    (fun _ _ ↦ subset_univ _)
    (fun a _ ↦ by
      induction a using Fin.lastCases with
      | last =>
        refine ⟨{Fin.last n}, ⟨mem_insert_self _ _, mem_singleton_self _⟩, ?_⟩
        rintro t ⟨ht, hat⟩
        simp only [mem_insert, mem_map, RelEmbedding.coe_toEmbedding, mapEmbedding_apply] at ht
        rcases ht with rfl | ⟨B, -, rfl⟩
        · rfl
        · simp [Fin.castSucc_ne_last] at hat
      | cast i =>
        obtain ⟨B, ⟨hB, hiB⟩, hu⟩ := π.existsUnique_mem (mem_univ i)
        refine ⟨B.map Fin.castSuccEmb, ⟨mem_insert_of_mem (mem_map_of_mem _ hB), ?_⟩, ?_⟩
        · simpa using hiB
        · rintro t ⟨ht, hat⟩
          simp only [mem_insert, mem_map, RelEmbedding.coe_toEmbedding,
            mapEmbedding_apply] at ht
          rcases ht with rfl | ⟨B', hB', rfl⟩
          · simp [Fin.castSucc_ne_last] at hat
          · rw [hu B' ⟨hB', by simpa using hat⟩])
    (by
      simp only [mem_insert, mem_map, RelEmbedding.coe_toEmbedding, mapEmbedding_apply,
        not_or]
      refine ⟨(singleton_ne_empty _).symm, ?_⟩
      rintro ⟨B, hB, h⟩
      exact π.ne_empty hB (map_eq_empty.1 h))
Used by 7
Used byRemoving the last customer undoes a seating · The block sizes follow Hoppe's urn · Blocks of the partition after opening a new table · Seating a customer by a seating choice · Injectivity of seating · Last draw opens a new block iff it is new · Last draw joins a block iff it matches that block

DefinitionSeating a customer at an occupied table#✓fully proved

Seat customer n at the occupied table B of π: the block B becomes B ∪ {n} and the other blocks are unchanged.

MathlibExt.Biology.PopulationGenetics.ChineseRestaurant.joinTable · 41 lines 
def joinTable {n : ℕ} (π : Finpartition (univ : Finset (Fin n))) (B : Finset (Fin n))
    (hB : B ∈ π.parts) : Finpartition (univ : Finset (Fin (n + 1))) :=
  Finpartition.ofExistsUnique
    (insert (insert (Fin.last n) (B.map Fin.castSuccEmb))
      ((π.parts.erase B).map (mapEmbedding Fin.castSuccEmb).toEmbedding))
    (fun _ _ ↦ subset_univ _)
    (fun a _ ↦ by
      induction a using Fin.lastCases with
      | last =>
        refine ⟨_, ⟨mem_insert_self _ _, mem_insert_self _ _⟩, ?_⟩
        rintro t ⟨ht, hat⟩
        simp only [mem_insert, mem_map, RelEmbedding.coe_toEmbedding, mapEmbedding_apply] at ht
        rcases ht with rfl | ⟨C, -, rfl⟩
        · rfl
        · simp [Fin.castSucc_ne_last] at hat
      | cast i =>
        obtain ⟨C, ⟨hC, hiC⟩, hu⟩ := π.existsUnique_mem (mem_univ i)
        by_cases hCB : C = B
        · subst hCB
          refine ⟨_, ⟨mem_insert_self _ _, by simpa using hiC⟩, ?_⟩
          rintro t ⟨ht, hat⟩
          simp only [mem_insert, mem_map, RelEmbedding.coe_toEmbedding,
            mapEmbedding_apply, mem_erase] at ht
          rcases ht with rfl | ⟨C', ⟨hC'C, hC'⟩, rfl⟩
          · rfl
          · exact absurd (hu C' ⟨hC', by simpa using hat⟩) hC'C
        · refine ⟨C.map Fin.castSuccEmb, ⟨mem_insert_of_mem (mem_map_of_mem _
            (mem_erase.2 ⟨hCB, hC⟩)), by simpa using hiC⟩, ?_⟩
          rintro t ⟨ht, hat⟩
          simp only [mem_insert, mem_map, RelEmbedding.coe_toEmbedding,
            mapEmbedding_apply, mem_erase] at ht
          rcases ht with rfl | ⟨C', ⟨-, hC'⟩, rfl⟩
          · have hiB : i ∈ B := by simpa [Fin.castSucc_ne_last] using hat
            exact absurd (hu B ⟨hB, hiB⟩).symm hCB
          · rw [hu C' ⟨hC', by simpa using hat⟩])
    (by
      simp only [mem_insert, mem_map, RelEmbedding.coe_toEmbedding, mapEmbedding_apply,
        not_or, mem_erase]
      refine ⟨(insert_ne_empty _ _).symm, ?_⟩
      rintro ⟨C, ⟨-, hC⟩, h⟩
      exact π.ne_empty hC (map_eq_empty.1 h))
Used by 7
Used byRemoving the last customer undoes a seating · The block sizes follow Hoppe's urn · Blocks of the partition after joining a table · Seating a customer by a seating choice · Injectivity of seating · Last draw opens a new block iff it is new · Last draw joins a block iff it matches that block

TheoremBlocks of the partition after opening a new table#✓fully proved

The blocks of newTable π.

@[simp]
theorem parts_newTable {n : ℕ} (π : Finpartition (univ : Finset (Fin n))) :
    (newTable π).parts =
      insert {Fin.last n} (π.parts.map (mapEmbedding Fin.castSuccEmb).toEmbedding)
Uses 1 · Used by 2
Statement usesSeating a customer at a new table
Used byRemoving the last customer undoes a seating · Injectivity of seating

TheoremBlocks of the partition after joining a table#✓fully proved

The blocks of joinTable π B hB.

@[simp]
theorem parts_joinTable {n : ℕ} (π : Finpartition (univ : Finset (Fin n))) (B : Finset (Fin n))
    (hB : B ∈ π.parts) :
    (joinTable π B hB).parts =
      insert (insert (Fin.last n) (B.map Fin.castSuccEmb))
        ((π.parts.erase B).map (mapEmbedding Fin.castSuccEmb).toEmbedding)
Uses 1 · Used by 2
Statement usesSeating a customer at an occupied table
Used byRemoving the last customer undoes a seating · Injectivity of seating

DefinitionSeating a customer by a seating choice#✓fully proved

Seat customer n according to the choice c: none opens a new table, some B joins the occupied table B.

def seat {n : ℕ} (π : Finpartition (univ : Finset (Fin n))) :
    Option π.parts → Finpartition (univ : Finset (Fin (n + 1)))
  | none => newTable π
  | some B => joinTable π B.1 B.2
Uses 2 · Used by 11
Statement usesSeating a customer at an occupied table · Seating a customer at a new table
Used byRemoving the last customer undoes a seating · Law of the Chinese restaurant process · The block sizes follow Hoppe's urn · Consistency of the Chinese restaurant process · Seating multiplies the closed-form law by the seating probability · One step of the Chinese restaurant process · Every partition arises from seating the last customer · Injectivity of seating · The 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

DefinitionSeating probabilities in the Chinese restaurant process#✓fully proved

The probability of each seating choice for customer n given the partition π of the first n customers: θ / (n + θ) for a new table, |B| / (n + θ) for the table B.

def seatWeight (θ : ℝ) {n : ℕ} (π : Finpartition (univ : Finset (Fin n))) :
    Option π.parts → ℝ
  | none => θ / (n + θ)
  | some B => #B.1 / (n + θ)
Used by 7
Used byLaw of the Chinese restaurant process · The block sizes follow Hoppe's urn · Seating multiplies the closed-form law by the seating probability · Seating choice distribution of a customer · Nonnegativity of seating probabilities · Seating probabilities sum to one · The ties of the Blackwell–MacQueen urn follow the Chinese restaurant process

TheoremNonnegativity of seating probabilities#✓fully proved

The seating probabilities are nonnegative for θ > 0.

theorem seatWeight_nonneg {θ : ℝ} (hθ : 0 < θ) {n : ℕ}
    (π : Finpartition (univ : Finset (Fin n))) (c : Option π.parts) :
    0 ≤ seatWeight θ π c
Uses 1 · Used by 2
Statement usesSeating probabilities in the Chinese restaurant process
Used byThe block sizes follow Hoppe's urn · Seating choice distribution of a customer

TheoremSeating probabilities sum to one#✓fully proved

The seating probabilities sum to one for θ > 0.

theorem sum_seatWeight {θ : ℝ} (hθ : 0 < θ) {n : ℕ}
    (π : Finpartition (univ : Finset (Fin n))) :
    ∑ c, seatWeight θ π c = 1
Uses 1 · Used by 1
Statement usesSeating probabilities in the Chinese restaurant process
Used bySeating choice distribution of a customer

DefinitionSeating choice distribution of a customer#✓fully proved

The seating choice of customer n, as a probability distribution.

def seatChoice (θ : ℝ) (hθ : 0 < θ) {n : ℕ} (π : Finpartition (univ : Finset (Fin n))) :
    PMF (Option π.parts) :=
  PMF.ofFintype (fun c ↦ ENNReal.ofReal (seatWeight θ π c)) (by
    rw [← ENNReal.ofReal_sum_of_nonneg (fun c _ ↦ seatWeight_nonneg hθ π c),
      sum_seatWeight hθ, ENNReal.ofReal_one])
Uses 3 · Used by 4
Statement usesSeating probabilities in the Chinese restaurant process · Nonnegativity of seating probabilities · Seating probabilities sum to one
Used byLaw of the Chinese restaurant process · The block sizes follow Hoppe's urn · Consistency of the Chinese restaurant process · One step of the Chinese restaurant process

DefinitionOne step of the Chinese restaurant process#✓fully proved

One step of the Chinese restaurant process: the law of the partition of Fin (n + 1) given the partition π of the first n customers.

def crpStep (θ : ℝ) (hθ : 0 < θ) {n : ℕ} (π : Finpartition (univ : Finset (Fin n))) :
    PMF (Finpartition (univ : Finset (Fin (n + 1)))) :=
  (seatChoice θ hθ π).map (seat π)
Uses 2 · Used by 4
Statement usesSeating a customer by a seating choice · Seating choice distribution of a customer
Used byChinese restaurant process · Law of the Chinese restaurant process · The block sizes follow Hoppe's urn · Consistency of the Chinese restaurant process

DefinitionChinese restaurant process#✓fully proved

The Chinese restaurant process with parameter θ > 0: the law of the random partition of the customers Fin n into tables, built one customer at a time by crpStep (Aldous 1985, §11; Pitman 2006, ch. 3).

def crp (θ : ℝ) (hθ : 0 < θ) : (n : ℕ) → PMF (Finpartition (univ : Finset (Fin n)))
  | 0 => PMF.pure ⊥
  | n + 1 => (crp θ hθ n).bind (crpStep θ hθ)
Uses 1 · Used by 10
Statement usesOne step of the Chinese restaurant process
Used byLaw of the Chinese restaurant process · Exchangeability · The allelic partition of the Chinese restaurant process follows the Ewens sampling formula · The block sizes follow Hoppe's urn · Exchangeability of the Chinese restaurant process · Consistency of the Chinese restaurant process · Consistency for every sample size · Chinese restaurant process law as a real number · Expected number of tables · The ties of the Blackwell–MacQueen urn follow the Chinese restaurant process

DefinitionClosed-form law of the Chinese restaurant process#✓fully proved

The closed-form law of the Chinese restaurant process, θ^{|π|} ∏_{B ∈ π} (|B| - 1)! / θ^{(n)} (Pitman 2006, §3.1). Every block is nonempty, so |B| - 1 is never a truncated natural subtraction.

def crpProb (θ : ℝ) {n : ℕ} (π : Finpartition (univ : Finset (Fin n))) : ℝ :=
  θ ^ #π.parts * π.cardProd (fun k ↦ ((k - 1).factorial : ℝ)) / (ascPochhammer ℝ n).eval θ
Uses 1 · Used by 5
Statement usesProduct over block sizes
Used byLaw of the Chinese restaurant process · Exchangeability · Seating multiplies the closed-form law by the seating probability · Chinese restaurant process law as a real number · The ties of the Blackwell–MacQueen urn follow the Chinese restaurant process

TheoremRemoving the last customer undoes a seating#✓fully proved

Removing the last customer undoes every seating: restricting seat π c to the first n customers gives back π.

theorem comap_castSucc_seat {n : ℕ} (π : Finpartition (univ : Finset (Fin n)))
    (c : Option π.parts) : (seat π c).comap Fin.castSucc = π
Uses 7 · Used by 3
Statement usesPull-back of a finite partition along a map · Seating a customer by a seating choice
Proof usesBlocks of a pulled-back partition · Seating a customer at an occupied table · Seating a customer at a new table · Blocks of the partition after joining a table · Blocks of the partition after opening a new table
Used byLaw of the Chinese restaurant process · Consistency of the Chinese restaurant process · The ties of the Blackwell–MacQueen urn follow the Chinese restaurant process

TheoremInjectivity of seating#✓fully proved

Different seating choices give different partitions.

theorem seat_injective {n : ℕ} (π : Finpartition (univ : Finset (Fin n))) :
    Function.Injective (seat π)
Uses 5 · Used by 1
Statement usesSeating a customer by a seating choice
Proof usesSeating a customer at an occupied table · Seating a customer at a new table · Blocks of the partition after joining a table · Blocks of the partition after opening a new table
Used byLaw of the Chinese restaurant process

TheoremEvery partition arises from seating the last customer#✓fully proved

Every partition of Fin (n + 1) arises by seating customer n into its restriction to the first n customers.

theorem exists_seat_eq {n : ℕ} (π' : Finpartition (univ : Finset (Fin (n + 1)))) :
    ∃ c, seat (π'.comap Fin.castSucc) c = π'
Uses 3 · Used by 4
Statement usesPull-back of a finite partition along a map · Seating a customer by a seating choice
Proof usesBlocks of a pulled-back partition
Used byLaw of the Chinese restaurant process · The 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

LemmaSeating multiplies the closed-form law by the seating probability#✓fully proved

One seating multiplies the closed-form law by the seating probability.

lemma crpProb_seat {θ : ℝ} (hθ : 0 < θ) {n : ℕ}
    (π : Finpartition (univ : Finset (Fin n))) (c : Option π.parts) :
    crpProb θ (seat π c) = crpProb θ π * seatWeight θ π c
Uses 4 · Used by 2
Statement usesClosed-form law of the Chinese restaurant process · Seating a customer by a seating choice · Seating probabilities in the Chinese restaurant process
Proof usesProduct over block sizes
Used byLaw of the Chinese restaurant process · The ties of the Blackwell–MacQueen urn follow the Chinese restaurant process

TheoremLaw of the Chinese restaurant process#✓fully proved

Law of the Chinese restaurant process (Pitman 2006, §3.1): P(π) = θ^{|π|} ∏_{B ∈ π} (|B| - 1)! / θ^{(n)}.

theorem crp_apply {θ : ℝ} (hθ : 0 < θ) {n : ℕ} (π : Finpartition (univ : Finset (Fin n))) :
    crp θ hθ n π = ENNReal.ofReal (crpProb θ π)
Uses 12 · Used by 2
Statement usesChinese restaurant process · Closed-form law of the Chinese restaurant process
Proof usesProduct over block sizes · Pull-back of a finite partition along a map · Removing the last customer undoes a seating · Seating multiplies the closed-form law by the seating probability · One step of the Chinese restaurant process · Every partition arises from seating the last customer · Seating a customer by a seating choice · Seating choice distribution of a customer · Seating probabilities in the Chinese restaurant process · Injectivity of seating
Used byExchangeability · Chinese restaurant process law as a real number

TheoremChinese restaurant process law as a real number#✓fully proved

The law of the Chinese restaurant process as a real number.

theorem crp_toReal {θ : ℝ} (hθ : 0 < θ) {n : ℕ} (π : Finpartition (univ : Finset (Fin n))) :
    (crp θ hθ n π).toReal = crpProb θ π
Uses 4 · Used by 1
Statement usesChinese restaurant process · Closed-form law of the Chinese restaurant process
Proof usesProduct over block sizes · Law of the Chinese restaurant process
Used byThe ties of the Blackwell–MacQueen urn follow the Chinese restaurant process

TheoremExchangeability#✓fully proved

Exchangeability, pointwise: relabeling the customers by a permutation σ does not change the probability of a partition.

theorem crp_comap_perm {θ : ℝ} (hθ : 0 < θ) {n : ℕ} (σ : Equiv.Perm (Fin n))
    (π : Finpartition (univ : Finset (Fin n))) :
    crp θ hθ n (π.comap σ) = crp θ hθ n π
Uses 7 · Used by 1
Statement usesPull-back of a finite partition along a map · Chinese restaurant process
Proof usesProduct over block sizes · Pull-back along an equivalence preserves block-size products · Pull-back along an equivalence preserves the number of blocks · Closed-form law of the Chinese restaurant process · Law of the Chinese restaurant process
Used byExchangeability of the Chinese restaurant process

TheoremExchangeability of the Chinese restaurant process#✓fully proved

Exchangeability of the Chinese restaurant process (Aldous 1985, §11): the law of the partition relabeled by any permutation of the customers is the law of the partition.

theorem crp_map_comap_perm {θ : ℝ} (hθ : 0 < θ) {n : ℕ} (σ : Equiv.Perm (Fin n)) :
    (crp θ hθ n).map (Finpartition.comap σ) = crp θ hθ n
Uses 4
Statement usesPull-back of a finite partition along a map · Chinese restaurant process
Proof usesPulling back along an equivalence and its inverse · Exchangeability

TheoremConsistency of the Chinese restaurant process#✓fully proved

Restricting the random partition of Fin (n + 1) to the first n customers gives the process with n customers.

theorem crp_map_restrict {θ : ℝ} (hθ : 0 < θ) (n : ℕ) :
    (crp θ hθ (n + 1)).map (Finpartition.comap Fin.castSucc) = crp θ hθ n
Uses 6 · Used by 1
Statement usesPull-back of a finite partition along a map · Chinese restaurant process
Proof usesRemoving the last customer undoes a seating · One step of the Chinese restaurant process · Seating a customer by a seating choice · Seating choice distribution of a customer
Used byConsistency for every sample size

TheoremConsistency for every sample size#✓fully proved

Restricting the random partition of Fin n to the first m ≤ n customers gives the process with m customers.

theorem crp_map_restrict_castLE {θ : ℝ} (hθ : 0 < θ) {m n : ℕ} (h : m ≤ n) :
    (crp θ hθ n).map (Finpartition.comap (Fin.castLE h)) = crp θ hθ m
Uses 5
Statement usesPull-back of a finite partition along a map · Chinese restaurant process
Proof usesPulling back a partition along a composite · Pulling back a partition along the identity · Consistency of the Chinese restaurant process

DefinitionAllelic partition of a set partition#✓fully proved

The allelic partition of a set partition of Fin n: the multiset of its block sizes, a partition of the integer n.

def blockSizes {n : ℕ} (π : Finpartition (univ : Finset (Fin n))) : n.Partition where
  parts := π.parts.val.map card
  parts_pos := by
    simp only [Multiset.mem_map, mem_val]
    rintro _ ⟨B, hB, rfl⟩
    exact (π.nonempty_of_mem_parts hB).card_pos
  parts_sum := by
    rw [← sum_eq_multiset_sum, π.sum_card_parts, card_univ, Fintype.card_fin]
Used by 3
Used byThe allelic partition of the Chinese restaurant process follows the Ewens sampling formula · The block sizes follow Hoppe's urn · Expected number of tables

TheoremThe block sizes follow Hoppe's urn#✓fully proved

The law of the multiset of block sizes after n customers is the law Ewens.hoppeLaw of Hoppe's urn on allelic partitions after n draws.

theorem crp_map_blockSizes_eq_hoppeLaw {θ : ℝ} (hθ : 0 < θ) {n : ℕ} (p : n.Partition) :
    (crp θ hθ n).map blockSizes p = ENNReal.ofReal (hoppeLaw θ n p)
Uses 13 · Used by 1
Statement usesAllelic partition of a set partition · Chinese restaurant process · Law of the allelic partition from Hoppe's urn
Proof usesOne step of the Chinese restaurant process · Seating a customer at an occupied table · Seating a customer at a new table · Seating a customer by a seating choice · Seating choice distribution of a customer · Seating probabilities in the Chinese restaurant process · Nonnegativity of seating probabilities · Nonnegativity of the Hoppe urn law · One step of Hoppe's urn · Hoppe urn transition probabilities are nonnegative
Used byThe allelic partition of the Chinese restaurant process follows the Ewens sampling formula

TheoremThe allelic partition of the Chinese restaurant process follows the Ewens sampling formula#✓fully proved

The allelic partition of the Chinese restaurant process follows the Ewens sampling formula (Ewens 1972; Hoppe 1984): the multiset of block sizes after n customers has law Ewens.ewensProb θ.

theorem crp_map_blockSizes {θ : ℝ} (hθ : 0 < θ) {n : ℕ} (p : n.Partition) :
    (crp θ hθ n).map blockSizes p = ENNReal.ofReal (ewensProb θ p)
Uses 6 · Used by 1
Statement usesAllelic partition of a set partition · Chinese restaurant process · Ewens sampling formula
Proof usesThe block sizes follow Hoppe's urn · Law of the allelic partition from Hoppe's urn · Hoppe's urn generates the Ewens sampling formula
Used byExpected number of tables

TheoremExpected number of tables#✓fully proved

Expected number of tables (expected number of alleles in a sample of n genes, Ewens 1972): E[|π|] = ∑_{i < n} θ / (θ + i).

theorem sum_crp_toReal_mul_card_parts {θ : ℝ} (hθ : 0 < θ) (n : ℕ) :
    ∑ π : Finpartition (univ : Finset (Fin n)), (crp θ hθ n π).toReal * #π.parts =
      ∑ i ∈ range n, θ / (θ + i)
Uses 6
Statement usesChinese restaurant process
Proof usesAllelic partition of a set partition · The allelic partition of the Chinese restaurant process follows the Ewens sampling formula · Ewens sampling formula · Nonnegativity of the Ewens sampling formula · Expected number of alleles
36 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.