Eigen's quasispecies error threshold

DefinitionMaster-sequence vector field of the single-peak quasispecies#✓fully proved

The master-sequence vector field of the single-peak quasispecies without back mutation: x' = σ Q x - (σ x + (1 - x)) x, where σ is the master fitness relative to the mutants and Q the probability of an error-free copy. Meaningful for σ > 1, 0 ≤ Q ≤ 1, 0 ≤ x ≤ 1; it is a polynomial and is defined for all reals.

def masterField (σ Q x : ℝ) : ℝ :=
  σ * Q * x - (σ * x + (1 - x)) * x

Used by 4

Used byMaster-sequence equation is logistic · Equilibria of the master-sequence frequency · Convergence above the threshold · Loss of the master at or below the threshold

DefinitionInterior equilibrium of the master-sequence frequency#✓fully proved

The interior equilibrium x* = (σ Q - 1) / (σ - 1) of the master frequency. For σ = 1 (no selective advantage) Lean's x / 0 = 0 gives the junk value 0; every result below assumes 1 < σ.

noncomputable def masterEquilibrium (σ Q : ℝ) : ℝ :=
  (σ * Q - 1) / (σ - 1)

Used by 8

Used byEigen's error threshold · Interior quasispecies equilibrium is at most 1 · Error threshold · Equilibria of the master-sequence frequency · Mutant frequency at the interior equilibrium · Continuity of the interior equilibrium in the copying fidelity · Fixed-q_L limit · Convergence above the threshold

TheoremMaster-sequence equation is logistic#✓fully proved

The master-sequence equation is logistic: x' = x ((σ Q - 1) - (σ - 1) x).

theorem masterField_eq (σ Q x : ℝ) :
    masterField σ Q x = x * ((σ * Q - 1) - (σ - 1) * x)

Uses 1 · Used by 3

Statement usesMaster-sequence vector field of the single-peak quasispecies

Used byEquilibria of the master-sequence frequency · Convergence above the threshold · Loss of the master at or below the threshold

TheoremEquilibria of the master-sequence frequency#✓fully proved

The equilibria of the master frequency are 0 and x* = (σ Q - 1)/(σ - 1).

theorem masterField_eq_zero_iff {σ Q x : ℝ} (hσ : 1 < σ) :
    masterField σ Q x = 0 ↔ x = 0 ∨ x = masterEquilibrium σ Q

Uses 3

Statement usesInterior equilibrium of the master-sequence frequency · Master-sequence vector field of the single-peak quasispecies

Proof usesMaster-sequence equation is logistic

TheoremMutant frequency at the interior equilibrium#✓fully proved

The mutant frequency at the interior equilibrium is 1 - x* = σ (1 - Q)/(σ - 1).

theorem one_sub_masterEquilibrium {σ : ℝ} (hσ : 1 < σ) (Q : ℝ) :
    1 - masterEquilibrium σ Q = σ * (1 - Q) / (σ - 1)

Uses 1

Statement usesInterior equilibrium of the master-sequence frequency

TheoremError threshold#✓fully proved

For σ > 1, the interior equilibrium is positive iff σ Q > 1.

theorem masterEquilibrium_pos_iff {σ : ℝ} (hσ : 1 < σ) (Q : ℝ) :
    0 < masterEquilibrium σ Q ↔ 1 < σ * Q

Uses 1 · Used by 1

Statement usesInterior equilibrium of the master-sequence frequency

Used byEigen's error threshold

TheoremInterior quasispecies equilibrium is at most 1#✓fully proved

For σ > 1 and Q ≤ 1 the interior equilibrium is at most 1.

theorem masterEquilibrium_le_one {σ Q : ℝ} (hσ : 1 < σ) (hQ : Q ≤ 1) :
    masterEquilibrium σ Q ≤ 1

Uses 1

Statement usesInterior equilibrium of the master-sequence frequency

TheoremMaximal genome length#✓fully proved

For per-site fidelity 0 < q < 1 and σ > 0, σ q ^ L > 1 iff L < log σ / (-log q).

theorem one_lt_mul_pow_iff {σ q : ℝ} (hσ : 0 < σ) (hq0 : 0 < q) (hq1 : q < 1) (L : ℕ) :
    1 < σ * q ^ L ↔ (L : ℝ) < log σ / (-log q)

TheoremContinuity of the interior equilibrium in the copying fidelity#✓fully proved

The interior equilibrium depends continuously on Q, so any sequence of fidelities with Q_L → Qlim has x*(Q_L) → x*(Qlim).

theorem tendsto_masterEquilibrium {σ : ℝ} {Q : ℕ → ℝ} {Qlim : ℝ}
    (hQ : Tendsto Q atTop (𝓝 Qlim)) :
    Tendsto (fun L ↦ masterEquilibrium σ (Q L)) atTop (𝓝 (masterEquilibrium σ Qlim))

Uses 1 · Used by 1

Statement usesInterior equilibrium of the master-sequence frequency

Used byFixed-q_L limit

TheoremFixed-q_L limit#✓fully proved

With per-site fidelity q_L = 1 - μ / L, so that the expected number of mutations per genome copy is μ, the error-free probability is q_L ^ L → e^{-μ} and the master equilibrium converges to (σ e^{-μ} - 1)/(σ - 1).

theorem tendsto_masterEquilibrium_fidelity (σ μ : ℝ) :
    Tendsto (fun L : ℕ ↦ masterEquilibrium σ ((1 - μ / L) ^ L)) atTop
      (𝓝 (masterEquilibrium σ (exp (-μ))))

Uses 2

Statement usesInterior equilibrium of the master-sequence frequency

Proof usesContinuity of the interior equilibrium in the copying fidelity

TheoremEigen's error threshold#✓fully proved

In the fixed-q_L limit the master sequence persists iff μ < log σ.

theorem masterEquilibrium_exp_pos_iff {σ : ℝ} (hσ : 1 < σ) (μ : ℝ) :
    0 < masterEquilibrium σ (exp (-μ)) ↔ μ < log σ

Uses 2

Statement usesInterior equilibrium of the master-sequence frequency

Proof usesError threshold

TheoremConvergence above the threshold#✓fully proved

If σ > 1, σ Q > 1 and x solves the master equation on [0, ∞) from a positive master frequency, then x t → x*.

theorem tendsto_master_of_one_lt {σ Q : ℝ} (hσ : 1 < σ) (hth : 1 < σ * Q) {x : ℝ → ℝ}
    (hx : ∀ t, 0 ≤ t → HasDerivAt x (masterField σ Q (x t)) t) (h0 : 0 < x 0) :
    Tendsto x atTop (𝓝 (masterEquilibrium σ Q))

Uses 3

Statement usesInterior equilibrium of the master-sequence frequency · Master-sequence vector field of the single-peak quasispecies

Proof usesMaster-sequence equation is logistic

TheoremLoss of the master at or below the threshold#✓fully proved

If σ > 1, σ Q ≤ 1 and x solves the master equation on [0, ∞) from a positive master frequency, then x t → 0.

theorem tendsto_master_zero_of_le_one {σ Q : ℝ} (hσ : 1 < σ) (hth : σ * Q ≤ 1) {x : ℝ → ℝ}
    (hx : ∀ t, 0 ≤ t → HasDerivAt x (masterField σ Q (x t)) t) (h0 : 0 < x 0) :
    Tendsto x atTop (𝓝 0)

Uses 2

Statement usesMaster-sequence vector field of the single-peak quasispecies

Proof usesMaster-sequence equation is logistic

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.