Wright–Fisher diffusion with mutation

DefinitionWright–Fisher generator with two-way mutation#✓fully proved

The backward generator of the Wright–Fisher diffusion with two-way mutation, time in units of 2N generations and scaled mutation rates θ₁ = 4N u₁ (towards the allele) and θ₂ = 4N u₂ (away from it): (L f)(x) = x (1 - x) / 2 · f''(x) + (θ₁ (1 - x) - θ₂ x) / 2 · f'(x).

noncomputable def mutationGenerator (θ₁ θ₂ : ℝ) (f : ℝ → ℝ) (x : ℝ) : ℝ :=
  x * (1 - x) / 2 * deriv (deriv f) x + (θ₁ * (1 - x) - θ₂ * x) / 2 * deriv f x

Used by 7

Used byIntegrability of the mutation generator under Wright's stationary law · Weak stationarity of Wright's law (Wright 1931; Ewens 2004, ch. 4) · Weak stationarity of Wright's law (density form) · Integrability of the mutation generator against the Beta density · Mutation generator applied to heterozygosity · Mutation generator applied to the allele frequency · Mutation generator without mutation is the neutral generator

TheoremMutation generator without mutation is the neutral generator#✓fully proved

Without mutation the generator is the neutral Wright–Fisher generator generator 0.

theorem mutationGenerator_zero_zero (f : ℝ → ℝ) (x : ℝ) :
    mutationGenerator 0 0 f x = generator 0 f x

Uses 2

Statement usesBackward generator of the Wright–Fisher diffusion with selection · Wright–Fisher generator with two-way mutation

TheoremBeta density as Wright's stationary density#✓fully proved

On (0, 1) the Beta(θ₁, θ₂) density is Wright's unnormalized density in the scaled rates α = θ₁ / 2, β = θ₂ / 2, divided by the Beta function B(θ₁, θ₂).

theorem betaPDFReal_eq_wrightDensity (θ₁ θ₂ : ℝ) {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
    betaPDFReal θ₁ θ₂ x = wrightDensity (θ₁ / 2) (θ₂ / 2) x / beta θ₁ θ₂

Uses 1 · Used by 2

Statement usesWright's stationary density of the Wright–Fisher diffusion

Used byZero probability flux (Wright 1931) · Integrability of the mutation generator against the Beta density

TheoremSmoothness of the Beta density on the open unit interval#✓fully proved

The Beta(θ₁, θ₂) density is analytic (C^ω), in particular smooth, on (0, 1), so the derivatives in flux_betaPDFReal and forwardEquation_betaPDFReal exist.

theorem contDiffOn_betaPDFReal (θ₁ θ₂ : ℝ) :
    ContDiffOn ℝ ⊤ (betaPDFReal θ₁ θ₂) (Ioo 0 1)

TheoremZero probability flux (Wright 1931)#✓fully proved

On (0, 1) the Beta(θ₁, θ₂) density π satisfies ½ (x (1 - x) π)' - (θ₁ (1 - x) - θ₂ x) / 2 · π = 0. The identity holds for all real θ₁, θ₂ (it is linear in π; Mathlib's density is identically 0 when B(θ₁, θ₂) = 0); π is a probability density when θ₁, θ₂ > 0 (isProbabilityMeasureBeta).

