Moran model

DefinitionUp-step probability of the Moran process#✓fully proved

Probability that one step of the Moran process with N individuals and mutant relative fitness r takes the mutant count from i to i + 1: a mutant is chosen to reproduce (probability r i / (r i + N - i)) and a wild type is chosen to die (probability (N - i) / N). Meaningful for 0 < r and i ≤ N (the real subtraction N - i is negative for i > N).

noncomputable def moranUp (r : ℝ) (N i : ℕ) : ℝ :=
  r * i / (r * i + (N - i)) * ((N - i) / N)

Used by 11

Used byUniqueness of the fixation probability · First-step equation (Moran 1958) · Moran process as a stochastic matrix · One-step transition probabilities of the Moran process · Moran up- and down-step probabilities sum to at most one · No up-step from the fixed state of the Moran process · Nonnegativity of the Moran up-step probability · Ratio of Moran down- and up-step probabilities · One-step expectation under the Moran process · Fixation probability of the chain · Loss probability of the chain

DefinitionDown-step probability of the Moran process#✓fully proved

Probability that one step of the Moran process takes the mutant count from i to i - 1: a wild type is chosen to reproduce (probability (N - i) / (r i + N - i)) and a mutant is chosen to die (probability i / N). Meaningful for 0 < r and i ≤ N.

noncomputable def moranDown (r : ℝ) (N i : ℕ) : ℝ :=
  (N - i) / (r * i + (N - i)) * (i / N)

Used by 11

Used byUniqueness of the fixation probability · Nonnegativity of the Moran down-step probability · No down-step from the empty state of the Moran process · First-step equation (Moran 1958) · Moran process as a stochastic matrix · One-step transition probabilities of the Moran process · Moran up- and down-step probabilities sum to at most one · Ratio of Moran down- and up-step probabilities · One-step expectation under the Moran process · Fixation probability of the chain · Loss probability of the chain

DefinitionFixation probability of the Moran process#✓fully proved

The fixation probability of the Moran process started from i mutants out of N: (1 - r⁻¹ ^ i) / (1 - r⁻¹ ^ N) for r ≠ 1, and i / N in the neutral case r = 1. The model's domain is 0 < r, N ≥ 1, i ≤ N; outside it the value is the closed formula evaluated with Lean's total division (e.g. x / 0 = 0) and carries no meaning.

noncomputable def moranFixation (r : ℝ) (N i : ℕ) : ℝ :=
  if r = 1 then i / N else (1 - r⁻¹ ^ i) / (1 - r⁻¹ ^ N)

Used by 7

Used byUniqueness of the fixation probability · First-step equation (Moran 1958) · A fixed mutant stays fixed · An absent mutant is never fixed · Fixation probability of the chain · Loss probability of the chain · Diffusion limit of the Moran fixation probability

DefinitionOne-step transition probabilities of the Moran process#✓fully proved

One-step transition probabilities of the Moran process on the states Fin (N + 1): a_i to i + 1, b_i to i - 1, 1 - a_i - b_i to i, and 0 elsewhere.

noncomputable def moranProb (r : ℝ) (N : ℕ) (i j : Fin (N + 1)) : ℝ :=
  if (j : ℕ) = i + 1 then moranUp r N i
  else if (j : ℕ) + 1 = i then moranDown r N i
  else if j = i then 1 - moranUp r N i - moranDown r N i
  else 0

Uses 2 · Used by 4

Statement usesDown-step probability of the Moran process · Up-step probability of the Moran process

Used byMoran process as a stochastic matrix · One-step expectation under the Moran process · Fixation probability of the chain · Loss probability of the chain

TheoremNo up-step from the fixed state of the Moran process#✓fully proved

No mutant can be added when the mutant type is fixed.

@[simp]
theorem moranUp_last (r : ℝ) (N : ℕ) : moranUp r N N = 0

Uses 1 · Used by 3

Statement usesUp-step probability of the Moran process

Used byOne-step expectation under the Moran process · Fixation probability of the chain · Loss probability of the chain

TheoremNo down-step from the empty state of the Moran process#✓fully proved

No mutant can be removed when the mutant type is absent.

@[simp]
theorem moranDown_zero (r : ℝ) (N : ℕ) : moranDown r N 0 = 0

Uses 1 · Used by 3

Statement usesDown-step probability of the Moran process

Used byOne-step expectation under the Moran process · Fixation probability of the chain · Loss probability of the chain

TheoremRatio of Moran down- and up-step probabilities#✓fully proved

The ratio of the down- and up-step probabilities is 1 / r: r · b_i = a_i.

theorem mul_moranDown (r : ℝ) (N i : ℕ) : r * moranDown r N i = moranUp r N i

Uses 2 · Used by 2

Statement usesDown-step probability of the Moran process · Up-step probability of the Moran process

Used byUniqueness of the fixation probability · First-step equation (Moran 1958)

TheoremNonnegativity of the Moran up-step probability#✓fully proved

The up-step probability is nonnegative on the states 0 ≤ i ≤ N.

theorem moranUp_nonneg {r : ℝ} (hr : 0 < r) {N i : ℕ} (hi : i ≤ N) : 0 ≤ moranUp r N i

