Fixation and absorption in the Wright–Fisher diffusion

DefinitionMartingale problem for the Wright–Fisher diffusion#✓fully proved

X solves the martingale problem for the Wright–Fisher diffusion with scaled genic selection coefficient σ = 2Ns (time in units of 2N generations) with respect to the filtration ℱ and the measure μ: X takes values in [0, 1], has continuous paths, is adapted to ℱ, and for every C² function f the process f (X t) - f (X 0) - ∫₀ᵗ generator σ f (X s) ds is an ℱ-martingale.

def IsWrightFisherSolution (σ : ℝ) (ℱ : Filtration ℝ≥0 mΩ) (μ : Measure Ω)
    (X : ℝ≥0 → Ω → ℝ) : Prop :=
  (∀ t ω, X t ω ∈ Set.Icc (0 : ℝ) 1) ∧ (∀ ω, Continuous fun t => X t ω) ∧
    StronglyAdapted ℱ X ∧
    ∀ f : ℝ → ℝ, ContDiff ℝ 2 f →
      Martingale (fun t ω => f (X t ω) - f (X 0 ω) -
        ∫ s in (0 : ℝ)..(t : ℝ), generator σ f (X (Real.toNNReal s) ω)) ℱ μ

noncomputable def generator (σ : ℝ) (u : ℝ → ℝ) (x : ℝ) : ℝ :=
  x * (1 - x) / 2 * deriv (deriv u) x + σ * x * (1 - x) * deriv u x

MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:93

Uses 1 · Used by 3

Statement usesBackward generator of the Wright–Fisher diffusion with selection

Used byAbsorption in finite time · Kimura–Ohta mean absorption time, process form · Kimura's fixation probability, process form

DefinitionAbsorption time of a frequency path#✓fully proved

The absorption time of a [0, 1]-valued path: the first time it is at 0 or 1 (the infimum of the empty set is 0 in ℝ≥0; the path is absorbed almost surely, see ae_exists_absorbed).

noncomputable def absorptionTime (X : ℝ≥0 → Ω → ℝ) (ω : Ω) : ℝ≥0 :=
  sInf {t | X t ω = 0 ∨ X t ω = 1}

Used by 1

Used byKimura–Ohta mean absorption time, process form

6 fully proved2 ready to state

Analytic lemmas

TheoremKimura's fixation probability is twice continuously differentiable#✓fully proved

Kimura's fixation probability is a C² function of the initial frequency on all of ℝ.

theorem _root_.MathlibExt.Biology.PopulationGenetics.Diffusion.contDiff_kimuraFixation
    (σ : ℝ) : ContDiff ℝ 2 (kimuraFixation σ)

Uses 2 · Used by 3

Statement usesKimura's fixation probability

Proof usesNeutral fixation probability equals the initial frequency

Used byAbsorption in finite time · Kimura–Ohta mean absorption time, process form · Kimura's fixation probability, process form

TheoremPositivity of Kimura's slope constant#●ready to state

The slope constant of Kimura's formula is positive.

TheoremStrict monotonicity of Kimura's fixation probability#●ready to state

Kimura's fixation probability is strictly increasing in the initial frequency.

Main results

TheoremAbsorption in finite time#✓fully proved

A solution of the Wright–Fisher martingale problem is almost surely absorbed: from some time on it is constantly 0 or constantly 1.

theorem ae_exists_absorbed {σ : ℝ} {ℱ : Filtration ℝ≥0 mΩ} {μ : Measure Ω}
    [IsProbabilityMeasure μ] {X : ℝ≥0 → Ω → ℝ} (hX : IsWrightFisherSolution σ ℱ μ X) :
    ∀ᵐ ω ∂μ, ∃ t₀ : ℝ≥0, (∀ t ≥ t₀, X t ω = 0) ∨ (∀ t ≥ t₀, X t ω = 1)

def IsWrightFisherSolution (σ : ℝ) (ℱ : Filtration ℝ≥0 mΩ) (μ : Measure Ω)
    (X : ℝ≥0 → Ω → ℝ) : Prop :=
  (∀ t ω, X t ω ∈ Set.Icc (0 : ℝ) 1) ∧ (∀ ω, Continuous fun t => X t ω) ∧
    StronglyAdapted ℱ X ∧
    ∀ f : ℝ → ℝ, ContDiff ℝ 2 f →
      Martingale (fun t ω => f (X t ω) - f (X 0 ω) -
        ∫ s in (0 : ℝ)..(t : ℝ), generator σ f (X (Real.toNNReal s) ω)) ℱ μ

MathlibExt/Biology/PopulationGenetics/Diffusion/KimuraFixationProcess.lean:94

Sources

Ethier & Kurtz (1986), ch. 10; Karlin & Taylor (1981), ch. 15. Proves the deferred entry ae_exists_absorbed.

Uses 12 · Used by 2

Statement usesMartingale problem for the Wright–Fisher diffusion

