Skip to content

Selection duality and general one-dimensional diffusions

56 fully proved

Ancestral selection graph duality

DefinitionGenerator of the ancestral selection graph line-counting process#✓fully proved

The generator of the line-counting process of the ancestral selection graph with scaled selection coefficient σ (time in units of 2N generations, the scaling of generator): from n lines, branching n → n + 1 at rate n σ and coalescence n → n - 1 at rate C(n, 2).

noncomputable def asgGenerator (σ : ℝ) (f : ℕ → ℝ) (n : ℕ) : ℝ :=
  n * σ * (f (n + 1) - f n) + (n.choose 2 : ℝ) * (f (n - 1) - f n)
Used by 1
Used bySelection duality in operator form

TheoremSelection duality (Mano 2009)#✓fully proved

Selection duality (Mano 2009) at generator level, with the line-counting process of the ancestral selection graph (Krone–Neuhauser 1997) as the dual: the Wright–Fisher generator with genic selection maps y ↦ (1 - y) ^ n to C(n, 2) ((1 - x)^(n-1) - (1 - x)^n) + n σ ((1 - x)^(n+1) - (1 - x)^n). This identity holds for every real σ; the dual is a Markov chain only for σ ≥ 0.

theorem generator_one_sub_pow (σ : ℝ) (n : ℕ) (x : ℝ) :
    generator σ (fun y => (1 - y) ^ n) x =
      (n.choose 2 : ℝ) * ((1 - x) ^ (n - 1) - (1 - x) ^ n) +
        n * σ * ((1 - x) ^ (n + 1) - (1 - x) ^ n)
Uses 1 · Used by 1
Statement usesBackward generator of the Wright–Fisher diffusion with selection
Used bySelection duality in operator form

TheoremSelection duality in operator form#✓fully proved

The selection duality in operator form: L_σ applied to y ↦ (1 - y) ^ n equals the ancestral-selection-graph generator applied to k ↦ (1 - x) ^ k at n.

theorem generator_one_sub_pow_eq_asgGenerator (σ : ℝ) (n : ℕ) (x : ℝ) :
    generator σ (fun y => (1 - y) ^ n) x = asgGenerator σ (fun k => (1 - x) ^ k) n
Uses 3
Statement usesGenerator of the ancestral selection graph line-counting process · Backward generator of the Wright–Fisher diffusion with selection
Proof usesSelection duality (Mano 2009)

DefinitionStationary law of the ancestral selection graph line counts#✓fully proved

The stationary law of the ancestral-selection-graph line-counting process with σ > 0: π_k = (2σ)^k / k! / (e^{2σ} - 1) for k ≥ 1 and π_0 = 0, a Poisson(2σ) law conditioned to be positive. For σ = 0 the stationary law is δ₁: branching vanishes, coalescence reaches state 1, and state 1 is absorbing, so π_1 = 1 and π_k = 0 otherwise (the limit of the σ > 0 formula as σ → 0).

noncomputable def asgStationary (σ : ℝ) (k : ℕ) : ℝ :=
  if σ = 0 then (if k = 1 then 1 else 0)
  else if k = 0 then 0 else (2 * σ) ^ k / k ! / (exp (2 * σ) - 1)
Used by 8
Used byDetailed balance · Global balance · Stationary weights under selection are nonnegative · Stationary weights under selection sum to one · Loss probability from the stationary ancestral selection graph · Generating function of the stationary law under selection · Neutral stationary law is the point mass at one · Neutral stationary weights sum to one

TheoremDetailed balance#✓fully proved

Detailed balance of the ancestral-selection-graph chain: π_k · (k σ) = π_{k+1} · C(k + 1, 2) for every k (the flux k → k + 1 equals the flux k + 1 → k). This is an identity for every real σ.

theorem asgStationary_detailed_balance (σ : ℝ) (k : ℕ) :
    asgStationary σ k * (k * σ) = asgStationary σ (k + 1) * ((k + 1).choose 2 : ℝ)
Uses 1 · Used by 1
Statement usesStationary law of the ancestral selection graph line counts
Used byGlobal balance

TheoremGlobal balance#✓fully proved

Global balance (stationarity π Q = 0) of the ancestral-selection-graph chain at state k + 1: the outflow π_{k+1} ((k + 1) σ + C(k + 1, 2)) equals the inflow π_k (k σ) + π_{k+2} C(k + 2, 2) (for k = 0 the inflow from the unreachable state 0 vanishes).

theorem asgStationary_global_balance (σ : ℝ) (k : ℕ) :
    asgStationary σ (k + 1) * ((k + 1 : ℕ) * σ + ((k + 1).choose 2 : ℝ)) =
      asgStationary σ k * (k * σ) + asgStationary σ (k + 2) * ((k + 2).choose 2 : ℝ)
Uses 2
Statement usesStationary law of the ancestral selection graph line counts
Proof usesDetailed balance

TheoremStationary weights under selection are nonnegative#✓fully proved

For σ > 0 the stationary weights are nonnegative.

theorem asgStationary_nonneg {σ : ℝ} (hσ : 0 < σ) (k : ℕ) : 0 ≤ asgStationary σ k
Uses 1
Statement usesStationary law of the ancestral selection graph line counts

TheoremGenerating function of the stationary law under selection#✓fully proved

The probability generating function of the stationary law: for σ > 0 and every real y, ∑ₖ π_k y^k = (e^{2σy} - 1) / (e^{2σ} - 1).

theorem hasSum_asgStationary_mul_pow {σ : ℝ} (hσ : 0 < σ) (y : ℝ) :
    HasSum (fun k => asgStationary σ k * y ^ k) ((exp (2 * σ * y) - 1) / (exp (2 * σ) - 1))