Uses 1 · Used by 1

Statement usesUp-step probability of the Moran process

Used byMoran process as a stochastic matrix

TheoremNonnegativity of the Moran down-step probability#✓fully proved

The down-step probability is nonnegative on the states 0 ≤ i ≤ N.

theorem moranDown_nonneg {r : ℝ} (hr : 0 < r) {N i : ℕ} (hi : i ≤ N) :
    0 ≤ moranDown r N i

Uses 1 · Used by 1

Statement usesDown-step probability of the Moran process

Used byMoran process as a stochastic matrix

TheoremMoran up- and down-step probabilities sum to at most one#✓fully proved

On the states 0 ≤ i ≤ N the up- and down-step probabilities sum to at most 1, so the probability 1 - a_i - b_i of staying is nonnegative.

theorem moranUp_add_moranDown_le_one {r : ℝ} (hr : 0 < r) {N i : ℕ} (hi : i ≤ N) :
    moranUp r N i + moranDown r N i ≤ 1

Uses 2 · Used by 1

Statement usesDown-step probability of the Moran process · Up-step probability of the Moran process

Used byMoran process as a stochastic matrix

TheoremOne-step expectation under the Moran process#✓fully proved

One-step expectation of a function f of the mutant count from state i: ∑ j, P i j f j = a_i f (i + 1) + b_i f (i - 1) + (1 - a_i - b_i) f i (the boundary terms vanish at i = 0 and i = N).

theorem sum_moranProb_mul (r : ℝ) (N : ℕ) (i : Fin (N + 1)) (f : ℕ → ℝ) :
    ∑ j, moranProb r N i j * f j = moranUp r N i * f (i + 1) + moranDown r N i * f (i - 1)
      + (1 - moranUp r N i - moranDown r N i) * f i

Uses 5 · Used by 3

Statement usesDown-step probability of the Moran process · One-step transition probabilities of the Moran process · Up-step probability of the Moran process

Proof usesNo down-step from the empty state of the Moran process · No up-step from the fixed state of the Moran process

Used byMoran process as a stochastic matrix · Fixation probability of the chain · Loss probability of the chain

DefinitionMoran process as a stochastic matrix#✓fully proved

The Moran process with N individuals and mutant relative fitness r > 0, as a stochastic matrix on the mutant counts Fin (N + 1).

noncomputable def moranMatrix (N : ℕ) {r : ℝ} (hr : 0 < r) : StochasticMatrix N where
  prob := moranProb r N
  nonneg i j := by
    have hi : (i : ℕ) ≤ N := Nat.lt_succ_iff.1 i.2
    unfold moranProb
    split_ifs
    · exact moranUp_nonneg hr hi
    · exact moranDown_nonneg hr hi
    · linarith [moranUp_add_moranDown_le_one hr hi]
    · exact le_rfl
  row_sum i := by
    simpa using sum_moranProb_mul r N i (fun _ => 1)

Uses 8 · Used by 2

Statement usesDown-step probability of the Moran process · Nonnegativity of the Moran down-step probability · One-step transition probabilities of the Moran process · Up-step probability of the Moran process · Moran up- and down-step probabilities sum to at most one · Nonnegativity of the Moran up-step probability · One-step expectation under the Moran process · Stochastic matrix

Used byFixation probability of the chain · Loss probability of the chain

TheoremAn absent mutant is never fixed#✓fully proved

A mutant that is absent is never fixed: φ_0 = 0.

@[simp]
theorem moranFixation_zero (r : ℝ) (N : ℕ) : moranFixation r N 0 = 0

Uses 1 · Used by 1

Statement usesFixation probability of the Moran process

Used byUniqueness of the fixation probability

TheoremA fixed mutant stays fixed#✓fully proved

A mutant that is already fixed stays fixed: φ_N = 1 (for N ≠ 0).

theorem moranFixation_self {r : ℝ} (hr : 0 < r) {N : ℕ} (hN : N ≠ 0) :
    moranFixation r N N = 1

Uses 1 · Used by 1

Statement usesFixation probability of the Moran process

Used byUniqueness of the fixation probability

TheoremFirst-step equation (Moran 1958)#✓fully proved

The fixation probability satisfies φ_i = a_i φ_{i+1} + b_i φ_{i-1} + (1 - a_i - b_i) φ_i. This is the first-step equation of the chain for the interior states 0 < i < N; the identity is algebraic (it follows from r · b_i = a_i), so it is stated for every i ≥ 1.

theorem moranFixation_eq_firstStep {r : ℝ} (hr : 0 < r) {N i : ℕ} (hi0 : 0 < i) :
    moranFixation r N i = moranUp r N i * moranFixation r N (i + 1)
      + moranDown r N i * moranFixation r N (i - 1)
      + (1 - moranUp r N i - moranDown r N i) * moranFixation r N i

Uses 4 · Used by 1

Statement usesDown-step probability of the Moran process · Fixation probability of the Moran process · Up-step probability of the Moran process

Proof usesRatio of Moran down- and up-step probabilities

Used byUniqueness of the fixation probability

