Wright's island model

DefinitionIdentity-by-descent recursion in Wright's island model#✓fully proved

One generation of Wright's island-model identity-by-descent recursion for a deme of M gene copies (M = 2N for N diploids) receiving a fraction m of migrants from an infinite pool: F' = (1 - m) ^ 2 * (1 / M + (1 - 1 / M) * F). Biologically meaningful for M ≥ 2 and 0 ≤ m ≤ 1; M = 1 is an algebraic extension (no pair of distinct copies exists), and at M = 0 Lean's 1 / 0 = 0 gives a junk value.

noncomputable def islandStep (M : ℕ) (m F : ℝ) : ℝ :=
  (1 - m) ^ 2 * (1 / M + (1 - 1 / M) * F)

Used by 4

Used byUniqueness of the island-model fixed point · Island-model equilibrium is a fixed point of the recursion · Geometric approach to equilibrium · Convergence to equilibrium

DefinitionEquilibrium \(F_{ST}\) of Wright's island model#✓fully proved

The equilibrium identity-by-descent probability (Wright's F_ST) of the island model: F* = (1 - m) ^ 2 / (M - (M - 1) (1 - m) ^ 2). Biologically meaningful for M ≥ 2 and 0 ≤ m ≤ 1; the denominator is positive already for M ≥ 1 (islandEquilibrium_denom_pos), where M = 1 is an algebraic extension.

noncomputable def islandEquilibrium (M : ℕ) (m : ℝ) : ℝ :=
  (1 - m) ^ 2 / (M - (M - 1) * (1 - m) ^ 2)

Used by 8

Used byUniqueness of the island-model fixed point · Island-model equilibrium lies in (0, 1) · Island-model equilibrium is below one under migration · Complete identity by descent in isolated demes · Island-model equilibrium is a fixed point of the recursion · Geometric approach to equilibrium · Wright's F_ST = 1 / (1 + 4 N m) (Wright 1931) · Convergence to equilibrium

TheoremIsland-model contraction factor lies in (0, 1)#✓fully proved

For M ≥ 1 and 0 ≤ m ≤ 1, the per-generation contraction factor (1 - m) ^ 2 (1 - 1 / M) lies in [0, 1).

theorem islandFactor_mem_Ico {M : ℕ} (hM : 0 < M) {m : ℝ} (hm : m ∈ Icc (0 : ℝ) 1) :
    (1 - m) ^ 2 * (1 - 1 / M) ∈ Ico (0 : ℝ) 1

Used by 1

Used byConvergence to equilibrium

TheoremPositivity of the island-model equilibrium denominator#✓fully proved

The denominator M - (M - 1) (1 - m) ^ 2 of the equilibrium is positive (at least 1) for M ≥ 1 and 0 ≤ m ≤ 1.

theorem islandEquilibrium_denom_pos {M : ℕ} (hM : 0 < M) {m : ℝ} (hm : m ∈ Icc (0 : ℝ) 1) :
    0 < (M : ℝ) - (M - 1) * (1 - m) ^ 2

Used by 4

Used byUniqueness of the island-model fixed point · Island-model equilibrium lies in (0, 1) · Island-model equilibrium is below one under migration · Island-model equilibrium is a fixed point of the recursion

TheoremIsland-model equilibrium is a fixed point of the recursion#✓fully proved

F* is a fixed point of the island-model recursion.

theorem islandStep_islandEquilibrium {M : ℕ} (hM : 0 < M) {m : ℝ} (hm : m ∈ Icc (0 : ℝ) 1) :
    islandStep M m (islandEquilibrium M m) = islandEquilibrium M m

Uses 3 · Used by 1

Statement usesEquilibrium \(F_{ST}\) of Wright's island model · Identity-by-descent recursion in Wright's island model

Proof usesPositivity of the island-model equilibrium denominator

Used byGeometric approach to equilibrium

TheoremUniqueness of the island-model fixed point#✓fully proved

F* is the only fixed point of the island-model recursion.

theorem eq_islandEquilibrium_of_islandStep_eq {M : ℕ} (hM : 0 < M) {m : ℝ}
    (hm : m ∈ Icc (0 : ℝ) 1) {F : ℝ} (hF : islandStep M m F = F) : F = islandEquilibrium M m

Uses 3

Statement usesEquilibrium \(F_{ST}\) of Wright's island model · Identity-by-descent recursion in Wright's island model

Proof usesPositivity of the island-model equilibrium denominator

TheoremGeometric approach to equilibrium#✓fully proved

After t generations, F_t - F* = ((1 - m) ^ 2 (1 - 1 / M)) ^ t (F_0 - F*).

theorem islandStep_iterate_sub {M : ℕ} (hM : 0 < M) {m : ℝ} (hm : m ∈ Icc (0 : ℝ) 1)
    (F₀ : ℝ) (t : ℕ) :
    (islandStep M m)^[t] F₀ - islandEquilibrium M m =
      ((1 - m) ^ 2 * (1 - 1 / M)) ^ t * (F₀ - islandEquilibrium M m)

Uses 3 · Used by 1

Statement usesEquilibrium \(F_{ST}\) of Wright's island model · Identity-by-descent recursion in Wright's island model

Proof usesIsland-model equilibrium is a fixed point of the recursion

Used byConvergence to equilibrium

TheoremConvergence to equilibrium#✓fully proved

For M ≥ 1 and 0 ≤ m ≤ 1, the island-model recursion converges to F* from every initial value F₀.

theorem tendsto_islandStep_iterate {M : ℕ} (hM : 0 < M) {m : ℝ} (hm : m ∈ Icc (0 : ℝ) 1)
    (F₀ : ℝ) :
    Tendsto (fun t => (islandStep M m)^[t] F₀) atTop (𝓝 (islandEquilibrium M m))

Uses 4

Statement usesEquilibrium \(F_{ST}\) of Wright's island model · Identity-by-descent recursion in Wright's island model

Proof usesIsland-model contraction factor lies in (0, 1) · Geometric approach to equilibrium

TheoremIsland-model equilibrium lies in (0, 1)#✓fully proved

The equilibrium identity-by-descent probability lies in [0, 1].

theorem islandEquilibrium_mem_Icc {M : ℕ} (hM : 0 < M) {m : ℝ} (hm : m ∈ Icc (0 : ℝ) 1) :
    islandEquilibrium M m ∈ Icc (0 : ℝ) 1

Uses 2

Statement usesEquilibrium \(F_{ST}\) of Wright's island model

Proof usesPositivity of the island-model equilibrium denominator

TheoremIsland-model equilibrium is below one under migration#✓fully proved

With migration (0 < m ≤ 1) the equilibrium identity-by-descent probability lies in [0, 1).

theorem islandEquilibrium_mem_Ico {M : ℕ} (hM : 0 < M) {m : ℝ} (hm : m ∈ Ioc (0 : ℝ) 1) :
    islandEquilibrium M m ∈ Ico (0 : ℝ) 1

Uses 2

Statement usesEquilibrium \(F_{ST}\) of Wright's island model

Proof usesPositivity of the island-model equilibrium denominator

TheoremComplete identity by descent in isolated demes#✓fully proved

Isolated demes (m = 0): the equilibrium is complete identity by descent, F* = 1.

@[simp]
theorem islandEquilibrium_zero_right (M : ℕ) : islandEquilibrium M 0 = 1

Uses 1

Statement usesEquilibrium \(F_{ST}\) of Wright's island model

TheoremWright's F_ST = 1 / (1 + 4 N m) (Wright 1931)#✓fully proved

For demes of N diploids (M = 2N gene copies) and migration fraction m = κ / (4N), so that 4 N m = κ is held fixed, the equilibrium F* tends to 1 / (1 + κ) as N → ∞.

theorem tendsto_islandEquilibrium {κ : ℝ} (hκ : 0 ≤ κ) :
    Tendsto (fun N : ℕ => islandEquilibrium (2 * N) (κ / (4 * N))) atTop
      (𝓝 (1 / (1 + κ)))

Uses 1

Statement usesEquilibrium \(F_{ST}\) of Wright's island model

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.