The Pitman–Yor partition

The two-parameter family of random partitions of [Pit06] §3.2, generated by the (α, θ) seating plan of the Chinese restaurant process: the first customer sits at a table of their own, and when n customers sit at k tables, n_i of them at table i, the next customer joins table i with probability (n_i - α) / (n + θ) and opens a new table with probability (θ + k α) / (n + θ). The seating is a sequence of table labels, each customer labelled by the first customer at their table, drawn from this prediction rule (crpRule, with seqLaw); pitmanYor α θ n is the law of the partition of Fin n it generates.

Theorem 3.2 of [Pit06] computes the law: a partition whose blocks have sizes n_1, …, n_k has probability

p(n_1, …, n_k) = (θ + α)_{k-1↑α} ∏ᵢ (1 - α)_{nᵢ-1↑1} / (θ + 1)_{n-1↑1},

where (x)_{m↑s} = x (x + s) ⋯ (x + (m - 1) s). This is pitmanYorEPPF, the exchangeable partition probability function: the probability depends on the partition only through its block sizes, so the law is invariant under relabelling, exchangeable in the sense of [Pit06] §2.1 (smulInvariantMeasure_pitmanYor).

Main definitions

• ProbabilityTheory.pitmanYorEPPF α θ s: the probability of a partition whose multiset of block sizes is s.
• ProbabilityTheory.crpRule α θ n: the seating plan on table labels, as a prediction rule.
• ProbabilityTheory.pitmanYor α θ n: the law of the partition of n customers by table.

Main results

• ProbabilityTheory.isProbabilityMeasure_pitmanYor: for 0 ≤ α ≤ 1 and -α < θ the seating plan defines a probability measure.
• ProbabilityTheory.seqLaw_crpRule_singleton: a sequence of table labels has the probability of the partition it generates if each label is the first customer at its table, and 0 otherwise.
• ProbabilityTheory.pitmanYor_real_singleton: the law of the partition is the EPPF ([Pit06] Theorem 3.2).
• ProbabilityTheory.smulInvariantMeasure_pitmanYor: the partition is exchangeable.
• ProbabilityTheory.pitmanYorEPPF_cons_one, ProbabilityTheory.pitmanYorEPPF_cons_succ_erase: the EPPF's two seating recursions, the second being [Pit06] (3.22).
• ProbabilityTheory.pitmanYorEPPF_zero_left: at α = 0 the EPPF is the Ewens sampling formula.

Implementation notes

Tables are labelled by their first customer, so a new table opened by customer n is labelled n and the valid label sequences are those equal to the labelling of their partition by least elements (Finpartition.minLabel). Each partition has exactly one such labelling, which gives the law of the partition from that of the labels. The seating plan starts from one customer at one table ([Pit06] p. 60): the rule for the first customer is the point mass at label 0, as the general formula would read θ / θ. The products in the EPPF are written over Ico 1 m, (θ + α)_{k-1↑α} = ∏_{1 ≤ i < k} (θ + i α) and so on, avoiding truncated subtraction. The parameters are unbundled: the measure is defined for all real α, θ, and the constraints of [Pit06] (3.5), second case, are hypotheses of the theorems that need them. The first case of (3.5), α < 0 with θ = m (-α), is not treated.

TODO

• The partitions Π_n are consistent as n grows and form an exchangeable random partition of ℕ ([Pit06] Theorem 3.2); this needs the label sequence as a trajectory measure (ProbabilityTheory.Kernel.traj).

References

• [Pit06]

Labelling by least elements

def Finpartition.minLabel {n : ℕ} (P : Finpartition Finset.univ) (i : Fin n) : ℕ

The label of i in a partition of Fin n is the least element of its block.

Equations

