Diffusion limit of the Wright–Fisher model

TheoremOne Wright–Fisher generation as a Bernstein approximation#✓fully proved

For M gene copies and current frequency x, the expected value of f at the next frequency, ∫ k, f (k / M) ∂Bin(M, x), is the M-th Bernstein approximation of f on [0, 1] evaluated at x.

theorem integral_binomial_eq_bernsteinApproximation (M : ℕ) {f : ℝ → ℝ} (hf : Continuous f)
    (x : I) :
    ∫ k, f (k / M) ∂(ProbabilityTheory.binomial M x) =
      bernsteinApproximation M ((⟨f, hf⟩ : C(ℝ, ℝ)).restrict I) x

Used by 1

Used byWright–Fisher diffusion limit, generator form (Feller 1951; Voronovskaya 1932)

TheoremWright–Fisher diffusion limit, generator form (Feller 1951; Voronovskaya 1932)#✓fully proved

For f of class C² and x ∈ [0, 1], the one-generation generator of the neutral Wright–Fisher chain with M gene copies, sped up by the factor M (time in units of M generations), converges to the neutral Wright–Fisher diffusion generator (L_0 f)(x) = x (1 - x) / 2 · f''(x).

theorem tendsto_wfGenerator {f : ℝ → ℝ} (hf : ContDiff ℝ 2 f) (x : I) :
    Tendsto (fun M : ℕ => (M : ℝ) *
        (∫ k, f (k / M) ∂(ProbabilityTheory.binomial M x) - f x)) atTop
      (𝓝 (generator 0 f x))

Uses 3

Statement usesBackward generator of the Wright–Fisher diffusion with selection

Proof usesOne Wright–Fisher generation as a Bernstein approximation · Voronovskaya's theorem (1932)

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.