Mutation–selection balance

26 fully proved

The linear recursion

DefinitionLinear mutation–selection recursion#✓fully proved

One generation of the linear model: x ↦ (1 - s) x + U.

def linStep (s U x : ℝ) : ℝ := (1 - s) * x + U

Used by 12

Used byFraction of de novo loss-of-function alleles · At equilibrium the de novo fraction is s_het · Binomial transition kernel for loss-of-function counts · Transition kernel entries are probabilities · Unique fixed point \(U/s\) of the linear recursion · Closed-form orbit of the linear mutation–selection recursion · Demography-free mean · Demography-free mean, one step · Rows of the transition kernel have total mass one · Binomial mean of the transition kernel · Global attraction · Expected loss-of-function frequency converges to \(U/s\)

TheoremClosed-form orbit of the linear mutation–selection recursion#✓fully proved

Closed-form orbit: x_t = U / s + (1 - s)^t (x_0 - U / s).

theorem linStep_iterate {s : ℝ} (hs : s ≠ 0) (U x : ℝ) (t : ℕ) :
    (linStep s U)^[t] x = U / s + (1 - s) ^ t * (x - U / s)

Uses 1 · Used by 1

Statement usesLinear mutation–selection recursion

Used byGlobal attraction

TheoremUnique fixed point \(U/s\) of the linear recursion#✓fully proved

U / s is the unique fixed point.

theorem linStep_eq_self_iff {s : ℝ} (hs : s ≠ 0) (U x : ℝ) :
    linStep s U x = x ↔ x = U / s

Uses 1 · Used by 1

Statement usesLinear mutation–selection recursion

Used byAt equilibrium the de novo fraction is s_het

TheoremGlobal attraction#✓fully proved

For 0 < s < 2 every orbit converges to U / s.

theorem tendsto_linStep_iterate {s : ℝ} (hs0 : 0 < s) (hs2 : s < 2) (U x : ℝ) :
    Tendsto (fun t => (linStep s U)^[t] x) atTop (𝓝 (U / s))

Uses 2 · Used by 1

Statement usesLinear mutation–selection recursion

Proof usesClosed-form orbit of the linear mutation–selection recursion

Used byExpected loss-of-function frequency converges to \(U/s\)

DefinitionFraction of de novo loss-of-function alleles#✓fully proved

The fraction of LoF alleles in the next generation that are new mutations, from frequency x: U / ((1 - s) x + U).

noncomputable def deNovoFraction (s U x : ℝ) : ℝ := U / linStep s U x

Uses 1 · Used by 1

Statement usesLinear mutation–selection recursion

Used byAt equilibrium the de novo fraction is s_het

TheoremAt equilibrium the de novo fraction is s_het#✓fully proved

At equilibrium the de novo fraction is s_het.

theorem deNovoFraction_eq {s U : ℝ} (hs : s ≠ 0) (hU : U ≠ 0) :
    deNovoFraction s U (U / s) = s

Uses 3

Statement usesFraction of de novo loss-of-function alleles

Proof usesLinear mutation–selection recursion · Unique fixed point \(U/s\) of the linear recursion

The linear Wright–Fisher chain with arbitrary population sizes

DefinitionBinomial transition kernel for loss-of-function counts#✓fully proved

The transition probability from i LoF copies among N to j copies among N': binomial sampling of N' copies with success probability (1 - s)(i / N) + U.