theorem flux_betaPDFReal (θ₁ θ₂ : ℝ) {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
    deriv (fun y => y * (1 - y) * betaPDFReal θ₁ θ₂ y) x / 2 -
      (θ₁ * (1 - x) - θ₂ * x) / 2 * betaPDFReal θ₁ θ₂ x = 0

Uses 3 · Used by 1

Proof usesBeta density as Wright's stationary density · Wright's stationary density (zero-flux form) · Wright's stationary density of the Wright–Fisher diffusion

Used byStationary forward equation (Wright 1931)

TheoremStationary forward equation (Wright 1931)#✓fully proved

On (0, 1) the Beta(θ₁, θ₂) density π solves the stationary Fokker–Planck equation ½ (a π)'' - (b π)' = 0 with a(x) = x (1 - x) and b(x) = (θ₁ (1 - x) - θ₂ x) / 2. Holds for all real θ₁, θ₂ (see flux_betaPDFReal).

theorem forwardEquation_betaPDFReal (θ₁ θ₂ : ℝ) {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
    deriv (deriv (fun y => y * (1 - y) * betaPDFReal θ₁ θ₂ y)) x / 2 -
      deriv (fun y => (θ₁ * (1 - y) - θ₂ * y) / 2 * betaPDFReal θ₁ θ₂ y) x = 0

Uses 1

Proof usesZero probability flux (Wright 1931)

TheoremIntegrability of the mutation generator against the Beta density#✓fully proved

For θ₁, θ₂ > 0 and f twice continuously differentiable on [0, 1], L f · π is integrable on [0, 1], so the integral in integral_mutationGenerator_mul_betaPDFReal is a genuine (not junk) value.

theorem intervalIntegrable_mutationGenerator_mul_betaPDFReal {θ₁ θ₂ : ℝ} (hθ₁ : 0 < θ₁)
    (hθ₂ : 0 < θ₂) {f : ℝ → ℝ} (hf : ContDiffOn ℝ 2 f (Icc 0 1)) :
    IntervalIntegrable (fun x => mutationGenerator θ₁ θ₂ f x * betaPDFReal θ₁ θ₂ x)
      volume 0 1

Uses 4 · Used by 2

Statement usesWright–Fisher generator with two-way mutation

Proof usesBeta density as Wright's stationary density · Integrability of Wright's density on the unit interval · Wright's stationary density of the Wright–Fisher diffusion

Used byIntegrability of the mutation generator under Wright's stationary law · Weak stationarity of Wright's law (density form)

TheoremWeak stationarity of Wright's law (density form)#✓fully proved

For θ₁, θ₂ > 0 and every f twice continuously differentiable on [0, 1], ∫₀¹ (L f)(x) π(x) dx = 0 for the Beta(θ₁, θ₂) density π. (L f uses deriv, which agrees with the one-sided derivatives inside (0, 1); its values at the endpoints do not affect the integral.) The proof is integration by parts: L f · π = (x ^ θ₁ (1 - x) ^ θ₂ f' / (2 B(θ₁, θ₂)))' on (0, 1) because the flux vanishes, and this boundary term is 0 at both endpoints since θ₁, θ₂ > 0.

theorem integral_mutationGenerator_mul_betaPDFReal {θ₁ θ₂ : ℝ} (hθ₁ : 0 < θ₁) (hθ₂ : 0 < θ₂)
    {f : ℝ → ℝ} (hf : ContDiffOn ℝ 2 f (Icc 0 1)) :
    ∫ x in (0 : ℝ)..1, mutationGenerator θ₁ θ₂ f x * betaPDFReal θ₁ θ₂ x = 0

Uses 2 · Used by 1

Statement usesWright–Fisher generator with two-way mutation

Proof usesIntegrability of the mutation generator against the Beta density

Used byWeak stationarity of Wright's law (Wright 1931; Ewens 2004, ch. 4)

TheoremIntegrability of the mutation generator under Wright's stationary law#✓fully proved

For θ₁, θ₂ > 0 and f twice continuously differentiable on [0, 1], L f is integrable against Wright's stationary law Beta(θ₁, θ₂).

theorem integrable_mutationGenerator_betaMeasure {θ₁ θ₂ : ℝ} (hθ₁ : 0 < θ₁) (hθ₂ : 0 < θ₂)
    {f : ℝ → ℝ} (hf : ContDiffOn ℝ 2 f (Icc 0 1)) :
    Integrable (mutationGenerator θ₁ θ₂ f) (betaMeasure θ₁ θ₂)

Uses 3

Statement usesWright–Fisher generator with two-way mutation

Proof usesIntegrability of the mutation generator against the Beta density · Nonnegativity of the beta density

TheoremWeak stationarity of Wright's law (Wright 1931; Ewens 2004, ch. 4)#✓fully proved

For θ₁, θ₂ > 0 and every f twice continuously differentiable on [0, 1], ∫ L f d(Beta(θ₁, θ₂)) = 0.

theorem integral_mutationGenerator_betaMeasure {θ₁ θ₂ : ℝ} (hθ₁ : 0 < θ₁) (hθ₂ : 0 < θ₂)
    {f : ℝ → ℝ} (hf : ContDiffOn ℝ 2 f (Icc 0 1)) :
    ∫ x, mutationGenerator θ₁ θ₂ f x ∂(betaMeasure θ₁ θ₂) = 0

Uses 3

Statement usesWright–Fisher generator with two-way mutation

Proof usesWeak stationarity of Wright's law (density form) · Nonnegativity of the beta density

TheoremMutation generator applied to the allele frequency#✓fully proved

The generator applied to the frequency itself is the mutation drift: L x = (θ₁ (1 - x) - θ₂ x) / 2.

theorem mutationGenerator_id (θ₁ θ₂ x : ℝ) :
    mutationGenerator θ₁ θ₂ id x = (θ₁ * (1 - x) - θ₂ * x) / 2

Uses 1

Statement usesWright–Fisher generator with two-way mutation

TheoremMutation generator applied to heterozygosity#✓fully proved

The generator applied to the heterozygosity H(x) = 2x (1 - x): L H = -2x (1 - x) + (θ₁ (1 - x) - θ₂ x) (1 - 2x) (drift decreases H at rate 1, mutation restores it).

theorem mutationGenerator_heterozygosity (θ₁ θ₂ x : ℝ) :
    mutationGenerator θ₁ θ₂ (fun y => 2 * y * (1 - y)) x =
      -(2 * x * (1 - x)) + (θ₁ * (1 - x) - θ₂ * x) * (1 - 2 * x)

Uses 1

Statement usesWright–Fisher generator with two-way mutation

DefinitionAllele frequency after one generation of two-way mutation#✓fully proved

Allele frequency after one generation of two-way mutation, before random sampling: an a copy mutates to A with probability u₁ and an A copy to a with probability u₂, so the frequency x of A becomes (1 - u₂) x + u₁ (1 - x) ∈ [0, 1].

noncomputable def mutatedFreq (u₁ u₂ x : unitInterval) : unitInterval :=
  ⟨(1 - u₂) * x + u₁ * (1 - x), by
    obtain ⟨hu₁, hu₁'⟩ := u₁.2
    obtain ⟨hu₂, hu₂'⟩ := u₂.2
    obtain ⟨hx, hx'⟩ := x.2
    constructor
    · nlinarith
    · nlinarith⟩

Used by 2

Used byDrift of the Wright–Fisher chain with mutation (Ewens 2004, ch. 4) · Infinitesimal variance of the Wright–Fisher chain with mutation

TheoremDrift of the Wright–Fisher chain with mutation (Ewens 2004, ch. 4)#✓fully proved

One generation of the Wright–Fisher chain on M gene copies (M = 2N): mutation moves the frequency x to p' = mutatedFreq u₁ u₂ x, then the new count is Binomial(M, p'). With u₁ = θ₁ / (2M), u₂ = θ₂ / (2M) (θᵢ = 4N uᵢ), the expected change of frequency per 2N = M generations is exactly the drift coefficient of mutationGenerator: M · (E[k / M] - x) = (θ₁ (1 - x) - θ₂ x) / 2, for every M.

theorem integral_binomial_mutatedFreq_drift {M : ℕ} (hM : M ≠ 0) {θ₁ θ₂ : ℝ}
    {u₁ u₂ : unitInterval} (hu₁ : (u₁ : ℝ) = θ₁ / (2 * M)) (hu₂ : (u₂ : ℝ) = θ₂ / (2 * M))
    (x : unitInterval) :
    M * (∫ k, (k : ℝ) / M ∂(binomial M (mutatedFreq u₁ u₂ x)) - x) =
      (θ₁ * (1 - x) - θ₂ * x) / 2

Uses 2

Statement usesAllele frequency after one generation of two-way mutation

Proof usesSecond moment of the binomial law

TheoremInfinitesimal variance of the Wright–Fisher chain with mutation#✓fully proved

In the setting of integral_binomial_mutatedFreq_drift, the scaled second moment of the frequency change is M · E[(k / M - x) ^ 2] = p' (1 - p') + (θ₁ (1 - x) - θ₂ x) ^ 2 / (4M) with p' = mutatedFreq u₁ u₂ x = x + (θ₁ (1 - x) - θ₂ x) / (2M). As M → ∞ with θ₁, θ₂, x fixed this tends to x (1 - x), the diffusion coefficient of mutationGenerator (the limit itself is not stated here).

theorem integral_binomial_mutatedFreq_sq {M : ℕ} (hM : M ≠ 0) {θ₁ θ₂ : ℝ}
    {u₁ u₂ : unitInterval} (hu₁ : (u₁ : ℝ) = θ₁ / (2 * M)) (hu₂ : (u₂ : ℝ) = θ₂ / (2 * M))
    (x : unitInterval) :
    M * ∫ k, ((k : ℝ) / M - x) ^ 2 ∂(binomial M (mutatedFreq u₁ u₂ x)) =
      (mutatedFreq u₁ u₂ x : ℝ) * (1 - mutatedFreq u₁ u₂ x) +
        (θ₁ * (1 - x) - θ₂ * x) ^ 2 / (4 * M)

Uses 2

Statement usesAllele frequency after one generation of two-way mutation

Proof usesSecond moment of the binomial law

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.