Uses 1 · Used by 2
Statement usesStationary law of the ancestral selection graph line counts
Used byStationary weights under selection sum to one · Loss probability from the stationary ancestral selection graph

TheoremStationary weights under selection sum to one#✓fully proved

For σ > 0 the stationary weights sum to 1.

theorem hasSum_asgStationary {σ : ℝ} (hσ : 0 < σ) : HasSum (asgStationary σ) 1
Uses 2
Statement usesStationary law of the ancestral selection graph line counts
Proof usesGenerating function of the stationary law under selection

TheoremNeutral stationary law is the point mass at one#✓fully proved

The neutral stationary law is δ₁: its generating function is y.

theorem hasSum_asgStationary_mul_pow_zero (y : ℝ) :
    HasSum (fun k => asgStationary 0 k * y ^ k) y
Uses 1
Statement usesStationary law of the ancestral selection graph line counts

TheoremNeutral stationary weights sum to one#✓fully proved

The neutral stationary weights sum to 1.

theorem hasSum_asgStationary_zero : HasSum (asgStationary 0) 1
Uses 1
Statement usesStationary law of the ancestral selection graph line counts

TheoremLoss probability in Kimura's fixation formula#✓fully proved

The loss probability in Kimura's formula, written with positive exponents: for σ ≠ 0, 1 - kimuraFixation σ x = (e^{2σ(1 - x)} - 1) / (e^{2σ} - 1).

theorem one_sub_kimuraFixation {σ : ℝ} (hσ : σ ≠ 0) (x : ℝ) :
    1 - kimuraFixation σ x = (exp (2 * σ * (1 - x)) - 1) / (exp (2 * σ) - 1)
Uses 1 · Used by 1
Statement usesKimura's fixation probability
Used byLoss probability from the stationary ancestral selection graph

TheoremLoss probability from the stationary ancestral selection graph#✓fully proved

Loss probability from the stationary ancestral selection graph (Mano 2009): for σ > 0, ∑ₖ π_k (1 - x)^k = 1 - kimuraFixation σ x, i.e. the loss probability of the favoured allele at frequency x is the probability that all lines of the stationary ancestral selection graph carry the unfavoured allele. Only the series identity is formalized; the sampling interpretation is not.

theorem hasSum_asgStationary_mul_one_sub_pow {σ : ℝ} (hσ : 0 < σ) (x : ℝ) :
    HasSum (fun k => asgStationary σ k * (1 - x) ^ k) (1 - kimuraFixation σ x)
Uses 4
Statement usesStationary law of the ancestral selection graph line counts · Kimura's fixation probability
Proof usesGenerating function of the stationary law under selection · Loss probability in Kimura's fixation formula

General one-dimensional diffusions

DefinitionBackward generator of a one-dimensional diffusion#✓fully proved

The backward generator of a one-dimensional diffusion with drift b and infinitesimal variance a: (L u)(x) = a(x) / 2 · u''(x) + b(x) · u'(x).

noncomputable def diffusionGenerator (b a u : ℝ → ℝ) (x : ℝ) : ℝ :=
  a x / 2 * deriv (deriv u) x + b x * deriv u x
Used by 8
Used byKimura (1962) · Green's representation (Ewens 2004, Chapter 4; Karlin–Taylor 1981, Chapter 15) · Conditional mean time to fixation, backward equation · Wright–Fisher generator with genic selection as a general diffusion · Uniqueness of the scale-function ratio (Kimura 1962) · Uniqueness for the Dirichlet problem · Solutions of L u = 0 · Kimura's formula as a corollary

DefinitionScale density of a one-dimensional diffusion#✓fully proved

The scale density ψ(y) = exp (-∫₀^y 2 b(z) / a(z) dz) of the diffusion with drift b and variance a (Karlin–Taylor 1981, Chapter 15).

noncomputable def scaleDensity (b a : ℝ → ℝ) (y : ℝ) : ℝ :=
  exp (-∫ z in (0 : ℝ)..y, 2 * b z / a z)
Used by 20
Used byThe general Green kernel specializes to Kimura's sojourn density · Continuity of the scale density on \((0, 1)\) · Continuity of the scale function on \((0, 1)\) · Kimura (1962) · Green's representation (Ewens 2004, Chapter 4; Karlin–Taylor 1981, Chapter 15) · Conditional mean time to fixation, backward equation · Solutions of L u = 0 · Kimura's scale-function ratio with dominance (Kimura 1962) · Dirichlet Green's function of a one-dimensional diffusion · General Green's function agrees with the neutral Wright–Fisher one · Derivative of the scale density · Derivative of the scale function is the scale density · The general h-transform specializes to Kimura–Ohta · Dirichlet condition of the Green's function at one · Dirichlet condition of the Green's function at zero · Positivity of the scale density · Scale density of the Wright–Fisher diffusion with genic selection · Scale function of a one-dimensional diffusion · Scale function vanishes at zero · Scale function is strictly increasing

DefinitionScale function of a one-dimensional diffusion#✓fully proved

The scale function S(p) = ∫₀^p ψ(y) dy, normalized by S(0) = 0.

noncomputable def scaleFunction (b a : ℝ → ℝ) (p : ℝ) : ℝ :=
  ∫ y in (0 : ℝ)..p, scaleDensity b a y
