Dirichlet process

DefinitionLeftover stick in stick breaking#✓fully proved

The stick left after breaking off the first k pieces at proportions b: ∏_{j<k} (1 - bⱼ).

def stickRemainder (b : ℕ → ℝ) (k : ℕ) : ℝ :=
  ∏ j ∈ range k, (1 - b j)

Used by 16

Used byRandom stick-breaking weights sum to one almost surely · Random stick-breaking weights lie in the unit interval almost surely · Leftover stick is decreasing · Stick-breaking weights sum to one iff the leftover stick tends to zero · Mean of a stick-breaking weight · Second moment of a stick-breaking weight · Mean of the random measure · Mixed second moment of the random measure · Measurability of the stick-breaking measure in its parameters · Measurability of the random stick-breaking weights · Random leftover stick · Stick-breaking measure has total mass at most one · Leftover stick lies in the unit interval · Stick-breaking weights · Nonnegativity of stick-breaking weights · Stick-breaking pieces and leftover make up the whole stick

DefinitionStick-breaking weights#✓fully proved

The k-th piece of a stick broken at proportions b: bₖ ∏_{j<k} (1 - bⱼ).

def stickWeight (b : ℕ → ℝ) (k : ℕ) : ℝ :=
  b k * stickRemainder b k

Uses 1 · Used by 14

Statement usesLeftover stick in stick breaking

Used byRandom stick-breaking weights sum to one almost surely · Stick-breaking weights sum to one iff the leftover stick tends to zero · Mean of a stick-breaking weight · Second moment of a stick-breaking weight · Stick-breaking measure is a probability measure · Mean of the random measure · Mixed second moment of the random measure · Measurability of the stick-breaking measure in its parameters · Stick-breaking measure · Mass of a set under the stick-breaking measure · Stick-breaking measure has total mass at most one · Nonnegativity of stick-breaking weights · Stick-breaking pieces and leftover make up the whole stick · Random stick-breaking weight

DefinitionStick-breaking measure#✓fully proved

The discrete measure ∑ₖ πₖ δ_{θₖ} with the stick-breaking weights πₖ = stickWeight b k (negative weights, which do not occur for proportions in [0, 1], are read as 0).

noncomputable def stickBreakingMeasure (b : ℕ → ℝ) (θ : ℕ → X) : Measure X :=
  Measure.sum fun k ↦ ENNReal.ofReal (stickWeight b k) • Measure.dirac (θ k)

Uses 1 · Used by 10

Statement usesStick-breaking weights

Used byMoments of the Dirichlet process for at most two draws · Dirichlet process · Random measure of a stick-breaking process · Stick-breaking measure is a probability measure · Mean of the Dirichlet process · Mean of the random measure · Measurability of the random stick-breaking measure · Measurability of the stick-breaking measure in its parameters · Mass of a set under the stick-breaking measure · Stick-breaking measure has total mass at most one

TheoremStick-breaking pieces and leftover make up the whole stick#✓fully proved

The first n pieces and the leftover stick make up the whole stick. Holds for all real b.

theorem sum_range_stickWeight_add_stickRemainder (b : ℕ → ℝ) (n : ℕ) :
    ∑ k ∈ range n, stickWeight b k + stickRemainder b n = 1

Uses 2 · Used by 2

Statement usesLeftover stick in stick breaking · Stick-breaking weights

Used byStick-breaking weights sum to one iff the leftover stick tends to zero · Stick-breaking measure has total mass at most one

TheoremLeftover stick lies in the unit interval#✓fully proved

The leftover stick is in [0, 1] for proportions in [0, 1].

theorem stickRemainder_mem_Icc {b : ℕ → ℝ} (hb : ∀ k, b k ∈ Set.Icc 0 1) (k : ℕ) :
    stickRemainder b k ∈ Set.Icc 0 1

Uses 1 · Used by 5

Statement usesLeftover stick in stick breaking

Used byRandom stick-breaking weights sum to one almost surely · Random stick-breaking weights lie in the unit interval almost surely · Leftover stick is decreasing · Stick-breaking measure has total mass at most one · Nonnegativity of stick-breaking weights

TheoremNonnegativity of stick-breaking weights#✓fully proved

The pieces are nonnegative for proportions in [0, 1].

theorem stickWeight_nonneg {b : ℕ → ℝ} (hb : ∀ k, b k ∈ Set.Icc 0 1) (k : ℕ) :
    0 ≤ stickWeight b k

Uses 3 · Used by 4

Statement usesStick-breaking weights

Proof usesLeftover stick in stick breaking · Leftover stick lies in the unit interval

Used byRandom stick-breaking weights lie in the unit interval almost surely · Stick-breaking weights sum to one iff the leftover stick tends to zero · Stick-breaking measure is a probability measure · Stick-breaking measure has total mass at most one

TheoremLeftover stick is decreasing#✓fully proved

The leftover stick shrinks for proportions in [0, 1].

theorem antitone_stickRemainder {b : ℕ → ℝ} (hb : ∀ k, b k ∈ Set.Icc 0 1) :
    Antitone (stickRemainder b)

Uses 2 · Used by 1

Statement usesLeftover stick in stick breaking

Proof usesLeftover stick lies in the unit interval

Used byRandom stick-breaking weights sum to one almost surely

TheoremStick-breaking weights sum to one iff the leftover stick tends to zero#✓fully proved

For proportions in [0, 1], the pieces sum to 1 iff the leftover stick tends to 0.

theorem hasSum_stickWeight_iff {b : ℕ → ℝ} (hb : ∀ k, b k ∈ Set.Icc 0 1) :
    HasSum (stickWeight b) 1 ↔ Tendsto (stickRemainder b) atTop (𝓝 0)

Uses 4 · Used by 1

Statement usesLeftover stick in stick breaking · Stick-breaking weights