Used byKimura–Ohta mean absorption time, process form · Kimura's fixation probability, process form

TheoremKimura's fixation probability, process form#✓fully proved

For a solution of the Wright–Fisher martingale problem with scaled selection coefficient σ = 2Ns started at frequency x, the probability that the allele is eventually fixed is (1 - e^{-2σx}) / (1 - e^{-2σ}) (x when σ = 0).

theorem measureReal_fixation {σ x : ℝ} {ℱ : Filtration ℝ≥0 mΩ} {μ : Measure Ω}
    [IsProbabilityMeasure μ] {X : ℝ≥0 → Ω → ℝ} (hX : IsWrightFisherSolution σ ℱ μ X)
    (hX0 : ∀ᵐ ω ∂μ, X 0 ω = x) :
    μ.real {ω | ∃ t₀ : ℝ≥0, ∀ t ≥ t₀, X t ω = 1} = kimuraFixation σ x

def IsWrightFisherSolution (σ : ℝ) (ℱ : Filtration ℝ≥0 mΩ) (μ : Measure Ω)
    (X : ℝ≥0 → Ω → ℝ) : Prop :=
  (∀ t ω, X t ω ∈ Set.Icc (0 : ℝ) 1) ∧ (∀ ω, Continuous fun t => X t ω) ∧
    StronglyAdapted ℱ X ∧
    ∀ f : ℝ → ℝ, ContDiff ℝ 2 f →
      Martingale (fun t ω => f (X t ω) - f (X 0 ω) -
        ∫ s in (0 : ℝ)..(t : ℝ), generator σ f (X (Real.toNNReal s) ω)) ℱ μ

MathlibExt/Biology/PopulationGenetics/Diffusion/KimuraFixationProcess.lean:94

noncomputable def kimuraFixation (σ x : ℝ) : ℝ :=
  if σ = 0 then x else (1 - exp (-2 * σ * x)) / (1 - exp (-2 * σ))

MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:98

Sources

Kimura (1962); Ewens (2004), ch. 4. Proves the deferred entry measureReal_fixation.

Uses 10

Statement usesMartingale problem for the Wright–Fisher diffusion · Kimura's fixation probability

Proof usesAbsorption in finite time · Kimura's fixation probability is twice continuously differentiable · Continuity of Kimura's fixation probability · Backward generator of the Wright–Fisher diffusion with selection · Kimura (1962) · Kimura's fixation probability lies in the unit interval · Kimura's fixation probability equals one at frequency one · Kimura's fixation probability vanishes at frequency zero

TheoremKimura–Ohta mean absorption time, process form#✓fully proved

For a solution of the neutral Wright–Fisher martingale problem started at frequency x, the expected time to loss or fixation, in units of 2N generations, is -2 (x log x + (1 - x) log (1 - x)).

theorem integral_absorptionTime {x : ℝ} {ℱ : Filtration ℝ≥0 mΩ} {μ : Measure Ω}
    [IsProbabilityMeasure μ] {X : ℝ≥0 → Ω → ℝ} (hX : IsWrightFisherSolution 0 ℱ μ X)
    (hX0 : ∀ᵐ ω ∂μ, X 0 ω = x) :
    Integrable (fun ω => (absorptionTime X ω : ℝ)) μ ∧
      ∫ ω, (absorptionTime X ω : ℝ) ∂μ = meanAbsorptionTime x

def IsWrightFisherSolution (σ : ℝ) (ℱ : Filtration ℝ≥0 mΩ) (μ : Measure Ω)
    (X : ℝ≥0 → Ω → ℝ) : Prop :=
  (∀ t ω, X t ω ∈ Set.Icc (0 : ℝ) 1) ∧ (∀ ω, Continuous fun t => X t ω) ∧
    StronglyAdapted ℱ X ∧
    ∀ f : ℝ → ℝ, ContDiff ℝ 2 f →
      Martingale (fun t ω => f (X t ω) - f (X 0 ω) -
        ∫ s in (0 : ℝ)..(t : ℝ), generator σ f (X (Real.toNNReal s) ω)) ℱ μ

MathlibExt/Biology/PopulationGenetics/Diffusion/KimuraFixationProcess.lean:94

noncomputable def absorptionTime (X : ℝ≥0 → Ω → ℝ) (ω : Ω) : ℝ≥0 :=
  sInf {t | X t ω = 0 ∨ X t ω = 1}

MathlibExt/Biology/PopulationGenetics/Diffusion/KimuraFixationProcess.lean:105

noncomputable def meanAbsorptionTime (x : ℝ) : ℝ :=
  -2 * (x * log x + (1 - x) * log (1 - x))

MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:104

Sources

Kimura & Ohta (1969); Ewens (2004), ch. 4. Proves the deferred entry integral_absorptionTime.

Uses 18

Statement usesMartingale problem for the Wright–Fisher diffusion · Absorption time of a frequency path · Kimura–Ohta mean absorption time of a neutral allele

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.