• P.minLabel i = ↑((P.part i).min' ⋯)

theorem Finpartition.minLabel_le {n : ℕ} (P : Finpartition Finset.univ) (i : Fin n) : P.minLabel i ≤ ↑i

theorem Finpartition.minLabel_eq_of_mem {n : ℕ} {P : Finpartition Finset.univ} {i j : Fin n} (hj : j ∈ P.part i) (hmin : ∀ k ∈ P.part i, j ≤ k) : P.minLabel i = ↑j

theorem Finpartition.ofFun_minLabel {n : ℕ} (P : Finpartition Finset.univ) : ofFun P.minLabel = P

A partition of Fin n is generated by its labelling by least elements.

theorem Finpartition.le_of_minLabel_ofFun_eq {n : ℕ} {s : Fin n → ℕ} (hs : (ofFun s).minLabel = s) (k : Fin n) : s k ≤ ↑k ∧ ∃ (h : s k < n), s ⟨s k, h⟩ = s k ∧ ∀ (k' : Fin n), s k = s k' → s k ≤ ↑k'

In a sequence of least-element labels, each label is the index where it first occurs.

theorem Finpartition.minLabel_ofFun_snoc {n : ℕ} {s : Fin n → ℕ} (hs : (ofFun s).minLabel = s) {c : ℕ} (hc : c ∈ Finset.image s Finset.univ ∨ c = n) : (ofFun (Fin.snoc s c)).minLabel = Fin.snoc s c

Appending an earlier label, or the next index, to a sequence of least-element labels gives a sequence of least-element labels.

theorem Finpartition.minLabel_ofFun_of_snoc {n : ℕ} {s : Fin n → ℕ} {c : ℕ} (hs : (ofFun (Fin.snoc s c)).minLabel = Fin.snoc s c) : (ofFun s).minLabel = s ∧ (c ∈ Finset.image s Finset.univ ∨ c = n)

A sequence of least-element labels stays one when its last entry is removed, and its last entry is an earlier label or the next index.

theorem Finpartition.image_snoc {n : ℕ} {β : Type u_2} [DecidableEq β] (s : Fin n → β) (c : β) : Finset.image (Fin.snoc s c) Finset.univ = insert c (Finset.image s Finset.univ)

theorem Finpartition.card_filter_snoc {n : ℕ} {β : Type u_2} [DecidableEq β] (s : Fin n → β) (c v : β) : {i : Fin (n + 1) | Fin.snoc s c i = v}.card = {i : Fin n | s i = v}.card + if c = v then 1 else 0

theorem Finpartition.partSizes_ofFun_snoc_of_notMem {n : ℕ} {β : Type u_2} [DecidableEq β] {s : Fin n → β} {c : β} (hc : c ∉ Finset.image s Finset.univ) : (ofFun (Fin.snoc s c)).partSizes = 1 ::ₘ (ofFun s).partSizes

Appending a new value adds a block of size one.

theorem Finpartition.partSizes_ofFun_snoc_of_mem {n : ℕ} {β : Type u_2} [DecidableEq β] {s : Fin n → β} {c : β} (hc : c ∈ Finset.image s Finset.univ) : (ofFun (Fin.snoc s c)).partSizes = ({i : Fin n | s i = c}.card + 1) ::ₘ (ofFun s).partSizes.erase {i : Fin n | s i = c}.card

Appending an existing value enlarges its block by one.

@[instance_reducible]

instance ProbabilityTheory.instMeasurableSpaceFinpartitionFinset_linglib {ι : Type u_1} [DecidableEq ι] {s : Finset ι} : MeasurableSpace (Finpartition s)

Equations

• ProbabilityTheory.instMeasurableSpaceFinpartitionFinset_linglib = ⊤

instance ProbabilityTheory.instDiscreteMeasurableSpaceFinpartitionFinset_linglib {ι : Type u_1} [DecidableEq ι] {s : Finset ι} : DiscreteMeasurableSpace (Finpartition s)

noncomputable def ProbabilityTheory.pitmanYorEPPF (α θ : ℝ) (s : Multiset ℕ) : ℝ

The exchangeable partition probability function of the Pitman–Yor partition ([Pit06] (3.6)): the probability that the seating of n customers is a given set partition whose multiset of block sizes is s, where n = s.sum.

Equations

• ProbabilityTheory.pitmanYorEPPF α θ s = (∏ i ∈ Finset.Ico 1 s.card, (θ + ↑i * α)) * (Multiset.map (fun (m : ℕ) => ∏ j ∈ Finset.Ico 1 m, (↑j - α)) s).prod / ∏ i ∈ Finset.Ico 1 s.sum, (θ + ↑i)

theorem ProbabilityTheory.pitmanYorEPPF_cons_one {α θ : ℝ} {s : Multiset ℕ} (hs : s.sum ≠ 0) : pitmanYorEPPF α θ (1 ::ₘ s) = pitmanYorEPPF α θ s * ((θ + ↑s.card * α) / (↑s.sum + θ))

Opening a new table multiplies the EPPF by the probability of doing so, (θ + k α) / (n + θ) when n customers sit at k tables ([Pit06] p. 61).

theorem ProbabilityTheory.pitmanYorEPPF_cons_succ_erase {α θ : ℝ} {s : Multiset ℕ} {m : ℕ} (hm : m ∈ s) (hm₀ : m ≠ 0) : pitmanYorEPPF α θ ((m + 1) ::ₘ s.erase m) = pitmanYorEPPF α θ s * ((↑m - α) / (↑s.sum + θ))

Joining a table of m customers multiplies the EPPF by the probability of doing so, (m - α) / (n + θ): the recursion (3.22) of [Pit06].

theorem ProbabilityTheory.pitmanYorEPPF_zero_left {θ : ℝ} {s : Multiset ℕ} (hθ : θ ≠ 0) (hs : s.sum ≠ 0) : pitmanYorEPPF 0 θ s = θ ^ s.card / Polynomial.eval θ (ascPochhammer ℝ s.sum) * (Multiset.map (fun (m : ℕ) => ↑(m - 1).factorial) s).prod

At α = 0 the EPPF is the Ewens sampling formula θ ^ k / (θ)_{n↑1} ∏ᵢ (nᵢ - 1)! ([Pit06] (2.19)), the partition of a sample from a Dirichlet process with parameter θ ([Pit06] p. 61).

The Chinese restaurant

noncomputable def ProbabilityTheory.crpRule (α θ : ℝ) (n : ℕ) : Kernel (Fin n → ℕ) ℕ

The (α, θ) seating plan on table labels, each customer labelled by the first customer at their table. The first customer opens table 0. When customers 0, …, n sit at k tables, label c used n_c times, customer n + 1 opens a new table, labelled n + 1, with probability (θ + k α) / (n + 1 + θ), and joins the table labelled c with probability (n_c - α) / (n + 1 + θ).

Equations

• One or more equations did not get rendered due to their size.
• ProbabilityTheory.crpRule α θ 0 = ProbabilityTheory.Kernel.const (Fin 0 → ℕ) (MeasureTheory.Measure.dirac 0)

noncomputable def ProbabilityTheory.pitmanYor (α θ : ℝ) (n : ℕ) : MeasureTheory.Measure (Finpartition Finset.univ)

The Pitman–Yor partition: the law of the partition of n customers by table under the (α, θ) seating plan.

Equations

• ProbabilityTheory.pitmanYor α θ n = MeasureTheory.Measure.map Finpartition.ofFun (ProbabilityTheory.seqLaw (ProbabilityTheory.crpRule α θ) n)

theorem ProbabilityTheory.crpRule_zero_apply {α θ : ℝ} (s : Fin 0 → ℕ) : (crpRule α θ 0) s = MeasureTheory.Measure.dirac 0

theorem ProbabilityTheory.crpRule_succ_apply_singleton {α θ : ℝ} {n : ℕ} (s : Fin (n + 1) → ℕ) (c : ℕ) : ((crpRule α θ (n + 1)) s) {c} = (if c = n + 1 then ENNReal.ofReal ((θ + ↑(Finset.image s Finset.univ).card * α) / (↑n + 1 + θ)) else 0) + if c ∈ Finset.image s Finset.univ then ENNReal.ofReal ((↑(countVec s c) - α) / (↑n + 1 + θ)) else 0

theorem ProbabilityTheory.pitmanYorEPPF_nonneg {α θ : ℝ} (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1) (hθ : -α < θ) (s : Multiset ℕ) : 0 ≤ pitmanYorEPPF α θ s

theorem ProbabilityTheory.isMarkovKernel_crpRule {α θ : ℝ} (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1) (hθ : -α < θ) (n : ℕ) : IsMarkovKernel (crpRule α θ n)

theorem ProbabilityTheory.isProbabilityMeasure_seqLaw_crpRule {α θ : ℝ} (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1) (hθ : -α < θ) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (seqLaw (crpRule α θ) n)

theorem ProbabilityTheory.isProbabilityMeasure_pitmanYor {α θ : ℝ} (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1) (hθ : -α < θ) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (pitmanYor α θ n)

theorem ProbabilityTheory.seqLaw_crpRule_singleton {α θ : ℝ} (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1) (hθ : -α < θ) {n : ℕ} (s : Fin n → ℕ) : (seqLaw (crpRule α θ) n) {s} = if (Finpartition.ofFun s).minLabel = s then ENNReal.ofReal (pitmanYorEPPF α θ (Finpartition.ofFun s).partSizes) else 0

The seating plan on labels. A sequence of table labels has the probability pitmanYorEPPF of the partition it generates if each label is the first customer at its table, and probability 0 otherwise.

theorem ProbabilityTheory.pitmanYor_singleton {α θ : ℝ} {n : ℕ} (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1) (hθ : -α < θ) (P : Finpartition Finset.univ) : (pitmanYor α θ n) {P} = ENNReal.ofReal (pitmanYorEPPF α θ P.partSizes)

Pitman's Theorem 3.2: the Pitman–Yor partition gives each partition of Fin n the probability pitmanYorEPPF of its block sizes ([Pit06] (3.6)).

theorem ProbabilityTheory.pitmanYor_real_singleton {α θ : ℝ} {n : ℕ} (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1) (hθ : -α < θ) (P : Finpartition Finset.univ) : (pitmanYor α θ n).real {P} = pitmanYorEPPF α θ P.partSizes

Pitman's Theorem 3.2, real form.

theorem ProbabilityTheory.smulInvariantMeasure_pitmanYor {α θ : ℝ} (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1) (hθ : -α < θ) (n : ℕ) : MeasureTheory.SMulInvariantMeasure (Equiv.Perm (Fin n)) (Finpartition Finset.univ) (pitmanYor α θ n)

The Pitman–Yor partition is exchangeable: relabelling the customers by a permutation does not change its law ([Pit06] Theorem 3.2).