Structured coalescent

17 fully proved

Structured Coalescent

InductiveState of two lineages in the island model#✓fully proved

The state of two ancestral lineages in the island model: in the same deme, in different demes, or coalesced (absorbing).

inductive PairState
  /-- Both lineages are in the same deme. -/
  | same
  /-- The lineages are in different demes. -/
  | different
  /-- The lineages have coalesced. -/
  | coalesced
  deriving DecidableEq

Used by 7

Used byExit rate of a structured-coalescent state · First-step equations for mean coalescence time · Mean coalescence times in the finite island model (Strobeck 1987; Slatkin 1991) · Closed-form mean coalescence times in the island model · First-step analysis in jump-chain form · Transition rates of the two-lineage structured coalescent · Sum over the island-model pair states

Pair State

TheoremSum over the island-model pair states#✓fully proved

A sum over the three states.

theorem sum_eq {β : Type*} [AddCommMonoid β] (f : PairState → β) :
    ∑ t, f t = f same + f different + f coalesced

Uses 1 · Used by 2

Statement usesState of two lineages in the island model

Used byMean coalescence times in the finite island model (Strobeck 1987; Slatkin 1991) · First-step analysis in jump-chain form

Structured Coalescent

DefinitionTransition rates of the two-lineage structured coalescent#✓fully proved

The transition rates q(s, t) (s ≠ t) of the two-lineage structured coalescent in the finite island model with d demes and M = 4Nm, time in units of 2N generations: same deme → coalesced at rate 1, same deme → different demes at rate M, different demes → same deme at rate M / (d - 1); all other rates (and the diagonal) are 0. Meaningful for d ≥ 2 and M ≥ 0.

noncomputable def rate (d : ℕ) (M : ℝ) : PairState → PairState → ℝ
  | same, coalesced => 1
  | same, different => M
  | different, same => M / (d - 1)
  | _, _ => 0

Uses 1 · Used by 4

Statement usesState of two lineages in the island model

Used byExit rate of a structured-coalescent state · First-step equations for mean coalescence time · Mean coalescence times in the finite island model (Strobeck 1987; Slatkin 1991) · First-step analysis in jump-chain form

DefinitionExit rate of a structured-coalescent state#✓fully proved

The total rate qₛ = ∑ₜ q(s, t) of leaving the state s.

noncomputable def exitRate (d : ℕ) (M : ℝ) (s : PairState) : ℝ := ∑ t, rate d M s t

Uses 2 · Used by 1

Statement usesState of two lineages in the island model · Transition rates of the two-lineage structured coalescent

Used byFirst-step analysis in jump-chain form

DefinitionFirst-step equations for mean coalescence time#✓fully proved

The first-step (backward Kolmogorov) equations for the mean time to coalescence: h coalesced = 0, and at each transient state s, ∑ₜ q(s, t) (h t - h s) = -1. (The vector of mean absorption times of a finite absorbing continuous-time Markov chain satisfies these equations; this file does not construct the chain.)

def FirstStepEquations (d : ℕ) (M : ℝ) (h : PairState → ℝ) : Prop :=
  h coalesced = 0 ∧ ∀ s, s ≠ coalesced → ∑ t, rate d M s t * (h t - h s) = -1

Uses 2 · Used by 2

Statement usesState of two lineages in the island model · Transition rates of the two-lineage structured coalescent

Used byMean coalescence times in the finite island model (Strobeck 1987; Slatkin 1991) · First-step analysis in jump-chain form

DefinitionMean coalescence time within a deme#✓fully proved

The mean coalescence time T₀ = d of two lineages in the same deme (units of 2N generations).

def withinTime (d : ℕ) : ℝ := d

Used by 4

Used byClosed-form mean coalescence times in the island model · Slatkin's F_ST for the finite island model · Slatkin's F_ST for the finite island model (Slatkin 1991) · Slatkin's mean total coalescence time

DefinitionMean coalescence time between demes#✓fully proved

The mean coalescence time T₁ = d + (d - 1) / M of two lineages in different demes (units of 2N generations). Meaningful for M > 0; betweenTime d 0 = d is a junk value (the true mean is infinite).

noncomputable def betweenTime (d : ℕ) (M : ℝ) : ℝ := d + (d - 1) / M

Used by 3

Used byClosed-form mean coalescence times in the island model · Slatkin's mean total coalescence time · Closed form of Slatkin's mean total coalescence time

DefinitionClosed-form mean coalescence times in the island model#✓fully proved

The closed-form mean time to coalescence from each state: T₀, T₁, and 0 once coalesced. firstStepEquations_iff shows it is the unique solution of the first-step equations.

noncomputable def meanCoalescenceTime (d : ℕ) (M : ℝ) : PairState → ℝ
  | same => withinTime d
  | different => betweenTime d M
  | coalesced => 0

Uses 3 · Used by 2

Statement usesState of two lineages in the island model · Mean coalescence time between demes · Mean coalescence time within a deme

Used byMean coalescence times in the finite island model (Strobeck 1987; Slatkin 1991) · First-step analysis in jump-chain form

TheoremMean coalescence times in the finite island model (Strobeck 1987; Slatkin 1991)#✓fully proved

For d ≥ 2 demes and M = 4Nm > 0, the first-step equations have the unique solution T₀ = d, T₁ = d + (d - 1) / M. In particular T₀ does not depend on the migration rate.

theorem firstStepEquations_iff {d : ℕ} (hd : 2 ≤ d) {M : ℝ} (hM : 0 < M)
    (h : PairState → ℝ) : FirstStepEquations d M h ↔ h = meanCoalescenceTime d M

