Ancestral lineage counting and Tavaré's formula

DefinitionWright–Fisher transition probability of the lineage count#✓fully proved

One-generation transition probability of the ancestral lineage count in a neutral Wright–Fisher population of M gene copies: k lineages pick their parents uniformly and independently among M copies, and j distinct parents occur with probability stirlingSecond k j * M.descFactorial j / M ^ k.

noncomputable def wfLineageProb (M k j : ℕ) : ℝ :=
  (Nat.stirlingSecond k j : ℝ) * (M.descFactorial j : ℝ) / (M : ℝ) ^ k

Used by 6

Used byScaled Wright–Fisher lineage matrix converges to Kingman's generator · Wright–Fisher transition matrix of the lineage count · Moment duality, one generation · Moment duality, one generation (polynomial identity) · Moment duality, m generations · One Wright–Fisher generation acting on monomials

DefinitionWright–Fisher transition matrix of the lineage count#✓fully proved

The one-generation transition matrix of the ancestral lineage count of a sample of at most n gene copies in a Wright–Fisher population of M copies; row k, column j is wfLineageProb M k j.

noncomputable def wfLineageMatrix (n M : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ :=
  Matrix.of fun k j => wfLineageProb M k j

Uses 1 · Used by 5

Statement usesWright–Fisher transition probability of the lineage count

Used byScaled Wright–Fisher lineage matrix converges to Kingman's generator · Kingman's theorem for the lineage count · Tavaré's probabilities are nonnegative · Convergence on polynomials · Moment duality, m generations

DefinitionGenerator of Kingman's block-counting process#✓fully proved

The rate matrix of Kingman's block-counting (pure-death) process on {0, …, n}: k lineages become k - 1 at rate k.choose 2, time in units of M = 2N generations.

noncomputable def blockCountingGenerator (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ :=
  Matrix.of fun k j =>
    if (j : ℕ) + 1 = k then ((k : ℕ).choose 2 : ℝ)
    else if j = k then -((k : ℕ).choose 2 : ℝ) else 0

Used by 24

Used byRight eigenvector equation for the block-counting generator · Left eigenvector equation for the block-counting generator · Left and right eigenvector matrices are mutually inverse · Tavaré's formula · Spectral decomposition of the block-counting transition matrix · Truncation consistency · The block-counting process never gains lineages · Scaled Wright–Fisher lineage matrix converges to Kingman's generator · Kingman's theorem for the lineage count · Tavaré's probabilities sum to one · Tavaré's probabilities are nonnegative · Kingman's formula intertwines the block-counting generator with the partition rate matrix · Exchangeability · The time-t marginal of the partition-valued coalescent · Time-t marginal via Tavaré's formula · Dual moment polynomial of Kingman's coalescent · Kernel form of Wright–Fisher moment duality · Semigroup law · Dual semigroup fixes the constant polynomial one · Dual semigroup at time zero is the identity · Strong continuity · Generator on polynomials · Convergence on polynomials · Moment duality for the diffusion

DefinitionTavaré's formula for the number of ancestral lineages#✓fully proved

Tavaré's closed form for the probability that i lineages of Kingman's coalescent have j ancestors t time units (2N generations each) earlier, for 1 ≤ j ≤ i.

noncomputable def tavareProb (i j : ℕ) (t : ℝ) : ℝ :=
  ∑ k ∈ Finset.Icc j i,
    Real.exp (-((k : ℝ) * (k - 1) * t / 2)) * (2 * k - 1) * (-1) ^ (k - j) *
      (j.ascFactorial (k - 1) : ℝ) * (i.descFactorial k : ℝ) /
      ((j.factorial : ℝ) * ((k - j).factorial : ℝ) * (i.ascFactorial k : ℝ))

Used by 29

Used byTavaré's formula · No anomalous gene trees on the balanced four-species tree · Coalescence along one branch of the species tree · Only balanced gene trees can be anomalous on the caterpillar · Additivity of the exit law · Exit law of a constant continuation · Nonnegativity of the exit law · No anomalous unrooted quartets, balanced species tree · Probability of quartet split 02|13 on the balanced tree · Probability of quartet split 03|12 on the balanced tree · Probability of the gene tree ((A, B), (C, D)) on the caterpillar · Probability of the gene tree ((A, C), (B, D)) on the caterpillar · Probability of the gene tree ((A, D), (B, C)) on the caterpillar · The matching gene tree · No anomalous unrooted quartets, caterpillar species tree · Probability of quartet split 02|13 on the caterpillar tree · Probability of quartet split 03|12 on the caterpillar tree · Probability of the discordant three-species gene tree with cherry \(\{0, 2\}\) · Probability of the discordant three-species gene tree with cherry \(\{1, 2\}\) · Three-species concordance · Tavaré's probabilities sum to one · Tavaré's probabilities are nonnegative · Three lineages have one ancestor at time \(t\) · Three lineages remain distinct with probability \(e^{-3t}\) · Three lineages have two ancestors at time \(t\) · Two lineages coalesce with probability \(1 - e^{-t}\) · Two lineages remain distinct with probability \(e^{-t}\) · Wright–Fisher limit of the no-coalescence probability · Time-t marginal via Tavaré's formula

16 fully proved

Kingman's limit

TheoremScaled Wright–Fisher lineage matrix converges to Kingman's generator#✓fully proved

The scaled one-generation increment M • (wfLineageMatrix n M - 1) converges entrywise to the block-counting generator: k lineages coalesce to k - 1 with probability (k.choose 2) / M + o(1/M), and to fewer with probability O(1/M²).

theorem tendsto_smul_wfLineageMatrix_sub_one (n : ℕ) :
    Tendsto (fun M : ℕ => (M : ℝ) • (wfLineageMatrix n M - 1)) atTop
      (𝓝 (blockCountingGenerator n))

Uses 7 · Used by 1

Statement usesGenerator of Kingman's block-counting process · Wright–Fisher transition matrix of the lineage count

Proof usesWright–Fisher transition probability of the lineage count · Probability of no coalescence in one Wright–Fisher generation · No-coalescence probability as a falling factorial ratio · Kingman's coalescence rate · No-coalescence probability tends to one

Used byKingman's theorem for the lineage count

TheoremKingman's theorem for the lineage count#✓fully proved

For t ≥ 0, the ⌊t M⌋-generation transition matrix of the Wright–Fisher ancestral lineage count converges, as the population size M tends to infinity, to the transition matrix exp (t • G) of the pure-death process with rates k.choose 2.

theorem tendsto_wfLineageMatrix_pow_floor (n : ℕ) {t : ℝ} (ht : 0 ≤ t) :
    Tendsto (fun M : ℕ => wfLineageMatrix n M ^ ⌊t * M⌋₊) atTop
      (𝓝 (NormedSpace.exp (t • blockCountingGenerator n)))

Sources

• Kingman (1982); Durrett (2008), ch. 1. Proves the deferred entry tendsto_wfLineageMatrix_pow_floor.

Uses 4 · Used by 2

Statement usesGenerator of Kingman's block-counting process · Wright–Fisher transition matrix of the lineage count

Proof usesScaled Wright–Fisher lineage matrix converges to Kingman's generator · Compound-interest limit in a Banach algebra

Used byTavaré's probabilities are nonnegative · Convergence on polynomials

Tavaré's formula

DefinitionRight eigenvectors of Kingman's block-counting generator#✓fully proved

Right eigenvectors of the block-counting generator, as columns: column k has entries i_{(k)} / i^{(k)} (falling over rising factorial) and eigenvalue -(k.choose 2).

noncomputable def blockCountingRightEigen (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ :=
  Matrix.of fun i k => ((i : ℕ).descFactorial k : ℝ) / ((i : ℕ).ascFactorial k : ℝ)

Used by 8

Used byRight eigenvector equation for the block-counting generator · Left and right eigenvector matrices are mutually inverse · Tavaré's formula · Spectral decomposition of the block-counting transition matrix · Truncation consistency · The block-counting process never gains lineages · Strong continuity · Generator on polynomials

DefinitionLeft eigenvectors of Kingman's block-counting generator#✓fully proved

Left eigenvectors of the block-counting generator, as rows: row 0 is the indicator of state 0, and for 1 ≤ k row k has entries (2k-1) (-1)^{k-j} j^{(k-1)} / (j! (k-j)!) for j ≤ k and 0 for j > k; the eigenvalue is -(k.choose 2).

noncomputable def blockCountingLeftEigen (n : ℕ) : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ :=
  Matrix.of fun k j =>
    if (k : ℕ) = 0 then (if (j : ℕ) = 0 then 1 else 0)
    else if (j : ℕ) ≤ k then
      (2 * (k : ℕ) - 1) * (-1) ^ ((k : ℕ) - j) * ((j : ℕ).ascFactorial ((k : ℕ) - 1) : ℝ) /
        (((j : ℕ).factorial : ℝ) * (((k : ℕ) - j).factorial : ℝ))
    else 0

Used by 8

Used byLeft eigenvector equation for the block-counting generator · Left and right eigenvector matrices are mutually inverse · Tavaré's formula · Spectral decomposition of the block-counting transition matrix · Truncation consistency · The block-counting process never gains lineages · Strong continuity · Generator on polynomials

DefinitionEigenvalues of Kingman's block-counting generator#✓fully proved

The eigenvalues of the block-counting generator, -(k.choose 2).

noncomputable def blockCountingEigenvalue (n : ℕ) (k : Fin (n + 1)) : ℝ :=
  -((k : ℕ).choose 2 : ℝ)

Used by 9

Used byRight eigenvector equation for the block-counting generator · Left eigenvector equation for the block-counting generator · Left and right eigenvector matrices are mutually inverse · Tavaré's formula · Spectral decomposition of the block-counting transition matrix · Truncation consistency · The block-counting process never gains lineages · Strong continuity · Generator on polynomials

TheoremRight eigenvector equation for the block-counting generator#✓fully proved

The columns of blockCountingRightEigen n are right eigenvectors: G V = V D.

theorem blockCountingGenerator_mul_rightEigen (n : ℕ) :
    blockCountingGenerator n * blockCountingRightEigen n =
      blockCountingRightEigen n * diagonal (blockCountingEigenvalue n)

Uses 3 · Used by 3

Statement usesEigenvalues of Kingman's block-counting generator · Generator of Kingman's block-counting process · Right eigenvectors of Kingman's block-counting generator

Used byLeft and right eigenvector matrices are mutually inverse · Spectral decomposition of the block-counting transition matrix · Generator on polynomials

TheoremLeft eigenvector equation for the block-counting generator#✓fully proved

The rows of blockCountingLeftEigen n are left eigenvectors: W G = D W.

theorem blockCountingLeftEigen_mul_generator (n : ℕ) :
    blockCountingLeftEigen n * blockCountingGenerator n =
      diagonal (blockCountingEigenvalue n) * blockCountingLeftEigen n

Uses 3 · Used by 1

Statement usesEigenvalues of Kingman's block-counting generator · Generator of Kingman's block-counting process · Left eigenvectors of Kingman's block-counting generator

Used byLeft and right eigenvector matrices are mutually inverse

TheoremLeft and right eigenvector matrices are mutually inverse#✓fully proved

The left and right eigenvector matrices are mutually inverse: W V = 1.

theorem blockCountingLeftEigen_mul_rightEigen (n : ℕ) :
    blockCountingLeftEigen n * blockCountingRightEigen n = 1

Uses 6 · Used by 2

Statement usesLeft eigenvectors of Kingman's block-counting generator · Right eigenvectors of Kingman's block-counting generator

Proof usesEigenvalues of Kingman's block-counting generator · Generator of Kingman's block-counting process · Right eigenvector equation for the block-counting generator · Left eigenvector equation for the block-counting generator

Used bySpectral decomposition of the block-counting transition matrix · Generator on polynomials

TheoremSpectral decomposition of the block-counting transition matrix#✓fully proved

The spectral decomposition of the transition matrix of the block-counting process: exp (t • G) = V diag(exp (-(k.choose 2) t)) W.

theorem exp_smul_blockCountingGenerator (n : ℕ) (t : ℝ) :
    NormedSpace.exp (t • blockCountingGenerator n) =
      blockCountingRightEigen n *
        diagonal (fun k => Real.exp (t * blockCountingEigenvalue n k)) *
        blockCountingLeftEigen n

Uses 6 · Used by 5

Statement usesEigenvalues of Kingman's block-counting generator · Generator of Kingman's block-counting process · Left eigenvectors of Kingman's block-counting generator · Right eigenvectors of Kingman's block-counting generator

Proof usesRight eigenvector equation for the block-counting generator · Left and right eigenvector matrices are mutually inverse

Used byTavaré's formula · Truncation consistency · The block-counting process never gains lineages · Strong continuity · Generator on polynomials

TheoremTavaré's formula#✓fully proved

The transition probabilities of Kingman's block-counting process from i to j lineages in time t, for 1 ≤ j ≤ i ≤ n, are given by tavareProb.

theorem exp_blockCountingGenerator_apply (n : ℕ) (t : ℝ) (i j : Fin (n + 1))
    (hj : 1 ≤ (j : ℕ)) (hji : j ≤ i) :
    NormedSpace.exp (t • blockCountingGenerator n) i j = tavareProb i j t

Sources

• Tavaré (1984). Proves the deferred entry exp_blockCountingGenerator_apply.

Uses 6 · Used by 3

Statement usesGenerator of Kingman's block-counting process · Tavaré's formula for the number of ancestral lineages

Proof usesEigenvalues of Kingman's block-counting generator · Left eigenvectors of Kingman's block-counting generator · Right eigenvectors of Kingman's block-counting generator · Spectral decomposition of the block-counting transition matrix

Used byTavaré's probabilities sum to one · Tavaré's probabilities are nonnegative · Time-t marginal via Tavaré's formula

TheoremTruncation consistency#✓fully proved

For n ≤ N, the top-left (n + 1) × (n + 1) block of the transition matrix exp (t • G) of the block-counting process on {0, …, N} is the transition matrix of the process on {0, …, n} (the process only moves down). Holds for every real t.

theorem exp_smul_blockCountingGenerator_castLE {n N : ℕ} (h : n ≤ N) (t : ℝ)
    (i j : Fin (n + 1)) :
    NormedSpace.exp (t • blockCountingGenerator N) (Fin.castLE (by omega) i)
        (Fin.castLE (by omega) j) =
      NormedSpace.exp (t • blockCountingGenerator n) i j

Uses 5 · Used by 1

Statement usesGenerator of Kingman's block-counting process

Proof usesEigenvalues of Kingman's block-counting generator · Left eigenvectors of Kingman's block-counting generator · Right eigenvectors of Kingman's block-counting generator · Spectral decomposition of the block-counting transition matrix

Used bySemigroup law

TheoremThe block-counting process never gains lineages#✓fully proved

The block-counting process never gains lineages: exp (t • G) i j = 0 for i < j. Holds for every real t.

theorem exp_smul_blockCountingGenerator_of_lt {n : ℕ} (t : ℝ) {i j : Fin (n + 1)} (h : i < j) :
    NormedSpace.exp (t • blockCountingGenerator n) i j = 0

Uses 5 · Used by 1

Statement usesGenerator of Kingman's block-counting process

Proof usesEigenvalues of Kingman's block-counting generator · Left eigenvectors of Kingman's block-counting generator · Right eigenvectors of Kingman's block-counting generator · Spectral decomposition of the block-counting transition matrix

Used bySemigroup law

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.