Natural selection, Fisher's theorem and the Price equation

16 fully proved

Haploid selection

DefinitionMean fitness of a population#✓fully proved

The mean fitness w̄ = ∑ i, p i * w i of a population with type frequencies p and fitnesses w.

def meanFitness (p w : ι → ℝ) : ℝ := ∑ i, p i * w i

Used by 7

Used byVariance of fitness · Mean fitness never decreases under haploid selection · Positivity of mean fitness on the simplex · Fisher's fundamental theorem of natural selection · One generation of haploid selection · Haploid selection preserves nonnegative frequencies · Haploid selection preserves total frequency one

DefinitionVariance of fitness#✓fully proved

The variance of fitness Var_p(w) = ∑ i, p i * (w i - w̄) ^ 2 under the type frequencies p.

def fitnessVariance (p w : ι → ℝ) : ℝ := ∑ i, p i * (w i - meanFitness p w) ^ 2

Uses 1 · Used by 2

Statement usesMean fitness of a population

Used byMean fitness never decreases under haploid selection · Fisher's fundamental theorem of natural selection

DefinitionOne generation of haploid selection#✓fully proved

One generation of haploid selection: select p w i = p i * w i / w̄.

noncomputable def select (p w : ι → ℝ) (i : ι) : ℝ := p i * w i / meanFitness p w

Uses 1 · Used by 4

Statement usesMean fitness of a population

Used byMean fitness never decreases under haploid selection · Fisher's fundamental theorem of natural selection · Haploid selection preserves nonnegative frequencies · Haploid selection preserves total frequency one

TheoremFisher's fundamental theorem of natural selection#✓fully proved

Fisher's fundamental theorem of natural selection in its exact haploid, discrete-generation form: the change in mean fitness over one generation of selection is the variance of fitness divided by the mean fitness, w̄(p') - w̄(p) = Var_p(w) / w̄(p) (cf. Fisher 1930, who states the theorem for the additive genetic variance). The identity needs only ∑ p = 1 and w̄ ≠ 0; the model domain is the simplex with w > 0 (meanFitness_pos).

theorem meanFitness_select_sub {p w : ι → ℝ} (hp : ∑ i, p i = 1) (hw : meanFitness p w ≠ 0) :
    meanFitness (select p w) w - meanFitness p w = fitnessVariance p w / meanFitness p w

Uses 3 · Used by 1

Statement usesVariance of fitness · Mean fitness of a population · One generation of haploid selection

Used byMean fitness never decreases under haploid selection

TheoremPositivity of mean fitness on the simplex#✓fully proved

Mean fitness is positive on the simplex when every fitness is positive.

theorem meanFitness_pos {p w : ι → ℝ} (hp0 : ∀ i, 0 ≤ p i) (hp : ∑ i, p i = 1)
    (hw : ∀ i, 0 < w i) : 0 < meanFitness p w

Uses 1 · Used by 2

Statement usesMean fitness of a population

Used byMean fitness never decreases under haploid selection · Haploid selection preserves nonnegative frequencies

TheoremMean fitness never decreases under haploid selection#✓fully proved