Proof usesNonnegativity of stick-breaking weights · Stick-breaking pieces and leftover make up the whole stick

Used byRandom stick-breaking weights sum to one almost surely

TheoremMass of a set under the stick-breaking measure#✓fully proved

The mass of a measurable set under the stick-breaking measure.

theorem stickBreakingMeasure_apply (b : ℕ → ℝ) (θ : ℕ → X) {A : Set X} (hA : MeasurableSet A) :
    stickBreakingMeasure b θ A = ∑' k, ENNReal.ofReal (stickWeight b k) * A.indicator 1 (θ k)

Uses 2 · Used by 5

Statement usesStick-breaking measure · Stick-breaking weights

Used byStick-breaking measure is a probability measure · Mean of the random measure · Mixed second moment of the random measure · Measurability of the stick-breaking measure in its parameters · Stick-breaking measure has total mass at most one

TheoremStick-breaking measure is a probability measure#✓fully proved

The stick-breaking measure is a probability measure when the pieces sum to 1.

theorem isProbabilityMeasure_stickBreakingMeasure {b : ℕ → ℝ} (hb : ∀ k, b k ∈ Set.Icc 0 1)
    (h : HasSum (stickWeight b) 1) (θ : ℕ → X) :
    IsProbabilityMeasure (stickBreakingMeasure b θ)

Uses 4 · Used by 2

Statement usesStick-breaking measure · Stick-breaking weights

Proof usesMass of a set under the stick-breaking measure · Nonnegativity of stick-breaking weights

Used byDirichlet process is almost surely a probability measure · Stick-breaking random measure is almost surely a probability measure

TheoremStick-breaking measure has total mass at most one#✓fully proved

The stick-breaking measure has total mass at most 1 for proportions in [0, 1].

theorem stickBreakingMeasure_apply_le_one {b : ℕ → ℝ} (hb : ∀ k, b k ∈ Set.Icc 0 1)
    (θ : ℕ → X) (A : Set X) : stickBreakingMeasure b θ A ≤ 1

Uses 7 · Used by 1

Statement usesStick-breaking measure

Proof usesMass of a set under the stick-breaking measure · Leftover stick in stick breaking · Leftover stick lies in the unit interval · Stick-breaking weights · Nonnegativity of stick-breaking weights · Stick-breaking pieces and leftover make up the whole stick

Used byVariance of the Dirichlet process

TheoremMeasurability of the stick-breaking measure in its parameters#✓fully proved

The stick-breaking measure depends measurably (for the Giry σ-algebra on Measure X) on the proportions and the atoms.

theorem measurable_stickBreakingMeasure :
    Measurable fun p : (ℕ → ℝ) × (ℕ → X) ↦ stickBreakingMeasure p.1 p.2

Uses 4 · Used by 3

Statement usesStick-breaking measure

Proof usesMass of a set under the stick-breaking measure · Leftover stick in stick breaking · Stick-breaking weights

Used byMoments of the Dirichlet process for at most two draws · Mean of the Dirichlet process · Measurability of the random stick-breaking measure

StructureStick-breaking process#✓fully proved

A stick-breaking process on the probability space (Ω, μ): independent proportions βₖ ∈ [0, 1] (almost surely, with arbitrary laws), i.i.d. atoms atom k with law H, and the proportion sequence independent of the atom sequence. Ishwaran–James (2001) take βₖ ∼ Beta(aₖ, bₖ); Sethuraman's Dirichlet process is IsDirichlet.

ProbabilityTheory.StickBreakingProcess · 21 lines

structure StickBreakingProcess (μ : Measure Ω) (X : Type*) [MeasurableSpace X] where
  /-- The stick-breaking proportions. -/
  β : ℕ → Ω → ℝ
  /-- The atoms. -/
  atom : ℕ → Ω → X
  /-- The base measure, the common law of the atoms. -/
  H : Measure X
  /-- The proportions are measurable. -/
  measurable_β : ∀ k, Measurable (β k)
  /-- The atoms are measurable. -/
  measurable_atom : ∀ k, Measurable (atom k)
  /-- The proportions lie in `[0, 1]` almost surely. -/
  ae_mem_Icc : ∀ k, ∀ᵐ ω ∂μ, β k ω ∈ Set.Icc 0 1
  /-- Each atom has law `H`. -/
  hasLaw_atom : ∀ k, HasLaw (atom k) H μ
  /-- The proportions are mutually independent. -/
  iIndepFun_β : iIndepFun β μ
  /-- The atoms are mutually independent. -/
  iIndepFun_atom : iIndepFun atom μ
  /-- The proportion sequence is independent of the atom sequence. -/
  indepFun_β_atom : IndepFun (fun ω k ↦ β k ω) (fun ω k ↦ atom k ω) μ

Used by 29

Used byMoments of the Dirichlet process for at most two draws · Stick-breaking proportions lie in the unit interval almost surely · Random stick-breaking weights sum to one almost surely · The Dirichlet-process weights sum to 1 almost surely · Dirichlet process is almost surely a probability measure · Stick-breaking random measure is almost surely a probability measure · Random stick-breaking weights lie in the unit interval almost surely · Random measure of a stick-breaking process · Mean proportion of a Dirichlet process · Expected leftover stick is the product of expected complements · Mean of a stick-breaking weight · Mean of a Dirichlet-process weight · Second moment of a stick-breaking weight · Sethuraman's stick-breaking representation of the Dirichlet process · Sethuraman's canonical model is a Dirichlet process · Base measure of a stick-breaking process is a probability measure · Mean of the random measure · Mean of the Dirichlet process · Mixed second moment of the random measure · Mixed second moment of the Dirichlet process · The Blackwell–MacQueen urn for two draws · Measurability of the random stick-breaking measure · Measurability of the random stick-breaking weights · Random leftover stick · Sethuraman's construction · Expected sum of squared stick-breaking weights · Probability that two Dirichlet process draws pick the same piece · Variance of the Dirichlet process · Random stick-breaking weight