noncomputable def kernel (s U : ℝ) (N N' : ℕ) (i : Fin (N + 1)) (j : Fin (N' + 1)) : ℝ :=
  (bernsteinPolynomial ℝ N' j).eval (linStep s U ((i : ℕ) / N))

Uses 1 · Used by 6

Statement usesLinear mutation–selection recursion

Used byTransition kernel entries are probabilities · Demography-free mean, one step · One generation of the chain on distributions · Rows of the transition kernel have total mass one · Binomial mean of the transition kernel · Pushing a distribution forward preserves total mass

DefinitionMean loss-of-function frequency of a distribution#✓fully proved

The mean LoF frequency ∑ μ_i (i / N) of a distribution μ on Fin (N + 1).

noncomputable def meanFreq (N : ℕ) (μ : Fin (N + 1) → ℝ) : ℝ := ∑ i, μ i * ((i : ℕ) / N)

Used by 3

Used byDemography-free mean · Demography-free mean, one step · Expected loss-of-function frequency converges to \(U/s\)

DefinitionOne generation of the chain on distributions#✓fully proved

One generation of the chain acting on distributions.

noncomputable def pushStep (s U : ℝ) (N N' : ℕ) (μ : Fin (N + 1) → ℝ) : Fin (N' + 1) → ℝ :=
  fun j => ∑ i, μ i * kernel s U N N' i j

Uses 1 · Used by 3

Statement usesBinomial transition kernel for loss-of-function counts

Used byLaw of the loss-of-function count under any demography · Demography-free mean, one step · Pushing a distribution forward preserves total mass

TheoremRows of the transition kernel have total mass one#✓fully proved

The kernel rows have total mass one (for every real sampling probability).

theorem sum_kernel (s U : ℝ) (N N' : ℕ) (i : Fin (N + 1)) : ∑ j, kernel s U N N' i j = 1

Uses 2 · Used by 1

Statement usesBinomial transition kernel for loss-of-function counts

Proof usesLinear mutation–selection recursion

Used byPushing a distribution forward preserves total mass

TheoremTransition kernel entries are probabilities#✓fully proved

The kernel entries are probabilities when the sampling probability is in [0, 1].

theorem kernel_nonneg {s U : ℝ} {N N' : ℕ} {i : Fin (N + 1)}
    (h0 : 0 ≤ linStep s U ((i : ℕ) / N)) (h1 : linStep s U ((i : ℕ) / N) ≤ 1)
    (j : Fin (N' + 1)) : 0 ≤ kernel s U N N' i j

Uses 2

Statement usesBinomial transition kernel for loss-of-function counts · Linear mutation–selection recursion

TheoremBinomial mean of the transition kernel#✓fully proved

The binomial mean: ∑_j kernel(i, j) (j / N') = (1 - s)(i / N) + U for N' > 0.

theorem sum_kernel_mul (s U : ℝ) (N : ℕ) {N' : ℕ} (hN' : 0 < N') (i : Fin (N + 1)) :
    ∑ j, kernel s U N N' i j * ((j : ℕ) / N') = linStep s U ((i : ℕ) / N)

Uses 2 · Used by 1

Statement usesBinomial transition kernel for loss-of-function counts · Linear mutation–selection recursion

Used byDemography-free mean, one step

TheoremDemography-free mean, one step#✓fully proved

For any sizes N, N' > 0 and any distribution μ of total mass one, the mean frequency after one generation is (1 - s) m + U.

theorem meanFreq_pushStep (s U : ℝ) (N : ℕ) {N' : ℕ} (hN' : 0 < N') {μ : Fin (N + 1) → ℝ}
    (hμ : ∑ i, μ i = 1) : meanFreq N' (pushStep s U N N' μ) = linStep s U (meanFreq N μ)

Uses 5 · Used by 1

Statement usesLinear mutation–selection recursion · Mean loss-of-function frequency of a distribution · One generation of the chain on distributions

Proof usesBinomial transition kernel for loss-of-function counts · Binomial mean of the transition kernel

Used byDemography-free mean

TheoremPushing a distribution forward preserves total mass#✓fully proved

Pushing a distribution forward preserves total mass.

theorem sum_pushStep (s U : ℝ) (N N' : ℕ) {μ : Fin (N + 1) → ℝ} (hμ : ∑ i, μ i = 1) :
    ∑ j, pushStep s U N N' μ j = 1

Uses 3 · Used by 1

Statement usesOne generation of the chain on distributions

Proof usesBinomial transition kernel for loss-of-function counts · Rows of the transition kernel have total mass one

Used byDemography-free mean

DefinitionLaw of the loss-of-function count under any demography#✓fully proved

The law of the LoF count in generation t for population sizes N t (any demography), started from μ₀.

noncomputable def law (s U : ℝ) (N : ℕ → ℕ) (μ₀ : Fin (N 0 + 1) → ℝ) :
    (t : ℕ) → Fin (N t + 1) → ℝ
  | 0 => μ₀
  | t + 1 => pushStep s U (N t) (N (t + 1)) (law s U N μ₀ t)

Uses 1 · Used by 2

Statement usesOne generation of the chain on distributions

Used byDemography-free mean · Expected loss-of-function frequency converges to \(U/s\)

TheoremDemography-free mean#✓fully proved

For every sequence of positive population sizes, E[X_t] follows the deterministic linear recursion (derived from the binomial mean). The identity holds for all real s, U; law is a probability law when 0 ≤ U ≤ s ≤ 1 and μ₀ is one.

theorem meanFreq_law (s U : ℝ) {N : ℕ → ℕ} (hN : ∀ t, 0 < N t) {μ₀ : Fin (N 0 + 1) → ℝ}
    (hμ₀ : ∑ i, μ₀ i = 1) (t : ℕ) :
    meanFreq (N t) (law s U N μ₀ t) = (linStep s U)^[t] (meanFreq (N 0) μ₀)

Uses 5 · Used by 1

Statement usesLaw of the loss-of-function count under any demography · Linear mutation–selection recursion · Mean loss-of-function frequency of a distribution

Proof usesDemography-free mean, one step · Pushing a distribution forward preserves total mass

Used byExpected loss-of-function frequency converges to \(U/s\)

TheoremExpected loss-of-function frequency converges to \(U/s\)#✓fully proved

The expected LoF frequency converges to U / s under any demography.

theorem tendsto_meanFreq_law {s : ℝ} (hs0 : 0 < s) (hs2 : s < 2) (U : ℝ) {N : ℕ → ℕ}
    (hN : ∀ t, 0 < N t) {μ₀ : Fin (N 0 + 1) → ℝ} (hμ₀ : ∑ i, μ₀ i = 1) :
    Tendsto (fun t => meanFreq (N t) (law s U N μ₀ t)) atTop (𝓝 (U / s))

Uses 5

Statement usesLaw of the loss-of-function count under any demography · Mean loss-of-function frequency of a distribution

Proof usesLinear mutation–selection recursion · Demography-free mean · Global attraction

The diploid model

DefinitionMean fitness under Hardy–Weinberg proportions#✓fully proved

Mean fitness under Hardy–Weinberg with LoF frequency q and fitnesses 1, 1 - s, 1 - t: 1 - 2 q (1 - q) s - q² t.

def meanFitness (s t q : ℝ) : ℝ := 1 - 2 * q * (1 - q) * s - q ^ 2 * t

Used by 7

Used byU / s is an equilibrium · Equilibria lie at or below U / s · Haldane–Muller load · Mean fitness under multiplicative fitness · Mean fitness at the multiplicative mutation–selection equilibrium · Positivity of mean fitness for allele frequencies below one · Loss-of-function frequency after selection

DefinitionLoss-of-function frequency after selection#✓fully proved

LoF frequency after selection: q (1 - s (1 - q) - t q) / w̄.

noncomputable def selected (s t q : ℝ) : ℝ := q * (1 - s * (1 - q) - t * q) / meanFitness s t q

Uses 1 · Used by 3

Statement usesMean fitness under Hardy–Weinberg proportions

Used byOne diploid generation of selection and mutation · U / s is an equilibrium · Equilibria lie at or below U / s

DefinitionOne diploid generation of selection and mutation#✓fully proved

One generation: selection, then mutation of wild-type alleles at rate U.

noncomputable def diploidStep (s t U q : ℝ) : ℝ := (1 - U) * selected s t q + U

Uses 1 · Used by 2

Statement usesLoss-of-function frequency after selection

Used byU / s is an equilibrium · Equilibria lie at or below U / s

TheoremMean fitness under multiplicative fitness#✓fully proved

With multiplicative fitness, w̄ = (1 - s q)² for every q.

theorem meanFitness_mult (s q : ℝ) : meanFitness s (2 * s - s ^ 2) q = (1 - s * q) ^ 2

Uses 1 · Used by 2

Statement usesMean fitness under Hardy–Weinberg proportions

Used byU / s is an equilibrium · Mean fitness at the multiplicative mutation–selection equilibrium

TheoremU / s is an equilibrium#✓fully proved

U / s is an equilibrium of the multiplicative diploid model (an algebraic identity for s ≠ 0, U ≠ 1; a frequency in [0, 1] when 0 ≤ U ≤ s).

theorem diploidStep_mult_fixed {s U : ℝ} (hs : s ≠ 0) (hU : U ≠ 1) :
    diploidStep s (2 * s - s ^ 2) U (U / s) = U / s

Uses 4

Statement usesOne diploid generation of selection and mutation

Proof usesMean fitness under Hardy–Weinberg proportions · Mean fitness under multiplicative fitness · Loss-of-function frequency after selection

TheoremMean fitness at the multiplicative mutation–selection equilibrium#✓fully proved

At the multiplicative equilibrium the mean fitness is (1 - U)², independent of s. Requires U ≠ 1, so that U / s is genuinely a fixed point (diploidStep_mult_fixed): for U = 1 the point U / s is not an equilibrium.

theorem meanFitness_mult_at_equilibrium {s U : ℝ} (hs : s ≠ 0) (hU : U ≠ 1) :
    meanFitness s (2 * s - s ^ 2) (U / s) = (1 - U) ^ 2

Uses 2 · Used by 1

Statement usesMean fitness under Hardy–Weinberg proportions

Proof usesMean fitness under multiplicative fitness

Used byHaldane–Muller load

TheoremHaldane–Muller load#✓fully proved

1 - w̄ = 2U - U² at the multiplicative equilibrium (U ≠ 1, so U / s is a fixed point).

theorem load_mult_at_equilibrium {s U : ℝ} (hs : s ≠ 0) (hU : U ≠ 1) :
    1 - meanFitness s (2 * s - s ^ 2) (U / s) = 2 * U - U ^ 2

Uses 2

Statement usesMean fitness under Hardy–Weinberg proportions

Proof usesMean fitness at the multiplicative mutation–selection equilibrium

TheoremPositivity of mean fitness for allele frequencies below one#✓fully proved

Mean fitness is positive for 0 ≤ q < 1 and s, t ≤ 1 (nonnegative fitnesses).

theorem meanFitness_pos {s t q : ℝ} (hs : s ≤ 1) (ht : t ≤ 1) (hq0 : 0 ≤ q) (hq1 : q < 1) :
    0 < meanFitness s t q

Uses 1 · Used by 1

Statement usesMean fitness under Hardy–Weinberg proportions

Used byEquilibria lie at or below U / s

TheoremEquilibria lie at or below U / s#✓fully proved

Equilibria lie at or below U / s when homozygotes are at least multiplicatively unfit (2s - s² ≤ t, which includes recessive lethality t = 1): every fixed point q ∈ [0, 1) of the diploid map satisfies q ≤ U / s.

theorem le_div_of_diploidStep_eq {s t U q : ℝ} (hs0 : 0 < s) (hs1 : s ≤ 1) (ht : t ≤ 1)
    (hst : 2 * s - s ^ 2 ≤ t) (hq0 : 0 ≤ q) (hq1 : q < 1) (hfix : diploidStep s t U q = q) :
    q ≤ U / s

Uses 4

Statement usesOne diploid generation of selection and mutation

Proof usesMean fitness under Hardy–Weinberg proportions · Positivity of mean fitness for allele frequencies below one · Loss-of-function frequency after selection

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.