Uses 1 · Used by 20
Statement usesScale density of a one-dimensional diffusion
Used byThe general Green kernel specializes to Kimura's sojourn density · Continuity of the scale function on \((0, 1)\) · Kimura (1962) · Green's representation (Ewens 2004, Chapter 4; Karlin–Taylor 1981, Chapter 15) · Conditional mean time to fixation, backward equation · Solutions of L u = 0 · Dirichlet ratio \(S(p)/S(1)\) of the scale function · Kimura's scale-function ratio with dominance (Kimura 1962) · Dirichlet ratio lies in \((0, 1)\) · Dirichlet ratio equals one at \(p = 1\) · Dirichlet ratio vanishes at \(p = 0\) · Dirichlet Green's function of a one-dimensional diffusion · General Green's function agrees with the neutral Wright–Fisher one · Derivative of the scale function is the scale density · The general h-transform specializes to Kimura–Ohta · Dirichlet condition of the Green's function at one · Dirichlet condition of the Green's function at zero · Scale function is positive at one · Scale function vanishes at zero · Scale function is strictly increasing

DefinitionDirichlet ratio \(S(p)/S(1)\) of the scale function#✓fully proved

The analytic Dirichlet ratio S(p) / S(1) for drift b and variance a (Kimura 1962; Ewens 2004, Chapter 4). This is the solution of the backward boundary-value problem L u = 0, u(0) = 0, u(1) = 1 (see eq_fixationProb_of_diffusionGenerator_eq_zero). It is the hitting probability P_p(hit 1 before 0) only when both boundaries are Feller-accessible; that is not implied by IsRegularDiffusion (see the module docstring for the a x = x² (1 - x)² counterexample).

noncomputable def fixationProb (b a : ℝ → ℝ) (p : ℝ) : ℝ :=
  scaleFunction b a p / scaleFunction b a 1
Uses 1 · Used by 12
Statement usesScale function of a one-dimensional diffusion
Used bySojourn density conditioned on fixation · Kimura (1962) · Conditional mean time to fixation, backward equation · Uniqueness of the scale-function ratio (Kimura 1962) · Uniqueness for the Dirichlet problem · Solutions of L u = 0 · Kimura's scale-function ratio with dominance (Kimura 1962) · Dirichlet ratio lies in \((0, 1)\) · Dirichlet ratio equals one at \(p = 1\) · Kimura's formula as a corollary · Dirichlet ratio vanishes at \(p = 0\) · The general h-transform specializes to Kimura–Ohta

DefinitionDirichlet Green's function of a one-dimensional diffusion#✓fully proved

The Green's function (analytic Green kernel) of -L with Dirichlet conditions at 0 and 1 (Ewens 2004, Chapter 4; Karlin–Taylor 1981, Chapter 15): G(p, x) = 2 S(min p x) (S(1) - S(max p x)) / (S(1) a(x) ψ(x)). In the diffusion reading (which requires Feller-accessible boundaries), G(p, x) dx is the expected time spent in (x, x + dx) before absorption.

noncomputable def greenFunction (b a : ℝ → ℝ) (p x : ℝ) : ℝ :=
  2 * scaleFunction b a (min p x) * (scaleFunction b a 1 - scaleFunction b a (max p x)) /
    (scaleFunction b a 1 * a x * scaleDensity b a x)
Uses 2 · Used by 8
Statement usesScale density of a one-dimensional diffusion · Scale function of a one-dimensional diffusion
Used byThe general Green kernel specializes to Kimura's sojourn density · Sojourn density conditioned on fixation · Green's representation (Ewens 2004, Chapter 4; Karlin–Taylor 1981, Chapter 15) · Conditional mean time to fixation, backward equation · General Green's function agrees with the neutral Wright–Fisher one · The general h-transform specializes to Kimura–Ohta · Dirichlet condition of the Green's function at one · Dirichlet condition of the Green's function at zero

StructureStanding regularity hypotheses for a diffusion on \((0, 1)\)#✓fully proved

Regularity hypotheses for a diffusion on (0, 1) with drift b and variance a: a is positive and continuous on (0, 1), b / a is continuous on (0, 1) and integrable on [0, 1] (so the scale function is finite up to both boundaries). The values of b and a at 0 and 1 are irrelevant. These are standing hypotheses for this file, not Feller's classification of regular boundaries: they do not imply that either endpoint is accessible (finite scale–speed integrals), so the hitting-probability reading of fixationProb needs that extra hypothesis.

structure IsRegularDiffusion (b a : ℝ → ℝ) : Prop where
  /-- The variance is positive inside the interval. -/
  pos : ∀ x ∈ Ioo (0 : ℝ) 1, 0 < a x
  /-- The variance is continuous inside the interval. -/
  continuousOn : ContinuousOn a (Ioo 0 1)
  /-- The drift-to-variance ratio is continuous inside the interval. -/
  continuousOn_div : ContinuousOn (fun x => b x / a x) (Ioo 0 1)
  /-- The drift-to-variance ratio is integrable on `[0, 1]`. -/
  intervalIntegrable_div : IntervalIntegrable (fun x => b x / a x) volume 0 1
Used by 16
Used byContinuity of the scale density on \((0, 1)\) · Continuity of the scale function on \((0, 1)\) · Kimura (1962) · Green's representation (Ewens 2004, Chapter 4; Karlin–Taylor 1981, Chapter 15) · Conditional mean time to fixation, backward equation · Uniqueness of the scale-function ratio (Kimura 1962) · Uniqueness for the Dirichlet problem · Solutions of L u = 0 · Dirichlet ratio lies in \((0, 1)\) · Dirichlet ratio equals one at \(p = 1\) · Derivative of the scale density · Derivative of the scale function is the scale density · Diffusion with dominance is regular · Wright–Fisher diffusion with genic selection is regular · Scale function is positive at one · Scale function is strictly increasing

TheoremPositivity of the scale density#✓fully proved

The scale density is positive.

