Sojourn times of the Wright–Fisher diffusion

DefinitionNeutral Wright–Fisher Green's function#✓fully proved

The neutral Wright–Fisher Green's function (sojourn density), time in units of 2N generations (Ewens 2004, Chapter 4): G(p, x) = 2 (1 - p) / (1 - x) for x ≤ p and G(p, x) = 2 p / x for p < x. In the diffusion reading, for 0 < x < 1, G(p, x) dx is the expected time a neutral allele started at frequency p spends at frequencies in (x, x + dx) before loss or fixation.

noncomputable def neutralGreen (p x : ℝ) : ℝ :=
  if x ≤ p then 2 * (1 - p) / (1 - x) else 2 * p / x

Used by 10

Used byNeutral case of the sojourn density · The neutral density from the Green's function · General Green's function agrees with the neutral Wright–Fisher one · The general h-transform specializes to Kimura–Ohta · Neutral conditional fixation time as an h-transformed sojourn integral · Neutral conditional loss time · Green's representation (Ewens 2004, Chapter 4) · Mean absorption time as a sojourn integral · Sojourn integral vanishes for an absent allele · Sojourn integral vanishes for a fixed allele

TheoremGreen's representation (Ewens 2004, Chapter 4)#✓fully proved

For continuous g and p ∈ (0, 1), the function u(q) = ∫ x in 0..1, G(q, x) g(x) solves the neutral backward equation L_0 u = -g at p. In the diffusion reading, u(p) is the expected value of ∫₀^T g(X_t) dt up to the absorption time T.

theorem generator_integral_neutralGreen {g : ℝ → ℝ} (hg : Continuous g) {p : ℝ}
    (hp : p ∈ Ioo (0 : ℝ) 1) :
    generator 0 (fun q => ∫ x in (0 : ℝ)..1, neutralGreen q x * g x) p = -g p

Uses 2

Statement usesBackward generator of the Wright–Fisher diffusion with selection · Neutral Wright–Fisher Green's function

TheoremSojourn integral vanishes for an absent allele#✓fully proved

Boundary value at 0: an allele that is absent spends no time in (0, 1), so ∫ x in 0..1, G(0, x) g(x) = 0.

theorem integral_neutralGreen_left (g : ℝ → ℝ) :
    ∫ x in (0 : ℝ)..1, neutralGreen 0 x * g x = 0

Uses 1

Statement usesNeutral Wright–Fisher Green's function

TheoremSojourn integral vanishes for a fixed allele#✓fully proved

Boundary value at 1: a fixed allele spends no time in (0, 1), so ∫ x in 0..1, G(1, x) g(x) = 0.

theorem integral_neutralGreen_right (g : ℝ → ℝ) :
    ∫ x in (0 : ℝ)..1, neutralGreen 1 x * g x = 0

Uses 1

Statement usesNeutral Wright–Fisher Green's function

TheoremMean absorption time as a sojourn integral#✓fully proved

For p ∈ [0, 1], the total expected sojourn time ∫ x in 0..1, G(p, x) is the Kimura–Ohta mean absorption time -2 (p log p + (1 - p) log (1 - p)) (units of 2N generations).

theorem integral_neutralGreen {p : ℝ} (hp : p ∈ Icc (0 : ℝ) 1) :
    ∫ x in (0 : ℝ)..1, neutralGreen p x = meanAbsorptionTime p

Uses 2

Statement usesKimura–Ohta mean absorption time of a neutral allele · Neutral Wright–Fisher Green's function

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.