Kingman's coalescent and Watterson's estimator

22 fully proved

Elementary sums

TheoremSum of reciprocals of binomial coefficients \(\binom{k}{2}\)#✓fully proved

∑_{k=2}^n (k.choose 2)⁻¹ = 2 (1 - 1/n) for n ≥ 1 (telescoping 2/(k(k-1))).

theorem sum_inv_choose_two {n : ℕ} (hn : 1 ≤ n) :
    ∑ k ∈ Icc 2 n, ((k.choose 2 : ℕ) : ℝ)⁻¹ = 2 * (1 - 1 / n)

Used by 2

Used byTotal merger rate of the Bolthausen–Sznitman coalescent · Expected time to the most recent common ancestor

TheoremWeighted sum of reciprocals of \(\binom{k}{2}\) is twice a harmonic number#✓fully proved

∑_{k=2}^n k (k.choose 2)⁻¹ = 2 H_{n-1}.

theorem sum_mul_inv_choose_two (n : ℕ) :
    ∑ k ∈ Icc 2 n, (k : ℝ) * ((k.choose 2 : ℕ) : ℝ)⁻¹ = 2 * (harmonic (n - 1) : ℝ)

Used by 2

Used byExpected total branch length of the coalescent · Pair coalescence time against the total branch length

The holding-time model

StructureHolding times of Kingman's coalescent#✓fully proved

Kingman's coalescent for a sample of size n, through its holding times: T k is the time (in units of 2N generations) during which the genealogy has exactly k lineages, for 2 ≤ k ≤ n. These are independent, and T k is exponential with rate k.choose 2. The values of T k for k ∉ [2, n] are irrelevant.

structure KingmanTimes (μ : Measure Ω) (n : ℕ) where
  /-- `T k` is the holding time while the genealogy has `k` lineages. -/
  T : ℕ → Ω → ℝ
  /-- `T k` is exponential with rate `k.choose 2`, the number of pairs of lineages. -/
  hasLaw : ∀ k ∈ Icc 2 n, HasLaw (T k) (expMeasure (k.choose 2 : ℕ)) μ
  /-- The holding times are mutually independent. -/
  indep : iIndepFun (fun k : Icc 2 n => T k) μ

Used by 20

Used byExpected site frequency spectrum · Integrability of coalescent holding times · Integrability of the total branch length · Expected number of segregating sites · Expected coalescent holding time · Expected time to the most recent common ancestor · Expected total branch length of the coalescent · Kingman coalescent from coordinate projections · Time to the most recent common ancestor · Total branch length of a coalescent genealogy · Variance of the time to the most recent common ancestor · Watterson's estimator is unbiased · Covariance of π and S · Pair coalescence time against the total branch length · Tajima's numerator has mean zero · Unbiased estimator of Tajima's variance term · Variance of the number of segregating sites · Tajima's variance identity · Variance of the total branch length · Achaz's estimator is unbiased under Kingman's coalescent

DefinitionTime to the most recent common ancestor#✓fully proved

Time to the most recent common ancestor of the sample.

def tmrca : Ω → ℝ := fun ω => ∑ k ∈ Icc 2 n, K.T k ω

Uses 1 · Used by 2

Statement usesHolding times of Kingman's coalescent

Used byExpected time to the most recent common ancestor · Variance of the time to the most recent common ancestor

DefinitionTotal branch length of a coalescent genealogy#✓fully proved

Total branch length of the sample genealogy: k branches during T k.

def totalLength : Ω → ℝ := fun ω => ∑ k ∈ Icc 2 n, (k : ℝ) * K.T k ω

Uses 1 · Used by 11

Statement usesHolding times of Kingman's coalescent

Used byIntegrability of the total branch length · Expected number of segregating sites · Expected total branch length of the coalescent · Watterson's estimator is unbiased · Covariance of π and S · Pair coalescence time against the total branch length · Tajima's numerator has mean zero · Unbiased estimator of Tajima's variance term · Variance of the number of segregating sites · Tajima's variance identity · Variance of the total branch length

LemmaPositivity of the number of pairs#✓fully proved

The number of pairs k.choose 2 is positive for k ∈ [2, n].

lemma choose_two_pos {k : ℕ} (hk : k ∈ Icc 2 n) : (0 : ℝ) < ((k.choose 2 : ℕ) : ℝ)

Used by 9

Used byIntegrability of coalescent holding times · Expected coalescent holding time · Kingman coalescent from coordinate projections · Variance of the time to the most recent common ancestor · Pair coalescence time against the total branch length · Variance of the total branch length · The skyline estimate is unbiased · Coordinate projections form a skyline model · Variance of the skyline estimate

TheoremIntegrability of coalescent holding times#✓fully proved

Each holding time is integrable.

theorem integrable_T {k : ℕ} (hk : k ∈ Icc 2 n) : Integrable (K.T k) μ

Uses 3 · Used by 5

Statement usesHolding times of Kingman's coalescent

Proof usesPositivity of the number of pairs · Exponentially distributed random variables are integrable

Used byExpected site frequency spectrum · Integrability of the total branch length · Expected time to the most recent common ancestor · Expected total branch length of the coalescent · Pair coalescence time against the total branch length