theorem scaleDensity_pos (b a : ℝ → ℝ) (y : ℝ) : 0 < scaleDensity b a y
Uses 1 · Used by 3
Statement usesScale density of a one-dimensional diffusion
Used byGreen's representation (Ewens 2004, Chapter 4; Karlin–Taylor 1981, Chapter 15) · Solutions of L u = 0 · Scale function is strictly increasing

TheoremScale function vanishes at zero#✓fully proved

The scale function vanishes at 0.

@[simp]
theorem scaleFunction_zero (b a : ℝ → ℝ) : scaleFunction b a 0 = 0
Uses 2 · Used by 6
Statement usesScale function of a one-dimensional diffusion
Proof usesScale density of a one-dimensional diffusion
Used byConditional mean time to fixation, backward equation · Solutions of L u = 0 · Dirichlet ratio lies in \((0, 1)\) · Dirichlet ratio vanishes at \(p = 0\) · Dirichlet condition of the Green's function at zero · Scale function is positive at one

TheoremContinuity of the scale density on \((0, 1)\)#✓fully proved

The scale density is continuous on [0, 1].

theorem continuousOn_scaleDensity (h : IsRegularDiffusion b a) :
    ContinuousOn (scaleDensity b a) (Icc 0 1)
Uses 2 · Used by 4
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\) · Scale density of a one-dimensional diffusion
Used byContinuity of the scale function on \((0, 1)\) · Green's representation (Ewens 2004, Chapter 4; Karlin–Taylor 1981, Chapter 15) · Derivative of the scale function is the scale density · Scale function is strictly increasing

TheoremDerivative of the scale density#✓fully proved

ψ' = -(2 b / a) ψ inside the interval.

theorem hasDerivAt_scaleDensity (h : IsRegularDiffusion b a) {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
    HasDerivAt (scaleDensity b a) (-(2 * b x / a x) * scaleDensity b a x) x
Uses 2 · Used by 3
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\) · Scale density of a one-dimensional diffusion
Used byKimura (1962) · Green's representation (Ewens 2004, Chapter 4; Karlin–Taylor 1981, Chapter 15) · Solutions of L u = 0

TheoremDerivative of the scale function is the scale density#✓fully proved

S' = ψ inside the interval.

theorem hasDerivAt_scaleFunction (h : IsRegularDiffusion b a) {x : ℝ}
    (hx : x ∈ Ioo (0 : ℝ) 1) : HasDerivAt (scaleFunction b a) (scaleDensity b a x) x
Uses 4 · Used by 3
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\) · Scale density of a one-dimensional diffusion · Scale function of a one-dimensional diffusion
Proof usesContinuity of the scale density on \((0, 1)\)
Used byKimura (1962) · Green's representation (Ewens 2004, Chapter 4; Karlin–Taylor 1981, Chapter 15) · Solutions of L u = 0

TheoremContinuity of the scale function on \((0, 1)\)#✓fully proved

The scale function is continuous on [0, 1].

theorem continuousOn_scaleFunction (h : IsRegularDiffusion b a) :
    ContinuousOn (scaleFunction b a) (Icc 0 1)
Uses 4 · Used by 3
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\) · Scale function of a one-dimensional diffusion
Proof usesContinuity of the scale density on \((0, 1)\) · Scale density of a one-dimensional diffusion
Used byGreen's representation (Ewens 2004, Chapter 4; Karlin–Taylor 1981, Chapter 15) · Conditional mean time to fixation, backward equation · Solutions of L u = 0

TheoremScale function is strictly increasing#✓fully proved

The scale function is strictly increasing on [0, 1].

theorem strictMonoOn_scaleFunction (h : IsRegularDiffusion b a) :
    StrictMonoOn (scaleFunction b a) (Icc 0 1)
Uses 5 · Used by 3
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\) · Scale function of a one-dimensional diffusion
Proof usesContinuity of the scale density on \((0, 1)\) · Scale density of a one-dimensional diffusion · Positivity of the scale density
Used byConditional mean time to fixation, backward equation · Dirichlet ratio lies in \((0, 1)\) · Scale function is positive at one

TheoremScale function is positive at one#✓fully proved

S(1) > 0, so the scale-function ratio and the Green's function have a positive denominator.

theorem scaleFunction_one_pos (h : IsRegularDiffusion b a) : 0 < scaleFunction b a 1
Uses 4 · Used by 6
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\) · Scale function of a one-dimensional diffusion
Proof usesScale function is strictly increasing · Scale function vanishes at zero
Used byKimura (1962) · Green's representation (Ewens 2004, Chapter 4; Karlin–Taylor 1981, Chapter 15) · Conditional mean time to fixation, backward equation · Solutions of L u = 0 · Dirichlet ratio lies in \((0, 1)\) · Dirichlet ratio equals one at \(p = 1\)

TheoremDirichlet ratio equals one at \(p = 1\)#✓fully proved

A fixed allele stays fixed.

theorem fixationProb_one (h : IsRegularDiffusion b a) : fixationProb b a 1 = 1
Uses 4
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\) · Dirichlet ratio \(S(p)/S(1)\) of the scale function
Proof usesScale function is positive at one · Scale function of a one-dimensional diffusion

TheoremDirichlet ratio lies in \((0, 1)\)#✓fully proved

The scale-function ratio lies in [0, 1].

theorem fixationProb_mem_Icc (h : IsRegularDiffusion b a) {p : ℝ} (hp : p ∈ Icc (0 : ℝ) 1) :
    fixationProb b a p ∈ Icc (0 : ℝ) 1
Uses 6
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\) · Dirichlet ratio \(S(p)/S(1)\) of the scale function
Proof usesScale function is positive at one · Scale function is strictly increasing · Scale function of a one-dimensional diffusion · Scale function vanishes at zero