DefinitionRandom stick-breaking weight#✓fully proved

The random piece πₖ = βₖ ∏_{j<k} (1 - βⱼ).

def weight (k : ℕ) (ω : Ω) : ℝ :=
  stickWeight (fun j ↦ P.β j ω) k

Uses 2 · Used by 13

Statement usesStick-breaking process · Stick-breaking weights

Used byRandom stick-breaking weights sum to one almost surely · The Dirichlet-process weights sum to 1 almost surely · Dirichlet process is almost surely a probability measure · Stick-breaking random measure is almost surely a probability measure · Random stick-breaking weights lie in the unit interval almost surely · Mean of a stick-breaking weight · Mean of a Dirichlet-process weight · Second moment of a stick-breaking weight · Mean of the random measure · Mixed second moment of the random measure · Measurability of the random stick-breaking weights · Expected sum of squared stick-breaking weights · Probability that two Dirichlet process draws pick the same piece

DefinitionRandom leftover stick#✓fully proved

The random leftover stick ∏_{j<k} (1 - βⱼ).

def remainder (k : ℕ) (ω : Ω) : ℝ :=
  stickRemainder (fun j ↦ P.β j ω) k

Uses 2 · Used by 2

Statement usesStick-breaking process · Leftover stick in stick breaking

Used byRandom stick-breaking weights sum to one almost surely · Expected leftover stick is the product of expected complements

DefinitionRandom measure of a stick-breaking process#✓fully proved

The random measure G = ∑ₖ πₖ δ_{θₖ}.

noncomputable def G (ω : Ω) : Measure X :=
  stickBreakingMeasure (fun j ↦ P.β j ω) (fun j ↦ P.atom j ω)

Uses 2 · Used by 10

Statement usesStick-breaking process · Stick-breaking measure

Used byMoments of the Dirichlet process for at most two draws · Dirichlet process is almost surely a probability measure · Stick-breaking random measure is almost surely a probability measure · Mean of the random measure · Mean of the Dirichlet process · Mixed second moment of the random measure · Mixed second moment of the Dirichlet process · The Blackwell–MacQueen urn for two draws · Measurability of the random stick-breaking measure · Variance of the Dirichlet process

DefinitionExpected sum of squared stick-breaking weights#✓fully proved

∑ₖ E[πₖ²]: given G, two independent draws from G pick the same piece k with probability ∑ₖ πₖ². For an atomless base measure the atoms are almost surely distinct, so this is also the probability that the two draws coincide (not used here).

noncomputable def sumSqWeight : ℝ≥0∞ :=
  ∑' k, ∫⁻ ω, ENNReal.ofReal (P.weight k ω) ^ 2 ∂μ

Uses 2 · Used by 3

Statement usesStick-breaking process · Random stick-breaking weight

Used byMixed second moment of the random measure · Mixed second moment of the Dirichlet process · Probability that two Dirichlet process draws pick the same piece

TheoremMeasurability of the random stick-breaking weights#✓fully proved

The pieces are measurable.

theorem measurable_weight (k : ℕ) : Measurable (P.weight k)

Uses 3 · Used by 3

Statement usesStick-breaking process · Random stick-breaking weight

Proof usesLeftover stick in stick breaking

Used byMean of the random measure · Mixed second moment of the random measure · Probability that two Dirichlet process draws pick the same piece

TheoremStick-breaking proportions lie in the unit interval almost surely#✓fully proved

Almost surely every proportion is in [0, 1].

theorem ae_forall_mem_Icc : ∀ᵐ ω ∂μ, ∀ k, P.β k ω ∈ Set.Icc 0 1

Uses 1 · Used by 5

Statement usesStick-breaking process

Used byRandom stick-breaking weights sum to one almost surely · Dirichlet process is almost surely a probability measure · Stick-breaking random measure is almost surely a probability measure · Random stick-breaking weights lie in the unit interval almost surely · Variance of the Dirichlet process

TheoremRandom stick-breaking weights lie in the unit interval almost surely#✓fully proved

Almost surely every piece is in [0, 1].

theorem ae_weight_mem_Icc : ∀ᵐ ω ∂μ, ∀ k, P.weight k ω ∈ Set.Icc 0 1

Uses 6 · Used by 2

Statement usesStick-breaking process · Random stick-breaking weight

Proof usesStick-breaking proportions lie in the unit interval almost surely · Leftover stick in stick breaking · Leftover stick lies in the unit interval · Nonnegativity of stick-breaking weights

Used byMean of the random measure · Probability that two Dirichlet process draws pick the same piece

TheoremMeasurability of the random stick-breaking measure#✓fully proved

The random measure depends measurably on ω.

theorem measurable_G : Measurable P.G

Uses 4 · Used by 1

Statement usesStick-breaking process · Random measure of a stick-breaking process

Proof usesMeasurability of the stick-breaking measure in its parameters · Stick-breaking measure

Used byVariance of the Dirichlet process

TheoremBase measure of a stick-breaking process is a probability measure#✓fully proved

The base measure is a probability measure.

theorem isProbabilityMeasure_H [IsProbabilityMeasure μ] : IsProbabilityMeasure P.H

Uses 1 · Used by 1

Statement usesStick-breaking process

Used byVariance of the Dirichlet process

TheoremExpected leftover stick is the product of expected complements#✓fully proved

E[∏_{j<k} (1 - βⱼ)] = ∏_{j<k} (1 - E[βⱼ]).

theorem integral_remainder [IsProbabilityMeasure μ] (k : ℕ) :
    μ[P.remainder k] = ∏ j ∈ range k, (1 - μ[P.β j])

Uses 2 · Used by 1

Statement usesStick-breaking process · Random leftover stick