TheoremExpected coalescent holding time#✓fully proved

E[T k] = (k.choose 2)⁻¹.

theorem integral_T {k : ℕ} (hk : k ∈ Icc 2 n) : μ[K.T k] = ((k.choose 2 : ℕ) : ℝ)⁻¹

Uses 3 · Used by 4

Statement usesHolding times of Kingman's coalescent

Proof usesPositivity of the number of pairs · Mean of an exponentially distributed random variable

Used byExpected site frequency spectrum · Expected time to the most recent common ancestor · Expected total branch length of the coalescent · Pair coalescence time against the total branch length

TheoremExpected time to the most recent common ancestor#✓fully proved

The expected time to the most recent common ancestor is 2 (1 - 1/n).

theorem integral_tmrca (hn : 1 ≤ n) : μ[K.tmrca] = 2 * (1 - 1 / (n : ℝ))

Uses 5

Statement usesHolding times of Kingman's coalescent · Time to the most recent common ancestor

Proof usesIntegrability of coalescent holding times · Expected coalescent holding time · Sum of reciprocals of binomial coefficients \(\binom{k}{2}\)

TheoremIntegrability of the total branch length#✓fully proved

The total branch length is integrable.

theorem integrable_totalLength : Integrable K.totalLength μ

Uses 3 · Used by 1

Statement usesHolding times of Kingman's coalescent · Total branch length of a coalescent genealogy

Proof usesIntegrability of coalescent holding times

Used byCovariance of π and S

TheoremExpected total branch length of the coalescent#✓fully proved

The expected total branch length is 2 H_{n-1}.

theorem integral_totalLength : μ[K.totalLength] = 2 * (harmonic (n - 1) : ℝ)

Uses 5 · Used by 3

Statement usesHolding times of Kingman's coalescent · Total branch length of a coalescent genealogy

Proof usesIntegrability of coalescent holding times · Expected coalescent holding time · Weighted sum of reciprocals of \(\binom{k}{2}\) is twice a harmonic number

Used byExpected number of segregating sites · Covariance of π and S · Variance of the number of segregating sites

TheoremVariance of the time to the most recent common ancestor#✓fully proved

The variance of the time to the most recent common ancestor is ∑_{k=2}^n ((k.choose 2)⁻¹)² (this uses independence).

theorem variance_tmrca :
    Var[K.tmrca; μ] = ∑ k ∈ Icc 2 n, (((k.choose 2 : ℕ) : ℝ)⁻¹) ^ 2

Uses 5

Statement usesHolding times of Kingman's coalescent · Time to the most recent common ancestor

Proof usesPositivity of the number of pairs · Variance of an exponentially distributed random variable · Finiteness of all moments of the exponential law

Watterson's estimator

TheoremExpected number of segregating sites#✓fully proved