TheoremDirichlet ratio vanishes at \(p = 0\)#✓fully proved

An absent allele is never fixed (for every b, a).

@[simp]
theorem fixationProb_zero (b a : ℝ → ℝ) : fixationProb b a 0 = 0
Uses 3
Statement usesDirichlet ratio \(S(p)/S(1)\) of the scale function
Proof usesScale function of a one-dimensional diffusion · Scale function vanishes at zero

TheoremKimura (1962)#✓fully proved

The scale-function ratio S / S(1) solves the backward equation a / 2 · u'' + b · u' = 0 on (0, 1).

theorem diffusionGenerator_fixationProb {b a : ℝ → ℝ} (h : IsRegularDiffusion b a) {x : ℝ}
    (hx : x ∈ Ioo (0 : ℝ) 1) : diffusionGenerator b a (fixationProb b a) x = 0
Uses 8
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\) · Backward generator of a one-dimensional diffusion · Dirichlet ratio \(S(p)/S(1)\) of the scale function
Proof usesDerivative of the scale density · Derivative of the scale function is the scale density · Scale function is positive at one · Scale density of a one-dimensional diffusion · Scale function of a one-dimensional diffusion

TheoremSolutions of L u = 0#✓fully proved

If u is continuous on [0, 1], differentiable on (0, 1) with derivative differentiable on (0, 1), and L u = 0 on (0, 1), then u = u(0) + (u(1) - u(0)) · S / S(1) on [0, 1].

theorem eq_of_diffusionGenerator_eq_zero {b a u : ℝ → ℝ} (h : IsRegularDiffusion b a)
    (hcont : ContinuousOn u (Icc 0 1)) (hdiff : DifferentiableOn ℝ u (Ioo 0 1))
    (hdiff' : DifferentiableOn ℝ (deriv u) (Ioo 0 1))
    (hgen : ∀ x ∈ Ioo (0 : ℝ) 1, diffusionGenerator b a u x = 0) :
    ∀ x ∈ Icc (0 : ℝ) 1, u x = u 0 + (u 1 - u 0) * fixationProb b a x
Uses 11 · Used by 2
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\) · Backward generator of a one-dimensional diffusion · Dirichlet ratio \(S(p)/S(1)\) of the scale function
Proof usesContinuity of the scale function on \((0, 1)\) · Derivative of the scale density · Derivative of the scale function is the scale density · Scale function is positive at one · Scale density of a one-dimensional diffusion · Positivity of the scale density · Scale function of a one-dimensional diffusion · Scale function vanishes at zero
Used byUniqueness of the scale-function ratio (Kimura 1962) · Uniqueness for the Dirichlet problem

TheoremUniqueness of the scale-function ratio (Kimura 1962)#✓fully proved

A function continuous on [0, 1], differentiable on (0, 1) with derivative differentiable on (0, 1), solving L u = 0 on (0, 1) with u(0) = 0 and u(1) = 1 equals S / S(1) on [0, 1].

theorem eq_fixationProb_of_diffusionGenerator_eq_zero {b a u : ℝ → ℝ}
    (h : IsRegularDiffusion b a) (hcont : ContinuousOn u (Icc 0 1))
    (hdiff : DifferentiableOn ℝ u (Ioo 0 1)) (hdiff' : DifferentiableOn ℝ (deriv u) (Ioo 0 1))
    (hgen : ∀ x ∈ Ioo (0 : ℝ) 1, diffusionGenerator b a u x = 0) (h0 : u 0 = 0) (h1 : u 1 = 1) :
    ∀ x ∈ Icc (0 : ℝ) 1, u x = fixationProb b a x
Uses 4 · Used by 1
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\) · Backward generator of a one-dimensional diffusion · Dirichlet ratio \(S(p)/S(1)\) of the scale function
Proof usesSolutions of L u = 0
Used byKimura's formula as a corollary

TheoremUniqueness for the Dirichlet problem#✓fully proved

Two functions continuous on [0, 1], differentiable on (0, 1) with derivatives differentiable on (0, 1), with L u = L v on (0, 1) and the same values at 0 and 1, agree on [0, 1]. Together with diffusionGenerator_integral_greenFunction this identifies the Green integral as the solution of L v = -g, v(0) = v(1) = 0 whenever it has this regularity.

theorem eq_of_diffusionGenerator_eq {b a u v : ℝ → ℝ} (h : IsRegularDiffusion b a)
    (hu : ContinuousOn u (Icc 0 1)) (hv : ContinuousOn v (Icc 0 1))
    (hu' : DifferentiableOn ℝ u (Ioo 0 1)) (hv' : DifferentiableOn ℝ v (Ioo 0 1))
    (hu'' : DifferentiableOn ℝ (deriv u) (Ioo 0 1))
    (hv'' : DifferentiableOn ℝ (deriv v) (Ioo 0 1))
    (hgen : ∀ x ∈ Ioo (0 : ℝ) 1, diffusionGenerator b a u x = diffusionGenerator b a v x)
    (h0 : u 0 = v 0) (h1 : u 1 = v 1) : ∀ x ∈ Icc (0 : ℝ) 1, u x = v x
Uses 4
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\) · Backward generator of a one-dimensional diffusion
Proof usesSolutions of L u = 0 · Dirichlet ratio \(S(p)/S(1)\) of the scale function

TheoremGreen's representation (Ewens 2004, Chapter 4; Karlin–Taylor 1981, Chapter 15)#✓fully proved