TheoremUniqueness of the fixation probability#✓fully proved

Any ψ with ψ 0 = 0, ψ N = 1 that satisfies the first-step equation ψ i = a_i ψ (i+1) + b_i ψ (i-1) + (1 - a_i - b_i) ψ i at every 0 < i < N equals moranFixation r N on 0 ≤ i ≤ N.

theorem eq_moranFixation {r : ℝ} (hr : 0 < r) {N : ℕ} (hN : N ≠ 0) {ψ : ℕ → ℝ}
    (h0 : ψ 0 = 0) (hN1 : ψ N = 1)
    (hψ : ∀ i, 0 < i → i < N → ψ i = moranUp r N i * ψ (i + 1) + moranDown r N i * ψ (i - 1)
      + (1 - moranUp r N i - moranDown r N i) * ψ i) :
    ∀ i ≤ N, ψ i = moranFixation r N i

Uses 7 · Used by 2

Statement usesDown-step probability of the Moran process · Fixation probability of the Moran process · Up-step probability of the Moran process

Proof usesFirst-step equation (Moran 1958) · A fixed mutant stays fixed · An absent mutant is never fixed · Ratio of Moran down- and up-step probabilities

Used byFixation probability of the chain · Loss probability of the chain

TheoremFixation probability of the chain#✓fully proved

For N ≠ 0, the probability that the Moran chain started at i is in state N after t steps tends to φ_i as t → ∞. Since N absorbs, this t-step probability is the probability of fixation by time t, so its limit is the probability of eventual fixation.

theorem tendsto_matPow_moranMatrix_last {r : ℝ} (hr : 0 < r) {N : ℕ} (hN : N ≠ 0)
    (i : Fin (N + 1)) :
    Tendsto (fun t => (moranMatrix N hr).matPow t i (Fin.last N)) atTop
      (𝓝 (moranFixation r N i))

Uses 13

Statement usesFixation probability of the Moran process · Moran process as a stochastic matrix · Matrix powers of a stochastic matrix

Proof usesUniqueness of the fixation probability · Down-step probability of the Moran process · No down-step from the empty state of the Moran process · One-step transition probabilities of the Moran process · Up-step probability of the Moran process · No up-step from the fixed state of the Moran process · One-step expectation under the Moran process · Stochastic matrix · Powers of a stochastic matrix are nonnegative · Powers of a stochastic matrix are stochastic

TheoremLoss probability of the chain#✓fully proved

For N ≠ 0, the probability that the Moran chain started at i is in state 0 after t steps tends to 1 - φ_i; together with tendsto_matPow_moranMatrix_last, absorption at 0 or N is certain.

theorem tendsto_matPow_moranMatrix_zero {r : ℝ} (hr : 0 < r) {N : ℕ} (hN : N ≠ 0)
    (i : Fin (N + 1)) :
    Tendsto (fun t => (moranMatrix N hr).matPow t i 0) atTop
      (𝓝 (1 - moranFixation r N i))

Uses 13

Statement usesFixation probability of the Moran process · Moran process as a stochastic matrix · Matrix powers of a stochastic matrix

Proof usesUniqueness of the fixation probability · Down-step probability of the Moran process · No down-step from the empty state of the Moran process · One-step transition probabilities of the Moran process · Up-step probability of the Moran process · No up-step from the fixed state of the Moran process · One-step expectation under the Moran process · Stochastic matrix · Powers of a stochastic matrix are nonnegative · Powers of a stochastic matrix are stochastic

TheoremClosed form of Kimura's fixation probability#✓fully proved

Kimura's diffusion fixation probability at scaled selection σ / 2 is (1 - e^{-σ x}) / (1 - e^{-σ}) (for σ ≠ 0).

theorem kimuraFixation_half {σ : ℝ} (hσ : σ ≠ 0) (x : ℝ) :
    kimuraFixation (σ / 2) x = (1 - exp (-σ * x)) / (1 - exp (-σ))

Uses 1 · Used by 1

Statement usesKimura's fixation probability

Used byDiffusion limit of the Moran fixation probability

TheoremDiffusion limit of the Moran fixation probability#✓fully proved

With relative fitness r_N = 1 + σ / N and initial count i_N = ⌊x N⌋, the fixation probability φ^{(N)}_{i_N} tends to Kimura's kimuraFixation (σ / 2) x, which is (1 - e^{-σ x}) / (1 - e^{-σ}) for σ ≠ 0 (kimuraFixation_half) and x for σ = 0. The initial frequency x is meaningful in [0, 1]; the limit of the closed formula holds for every x ≥ 0, so only 0 ≤ x is assumed (for negative x, ⌊x N⌋₊ = 0 is a junk value of the truncated floor).

theorem tendsto_moranFixation_diffusion (σ : ℝ) {x : ℝ} (hx : 0 ≤ x) :
    Tendsto (fun N : ℕ => moranFixation (1 + σ / N) N ⌊x * N⌋₊) atTop
      (𝓝 (kimuraFixation (σ / 2) x))

Uses 3

Statement usesKimura's fixation probability · Fixation probability of the Moran process

Proof usesClosed form of Kimura's fixation probability

20 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.