Used byRandom stick-breaking weights sum to one almost surely

TheoremMean of a stick-breaking weight#✓fully proved

E[πₖ] = E[βₖ] ∏_{j<k} (1 - E[βⱼ]).

theorem integral_weight [IsProbabilityMeasure μ] (k : ℕ) :
    μ[P.weight k] = μ[P.β k] * ∏ j ∈ range k, (1 - μ[P.β j])

Uses 4 · Used by 1

Statement usesStick-breaking process · Random stick-breaking weight

Proof usesLeftover stick in stick breaking · Stick-breaking weights

Used byMean of a Dirichlet-process weight

TheoremSecond moment of a stick-breaking weight#✓fully proved

E[πₖ²] = E[βₖ²] ∏_{j<k} E[(1 - βⱼ)²].

theorem integral_weight_sq [IsProbabilityMeasure μ] (k : ℕ) :
    μ[fun ω ↦ P.weight k ω ^ 2] =
      μ[fun ω ↦ P.β k ω ^ 2] * ∏ j ∈ range k, μ[fun ω ↦ (1 - P.β j ω) ^ 2]

Uses 4 · Used by 1

Statement usesStick-breaking process · Random stick-breaking weight

Proof usesLeftover stick in stick breaking · Stick-breaking weights

Used byProbability that two Dirichlet process draws pick the same piece

TheoremRandom stick-breaking weights sum to one almost surely#✓fully proved

If the expected leftover stick ∏_{j<k} (1 - E[βⱼ]) tends to 0, the pieces sum to 1 almost surely.

theorem ae_hasSum_weight [IsProbabilityMeasure μ]
    (h : Tendsto (fun k ↦ ∏ j ∈ range k, (1 - μ[P.β j])) atTop (𝓝 0)) :
    ∀ᵐ ω ∂μ, HasSum (fun k ↦ P.weight k ω) 1

Uses 10 · Used by 1

Statement usesStick-breaking process · Random stick-breaking weight

Proof usesStick-breaking proportions lie in the unit interval almost surely · Expected leftover stick is the product of expected complements · Random leftover stick · Leftover stick is decreasing · Stick-breaking weights sum to one iff the leftover stick tends to zero · Leftover stick in stick breaking · Leftover stick lies in the unit interval · Stick-breaking weights

Used byThe Dirichlet-process weights sum to 1 almost surely

TheoremStick-breaking random measure is almost surely a probability measure#✓fully proved

When the pieces sum to 1 almost surely, G is almost surely a probability measure.

theorem ae_isProbabilityMeasure_G_of_hasSum (h : ∀ᵐ ω ∂μ, HasSum (fun k ↦ P.weight k ω) 1) :
    ∀ᵐ ω ∂μ, IsProbabilityMeasure (P.G ω)

Uses 5 · Used by 1

Statement usesStick-breaking process · Random measure of a stick-breaking process · Random stick-breaking weight

Proof usesStick-breaking proportions lie in the unit interval almost surely · Stick-breaking measure is a probability measure

Used byMixed second moment of the random measure

TheoremMean of the random measure#✓fully proved

If the pieces sum to 1 almost surely, then E[G(A)] = H(A) for every measurable A.

theorem lintegral_G_apply [IsProbabilityMeasure μ] (h : ∀ᵐ ω ∂μ, HasSum (fun k ↦ P.weight k ω) 1)
    {A : Set X} (hA : MeasurableSet A) :
    ∫⁻ ω, P.G ω A ∂μ = P.H A

Uses 9 · Used by 1

Statement usesStick-breaking process · Random measure of a stick-breaking process · Random stick-breaking weight

Proof usesRandom stick-breaking weights lie in the unit interval almost surely · Measurability of the random stick-breaking weights · Stick-breaking measure · Mass of a set under the stick-breaking measure · Leftover stick in stick breaking · Stick-breaking weights

Used byMean of the Dirichlet process

TheoremMixed second moment of the random measure#✓fully proved

If the pieces sum to 1 almost surely, then E[G(A) G(B)] = (1 - s) H(A) H(B) + s H(A ∩ B) with s = ∑ₖ E[πₖ²] (sumSqWeight, at most 1 under this hypothesis): two draws from G pick the same piece with probability s, and otherwise land on two independent atoms.

theorem lintegral_G_mul_G [IsProbabilityMeasure μ]
    (h : ∀ᵐ ω ∂μ, HasSum (fun k ↦ P.weight k ω) 1) {A B : Set X} (hA : MeasurableSet A)
    (hB : MeasurableSet B) :
    ∫⁻ ω, P.G ω A * P.G ω B ∂μ =
      (1 - P.sumSqWeight) * P.H A * P.H B + P.sumSqWeight * P.H (A ∩ B)

Uses 9 · Used by 1

Statement usesStick-breaking process · Random measure of a stick-breaking process · Expected sum of squared stick-breaking weights · Random stick-breaking weight

Proof usesStick-breaking random measure is almost surely a probability measure · Measurability of the random stick-breaking weights · Mass of a set under the stick-breaking measure · Leftover stick in stick breaking · Stick-breaking weights

Used byMixed second moment of the Dirichlet process

StructureSethuraman's stick-breaking representation of the Dirichlet process#✓fully proved

Sethuraman's stick-breaking representation of the Dirichlet process DP(α, H) (Sethuraman 1994): the proportions are Beta(1, α) with α > 0. We take this construction as the definition of DP(α, H); Sethuraman's theorem that it has Ferguson's Dirichlet marginals is recorded in WantedExt/Probability/DirichletProcessWanted.lean.

structure IsDirichlet (α : ℝ) : Prop where
  /-- The concentration parameter is positive. -/
  pos : 0 < α
  /-- Each proportion has law `Beta(1, α)`. -/
  hasLaw_β : ∀ k, HasLaw (P.β k) (betaMeasure 1 α) μ