Let g be continuous on (0, 1) and assume the two halves of the Green integral are integrable away from the opposite boundary: S g / (a ψ) on [0, q] and (S(1) - S) g / (a ψ) on [q, 1] for every q ∈ (0, 1) (true for every g continuous on [0, 1] under genic selection, where S / (a ψ) is bounded near 0 and (S(1) - S) / (a ψ) near 1). Then v(q) = ∫₀¹ G(q, x) g(x) dx solves L v = -g on (0, 1).

theorem diffusionGenerator_integral_greenFunction {b a g : ℝ → ℝ} (h : IsRegularDiffusion b a)
    (hg : ContinuousOn g (Ioo 0 1))
    (hL : ∀ q ∈ Ioo (0 : ℝ) 1, IntervalIntegrable
      (fun x => scaleFunction b a x * g x / (a x * scaleDensity b a x)) volume 0 q)
    (hR : ∀ q ∈ Ioo (0 : ℝ) 1, IntervalIntegrable
      (fun x => (scaleFunction b a 1 - scaleFunction b a x) * g x / (a x * scaleDensity b a x))
      volume q 1)
    {p : ℝ} (hp : p ∈ Ioo (0 : ℝ) 1) :
    diffusionGenerator b a (fun q => ∫ x in (0 : ℝ)..1, greenFunction b a q x * g x) p = -g p
Uses 11 · Used by 1
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\) · Backward generator of a one-dimensional diffusion · Dirichlet Green's function of a one-dimensional diffusion · Scale density of a one-dimensional diffusion · Scale function of a one-dimensional diffusion
Proof usesContinuity of the scale density on \((0, 1)\) · Continuity of the scale function on \((0, 1)\) · Derivative of the scale density · Derivative of the scale function is the scale density · Scale function is positive at one · Positivity of the scale density
Used byConditional mean time to fixation, backward equation

TheoremDirichlet condition of the Green's function at zero#✓fully proved

Dirichlet condition at 0: ∫₀¹ G(0, x) g(x) dx = 0 (for every b, a, g).

theorem integral_greenFunction_zero_left (b a g : ℝ → ℝ) :
    ∫ x in (0 : ℝ)..1, greenFunction b a 0 x * g x = 0
Uses 4
Statement usesDirichlet Green's function of a one-dimensional diffusion
Proof usesScale density of a one-dimensional diffusion · Scale function of a one-dimensional diffusion · Scale function vanishes at zero

TheoremDirichlet condition of the Green's function at one#✓fully proved

Dirichlet condition at 1: ∫₀¹ G(1, x) g(x) dx = 0 (for every b, a, g).

theorem integral_greenFunction_one_left (b a g : ℝ → ℝ) :
    ∫ x in (0 : ℝ)..1, greenFunction b a 1 x * g x = 0
Uses 3
Statement usesDirichlet Green's function of a one-dimensional diffusion
Proof usesScale density of a one-dimensional diffusion · Scale function of a one-dimensional diffusion

Genic selection and dominance

TheoremWright–Fisher generator with genic selection as a general diffusion#✓fully proved

The general generator with drift σ x (1 - x) and variance x (1 - x) is the Wright–Fisher generator with genic selection.

theorem diffusionGenerator_wrightFisher (σ : ℝ) (u : ℝ → ℝ) :
    diffusionGenerator (fun x => σ * x * (1 - x)) (fun x => x * (1 - x)) u = generator σ u
Uses 2 · Used by 1
Statement usesBackward generator of a one-dimensional diffusion · Backward generator of the Wright–Fisher diffusion with selection
Used byKimura's formula as a corollary

TheoremWright–Fisher diffusion with genic selection is regular#✓fully proved

The Wright–Fisher diffusion with genic selection is regular.

theorem isRegularDiffusion_wrightFisher (σ : ℝ) :
    IsRegularDiffusion (fun x => σ * x * (1 - x)) (fun x => x * (1 - x))
Uses 1 · Used by 1
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\)
Used byKimura's formula as a corollary

TheoremScale density of the Wright–Fisher diffusion with genic selection#✓fully proved

The scale density of the Wright–Fisher diffusion with genic selection is e^{-2σy} on [0, 1].

theorem scaleDensity_wrightFisher (σ : ℝ) {y : ℝ} (hy : y ∈ Icc (0 : ℝ) 1) :
    scaleDensity (fun x => σ * x * (1 - x)) (fun x => x * (1 - x)) y = exp (-2 * σ * y)
Uses 1 · Used by 1
Statement usesScale density of a one-dimensional diffusion
Used byThe general Green kernel specializes to Kimura's sojourn density

TheoremKimura's formula as a corollary#✓fully proved

For genic selection the general scale-function ratio is kimuraFixation σ p on [0, 1].

theorem fixationProb_wrightFisher (σ : ℝ) {p : ℝ} (hp : p ∈ Icc (0 : ℝ) 1) :
    fixationProb (fun x => σ * x * (1 - x)) (fun x => x * (1 - x)) p = kimuraFixation σ p
Uses 14
Statement usesDirichlet ratio \(S(p)/S(1)\) of the scale function · Kimura's fixation probability
Proof usesContinuity of Kimura's fixation probability · Derivative of Kimura's fixation probability as a function · Backward generator of a one-dimensional diffusion · Wright–Fisher generator with genic selection as a general diffusion · Uniqueness of the scale-function ratio (Kimura 1962) · Backward generator of the Wright–Fisher diffusion with selection · Kimura (1962) · Derivative of Kimura's fixation probability at a point · Wright–Fisher diffusion with genic selection is regular · Kimura's fixation probability equals one at frequency one · Kimura's fixation probability vanishes at frequency zero · Slope constant of Kimura's fixation probability

