Partition-valued Kingman coalescent

AbbreviationSet partitions of a labeled sample#✓fully proved

The set partitions of a sample of n labeled genes {0, …, n - 1}.

abbrev SamplePartition (n : ℕ) : Type := Finpartition (univ : Finset (Fin n))

Used by 35

Used byKingman's formula intertwines the block-counting generator with the partition rate matrix · Mergers · Partition coalescent transition matrix is row-stochastic · Partition obtained by merging two blocks · Partition rate matrix is a rate matrix · Law of Kingman's jump chain after m jumps · Exchangeability · Kingman's formula · Jump chain of Kingman's coalescent · Kingman's jump-chain matrix is row-stochastic · Kingman's formula arranged by number of blocks · Last row of Kingman's matrix is the singleton point mass · Kingman's formula · Kingman's formula at the partition into singletons · Kingman's formula is invariant under relabeling · Kingman's formula for a partition with k blocks · Number of blocks of a sample partition · Rate matrix of Kingman's partition-valued coalescent · Lumpability of restriction · Path probability of the Kingman coalescent jump chain · Restriction matrix on sample partitions · Jump-chain law sums to one · Kingman's formula is a probability distribution · Backward equation of Kingman's formula · Rows of the partition rate matrix sum to zero · Consistency of the jump chains · Time-t marginal sums to one · Consistency · Time-t marginal of Kingman's coalescent · Exchangeability · The time-t marginal of the partition-valued coalescent · Time-t marginal as a continuous-time chain transition · Time-t marginal via Tavaré's formula · Nonnegativity of the time-t marginal · Splitting identity

DefinitionPartition obtained by merging two blocks#✓fully proved

π' arises from π by merging two blocks: π refines π' and has exactly one more block (so exactly two blocks of π lie in one block of π', and the others are blocks of π').