Uses 1 · Used by 10

Statement usesStick-breaking process

Used byThe Dirichlet-process weights sum to 1 almost surely · Dirichlet process is almost surely a probability measure · Mean proportion of a Dirichlet process · Mean of a Dirichlet-process weight · Sethuraman's canonical model is a Dirichlet process · Mean of the Dirichlet process · Mixed second moment of the Dirichlet process · The Blackwell–MacQueen urn for two draws · Probability that two Dirichlet process draws pick the same piece · Variance of the Dirichlet process

DefinitionBlackwell–MacQueen urn predictive law#✓fully proved

The predictive law in the Blackwell–MacQueen urn: after observations x₀, …, x_{n-1}, the next observation has law (α H + ∑ᵢ δ_{xᵢ}) / (α + n). It is a probability measure for α > 0 and a probability measure H (isProbabilityMeasure_polyaUrnPredictive); outside that domain the definition is total but meaningless (e.g. α = n = 0 gives the zero measure).

noncomputable def polyaUrnPredictive (α : ℝ) (H : Measure X) {n : ℕ} (xs : Fin n → X) :
    Measure X :=
  (ENNReal.ofReal (α + n))⁻¹ • (ENNReal.ofReal α • H + ∑ i, Measure.dirac (xs i))

Used by 12

Used byBlackwell–MacQueen urn · The 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 · Measurability of the Pólya urn predictive law · Pólya urn predictive law is invariant under reordering · Blackwell–MacQueen predictive law is a probability measure · The Blackwell–MacQueen urn for two draws · Predictive probability of a set in the Blackwell–MacQueen urn · Ferguson's conjugacy

TheoremPredictive probability of a set in the Blackwell–MacQueen urn#✓fully proved