TheoremGeneral Green's function agrees with the neutral Wright–Fisher one#✓fully proved

The general Green's function of the neutral Wright–Fisher diffusion (b = 0, a = x (1 - x)) is the neutral Green's function of Sojourn.lean for x ∈ (0, 1).

theorem greenFunction_neutral (p : ℝ) {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
    greenFunction (fun _ => 0) (fun x => x * (1 - x)) p x = neutralGreen p x
Uses 4 · Used by 1
Statement usesDirichlet Green's function of a one-dimensional diffusion · Neutral Wright–Fisher Green's function
Proof usesScale density of a one-dimensional diffusion · Scale function of a one-dimensional diffusion
Used byThe general h-transform specializes to Kimura–Ohta

DefinitionDrift of an allele under selection with dominance#✓fully proved

The drift 2 c x (1 - x) (h + (1 - 2h) x) of an allele at frequency x with genotype fitnesses 1, 1 + h s, 1 + s (for zero, one and two copies), c = N s, time in units of 2N generations (Kimura 1962). For h = 1/2 it is genic selection with σ = c.

noncomputable def dominanceDrift (c h x : ℝ) : ℝ :=
  2 * c * x * (1 - x) * (h + (1 - 2 * h) * x)
Used by 2
Used byKimura's scale-function ratio with dominance (Kimura 1962) · Diffusion with dominance is regular

TheoremDiffusion with dominance is regular#✓fully proved

The diffusion with dominance is regular.

theorem isRegularDiffusion_dominance (c h : ℝ) :
    IsRegularDiffusion (dominanceDrift c h) (fun x => x * (1 - x))
Uses 2
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\) · Drift of an allele under selection with dominance

TheoremKimura's scale-function ratio with dominance (Kimura 1962)#✓fully proved

With D = 2h - 1, for p ∈ [0, 1], u(p) = ∫₀^p e^{-2cDx(1-x) - 2cx} dx / ∫₀¹ e^{-2cDx(1-x) - 2cx} dx.

theorem fixationProb_dominance (c h : ℝ) {p : ℝ} (hp : p ∈ Icc (0 : ℝ) 1) :
    fixationProb (dominanceDrift c h) (fun x => x * (1 - x)) p =
      (∫ x in (0 : ℝ)..p, exp (-2 * c * (2 * h - 1) * x * (1 - x) - 2 * c * x)) /
        ∫ x in (0 : ℝ)..1, exp (-2 * c * (2 * h - 1) * x * (1 - x) - 2 * c * x)
Uses 4
Statement usesDrift of an allele under selection with dominance · Dirichlet ratio \(S(p)/S(1)\) of the scale function
Proof usesScale density of a one-dimensional diffusion · Scale function of a one-dimensional diffusion

Conditional fixation and loss times

DefinitionSojourn density conditioned on fixation#✓fully proved

The sojourn density conditioned on fixation, the Doob h-transform of the Green's function by the fixation probability u: G(p, x) u(x) / u(p) (Kimura–Ohta 1969; Ewens 2004, Chapter 4). At p = 0 it is the junk value 0.

noncomputable def conditionalGreen (b a : ℝ → ℝ) (p x : ℝ) : ℝ :=
  greenFunction b a p x * fixationProb b a x / fixationProb b a p
Uses 2 · Used by 2
Statement usesDirichlet ratio \(S(p)/S(1)\) of the scale function · Dirichlet Green's function of a one-dimensional diffusion
Used byConditional mean time to fixation, backward equation · The general h-transform specializes to Kimura–Ohta

TheoremConditional mean time to fixation, backward equation#✓fully proved

Under the hypotheses of diffusionGenerator_integral_greenFunction for g = u (the fixation probability), the function w(q) = u(q) · ∫₀¹ G*(q, x) dx, with G* the conditional sojourn density, solves L w = -u on (0, 1) (Ewens 2004, Chapter 4).

theorem diffusionGenerator_mul_integral_conditionalGreen {b a : ℝ → ℝ}
    (h : IsRegularDiffusion b a)
    (hL : ∀ q ∈ Ioo (0 : ℝ) 1, IntervalIntegrable (fun x => scaleFunction b a x *
      fixationProb b a x / (a x * scaleDensity b a x)) volume 0 q)
    (hR : ∀ q ∈ Ioo (0 : ℝ) 1, IntervalIntegrable (fun x =>
      (scaleFunction b a 1 - scaleFunction b a x) * fixationProb b a x /
        (a x * scaleDensity b a x)) volume q 1)
    {p : ℝ} (hp : p ∈ Ioo (0 : ℝ) 1) :
    diffusionGenerator b a
      (fun q => fixationProb b a q * ∫ x in (0 : ℝ)..1, conditionalGreen b a q x) p =
      -fixationProb b a p
Uses 12
Statement usesStanding regularity hypotheses for a diffusion on \((0, 1)\) · Sojourn density conditioned on fixation · Backward generator of a one-dimensional diffusion · Dirichlet ratio \(S(p)/S(1)\) of the scale function · Scale density of a one-dimensional diffusion · Scale function of a one-dimensional diffusion
Proof usesContinuity of the scale function on \((0, 1)\) · Scale function is positive at one · Scale function is strictly increasing · Green's representation (Ewens 2004, Chapter 4; Karlin–Taylor 1981, Chapter 15) · Dirichlet Green's function of a one-dimensional diffusion · Scale function vanishes at zero

DefinitionNeutral conditional mean time to fixation#✓fully proved

The neutral conditional mean time to fixation t̄₁(p) = -2 (1 - p) log (1 - p) / p, in units of 2N generations (Kimura–Ohta 1969). It is meaningful for p ∈ (0, 1); at p = 0 the division gives the junk value 0 (the limit is 2, see tendsto_neutralFixationTime_zero).

