Baum–Eagon inequality for diploid selection

TheoremMean fitness stays positive under diploid selection#✓fully proved

Mean fitness stays positive after one generation of diploid viability selection (for nonnegative frequencies and fitnesses; normalization is not needed).

theorem diploidMeanFitness_diploidSelect_pos {p : ι → ℝ} {w : ι → ι → ℝ}
    (hp0 : ∀ i, 0 ≤ p i) (hw0 : ∀ i j, 0 ≤ w i j)
    (hpos : 0 < diploidMeanFitness p w) :
    0 < diploidMeanFitness (diploidSelect p w) w

Uses 4 · Used by 2

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

Proof usesMarginal fitness of an allele · Diploid selection preserves total allele frequency one

Used byMean fitness never decreases · Diploid Baum–Eagon mean-fitness inequality, sharp form

TheoremDiploid Baum–Eagon mean-fitness inequality, sharp form#✓fully proved

With nonnegative allele frequencies and genotype fitnesses and positive mean fitness, one generation of selection raises the log mean fitness by at least twice the relative entropy ∑ i, p'_i log (p'_i / p_i) of the new allele frequencies p' from the old ones p (Baum–Eagon's argument for the quadratic form w̄). Alleles absent before selection stay absent (p_i = 0 → p'_i = 0), so the summands with p_i = 0 vanish. The inequality does not need ∑ p = 1; on the simplex its right side is nonnegative (Gibbs' inequality). This is a mean-fitness monotonicity inequality, not Fisher's fundamental theorem: Fisher's theorem concerns the change attributable to selection expressed through additive genetic variance.

theorem two_mul_relEntropy_le_log_diploidMeanFitness_diploidSelect {p : ι → ℝ}
    {w : ι → ι → ℝ} (hp0 : ∀ i, 0 ≤ p i) (hw0 : ∀ i j, 0 ≤ w i j)
    (hpos : 0 < diploidMeanFitness p w) :
    2 * ∑ i, diploidSelect p w i * Real.log (diploidSelect p w i / p i) ≤
      Real.log (diploidMeanFitness (diploidSelect p w) w) -
        Real.log (diploidMeanFitness p w)

Uses 5 · Used by 2

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

Proof usesMean fitness stays positive under diploid selection · Marginal fitness of an allele · Diploid selection preserves total allele frequency one

Used byMean fitness is unchanged exactly at selection equilibria · Mean fitness never decreases

TheoremMean fitness never decreases#✓fully proved

Mean fitness never decreases under diploid multi-allele viability selection with random mating (Mulholland–Smith 1959; Scheuer–Mandel 1959; Kingman 1961).

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

Uses 6 · Used by 1

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

Proof usesMean fitness stays positive under diploid selection · Marginal fitness of an allele · Diploid selection preserves total allele frequency one · Diploid Baum–Eagon mean-fitness inequality, sharp form

Used byDiploid selection strictly increases mean fitness off equilibria

TheoremMean fitness is unchanged exactly at selection equilibria#✓fully proved

Mean fitness is unchanged by one generation of selection exactly when the allele frequencies are at an equilibrium of the selection map.

theorem diploidMeanFitness_diploidSelect_eq_iff {p : ι → ℝ} {w : ι → ι → ℝ}
    (hp0 : ∀ i, 0 ≤ p i) (hp : ∑ i, p i = 1) (hw0 : ∀ i j, 0 ≤ w i j)
    (hpos : 0 < diploidMeanFitness p w) :
    diploidMeanFitness (diploidSelect p w) w = diploidMeanFitness p w ↔
      diploidSelect p w = p

Uses 5 · Used by 1

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

Proof usesMarginal fitness of an allele · Diploid selection preserves total allele frequency one · Diploid Baum–Eagon mean-fitness inequality, sharp form

Used byDiploid selection strictly increases mean fitness off equilibria

TheoremDiploid selection strictly increases mean fitness off equilibria#✓fully proved

Away from equilibria, mean fitness strictly increases under diploid viability selection.

theorem diploidMeanFitness_lt_diploidMeanFitness_diploidSelect {p : ι → ℝ} {w : ι → ι → ℝ}
    (hp0 : ∀ i, 0 ≤ p i) (hp : ∑ i, p i = 1) (hw0 : ∀ i j, 0 ≤ w i j)
    (hpos : 0 < diploidMeanFitness p w) (hne : diploidSelect p w ≠ p) :
    diploidMeanFitness p w < diploidMeanFitness (diploidSelect p w) w

Uses 4

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

Proof usesMean fitness is unchanged exactly at selection equilibria · Mean fitness never decreases

TheoremDerivative of two-allele mean fitness#✓fully proved

For two alleles with frequencies (x, 1 - x), the mean fitness w̄(x) = x² w₀₀ + x (1 - x) (w₀₁ + w₁₀) + (1 - x)² w₁₁ has derivative 2 (m₀ - m₁), twice the difference of the marginal fitnesses. This holds for every real x.

theorem hasDerivAt_diploidMeanFitness_two (w : Fin 2 → Fin 2 → ℝ) (x : ℝ) :
    HasDerivAt (fun y => diploidMeanFitness ![y, 1 - y] w)
      (2 * (marginalFitness ![x, 1 - x] w 0 - marginalFitness ![x, 1 - x] w 1)) x

Uses 2 · Used by 1

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

Used byWright's formula

TheoremWright's formula#✓fully proved

Wright's formula (Wright 1937): for two alleles with frequencies (x, 1 - x), one generation of viability selection changes the frequency of allele 0 by Δx = x (1 - x) (dw̄/dx) / (2 w̄). The identity is algebraic and holds for every real x with w̄(x) ≠ 0; the model domain is x ∈ [0, 1] with nonnegative fitnesses.

theorem diploidSelect_two_sub (w : Fin 2 → Fin 2 → ℝ) (x : ℝ)
    (hw : diploidMeanFitness ![x, 1 - x] w ≠ 0) :
    diploidSelect ![x, 1 - x] w 0 - x =
      x * (1 - x) * deriv (fun y => diploidMeanFitness ![y, 1 - y] w) x /
        (2 * diploidMeanFitness ![x, 1 - x] w)

Uses 4

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

Proof usesDerivative of two-allele mean fitness · Marginal fitness of an allele

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.