Mean fitness never decreases under haploid selection (corollary of Fisher's theorem).

theorem meanFitness_le_meanFitness_select {p w : ι → ℝ} (hp0 : ∀ i, 0 ≤ p i)
    (hp : ∑ i, p i = 1) (hw : ∀ i, 0 < w i) : meanFitness p w ≤ meanFitness (select p w) w

Uses 5

Statement usesMean fitness of a population · One generation of haploid selection

Proof usesVariance of fitness · Positivity of mean fitness on the simplex · Fisher's fundamental theorem of natural selection

TheoremHaploid selection preserves nonnegative frequencies#✓fully proved

Haploid selection keeps frequencies nonnegative.

theorem select_nonneg {p w : ι → ℝ} (hp0 : ∀ i, 0 ≤ p i) (hp : ∑ i, p i = 1)
    (hw : ∀ i, 0 < w i) (i : ι) : 0 ≤ select p w i

Uses 3

Statement usesOne generation of haploid selection

Proof usesMean fitness of a population · Positivity of mean fitness on the simplex

TheoremHaploid selection preserves total frequency one#✓fully proved

Haploid selection keeps the frequencies summing to 1 whenever w̄ ≠ 0 (for w̄ = 0 the division by zero would give 0).

theorem sum_select {p w : ι → ℝ} (hw : meanFitness p w ≠ 0) : ∑ i, select p w i = 1

Uses 2

Statement usesMean fitness of a population · One generation of haploid selection

Diploid viability selection under Hardy–Weinberg proportions

DefinitionMarginal fitness of an allele#✓fully proved

The marginal fitness ∑ j, (w i j + w j i) / 2 * p j of allele i: the mean fitness of a genotype carrying i whose other allele is drawn from the frequencies p, averaging the two positions at which i can sit in the ordered genotype.

noncomputable def marginalFitness (p : ι → ℝ) (w : ι → ι → ℝ) (i : ι) : ℝ :=
  ∑ j, (w i j + w j i) / 2 * p j

Used by 10

Used byMean fitness is unchanged exactly at selection equilibria · Mean fitness stays positive under diploid selection · Mean fitness never decreases · Wright's formula · Derivative of two-allele mean fitness · Diploid Baum–Eagon mean-fitness inequality, sharp form · One generation of diploid viability selection · Diploid selection preserves nonnegative allele frequencies · Marginal fitness for symmetric genotype fitnesses · Diploid selection preserves total allele frequency one

TheoremMarginal fitness for symmetric genotype fitnesses#✓fully proved

For symmetric genotype fitnesses the marginal fitness is the row marginal ∑ j, w i j * p j.

theorem marginalFitness_of_symm {p : ι → ℝ} {w : ι → ι → ℝ} (hw : ∀ i j, w i j = w j i)
    (i : ι) : marginalFitness p w i = ∑ j, w i j * p j

Uses 1

Statement usesMarginal fitness of an allele

DefinitionDiploid mean fitness under Hardy–Weinberg proportions#✓fully proved

The mean fitness w̄ = ∑ i, ∑ j, p i * p j * w i j of a population in Hardy–Weinberg proportions with allele frequencies p and genotype fitnesses w.

def diploidMeanFitness (p : ι → ℝ) (w : ι → ι → ℝ) : ℝ := ∑ i, ∑ j, p i * p j * w i j

Used by 11

Used byMean fitness is unchanged exactly at selection equilibria · Mean fitness stays positive under diploid selection · Mean fitness never decreases · Diploid selection strictly increases mean fitness off equilibria · Wright's formula · Derivative of two-allele mean fitness · Diploid Baum–Eagon mean-fitness inequality, sharp form · Positivity of diploid mean fitness · One generation of diploid viability selection · Diploid selection preserves nonnegative allele frequencies · Diploid selection preserves total allele frequency one

DefinitionOne generation of diploid viability selection#✓fully proved

One generation of diploid viability selection under random mating, followed by Mendelian transmission of either allele of each survivor: diploidSelect p w i = p i * (∑ j, (w i j + w j i) / 2 * p j) / w̄.

noncomputable def diploidSelect (p : ι → ℝ) (w : ι → ι → ℝ) (i : ι) : ℝ :=
  p i * marginalFitness p w i / diploidMeanFitness p w

Uses 2 · Used by 8

Statement usesDiploid mean fitness under Hardy–Weinberg proportions · Marginal fitness of an allele

Used byMean fitness is unchanged exactly at selection equilibria · Mean fitness stays positive under diploid selection · Mean fitness never decreases · Diploid selection strictly increases mean fitness off equilibria · Wright's formula · Diploid Baum–Eagon mean-fitness inequality, sharp form · Diploid selection preserves nonnegative allele frequencies · Diploid selection preserves total allele frequency one

TheoremPositivity of diploid mean fitness#✓fully proved

Diploid mean fitness is positive on the simplex when every genotype fitness is positive.

theorem diploidMeanFitness_pos {p : ι → ℝ} {w : ι → ι → ℝ} (hp0 : ∀ i, 0 ≤ p i)
    (hp : ∑ i, p i = 1) (hw : ∀ i j, 0 < w i j) : 0 < diploidMeanFitness p w

Uses 1 · Used by 1

Statement usesDiploid mean fitness under Hardy–Weinberg proportions

Used byDiploid selection preserves nonnegative allele frequencies

TheoremDiploid selection preserves nonnegative allele frequencies#✓fully proved

Diploid viability selection keeps allele frequencies nonnegative.

theorem diploidSelect_nonneg {p : ι → ℝ} {w : ι → ι → ℝ} (hp0 : ∀ i, 0 ≤ p i)
    (hp : ∑ i, p i = 1) (hw : ∀ i j, 0 < w i j) (i : ι) : 0 ≤ diploidSelect p w i

Uses 4

Statement usesOne generation of diploid viability selection

Proof usesDiploid mean fitness under Hardy–Weinberg proportions · Positivity of diploid mean fitness · Marginal fitness of an allele

TheoremDiploid selection preserves total allele frequency one#✓fully proved

Diploid viability selection keeps allele frequencies summing to 1.

theorem sum_diploidSelect {p : ι → ℝ} {w : ι → ι → ℝ} (hw : diploidMeanFitness p w ≠ 0) :
    ∑ i, diploidSelect p w i = 1

Uses 3 · Used by 4

Statement usesDiploid mean fitness under Hardy–Weinberg proportions · One generation of diploid viability selection

Proof usesMarginal fitness of an allele

Used byMean fitness is unchanged exactly at selection equilibria · Mean fitness stays positive under diploid selection · Mean fitness never decreases · Diploid Baum–Eagon mean-fitness inequality, sharp form

The Price equation

TheoremPrice equation#✓fully proved

The Price equation (exact, finite population). Individual i has fitness w i (number of offspring), trait value z i, and mean offspring trait value z' i. With population means w̄ = 𝔼 i, w i, z̄ = 𝔼 i, z i and offspring mean trait z̄' = ∑ i, w i * z' i / ∑ i, w i, w̄ (z̄' - z̄) = Cov(w, z) + E[w (z' - z)], where Cov is the population covariance (Price 1970). Nonnegativity of w is not needed; only a nonzero total offspring number.

theorem price (w z z' : ι → ℝ) (hw : ∑ i, w i ≠ 0) :
    (𝔼 i, w i) * ((∑ i, w i * z' i) / ∑ i, w i - 𝔼 i, z i) =
      (𝔼 i, (w i - 𝔼 j, w j) * (z i - 𝔼 j, z j)) + 𝔼 i, w i * (z' i - z i)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.