Infinite-sites mutation at rate θ/2 per lineage per unit time: if the number of segregating sites S is integrable and has conditional mean (θ/2) L given the genealogy σ-algebra m, then E S = θ H_{n-1}. (Integrability matters: Mathlib's conditional expectation of a non-integrable function is 0.)

theorem integral_segSites (hm : m ≤ mΩ) [SigmaFinite (μ.trim hm)] (hSi : Integrable S μ)
    (hS : μ[S | m] =ᵐ[μ] fun ω => θ / 2 * K.totalLength ω) :
    μ[S] = θ * (harmonic (n - 1) : ℝ)

Uses 3 · Used by 2

Statement usesHolding times of Kingman's coalescent · Total branch length of a coalescent genealogy

Proof usesExpected total branch length of the coalescent

Used byWatterson's estimator is unbiased · Unbiased estimator of Tajima's variance term

TheoremIntegrability of Watterson's estimator#✓fully proved

Watterson's estimator S / H_{n-1} is integrable when S is.

theorem integrable_watterson (hSi : Integrable S μ) :
    Integrable (fun ω => S ω / (harmonic (n - 1) : ℝ)) μ

TheoremWatterson's estimator is unbiased#✓fully proved

E[S / H_{n-1}] = θ for a sample of size n ≥ 2.

theorem watterson_unbiased (hm : m ≤ mΩ) [SigmaFinite (μ.trim hm)] (hSi : Integrable S μ)
    (hS : μ[S | m] =ᵐ[μ] fun ω => θ / 2 * K.totalLength ω) (hn : 2 ≤ n) :
    μ[fun ω => S ω / (harmonic (n - 1) : ℝ)] = θ

Uses 3 · Used by 1

Statement usesHolding times of Kingman's coalescent · Total branch length of a coalescent genealogy

Proof usesExpected number of segregating sites

Used byTajima's numerator has mean zero

A concrete model

DefinitionCanonical probability space for Kingman holding times#✓fully proved

The canonical probability space for the Kingman holding times of a sample of size n: the product of the exponential laws Exp (k.choose 2), 2 ≤ k ≤ n.

def piMeasure (n : ℕ) : Measure (Icc 2 n → ℝ) :=
  Measure.pi fun k : Icc 2 n => expMeasure ((k : ℕ).choose 2 : ℕ)

Used by 1

Used byKingman coalescent from coordinate projections

DefinitionKingman coalescent from coordinate projections#✓fully proved

The coordinate projections of piMeasure n form a Kingman coalescent; in particular KingmanTimes is inhabited for every sample size.

MathlibExt.Biology.PopulationGenetics.Coalescent.KingmanTimes.ofPi · 18 lines

def KingmanTimes.ofPi (n : ℕ) : KingmanTimes (piMeasure n) n where
  T k ω := if h : k ∈ Icc 2 n then ω ⟨k, h⟩ else 0
  hasLaw k hk := by
    have hT : (fun ω : Icc 2 n → ℝ => if h : k ∈ Icc 2 n then ω ⟨k, h⟩ else 0)
        = fun ω => ω ⟨k, hk⟩ := by
      funext ω
      simp [hk]
    rw [hT]
    exact (measurePreserving_eval (fun i : Icc 2 n => expMeasure (((i : ℕ).choose 2 : ℕ) : ℝ))
      ⟨k, hk⟩).hasLaw
  indep := by
    have hT : (fun k : Icc 2 n => fun ω : Icc 2 n → ℝ =>
        if h : (k : ℕ) ∈ Icc 2 n then ω ⟨k, h⟩ else 0) = fun k ω => id (ω k) := by
      funext k ω
      simp [k.2]
    rw [hT]
    exact iIndepFun_pi (μ := fun i : Icc 2 n => expMeasure (((i : ℕ).choose 2 : ℕ) : ℝ))
      (fun _ => aemeasurable_id)

Uses 3

Statement usesHolding times of Kingman's coalescent · Positivity of the number of pairs · Canonical probability space for Kingman holding times

Wright–Fisher → Kingman

DefinitionProbability of no coalescence in one Wright–Fisher generation#✓fully proved

In a Wright–Fisher population of M gene copies, the probability that k lineages, choosing their parents independently and uniformly, have k distinct parents.

def noCoalProb (M k : ℕ) : ℝ := ∏ i ∈ range k, (1 - (i : ℝ) / M)

Used by 6

Used byScaled Wright–Fisher lineage matrix converges to Kingman's generator · No-coalescence probability as a falling factorial ratio · Kingman's coalescence rate · No-coalescence probability tends to one · Wright–Fisher coalescence times converge to exponential laws · Wright–Fisher limit of the no-coalescence probability

TheoremNo-coalescence probability as a falling factorial ratio#✓fully proved

noCoalProb M k is the falling factorial M (M-1) ⋯ (M-k+1) divided by M ^ k.

theorem noCoalProb_eq_descFactorial_div {M : ℕ} (hM : 0 < M) (k : ℕ) :
    noCoalProb M k = (M.descFactorial k : ℝ) / (M : ℝ) ^ k

Uses 1 · Used by 1

Statement usesProbability of no coalescence in one Wright–Fisher generation

Used byScaled Wright–Fisher lineage matrix converges to Kingman's generator

TheoremNo-coalescence probability tends to one#✓fully proved

noCoalProb M k → 1 as M → ∞.

theorem tendsto_noCoalProb_one (k : ℕ) :
    Tendsto (fun M : ℕ => noCoalProb M k) atTop (𝓝 1)

Uses 1 · Used by 3

Statement usesProbability of no coalescence in one Wright–Fisher generation

Used byScaled Wright–Fisher lineage matrix converges to Kingman's generator · Kingman's coalescence rate · Wright–Fisher coalescence times converge to exponential laws

TheoremKingman's coalescence rate#✓fully proved

For M gene copies (M = 2N), the per-generation probability that some of k lineages coalesce is (k.choose 2) / M + o(1/M); i.e. in time units of M generations, coalescences occur at rate k.choose 2.

theorem tendsto_coalescence_rate (k : ℕ) :
    Tendsto (fun M : ℕ => (M : ℝ) * (1 - noCoalProb M k)) atTop (𝓝 (k.choose 2 : ℕ))

Uses 2 · Used by 2

Statement usesProbability of no coalescence in one Wright–Fisher generation

Proof usesNo-coalescence probability tends to one

Used byScaled Wright–Fisher lineage matrix converges to Kingman's generator · Wright–Fisher coalescence times converge to exponential laws

TheoremWright–Fisher coalescence times converge to exponential laws#✓fully proved

After ⌊t M⌋ Wright–Fisher generations (t ≥ 0 coalescent time units), the probability that k lineages have not coalesced tends to exp (-(k.choose 2) t), the survival function of the exponential law with rate k.choose 2.

theorem tendsto_noCoalProb_pow_floor (k : ℕ) {t : ℝ} (ht : 0 ≤ t) :
    Tendsto (fun M : ℕ => noCoalProb M k ^ ⌊t * M⌋₊) atTop
      (𝓝 (Real.exp (-((k.choose 2 : ℕ) : ℝ) * t)))

Uses 3 · Used by 1

Statement usesProbability of no coalescence in one Wright–Fisher generation

Proof usesKingman's coalescence rate · No-coalescence probability tends to one

Used byWright–Fisher limit of the no-coalescence probability

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.