Uses 5 · Used by 1

Statement usesFirst-step equations for mean coalescence time · State of two lineages in the island model · Closed-form mean coalescence times in the island model

Proof usesSum over the island-model pair states · Transition rates of the two-lineage structured coalescent

Used byFirst-step analysis in jump-chain form

TheoremFirst-step analysis in jump-chain form#✓fully proved

At each transient state s the exit rate is positive and the mean coalescence time is the mean holding time 1 / qₛ plus the mean time from the next state, h s = 1 / qₛ + ∑ₜ (q(s, t) / qₛ) h t.

theorem meanCoalescenceTime_eq_firstStep {d : ℕ} (hd : 2 ≤ d) {M : ℝ} (hM : 0 < M)
    {s : PairState} (hs : s ≠ coalesced) :
    0 < exitRate d M s ∧ meanCoalescenceTime d M s =
      1 / exitRate d M s + ∑ t, rate d M s t / exitRate d M s * meanCoalescenceTime d M t

Uses 7

Statement usesState of two lineages in the island model · Exit rate of a structured-coalescent state · Closed-form mean coalescence times in the island model · Transition rates of the two-lineage structured coalescent

Proof usesFirst-step equations for mean coalescence time · Sum over the island-model pair states · Mean coalescence times in the finite island model (Strobeck 1987; Slatkin 1991)

DefinitionSlatkin's mean total coalescence time#✓fully proved

Slatkin's mean coalescence time T̄ = T₀ / d + (d - 1) T₁ / d of two genes drawn from two demes chosen independently and uniformly at random.

noncomputable def totalTime (d : ℕ) (M : ℝ) : ℝ :=
  withinTime d / d + (d - 1) / d * betweenTime d M

Uses 2 · Used by 4

Statement usesMean coalescence time between demes · Mean coalescence time within a deme

Used bySlatkin's F_ST for the finite island model · Slatkin's F_ST for the finite island model (Slatkin 1991) · Closed form of Slatkin's mean total coalescence time · Positivity of Slatkin's mean total coalescence time

DefinitionSlatkin's F_ST for the finite island model#✓fully proved

Slatkin's (1991) F_ST = (T̄ - T₀) / T̄ for the finite island model.

noncomputable def slatkinFST (d : ℕ) (M : ℝ) : ℝ :=
  (totalTime d M - withinTime d) / totalTime d M

Uses 2 · Used by 3

Statement usesSlatkin's mean total coalescence time · Mean coalescence time within a deme

Used bySlatkin's F_ST for the finite island model (Slatkin 1991) · Slatkin's F_ST lies strictly between 0 and 1 · Many demes (Slatkin 1991)

TheoremClosed form of Slatkin's mean total coalescence time#✓fully proved

T̄ = d + (d - 1)² / (d M) for d ≥ 1.

theorem totalTime_eq {d : ℕ} (hd : 1 ≤ d) (M : ℝ) :
    totalTime d M = d + (d - 1) ^ 2 / (d * M)

Uses 2 · Used by 2

Statement usesSlatkin's mean total coalescence time

Proof usesMean coalescence time between demes

Used bySlatkin's F_ST for the finite island model (Slatkin 1991) · Positivity of Slatkin's mean total coalescence time

TheoremPositivity of Slatkin's mean total coalescence time#✓fully proved

The denominator of Slatkin's F_ST is positive: 0 < T̄ for d ≥ 1 and M > 0.

theorem totalTime_pos {d : ℕ} (hd : 1 ≤ d) {M : ℝ} (hM : 0 < M) : 0 < totalTime d M

Uses 2

Statement usesSlatkin's mean total coalescence time

Proof usesClosed form of Slatkin's mean total coalescence time

TheoremSlatkin's F_ST for the finite island model (Slatkin 1991)#✓fully proved

For d ≥ 2 demes and M = 4Nm > 0, F_ST = 1 / (1 + M d² / (d - 1)²).

theorem slatkinFST_eq {d : ℕ} (hd : 2 ≤ d) {M : ℝ} (hM : 0 < M) :
    slatkinFST d M = 1 / (1 + M * d ^ 2 / (d - 1) ^ 2)

Uses 4 · Used by 2

Statement usesSlatkin's F_ST for the finite island model

Proof usesSlatkin's mean total coalescence time · Closed form of Slatkin's mean total coalescence time · Mean coalescence time within a deme

Used bySlatkin's F_ST lies strictly between 0 and 1 · Many demes (Slatkin 1991)

TheoremSlatkin's F_ST lies strictly between 0 and 1#✓fully proved

Slatkin's F_ST lies in (0, 1) for d ≥ 2 and M > 0.

theorem slatkinFST_mem_Ioo {d : ℕ} (hd : 2 ≤ d) {M : ℝ} (hM : 0 < M) :
    slatkinFST d M ∈ Set.Ioo (0 : ℝ) 1

Uses 2

Statement usesSlatkin's F_ST for the finite island model

Proof usesSlatkin's F_ST for the finite island model (Slatkin 1991)

TheoremMany demes (Slatkin 1991)#✓fully proved

As the number of demes grows, Slatkin's F_ST tends to Wright's 1 / (1 + M) = 1 / (1 + 4Nm) for every M > 0.

theorem tendsto_slatkinFST {M : ℝ} (hM : 0 < M) :
    Tendsto (fun d : ℕ => slatkinFST d M) atTop (𝓝 (1 / (1 + M)))

Uses 2

Statement usesSlatkin's F_ST for the finite island model

Proof usesSlatkin's F_ST for the finite island model (Slatkin 1991)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.