Infinite-alleles model and homozygosity

DefinitionHomozygosity recursion in the infinite-alleles model#✓fully proved

One generation of drift and mutation in the infinite-alleles model with M gene copies and mutation probability u per copy: F' = (1 - u)² (1/M + (1 - 1/M) F). The model domain is 2 ≤ M (two distinct copies must exist) and 0 ≤ u ≤ 1; the theorems below assume only 1 ≤ M, and M = 1 is an algebraic extension with no biological meaning. For M = 0 the definition uses the junk value 1/0 = 0.

noncomputable def homozygosityStep (M : ℕ) (u F : ℝ) : ℝ :=
  (1 - u) ^ 2 * (1 / M + (1 - 1 / M) * F)

Used by 3

Used byEquilibrium homozygosity is a fixed point of the recursion · Uniqueness of the equilibrium homozygosity · Convergence of homozygosity to equilibrium

DefinitionEquilibrium homozygosity in the infinite-alleles model#✓fully proved

The equilibrium homozygosity F* = (1 - u)² / (M - (M - 1)(1 - u)²). Biologically meaningful for 2 ≤ M; its denominator is positive for 1 ≤ M and 0 < u ≤ 1, the hypotheses of the theorems below (M = 1 being an algebraic extension).

noncomputable def eqHomozygosity (M : ℕ) (u : ℝ) : ℝ :=
  (1 - u) ^ 2 / (M - (M - 1) * (1 - u) ^ 2)

Used by 5

Used byEquilibrium homozygosity is a fixed point of the recursion · Uniqueness of the equilibrium homozygosity · Kimura–Crow limit · Convergence of homozygosity to equilibrium · Limit \(\theta/(1+\theta)\) of the equilibrium heterozygosity

TheoremEquilibrium homozygosity is a fixed point of the recursion#✓fully proved

F* is a fixed point of the homozygosity recursion.

theorem homozygosityStep_eqHomozygosity {M : ℕ} (hM : 0 < M) {u : ℝ} (hu0 : 0 < u)
    (hu1 : u ≤ 1) : homozygosityStep M u (eqHomozygosity M u) = eqHomozygosity M u

Uses 2 · Used by 1

Statement usesEquilibrium homozygosity in the infinite-alleles model · Homozygosity recursion in the infinite-alleles model

Used byUniqueness of the equilibrium homozygosity

TheoremUniqueness of the equilibrium homozygosity#✓fully proved

For 0 < u ≤ 1, F* is the unique fixed point of the homozygosity recursion.

theorem homozygosityStep_eq_self_iff {M : ℕ} (hM : 0 < M) {u : ℝ} (hu0 : 0 < u) (hu1 : u ≤ 1)
    (F : ℝ) : homozygosityStep M u F = F ↔ F = eqHomozygosity M u

Uses 3

Statement usesEquilibrium homozygosity in the infinite-alleles model · Homozygosity recursion in the infinite-alleles model

Proof usesEquilibrium homozygosity is a fixed point of the recursion

TheoremConvergence of homozygosity to equilibrium#✓fully proved

For 0 < u ≤ 1 the homozygosity converges to F* from every initial value F₀.

theorem tendsto_iterate_homozygosityStep {M : ℕ} (hM : 0 < M) {u : ℝ} (hu0 : 0 < u)
    (hu1 : u ≤ 1) (F₀ : ℝ) :
    Tendsto (fun t : ℕ => (homozygosityStep M u)^[t] F₀) atTop (𝓝 (eqHomozygosity M u))

Uses 2

Statement usesEquilibrium homozygosity in the infinite-alleles model · Homozygosity recursion in the infinite-alleles model

TheoremKimura–Crow limit#✓fully proved

With M = 2N gene copies and mutation probability u = θ/(4N) (so that θ = 4Nu), the equilibrium homozygosity tends to 1/(1 + θ) as N → ∞.

theorem tendsto_eqHomozygosity {θ : ℝ} (hθ : 0 < θ) :
    Tendsto (fun N : ℕ => eqHomozygosity (2 * N) (θ / (4 * N))) atTop (𝓝 (1 / (1 + θ)))

Uses 1 · Used by 1

Statement usesEquilibrium homozygosity in the infinite-alleles model

Used byLimit \(\theta/(1+\theta)\) of the equilibrium heterozygosity

TheoremLimit \(\theta/(1+\theta)\) of the equilibrium heterozygosity#✓fully proved

The equilibrium heterozygosity H* = 1 - F* tends to θ/(1 + θ) as N → ∞ with M = 2N and u = θ/(4N).

theorem tendsto_one_sub_eqHomozygosity {θ : ℝ} (hθ : 0 < θ) :
    Tendsto (fun N : ℕ => 1 - eqHomozygosity (2 * N) (θ / (4 * N))) atTop
      (𝓝 (θ / (1 + θ)))

Uses 2

Statement usesEquilibrium homozygosity in the infinite-alleles model

Proof usesKimura–Crow limit

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.