noncomputable def neutralFixationTime (p : ℝ) : ℝ :=
  -2 * (1 - p) * log (1 - p) / p
Used by 7
Used byBackward equation for the neutral conditional fixation time · The general h-transform specializes to Kimura–Ohta · Neutral conditional fixation time as an h-transformed sojourn integral · Neutral conditional loss time · Total expectation · Neutral loss time equals fixation time at \(1 - p\) · t̄₁(0⁺) = 2

DefinitionNeutral conditional mean time to loss#✓fully proved

The neutral conditional mean time to loss t̄₀(p) = -2 p log p / (1 - p), in units of 2N generations (Kimura–Ohta 1969). It is meaningful for p ∈ (0, 1).

noncomputable def neutralLossTime (p : ℝ) : ℝ :=
  -2 * p * log p / (1 - p)
Used by 3
Used byNeutral conditional loss time · Total expectation · Neutral loss time equals fixation time at \(1 - p\)

TheoremNeutral loss time equals fixation time at \(1 - p\)#✓fully proved

Loss of an allele at frequency p is fixation of the other allele at 1 - p.

theorem neutralLossTime_eq (p : ℝ) : neutralLossTime p = neutralFixationTime (1 - p)
Uses 2 · Used by 1
Statement usesNeutral conditional mean time to fixation · Neutral conditional mean time to loss
Used byNeutral conditional loss time

TheoremNeutral conditional fixation time as an h-transformed sojourn integral#✓fully proved

For p ∈ (0, 1), ∫₀¹ G(p, x) · x / p dx = -2 (1 - p) log (1 - p) / p, with G the neutral Green's function and u(x) = x the neutral fixation probability.

theorem integral_neutralGreen_mul_div {p : ℝ} (hp : p ∈ Ioo (0 : ℝ) 1) :
    ∫ x in (0 : ℝ)..1, neutralGreen p x * (x / p) = neutralFixationTime p
Uses 2 · Used by 2
Statement usesNeutral conditional mean time to fixation · Neutral Wright–Fisher Green's function
Used byThe general h-transform specializes to Kimura–Ohta · Neutral conditional loss time

TheoremNeutral conditional loss time#✓fully proved

For p ∈ (0, 1), ∫₀¹ G(p, x) · (1 - x) / (1 - p) dx = -2 p log p / (1 - p).

theorem integral_neutralGreen_mul_one_sub_div {p : ℝ} (hp : p ∈ Ioo (0 : ℝ) 1) :
    ∫ x in (0 : ℝ)..1, neutralGreen p x * ((1 - x) / (1 - p)) = neutralLossTime p
Uses 5
Statement usesNeutral Wright–Fisher Green's function · Neutral conditional mean time to loss
Proof usesNeutral conditional fixation time as an h-transformed sojourn integral · Neutral conditional mean time to fixation · Neutral loss time equals fixation time at \(1 - p\)

TheoremThe general h-transform specializes to Kimura–Ohta#✓fully proved

For the neutral Wright–Fisher diffusion (b = 0, a = x (1 - x)) and p ∈ (0, 1), the total conditional sojourn time ∫₀¹ G(p, x) u(x) / u(p) dx is -2 (1 - p) log (1 - p) / p.

theorem integral_conditionalGreen_neutral {p : ℝ} (hp : p ∈ Ioo (0 : ℝ) 1) :
    ∫ x in (0 : ℝ)..1, conditionalGreen (fun _ => 0) (fun x => x * (1 - x)) p x =
      neutralFixationTime p
Uses 9
Statement usesSojourn density conditioned on fixation · Neutral conditional mean time to fixation
Proof usesDirichlet ratio \(S(p)/S(1)\) of the scale function · Dirichlet Green's function of a one-dimensional diffusion · General Green's function agrees with the neutral Wright–Fisher one · Neutral conditional fixation time as an h-transformed sojourn integral · Neutral Wright–Fisher Green's function · Scale density of a one-dimensional diffusion · Scale function of a one-dimensional diffusion

TheoremBackward equation for the neutral conditional fixation time#✓fully proved

The neutral conditional fixation time satisfies the conditioned backward equation L_0 (p · t̄₁(p)) = -p on (0, 1).

theorem generator_mul_neutralFixationTime {p : ℝ} (hp : p ∈ Ioo (0 : ℝ) 1) :
    generator 0 (fun q => q * neutralFixationTime q) p = -p
Uses 2
Statement usesBackward generator of the Wright–Fisher diffusion with selection · Neutral conditional mean time to fixation

Theoremt̄₁(0⁺) = 2#✓fully proved

A new neutral mutation that is destined to fix takes on average 2 units (4N generations) to do so (Kimura–Ohta 1969).

theorem tendsto_neutralFixationTime_zero :
    Tendsto neutralFixationTime (𝓝[>] 0) (𝓝 2)
Uses 1
Statement usesNeutral conditional mean time to fixation

TheoremTotal expectation#✓fully proved

For p ∈ (0, 1), p · t̄₁(p) + (1 - p) · t̄₀(p) = -2 (p log p + (1 - p) log (1 - p)), the unconditional mean absorption time.

theorem mul_neutralFixationTime_add_mul_neutralLossTime {p : ℝ} (hp : p ∈ Ioo (0 : ℝ) 1) :
    p * neutralFixationTime p + (1 - p) * neutralLossTime p = meanAbsorptionTime p
Uses 3
Statement usesKimura–Ohta mean absorption time of a neutral allele · Neutral conditional mean time to fixation · Neutral conditional mean time to loss

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.