def IsMerge (π π' : SamplePartition n) : Prop :=
  π ≤ π' ∧ #π'.parts + 1 = #π.parts

Uses 1 · Used by 11

Statement usesSet partitions of a labeled sample

Used byKingman's formula intertwines the block-counting generator with the partition rate matrix · Mergers · Partition rate matrix is a rate matrix · Kingman's formula · Jump chain of Kingman's coalescent · Kingman's jump-chain matrix is row-stochastic · Rate matrix of Kingman's partition-valued coalescent · Lumpability of restriction · Backward equation of Kingman's formula · Rows of the partition rate matrix sum to zero · Splitting identity

DefinitionJump chain of Kingman's coalescent#✓fully proved

The transition matrix of the jump chain of Kingman's coalescent: from a partition with k ≥ 2 blocks, move to each of the k.choose 2 partitions obtained by merging two blocks with probability 1 / k.choose 2; a partition with at most one block is absorbing.

noncomputable def jumpMatrix (n : ℕ) : Matrix (SamplePartition n) (SamplePartition n) ℝ :=
  Matrix.of fun π π' =>
    if 2 ≤ #π.parts then (if IsMerge π π' then (((#π.parts).choose 2 : ℕ) : ℝ)⁻¹ else 0)
    else if π = π' then 1 else 0

Uses 2 · Used by 5

Statement usesPartition obtained by merging two blocks · Set partitions of a labeled sample

Used byLaw of Kingman's jump chain after m jumps · Kingman's formula · Kingman's jump-chain matrix is row-stochastic · Path probability of the Kingman coalescent jump chain · Jump-chain law sums to one

DefinitionLaw of Kingman's jump chain after m jumps#✓fully proved

The law of the jump chain after m jumps, started from the partition into singletons: jumpLaw n m π is the probability that the partition after m coalescences is π.

noncomputable def jumpLaw (n m : ℕ) (π : SamplePartition n) : ℝ :=
  (jumpMatrix n ^ m) ⊥ π

Uses 2 · Used by 4

Statement usesSet partitions of a labeled sample · Jump chain of Kingman's coalescent

Used byExchangeability · Kingman's formula · Jump-chain law sums to one · Kingman's formula is a probability distribution

DefinitionKingman's formula#✓fully proved

The probability (n - k)! k! (k - 1)! ∏_{B ∈ π} |B|! / (n! (n - 1)!) of a partition π with k blocks of a sample of size n (meaningful for 1 ≤ k ≤ n; for the empty sample it gives 1 to the empty partition).

noncomputable def kingmanProb (n : ℕ) (π : SamplePartition n) : ℝ :=
  (((n - #π.parts).factorial * (#π.parts).factorial * (#π.parts - 1).factorial *
      π.cardProd Nat.factorial : ℕ) : ℝ) /
    ((n.factorial * (n - 1).factorial : ℕ) : ℝ)

Uses 2 · Used by 13

Statement usesProduct over block sizes · Set partitions of a labeled sample

Used byKingman's formula intertwines the block-counting generator with the partition rate matrix · Exchangeability · Kingman's formula · Kingman's formula arranged by number of blocks · Last row of Kingman's matrix is the singleton point mass · Kingman's formula at the partition into singletons · Kingman's formula is invariant under relabeling · Kingman's formula for a partition with k blocks · Kingman's formula is a probability distribution · Backward equation of Kingman's formula · Exchangeability · The time-t marginal of the partition-valued coalescent · Time-t marginal via Tavaré's formula

DefinitionRate matrix of Kingman's partition-valued coalescent#✓fully proved

The rate matrix of Kingman's partition-valued coalescent: each pair of blocks merges at rate 1, so a partition with k blocks is left at total rate k.choose 2 (time in units of 2N generations).

noncomputable def partitionRate (n : ℕ) : Matrix (SamplePartition n) (SamplePartition n) ℝ :=
  Matrix.of fun π π' =>
    if IsMerge π π' then 1 else if π = π' then -(((#π.parts).choose 2 : ℕ) : ℝ) else 0

Uses 2 · Used by 11

Statement usesPartition obtained by merging two blocks · Set partitions of a labeled sample

Used byKingman's formula intertwines the block-counting generator with the partition rate matrix · Partition coalescent transition matrix is row-stochastic · Partition rate matrix is a rate matrix · Lumpability of restriction · Rows of the partition rate matrix sum to zero · Time-t marginal sums to one · Consistency · Time-t marginal of Kingman's coalescent · The time-t marginal of the partition-valued coalescent · Time-t marginal as a continuous-time chain transition · Nonnegativity of the time-t marginal

DefinitionTime-t marginal of Kingman's coalescent#✓fully proved

The time-t marginal of Kingman's n-coalescent started from singletons: timeLaw n t π = exp (t • partitionRate n) ⊥ π is the probability that the ancestral partition of the sample at time t ≥ 0 (in units of 2N generations) is π. The matrix exponential is defined for every real t; the identities below hold for every real t.

noncomputable def timeLaw (n : ℕ) (t : ℝ) (π : SamplePartition n) : ℝ :=
  NormedSpace.exp (t • partitionRate n) ⊥ π

Uses 2 · Used by 7

Statement usesSet partitions of a labeled sample · Rate matrix of Kingman's partition-valued coalescent

Used byTime-t marginal sums to one · Consistency · Exchangeability · The time-t marginal of the partition-valued coalescent · Time-t marginal as a continuous-time chain transition · Time-t marginal via Tavaré's formula · Nonnegativity of the time-t marginal

DefinitionRestriction matrix on sample partitions#✓fully proved

The restriction map as a 0/1 matrix: entry (π, ρ) is 1 iff π.comap Fin.castSucc = ρ.

noncomputable def restrictMatrix (n : ℕ) :
    Matrix (SamplePartition (n + 1)) (SamplePartition n) ℝ :=
  Matrix.of fun π ρ => if π.comap Fin.castSucc = ρ then 1 else 0

Uses 2 · Used by 2

Statement usesPull-back of a finite partition along a map · Set partitions of a labeled sample

Used byLumpability of restriction · Consistency

TheoremMergers#✓fully proved

A partition with k blocks has exactly k.choose 2 partitions that arise from it by merging two blocks.

theorem card_isMerge (π : SamplePartition n) :
    #{π' | IsMerge π π'} = (#π.parts).choose 2

Uses 2 · Used by 2

Statement usesPartition obtained by merging two blocks · Set partitions of a labeled sample

Used byKingman's jump-chain matrix is row-stochastic · Rows of the partition rate matrix sum to zero

TheoremSplitting identity#✓fully proved

Summing ∏_{B ∈ π} |B|! over the partitions π that merge to π' gives (n - #π'.parts) / 2 · ∏_{B ∈ π'} |B|!: a block of size b has (2^b - 2) / 2 splits into two blocks, and ∑_{∅ ≠ A ⊊ B} |A|! |B \ A|! = (b - 1) b!.

theorem two_mul_sum_prod_factorial_isMerge (π' : SamplePartition n) :
    2 * ∑ π with IsMerge π π', π.cardProd Nat.factorial =
      (n - #π'.parts) * π'.cardProd Nat.factorial

Uses 3 · Used by 1

Statement usesProduct over block sizes · Partition obtained by merging two blocks · Set partitions of a labeled sample

Used byBackward equation of Kingman's formula

TheoremKingman's formula at the partition into singletons#✓fully proved

Kingman's formula gives probability 1 to the partition into singletons.

theorem kingmanProb_bot : kingmanProb n ⊥ = 1

Uses 3 · Used by 2

Statement usesSet partitions of a labeled sample · Kingman's formula

Proof usesProduct over block sizes

Used byKingman's formula · Last row of Kingman's matrix is the singleton point mass

TheoremKingman's formula for a partition with k blocks#✓fully proved

Kingman's formula for a partition with k blocks.

theorem kingmanProb_of_card {π : SamplePartition n} {k : ℕ} (h : #π.parts = k) :
    kingmanProb n π = ((n - k).factorial * k.factorial * (k - 1).factorial : ℝ) *
      ((π.cardProd Nat.factorial : ℕ) : ℝ) / (n.factorial * (n - 1).factorial : ℝ)

Uses 3 · Used by 1

Statement usesProduct over block sizes · Set partitions of a labeled sample · Kingman's formula

Used byBackward equation of Kingman's formula

TheoremBackward equation of Kingman's formula#✓fully proved

For a partition π' with k blocks, 1 ≤ k < n, the Kingman probabilities of the partitions merging to π' sum to (k + 1).choose 2 times the Kingman probability of π'.

theorem sum_kingmanProb_isMerge (π' : SamplePartition n) (h1 : 1 ≤ #π'.parts)
    (hn : #π'.parts < n) :
    ∑ π with IsMerge π π', kingmanProb n π =
      (((#π'.parts + 1).choose 2 : ℕ) : ℝ) * kingmanProb n π'

Uses 6 · Used by 2

Statement usesPartition obtained by merging two blocks · Set partitions of a labeled sample · Kingman's formula

Proof usesProduct over block sizes · Kingman's formula for a partition with k blocks · Splitting identity

Used byKingman's formula intertwines the block-counting generator with the partition rate matrix · Kingman's formula

TheoremKingman's jump-chain matrix is row-stochastic#✓fully proved

The jump-chain transition matrix is row-stochastic.

theorem jumpMatrix_mem_rowStochastic : jumpMatrix n ∈ rowStochastic ℝ (SamplePartition n)

Uses 4 · Used by 1

Statement usesSet partitions of a labeled sample · Jump chain of Kingman's coalescent

Proof usesPartition obtained by merging two blocks · Mergers

Used byJump-chain law sums to one

TheoremKingman's formula#✓fully proved

Kingman's formula (Kingman 1982; Durrett 2008, ch. 1). For m < n, after m coalescences the jump chain started from singletons is at a partition π with probability kingmanProb n π = (n - k)! k! (k - 1)! ∏_{B ∈ π} |B|! / (n! (n - 1)!) if π has k = n - m blocks, and 0 otherwise. (For m ≥ n - 1 the chain has been absorbed at the one-block partition.)

theorem jumpLaw_eq {m : ℕ} (hm : m < n) (π : SamplePartition n) :
    jumpLaw n m π = if #π.parts + m = n then kingmanProb n π else 0

Uses 8 · Used by 2

Statement usesSet partitions of a labeled sample · Law of Kingman's jump chain after m jumps · Kingman's formula

Proof usesRecognizing the partition into singletons by its number of blocks · Partition obtained by merging two blocks · Jump chain of Kingman's coalescent · Kingman's formula at the partition into singletons · Backward equation of Kingman's formula

Used byExchangeability · Kingman's formula is a probability distribution

TheoremJump-chain law sums to one#✓fully proved

The jump chain's law after m jumps sums to one (its entries are nonnegative by jumpMatrix_mem_rowStochastic).

theorem sum_jumpLaw (m : ℕ) : ∑ π, jumpLaw n m π = 1

Uses 4 · Used by 1

Statement usesSet partitions of a labeled sample · Law of Kingman's jump chain after m jumps

Proof usesJump chain of Kingman's coalescent · Kingman's jump-chain matrix is row-stochastic

Used byKingman's formula is a probability distribution

TheoremKingman's formula is a probability distribution#✓fully proved

Kingman's formula is a probability distribution on the partitions with k blocks, for 1 ≤ k ≤ n. Equivalently, ∑_{π, k blocks} ∏_{B ∈ π} |B|! = n! (n - 1)! / ((n - k)! k! (k - 1)!), the Lah number L(n, k).

theorem sum_kingmanProb {k : ℕ} (hk : 1 ≤ k) (hkn : k ≤ n) :
    ∑ π with #π.parts = k, kingmanProb n π = 1

Uses 5

Statement usesSet partitions of a labeled sample · Kingman's formula

Proof usesLaw of Kingman's jump chain after m jumps · Kingman's formula · Jump-chain law sums to one

TheoremKingman's formula is invariant under relabeling#✓fully proved

Relabeling the sample by a permutation (Finpartition.comap) preserves Kingman's formula.

theorem kingmanProb_comap_perm (σ : Equiv.Perm (Fin n)) (π : SamplePartition n) :
    kingmanProb n (π.comap σ) = kingmanProb n π

Uses 6 · Used by 2

Statement usesPull-back of a finite partition along a map · Set partitions of a labeled sample · Kingman's formula

Proof usesProduct over block sizes · Pull-back along an equivalence preserves block-size products · Pull-back along an equivalence preserves the number of blocks

Used byExchangeability · Exchangeability

TheoremExchangeability#✓fully proved

Exchangeability of the jump chain: for m < n, relabeling the sample does not change the probability of a partition after m coalescences.

theorem jumpLaw_comap_perm {m : ℕ} (hm : m < n) (σ : Equiv.Perm (Fin n))
    (π : SamplePartition n) : jumpLaw n m (π.comap σ) = jumpLaw n m π

Uses 7

Statement usesPull-back of a finite partition along a map · Set partitions of a labeled sample · Law of Kingman's jump chain after m jumps

Proof usesPull-back along an equivalence preserves the number of blocks · Kingman's formula · Kingman's formula · Kingman's formula is invariant under relabeling

DefinitionNumber of blocks of a sample partition#✓fully proved

The number of blocks of a partition of a sample of n, as an element of Fin (n + 1) (a state of the block-counting process).

def numBlocks (π : SamplePartition n) : Fin (n + 1) :=
  ⟨#π.parts, Nat.lt_succ_of_le (by simpa using π.card_parts_le_card)⟩

Uses 1 · Used by 3

Statement usesSet partitions of a labeled sample

Used byExchangeability · The time-t marginal of the partition-valued coalescent · Time-t marginal via Tavaré's formula

DefinitionKingman's formula arranged by number of blocks#✓fully proved

Kingman's formula arranged by number of blocks: entry (k, π) is kingmanProb n π if π has k blocks and 0 otherwise. For 1 ≤ k ≤ n, row k is the law of the jump chain after n - k jumps (jumpLaw_eq).

noncomputable def kingmanMatrix (n : ℕ) : Matrix (Fin (n + 1)) (SamplePartition n) ℝ :=
  Matrix.of fun k π => if #π.parts = (k : ℕ) then kingmanProb n π else 0

Uses 2 · Used by 3

Statement usesSet partitions of a labeled sample · Kingman's formula

Used byKingman's formula intertwines the block-counting generator with the partition rate matrix · Last row of Kingman's matrix is the singleton point mass · The time-t marginal of the partition-valued coalescent

TheoremLast row of Kingman's matrix is the singleton point mass#✓fully proved

Row n of kingmanMatrix n is the point mass at the partition into singletons.

theorem kingmanMatrix_last (π : SamplePartition n) :
    kingmanMatrix n (Fin.last n) π = if π = ⊥ then 1 else 0

Uses 5 · Used by 1

Statement usesSet partitions of a labeled sample · Kingman's formula arranged by number of blocks

Proof usesRecognizing the partition into singletons by its number of blocks · Kingman's formula · Kingman's formula at the partition into singletons

Used byThe time-t marginal of the partition-valued coalescent

TheoremKingman's formula intertwines the block-counting generator with the partition rate matrix#✓fully proved

Kingman's formula intertwines the block-counting generator with the partition rate matrix: G * Λ = Λ * Q. This is the backward equation sum_kingmanProb_isMerge in matrix form.

theorem blockCountingGenerator_mul_kingmanMatrix :
    blockCountingGenerator n * kingmanMatrix n = kingmanMatrix n * partitionRate n

Uses 8 · Used by 1

Statement usesGenerator of Kingman's block-counting process · Set partitions of a labeled sample · Kingman's formula arranged by number of blocks · Rate matrix of Kingman's partition-valued coalescent

Proof usesA partition has a block exactly when its ground set is nonempty · Partition obtained by merging two blocks · Kingman's formula · Backward equation of Kingman's formula

Used byThe time-t marginal of the partition-valued coalescent

TheoremThe time-t marginal of the partition-valued coalescent#✓fully proved

The time-t marginal of the partition-valued coalescent (Kingman 1982): for every real t, the probability of a partition π with k blocks is the probability that the block-counting process goes from n to k lineages in time t, times Kingman's formula.

theorem timeLaw_eq (t : ℝ) (π : SamplePartition n) :
    timeLaw n t π =
      NormedSpace.exp (t • blockCountingGenerator n) (Fin.last n) (numBlocks π) *
        kingmanProb n π

Uses 10 · Used by 2

Statement usesGenerator of Kingman's block-counting process · Set partitions of a labeled sample · Kingman's formula · Number of blocks of a sample partition · Time-t marginal of Kingman's coalescent

Proof usesKingman's formula intertwines the block-counting generator with the partition rate matrix · Kingman's formula arranged by number of blocks · Last row of Kingman's matrix is the singleton point mass · Rate matrix of Kingman's partition-valued coalescent · Intertwining passes to the exponential

Used byExchangeability · Time-t marginal via Tavaré's formula

TheoremTime-t marginal via Tavaré's formula#✓fully proved

The time-t marginal with Tavaré's closed form for the block-counting factor: for a partition π of a sample of n (so π has at least one block when n ≥ 1), P(Π_t = π) = tavareProb n k t · kingmanProb n π with k = #π.parts.

theorem timeLaw_eq_tavareProb (hn : 1 ≤ n) (t : ℝ) (π : SamplePartition n) :
    timeLaw n t π = tavareProb n #π.parts t * kingmanProb n π

Uses 9

Statement usesTavaré's formula for the number of ancestral lineages · Set partitions of a labeled sample · Kingman's formula · Time-t marginal of Kingman's coalescent

Proof usesA partition has a block exactly when its ground set is nonempty · Generator of Kingman's block-counting process · Tavaré's formula · Number of blocks of a sample partition · The time-t marginal of the partition-valued coalescent

TheoremExchangeability#✓fully proved

Exchangeability of the time-t marginal.

theorem timeLaw_comap_perm (t : ℝ) (σ : Equiv.Perm (Fin n)) (π : SamplePartition n) :
    timeLaw n t (π.comap σ) = timeLaw n t π

Uses 9

Statement usesPull-back of a finite partition along a map · Set partitions of a labeled sample · Time-t marginal of Kingman's coalescent

Proof usesPull-back along an equivalence preserves the number of blocks · Generator of Kingman's block-counting process · Kingman's formula · Kingman's formula is invariant under relabeling · Number of blocks of a sample partition · The time-t marginal of the partition-valued coalescent

TheoremRows of the partition rate matrix sum to zero#✓fully proved

Each row of the partition rate matrix sums to 0: a partition with k blocks has k.choose 2 mergers (card_isMerge), each at rate 1.

theorem sum_partitionRate (π : SamplePartition n) : ∑ π', partitionRate n π π' = 0

Uses 4 · Used by 2

Statement usesSet partitions of a labeled sample · Rate matrix of Kingman's partition-valued coalescent

Proof usesPartition obtained by merging two blocks · Mergers

Used byPartition rate matrix is a rate matrix · Time-t marginal sums to one

TheoremPartition rate matrix is a rate matrix#✓fully proved

The partition rate matrix is a rate matrix: off-diagonal entries are 0 or 1, and each row sums to 0 (sum_partitionRate).

theorem isRateMatrix_partitionRate : ProbabilityTheory.IsRateMatrix (partitionRate n)

Uses 5 · Used by 2

Statement usesSet partitions of a labeled sample · Rate matrix of Kingman's partition-valued coalescent · Rate matrix

Proof usesPartition obtained by merging two blocks · Rows of the partition rate matrix sum to zero

Used byPartition coalescent transition matrix is row-stochastic · Nonnegativity of the time-t marginal

TheoremTime-t marginal as a continuous-time chain transition#✓fully proved

timeLaw is a row of the transition function P t = exp (t • partitionRate n) of the continuous-time chain with rate matrix partitionRate n.

theorem timeLaw_eq_ctmcTransition (t : ℝ) (π : SamplePartition n) :
    timeLaw n t π = ProbabilityTheory.ctmcTransition (partitionRate n) t ⊥ π

Uses 4

Statement usesSet partitions of a labeled sample · Rate matrix of Kingman's partition-valued coalescent · Time-t marginal of Kingman's coalescent · Transition semigroup of a continuous-time Markov chain

TheoremPartition coalescent transition matrix is row-stochastic#✓fully proved

For t ≥ 0 the transition matrix exp (t • partitionRate n) is row-stochastic.

theorem ctmcTransition_partitionRate_mem_rowStochastic {t : ℝ} (ht : 0 ≤ t) :
    ProbabilityTheory.ctmcTransition (partitionRate n) t ∈ rowStochastic ℝ (SamplePartition n)

Uses 5

Statement usesSet partitions of a labeled sample · Rate matrix of Kingman's partition-valued coalescent · Transition semigroup of a continuous-time Markov chain

Proof usesPartition rate matrix is a rate matrix · Transition function of a rate matrix is row-stochastic

TheoremNonnegativity of the time-t marginal#✓fully proved

For t ≥ 0 the time-t marginal is nonnegative; with sum_timeLaw it is a probability distribution on the partitions of the sample.

theorem timeLaw_nonneg {t : ℝ} (ht : 0 ≤ t) (π : SamplePartition n) : 0 ≤ timeLaw n t π

Uses 5

Statement usesSet partitions of a labeled sample · Time-t marginal of Kingman's coalescent

Proof usesPartition rate matrix is a rate matrix · Rate matrix of Kingman's partition-valued coalescent · Nonnegativity of the transition function of a rate matrix

TheoremTime-t marginal sums to one#✓fully proved

The time-t marginal sums to one over all partitions: ∑_π timeLaw n t π = 1 (for every real t, since the rows of the rate matrix sum to 0).

theorem sum_timeLaw (t : ℝ) : ∑ π, timeLaw n t π = 1

Uses 5

Statement usesSet partitions of a labeled sample · Time-t marginal of Kingman's coalescent

Proof usesRate matrix of Kingman's partition-valued coalescent · Rows of the partition rate matrix sum to zero · Intertwining passes to the exponential

TheoremLumpability of restriction#✓fully proved

Lumpability of restriction (Kingman 1982): restricting to the first n genes intertwines the rate matrices of the (n + 1)- and n-coalescents.

theorem partitionRate_mul_restrictMatrix :
    partitionRate (n + 1) * restrictMatrix n = restrictMatrix n * partitionRate n

Uses 6 · Used by 1

Statement usesSet partitions of a labeled sample · Rate matrix of Kingman's partition-valued coalescent · Restriction matrix on sample partitions

Proof usesPull-back of a finite partition along a map · Blocks of a pulled-back partition · Partition obtained by merging two blocks

Used byConsistency

TheoremConsistency#✓fully proved

Consistency (Kingman 1982): the time-t law of the restriction of the (n + 1)-coalescent to the first n genes is the time-t law of the n-coalescent.

theorem sum_timeLaw_restrict (t : ℝ) (ρ : SamplePartition n) :
    ∑ π with π.comap Fin.castSucc = ρ, timeLaw (n + 1) t π = timeLaw n t ρ

Uses 8

Statement usesPull-back of a finite partition along a map · Set partitions of a labeled sample · Time-t marginal of Kingman's coalescent

Proof usesBlocks of a pulled-back partition · Rate matrix of Kingman's partition-valued coalescent · Lumpability of restriction · Restriction matrix on sample partitions · Intertwining passes to the exponential

DefinitionPath probability of the Kingman coalescent jump chain#✓fully proved

The probability that the jump chain of Kingman's n-coalescent, started from the partition into singletons, follows the list of partitions l: 0 unless l starts at the partition into singletons, and otherwise the product of the one-step transition probabilities jumpMatrix n along l. The empty list has probability 0.

noncomputable def pathProb (n : ℕ) : List (SamplePartition n) → ℝ
  | [] => 0
  | π :: l => (if π = ⊥ then 1 else 0) * (List.zipWith (jumpMatrix n) (π :: l) l).prod

Uses 2 · Used by 1

Statement usesSet partitions of a labeled sample · Jump chain of Kingman's coalescent

Used byConsistency of the jump chains

TheoremConsistency of the jump chains#●ready to prove

Consistency of the jump chains (Kingman 1982): for n ≥ 1, restricting each partition of a path of the (n + 1)-jump chain (a list of n + 1 partitions) to the first n genes and deleting consecutive repetitions gives a list of n partitions of Fin n distributed as the path of the n-jump chain.

theorem_wanted sum_pathProb_restrict (n : ℕ) (hn : 1 ≤ n) (ρs : List (SamplePartition n))
    (hρs : ρs.length = n) :
    ∑ p : Fin (n + 1) → SamplePartition (n + 1)
        with ((List.ofFn p).map (Finpartition.comap Fin.castSucc)).destutter (· ≠ ·) = ρs,
      pathProb (n + 1) (List.ofFn p) = pathProb n ρs

Sources

• Kingman (1982); Durrett (2008), ch. 1.

Uses 3

Statement usesPull-back of a finite partition along a map · Set partitions of a labeled sample · Path probability of the Kingman coalescent jump chain

35 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.