The predictive probability of a measurable set: (α H(A) + #{i | xᵢ ∈ A}) / (α + n).

theorem polyaUrnPredictive_apply (α : ℝ) (H : Measure X) {n : ℕ} (xs : Fin n → X) {A : Set X}
    (hA : MeasurableSet A) :
    polyaUrnPredictive α H xs A =
      (ENNReal.ofReal α * H A + (univ.filter fun i ↦ xs i ∈ A).card) /
        ENNReal.ofReal (α + n)

Uses 1 · Used by 4

Statement usesBlackwell–MacQueen urn predictive law

Used byThe ties of the Blackwell–MacQueen urn follow the Chinese restaurant process · Moments of the Dirichlet process for at most two draws · Blackwell–MacQueen predictive law is a probability measure · The Blackwell–MacQueen urn for two draws

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

The predictive law is a probability measure for α > 0 and a probability measure H.

theorem isProbabilityMeasure_polyaUrnPredictive {α : ℝ} (hα : 0 < α) {H : Measure X}
    [IsProbabilityMeasure H] {n : ℕ} (xs : Fin n → X) :
    IsProbabilityMeasure (polyaUrnPredictive α H xs)

Uses 2 · Used by 2

Statement usesBlackwell–MacQueen urn predictive law

Proof usesPredictive probability of a set in the Blackwell–MacQueen urn

Used byBlackwell–MacQueen urn law is a probability measure · Ferguson's conjugacy

TheoremBeta law is concentrated on the unit interval#✓fully proved

The Beta law is concentrated on [0, 1].

theorem ae_mem_Icc_betaMeasure (a b : ℝ) : ∀ᵐ x ∂betaMeasure a b, x ∈ Set.Icc (0 : ℝ) 1

Used by 2

Used bySecond moment of \(1 - X\) under \(\mathrm{Beta}(1, \alpha)\) · Sethuraman's construction

TheoremSecond moment of \(1 - X\) under \(\mathrm{Beta}(1, \alpha)\)#✓fully proved

E[(1 - x)²] = α / (α + 2) under Beta(1, α).

theorem integral_one_sub_sq_betaMeasure_one {α : ℝ} (hα : 0 < α) :
    ∫ x, (1 - x) ^ 2 ∂betaMeasure 1 α = α / (α + 2)

Uses 3 · Used by 1

Proof usesBeta law is concentrated on the unit interval · Mean of the beta law · Second moment of the beta law

Used byProbability that two Dirichlet process draws pick the same piece

TheoremMean proportion of a Dirichlet process#✓fully proved

The proportions of a Dirichlet process have mean 1 / (1 + α).

theorem integral_β (hP : P.IsDirichlet α) (k : ℕ) : μ[P.β k] = 1 / (1 + α)

Uses 3 · Used by 2

Statement usesStick-breaking process · Sethuraman's stick-breaking representation of the Dirichlet process

Proof usesMean of the beta law

Used byThe Dirichlet-process weights sum to 1 almost surely · Mean of a Dirichlet-process weight

TheoremMean of a Dirichlet-process weight#✓fully proved

Mean of a Dirichlet-process weight (Sethuraman 1994): E[πₖ] = αᵏ / (1 + α)^(k+1) (α^{k-1} / (1 + α)^k for Sethuraman's π_k, indexed from 1).

theorem integral_weight [IsProbabilityMeasure μ] (hP : P.IsDirichlet α) (k : ℕ) :
    μ[P.weight k] = α ^ k / (1 + α) ^ (k + 1)

Uses 5

Statement usesStick-breaking process · Sethuraman's stick-breaking representation of the Dirichlet process · Random stick-breaking weight

Proof usesMean proportion of a Dirichlet process · Mean of a stick-breaking weight

TheoremThe Dirichlet-process weights sum to 1 almost surely#✓fully proved

The Dirichlet-process weights sum to 1 almost surely (Sethuraman 1994): the leftover stick tends to 0.

theorem ae_hasSum_weight [IsProbabilityMeasure μ] (hP : P.IsDirichlet α) :
    ∀ᵐ ω ∂μ, HasSum (fun k ↦ P.weight k ω) 1

Uses 5 · Used by 3

Statement usesStick-breaking process · Sethuraman's stick-breaking representation of the Dirichlet process · Random stick-breaking weight

Proof usesMean proportion of a Dirichlet process · Random stick-breaking weights sum to one almost surely

Used byDirichlet process is almost surely a probability measure · Mean of the Dirichlet process · Mixed second moment of the Dirichlet process

TheoremDirichlet process is almost surely a probability measure#✓fully proved

A Dirichlet process is almost surely a probability measure.

theorem ae_isProbabilityMeasure_G [IsProbabilityMeasure μ] (hP : P.IsDirichlet α) :
    ∀ᵐ ω ∂μ, IsProbabilityMeasure (P.G ω)

Uses 7

Statement usesStick-breaking process · Random measure of a stick-breaking process · Sethuraman's stick-breaking representation of the Dirichlet process

Proof usesThe Dirichlet-process weights sum to 1 almost surely · Stick-breaking proportions lie in the unit interval almost surely · Random stick-breaking weight · Stick-breaking measure is a probability measure

TheoremMean of the Dirichlet process#✓fully proved

Mean of the Dirichlet process (Ferguson 1973): E[G(A)] = H(A).

theorem lintegral_G_apply [IsProbabilityMeasure μ] (hP : P.IsDirichlet α) {A : Set X}
    (hA : MeasurableSet A) : ∫⁻ ω, P.G ω A ∂μ = P.H A

Uses 5 · Used by 2

Statement usesStick-breaking process · Random measure of a stick-breaking process · Sethuraman's stick-breaking representation of the Dirichlet process

Proof usesThe Dirichlet-process weights sum to 1 almost surely · Mean of the random measure

Used byMean of the Dirichlet process · Variance of the Dirichlet process

TheoremProbability that two Dirichlet process draws pick the same piece#✓fully proved

Two draws from a Dirichlet process pick the same piece with probability 1 / (1 + α): ∑ₖ E[πₖ²] = 1 / (1 + α). This is the probability that the second customer of the Chinese restaurant process with parameter α joins the first one's table.

theorem sumSqWeight_eq [IsProbabilityMeasure μ] (hP : P.IsDirichlet α) :
    P.sumSqWeight = ENNReal.ofReal (1 / (1 + α))

Uses 9 · Used by 1

Statement usesStick-breaking process · Sethuraman's stick-breaking representation of the Dirichlet process · Expected sum of squared stick-breaking weights

Proof usesRandom stick-breaking weights lie in the unit interval almost surely · Second moment of a stick-breaking weight · Measurability of the random stick-breaking weights · Random stick-breaking weight · Second moment of \(1 - X\) under \(\mathrm{Beta}(1, \alpha)\) · Second moment of the beta law

Used byMixed second moment of the Dirichlet process

TheoremMixed second moment of the Dirichlet process#✓fully proved

Mixed second moment of the Dirichlet process (Ferguson 1973): E[G(A) G(B)] = (α H(A) H(B) + H(A ∩ B)) / (α + 1).

theorem lintegral_G_mul_G [IsProbabilityMeasure μ] (hP : P.IsDirichlet α) {A B : Set X}
    (hA : MeasurableSet A) (hB : MeasurableSet B) :
    ∫⁻ ω, P.G ω A * P.G ω B ∂μ =
      (ENNReal.ofReal α * P.H A * P.H B + P.H (A ∩ B)) / ENNReal.ofReal (α + 1)

Uses 7 · Used by 2

Statement usesStick-breaking process · Random measure of a stick-breaking process · Sethuraman's stick-breaking representation of the Dirichlet process

Proof usesThe Dirichlet-process weights sum to 1 almost surely · Probability that two Dirichlet process draws pick the same piece · Mixed second moment of the random measure · Expected sum of squared stick-breaking weights

Used byThe Blackwell–MacQueen urn for two draws · Variance of the Dirichlet process

TheoremThe Blackwell–MacQueen urn for two draws#✓fully proved

The Blackwell–MacQueen urn for two draws (Blackwell–MacQueen 1973): if X₁, X₂ are i.i.d. draws from a Dirichlet process G, then P(X₁ ∈ A, X₂ ∈ B) = E[G(A) G(B)] equals ∫_A P(X₂ ∈ B | X₁ = x) dH(x) with the predictive law polyaUrnPredictive α H ![x] = (α H + δₓ) / (α + 1).

theorem lintegral_G_mul_G_eq_predictive [IsProbabilityMeasure μ] (hP : P.IsDirichlet α)
    {A B : Set X} (hA : MeasurableSet A) (hB : MeasurableSet B) :
    ∫⁻ ω, P.G ω A * P.G ω B ∂μ = ∫⁻ x in A, polyaUrnPredictive α P.H ![x] B ∂P.H

Uses 6 · Used by 1

Statement usesStick-breaking process · Random measure of a stick-breaking process · Sethuraman's stick-breaking representation of the Dirichlet process · Blackwell–MacQueen urn predictive law

Proof usesMixed second moment of the Dirichlet process · Predictive probability of a set in the Blackwell–MacQueen urn

Used byMoments of the Dirichlet process for at most two draws

TheoremVariance of the Dirichlet process#✓fully proved

Variance of the Dirichlet process (Ferguson 1973): Var(G(A)) = H(A) (1 - H(A)) / (α + 1).

theorem variance_G_apply [IsProbabilityMeasure μ] (hP : P.IsDirichlet α) {A : Set X}
    (hA : MeasurableSet A) :
    Var[fun ω ↦ (P.G ω A).toReal; μ] = P.H.real A * (1 - P.H.real A) / (α + 1)

Uses 9

Statement usesStick-breaking process · Random measure of a stick-breaking process · Sethuraman's stick-breaking representation of the Dirichlet process

Proof usesMean of the Dirichlet process · Mixed second moment of the Dirichlet process · Stick-breaking proportions lie in the unit interval almost surely · Base measure of a stick-breaking process is a probability measure · Measurability of the random stick-breaking measure · Stick-breaking measure has total mass at most one

DefinitionSethuraman's canonical probability space#✓fully proved

The product probability space (ℕ → ℝ) × (ℕ → X) carrying i.i.d. Beta(1, α) proportions and, independently, i.i.d. H atoms.

noncomputable def sethuramanMeasure (α : ℝ) (hα : 0 < α) (H : Measure X)
    [IsProbabilityMeasure H] : Measure ((ℕ → ℝ) × (ℕ → X)) :=
  haveI := isProbabilityMeasureBeta zero_lt_one hα
  (Measure.infinitePi fun _ : ℕ ↦ betaMeasure 1 α).prod (Measure.infinitePi fun _ : ℕ ↦ H)

Used by 9

Used byMoments of the Dirichlet process for at most two draws · Dirichlet process · Law of each proportion in Sethuraman's space · Law of each atom in Sethuraman's space · Sethuraman's canonical model is a Dirichlet process · Mean of the Dirichlet process · Law of the proportion coordinate of Sethuraman's space · Law of the atom coordinate of Sethuraman's space · Sethuraman's construction

TheoremLaw of the proportion coordinate of Sethuraman's space#✓fully proved

The proportion coordinate of the canonical space has law ⊗ₖ Beta(1, α).

theorem measurePreserving_fst_sethuramanMeasure {α : ℝ} (hα : 0 < α) (H : Measure X)
    [IsProbabilityMeasure H] :
    haveI := isProbabilityMeasureBeta zero_lt_one hα
    MeasurePreserving Prod.fst (sethuramanMeasure α hα H)
      (Measure.infinitePi fun _ : ℕ ↦ betaMeasure 1 α)

Uses 1 · Used by 2

Statement usesSethuraman's canonical probability space

Used byLaw of each proportion in Sethuraman's space · Sethuraman's construction

TheoremLaw of the atom coordinate of Sethuraman's space#✓fully proved

The atom coordinate of the canonical space has law ⊗ₖ H.

theorem measurePreserving_snd_sethuramanMeasure {α : ℝ} (hα : 0 < α) (H : Measure X)
    [IsProbabilityMeasure H] :
    MeasurePreserving Prod.snd (sethuramanMeasure α hα H) (Measure.infinitePi fun _ : ℕ ↦ H)

Uses 1 · Used by 2

Statement usesSethuraman's canonical probability space

Used byLaw of each atom in Sethuraman's space · Sethuraman's construction

TheoremLaw of each proportion in Sethuraman's space#✓fully proved

Each proportion of the canonical space has law Beta(1, α).

theorem hasLaw_fst_sethuramanMeasure {α : ℝ} (hα : 0 < α) (H : Measure X)
    [IsProbabilityMeasure H] (k : ℕ) :
    HasLaw (fun p : (ℕ → ℝ) × (ℕ → X) ↦ p.1 k) (betaMeasure 1 α) (sethuramanMeasure α hα H)

Uses 2 · Used by 2

Statement usesSethuraman's canonical probability space

Proof usesLaw of the proportion coordinate of Sethuraman's space

Used bySethuraman's canonical model is a Dirichlet process · Sethuraman's construction

TheoremLaw of each atom in Sethuraman's space#✓fully proved

Each atom of the canonical space has law H.

theorem hasLaw_snd_sethuramanMeasure {α : ℝ} (hα : 0 < α) (H : Measure X)
    [IsProbabilityMeasure H] (k : ℕ) :
    HasLaw (fun p : (ℕ → ℝ) × (ℕ → X) ↦ p.2 k) H (sethuramanMeasure α hα H)

Uses 2 · Used by 1

Statement usesSethuraman's canonical probability space

Proof usesLaw of the atom coordinate of Sethuraman's space

Used bySethuraman's construction

DefinitionSethuraman's construction#✓fully proved

Sethuraman's construction on the canonical space: the coordinates of the two factors are the proportions and the atoms.

ProbabilityTheory.sethuraman · 23 lines

noncomputable def sethuraman (α : ℝ) (hα : 0 < α) (H : Measure X) [IsProbabilityMeasure H] :
    StickBreakingProcess (sethuramanMeasure α hα H) X where
  β k p := p.1 k
  atom k p := p.2 k
  H := H
  measurable_β k := by fun_prop
  measurable_atom k := by fun_prop
  ae_mem_Icc k := (hasLaw_fst_sethuramanMeasure hα H k).ae_iff (p := (· ∈ Set.Icc 0 1))
    measurableSet_Icc.mem |>.2 (ae_mem_Icc_betaMeasure 1 α)
  hasLaw_atom k := hasLaw_snd_sethuramanMeasure hα H k
  iIndepFun_β := by
    rw [iIndepFun_iff_map_fun_eq_infinitePi_map fun k ↦ by fun_prop]
    simp_rw [fun k ↦ (hasLaw_fst_sethuramanMeasure hα H k).map_eq]
    exact (measurePreserving_fst_sethuramanMeasure hα H).map_eq
  iIndepFun_atom := by
    rw [iIndepFun_iff_map_fun_eq_infinitePi_map fun k ↦ by fun_prop]
    simp_rw [fun k ↦ (hasLaw_snd_sethuramanMeasure hα H k).map_eq]
    exact (measurePreserving_snd_sethuramanMeasure hα H).map_eq
  indepFun_β_atom := by
    rw [indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop),
      (measurePreserving_fst_sethuramanMeasure hα H).map_eq,
      (measurePreserving_snd_sethuramanMeasure hα H).map_eq]
    exact Measure.map_id

Uses 7 · Used by 3

Statement usesStick-breaking process · Beta law is concentrated on the unit interval · Law of each proportion in Sethuraman's space · Law of each atom in Sethuraman's space · Law of the proportion coordinate of Sethuraman's space · Law of the atom coordinate of Sethuraman's space · Sethuraman's canonical probability space

Used byMoments of the Dirichlet process for at most two draws · Sethuraman's canonical model is a Dirichlet process · Mean of the Dirichlet process

TheoremSethuraman's canonical model is a Dirichlet process#✓fully proved

The canonical model is a Dirichlet process.

theorem StickBreakingProcess.isDirichlet_sethuraman (α : ℝ) (hα : 0 < α) (H : Measure X)
    [IsProbabilityMeasure H] : (sethuraman α hα H).IsDirichlet α

Uses 5 · Used by 2

Statement usesSethuraman's stick-breaking representation of the Dirichlet process · Sethuraman's construction · Sethuraman's canonical probability space

Proof usesStick-breaking process · Law of each proportion in Sethuraman's space

Used byMoments of the Dirichlet process for at most two draws · Mean of the Dirichlet process

DefinitionDirichlet process#✓fully proved

The Dirichlet process DP(α, H) as a law on Measure X, defined as the law of Sethuraman's (1994) stick-breaking measure with Beta(1, α) proportions and H atoms. Ferguson's (1973) definition by Dirichlet marginals is the wanted statement map_dirichletProcess_partition.

noncomputable def dirichletProcess (α : ℝ) (hα : 0 < α) (H : Measure X)
    [IsProbabilityMeasure H] : Measure (Measure X) :=
  (sethuramanMeasure α hα H).map fun p ↦ stickBreakingMeasure p.1 p.2

Uses 2 · Used by 5

Statement usesSethuraman's canonical probability space · Stick-breaking measure

Used byMoments of the Dirichlet process for at most two draws · Mean of the Dirichlet process · The moments of the Dirichlet process are the Blackwell–MacQueen urn · Finite-dimensional marginals of the Dirichlet process · Ferguson's conjugacy

TheoremMean of the Dirichlet process#✓fully proved

Mean of the Dirichlet process, law form: ∫ ν(A) dDP(α, H)(ν) = H(A).

theorem lintegral_dirichletProcess_apply (α : ℝ) (hα : 0 < α) (H : Measure X)
    [IsProbabilityMeasure H] {A : Set X} (hA : MeasurableSet A) :
    ∫⁻ ν, ν A ∂dirichletProcess α hα H = H A

Uses 7 · Used by 1

Statement usesDirichlet process

Proof usesMean of the Dirichlet process · Sethuraman's canonical model is a Dirichlet process · Measurability of the stick-breaking measure in its parameters · Sethuraman's construction · Sethuraman's canonical probability space · Stick-breaking measure

Used byMoments of the Dirichlet process for at most two draws

TheoremFinite-dimensional marginals of the Dirichlet process#●ready to prove

Finite-dimensional marginals of the Dirichlet process (Ferguson 1973, §3; Sethuraman 1994, Theorem 3.4): on a measurable partition A₀, …, A_m of X with H(Aᵢ) > 0, the vector (G(A₀), …, G(A_m)) has the Dirichlet law Dir(α H(A₀), …, α H(A_m)).

theorem_wanted map_dirichletProcess_partition (α : ℝ) (hα : 0 < α) (H : Measure X)
    [IsProbabilityMeasure H] {m : ℕ} (A : Fin (m + 1) → Set X) (hA : ∀ i, MeasurableSet (A i))
    (hdisj : Pairwise (Function.onFun Disjoint A)) (hcover : ⋃ i, A i = Set.univ)
    (hpos : ∀ i, 0 < H (A i)) :
    (dirichletProcess α hα H).map (fun ν i ↦ (ν (A i)).toReal) =
      dirichletMeasure fun i ↦ α * H.real (A i)

Uses 2

Statement usesDirichlet distribution · Dirichlet process

TheoremThe moments of the Dirichlet process are the Blackwell–MacQueen urn#●ready to prove

The moments of the Dirichlet process are the Blackwell–MacQueen urn (Blackwell–MacQueen 1973): E[∏ᵢ G(Aᵢ)] = P(X₀ ∈ A₀, …, X_{n-1} ∈ A_{n-1}) for the urn's first n draws.

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

Uses 2

Statement usesBlackwell–MacQueen urn · Dirichlet process

TheoremFerguson's conjugacy#●ready to prove

Ferguson's conjugacy (Ferguson 1973, Theorem 1): given n observations xs from G ∼ DP(α, H), the posterior of G is DP(α + n, (α H + ∑ᵢ δ_{xsᵢ}) / (α + n)). Stated as the disintegration P(G ∈ S, X₀ ∈ A₀, …) = ∫_{∏ Aᵢ} DP(α + n, posterior base)(S) dP(xs) over the urn law of the observations.

theorem_wanted setLIntegral_dirichletProcess_prod (α : ℝ) (hα : 0 < α) (H : Measure X)
    [IsProbabilityMeasure H] {n : ℕ} (A : Fin n → Set X) (hA : ∀ i, MeasurableSet (A i))
    {S : Set (Measure X)} (hS : MeasurableSet S) :
    ∫⁻ ν in S, ∏ i, ν (A i) ∂dirichletProcess α hα H =
      ∫⁻ xs in Set.univ.pi A,
        (haveI := isProbabilityMeasure_polyaUrnPredictive hα (H := H) xs;
          dirichletProcess (α + n) (add_pos_of_pos_of_nonneg hα n.cast_nonneg)
            (polyaUrnPredictive α H xs)) S ∂blackwellMacQueen α H n

Uses 4

Statement usesBlackwell–MacQueen urn · Dirichlet process · Blackwell–MacQueen predictive law is a probability measure · Blackwell–MacQueen urn predictive law

53 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.