Wright–Fisher diffusion
DefinitionBackward generator of the Wright–Fisher diffusion with selection#✓fully proved
The backward generator of the Wright–Fisher diffusion with genic selection, time in units
of 2N generations and scaled selection coefficient σ = 2Ns:
(L_σ u)(x) = x (1 - x) / 2 · u''(x) + σ x (1 - x) · u'(x).
noncomputable def generator (σ : ℝ) (u : ℝ → ℝ) (x : ℝ) : ℝ :=
x * (1 - x) / 2 * deriv (deriv u) x + σ * x * (1 - x) * deriv u xUsed by 24
DefinitionKimura's fixation probability#✓fully proved
Kimura's fixation probability of an allele at initial frequency x with scaled selection
coefficient σ = 2Ns: (1 - e^{-2σx}) / (1 - e^{-2σ}), and x in the neutral case.
noncomputable def kimuraFixation (σ x : ℝ) : ℝ :=
if σ = 0 then x else (1 - exp (-2 * σ * x)) / (1 - exp (-2 * σ))Used by 53
1 · Boundary normalization at 0 · Kimura's formula as a corollary · Loss probability from the stationary ancestral selection graph · Loss probability in Kimura's fixation formula · Continuity of Kimura's fixation probability · Derivative of Kimura's fixation probability as a function · Uniqueness of the fixation probability · Uniqueness of the fixation probability (Kimura 1962) · Kimura (1962) · Derivative of Kimura's fixation probability at a point · Kimura's fixation probability is at most one · Kimura's fixation probability lies in the unit interval · Neutral fixation probability equals the initial frequency · Nonnegativity of Kimura's fixation probability · Kimura's fixation probability equals one at frequency one · Kimura's fixation probability vanishes at frequency zero · Advantageous alleles fix more often than their initial frequency · Closed form of Kimura's fixation probability · Diffusion limit of the Moran fixation probabilityDefinitionKimura–Ohta mean absorption time of a neutral allele#✓fully proved
Kimura–Ohta mean time to absorption (loss or fixation) of a neutral allele at frequency x,
in units of 2N generations: -2 (x log x + (1 - x) log (1 - x)). In generations this is
-4N (x ln x + (1 - x) ln (1 - x)).
Used by 7
DefinitionWright's stationary density of the Wright–Fisher diffusion#✓fully proved
Wright's (unnormalized) stationary density of the Wright–Fisher diffusion with scaled
mutation rates α (towards the allele) and β (away from it):
x ^ (2α - 1) (1 - x) ^ (2β - 1) (real powers).
noncomputable def wrightDensity (α β x : ℝ) : ℝ :=
x ^ (2 * α - 1) * (1 - x) ^ (2 * β - 1)Used by 7
DefinitionSlope constant of Kimura's fixation probability#✓fully proved
The constant K σ such that (kimuraFixation σ)' x = K σ · e^{-2σx}:
1 if σ = 0, and 2σ / (1 - e^{-2σ}) otherwise.
noncomputable def kimuraSlope (σ : ℝ) : ℝ :=
if σ = 0 then 1 else 2 * σ / (1 - exp (-2 * σ))Used by 29
TheoremDenominator of Kimura's formula is nonzero#✓fully proved
For σ ≠ 0 the denominator 1 - e^{-2σ} of Kimura's formula does not vanish.
theorem one_sub_exp_ne_zero {σ : ℝ} (hσ : σ ≠ 0) : 1 - exp (-2 * σ) ≠ 0TheoremKimura's fixation probability vanishes at frequency zero#✓fully proved
An allele that is absent is never fixed.
@[simp]
theorem kimuraFixation_zero_right (σ : ℝ) : kimuraFixation σ 0 = 0noncomputable def kimuraFixation (σ x : ℝ) : ℝ :=
if σ = 0 then x else (1 - exp (-2 * σ * x)) / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:98
Uses 1 · Used by 13
1 · Kimura's formula as a corollary · Uniqueness of the fixation probability (Kimura 1962)TheoremKimura's fixation probability equals one at frequency one#✓fully proved
An allele that is already fixed stays fixed.
@[simp]
theorem kimuraFixation_one_right (σ : ℝ) : kimuraFixation σ 1 = 1noncomputable def kimuraFixation (σ x : ℝ) : ℝ :=
if σ = 0 then x else (1 - exp (-2 * σ * x)) / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:98
Uses 2 · Used by 12
0 · Kimura's formula as a corollary · Uniqueness of the fixation probability (Kimura 1962)TheoremNeutral fixation probability equals the initial frequency#✓fully proved
Neutral case: the fixation probability equals the initial frequency.
@[simp]
theorem kimuraFixation_neutral (x : ℝ) : kimuraFixation 0 x = xnoncomputable def kimuraFixation (σ x : ℝ) : ℝ :=
if σ = 0 then x else (1 - exp (-2 * σ * x)) / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:98
Uses 1 · Used by 8
TheoremSlope constant of Kimura's formula is nonzero#✓fully proved
The slope constant of Kimura's formula never vanishes.
theorem kimuraSlope_ne_zero (σ : ℝ) : kimuraSlope σ ≠ 0noncomputable def kimuraSlope (σ : ℝ) : ℝ :=
if σ = 0 then 1 else 2 * σ / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:115
Uses 2 · Used by 2
TheoremDerivative of Kimura's fixation probability at a point#✓fully proved
The derivative of Kimura's fixation probability: u'(x) = K σ · e^{-2σx}.
theorem hasDerivAt_kimuraFixation (σ x : ℝ) :
HasDerivAt (kimuraFixation σ) (kimuraSlope σ * exp (-2 * σ * x)) xnoncomputable def kimuraFixation (σ x : ℝ) : ℝ :=
if σ = 0 then x else (1 - exp (-2 * σ * x)) / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:98
noncomputable def kimuraSlope (σ : ℝ) : ℝ :=
if σ = 0 then 1 else 2 * σ / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:115
Uses 3 · Used by 15
TheoremContinuity of Kimura's fixation probability#✓fully proved
Kimura's fixation probability is continuous in the initial frequency.
theorem continuous_kimuraFixation (σ : ℝ) : Continuous (kimuraFixation σ)noncomputable def kimuraFixation (σ x : ℝ) : ℝ :=
if σ = 0 then x else (1 - exp (-2 * σ * x)) / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:98
Uses 3 · Used by 11
1 · Boundary normalization at 0 · Kimura's formula as a corollary · Uniqueness of the fixation probability (Kimura 1962)TheoremDerivative of Kimura's fixation probability as a function#✓fully proved
The derivative of Kimura's fixation probability, as a function.
theorem deriv_kimuraFixation (σ : ℝ) :
deriv (kimuraFixation σ) = fun y => kimuraSlope σ * exp (-2 * σ * y)noncomputable def kimuraFixation (σ x : ℝ) : ℝ :=
if σ = 0 then x else (1 - exp (-2 * σ * x)) / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:98
noncomputable def kimuraSlope (σ : ℝ) : ℝ :=
if σ = 0 then 1 else 2 * σ / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:115
Uses 3 · Used by 7
TheoremKimura (1962)#✓fully proved
The fixation probability solves the backward equation
x (1 - x) / 2 · u'' + σ x (1 - x) · u' = 0 (everywhere).
theorem generator_kimuraFixation (σ x : ℝ) : generator σ (kimuraFixation σ) x = 0noncomputable def generator (σ : ℝ) (u : ℝ → ℝ) (x : ℝ) : ℝ :=
x * (1 - x) / 2 * deriv (deriv u) x + σ * x * (1 - x) * deriv u xMathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:93
noncomputable def kimuraFixation (σ x : ℝ) : ℝ :=
if σ = 0 then x else (1 - exp (-2 * σ * x)) / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:98
Uses 4 · Used by 4
TheoremUniqueness of the fixation probability (Kimura 1962)#✓fully proved
If u is continuous on [0, 1],
differentiable on (0, 1) with derivative u' differentiable on (0, 1), solves the backward
equation L_σ u = 0 on (0, 1), and satisfies u 0 = 0, u 1 = 1, then u is Kimura's
fixation probability on [0, 1].
theorem eq_kimuraFixation_of_generator_eq_zero {σ : ℝ} {u : ℝ → ℝ}
(hcont : ContinuousOn u (Icc 0 1)) (hdiff : DifferentiableOn ℝ u (Ioo 0 1))
(hdiff' : DifferentiableOn ℝ (deriv u) (Ioo 0 1))
(hgen : ∀ x ∈ Ioo (0 : ℝ) 1, generator σ u x = 0) (h0 : u 0 = 0) (h1 : u 1 = 1) :
∀ x ∈ Icc (0 : ℝ) 1, u x = kimuraFixation σ xnoncomputable def generator (σ : ℝ) (u : ℝ → ℝ) (x : ℝ) : ℝ :=
x * (1 - x) / 2 * deriv (deriv u) x + σ * x * (1 - x) * deriv u xMathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:93
noncomputable def kimuraFixation (σ x : ℝ) : ℝ :=
if σ = 0 then x else (1 - exp (-2 * σ * x)) / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:98
Uses 8 · Used by 2
TheoremUniqueness of the fixation probability#✓fully proved
Uniqueness of the fixation probability, C² form: a function continuous on [0, 1],
C² on (0, 1), solving L_σ u = 0 on (0, 1) with u 0 = 0, u 1 = 1 equals Kimura's
fixation probability on [0, 1].
theorem eq_kimuraFixation_of_contDiffOn {σ : ℝ} {u : ℝ → ℝ}
(hcont : ContinuousOn u (Icc 0 1)) (hu : ContDiffOn ℝ 2 u (Ioo 0 1))
(hgen : ∀ x ∈ Ioo (0 : ℝ) 1, generator σ u x = 0) (h0 : u 0 = 0) (h1 : u 1 = 1) :
∀ x ∈ Icc (0 : ℝ) 1, u x = kimuraFixation σ xnoncomputable def generator (σ : ℝ) (u : ℝ → ℝ) (x : ℝ) : ℝ :=
x * (1 - x) / 2 * deriv (deriv u) x + σ * x * (1 - x) * deriv u xMathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:93
noncomputable def kimuraFixation (σ x : ℝ) : ℝ :=
if σ = 0 then x else (1 - exp (-2 * σ * x)) / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:98
TheoremNonnegativity of Kimura's fixation probability#✓fully proved
Kimura's fixation probability is nonnegative at nonnegative frequencies, for every
selection coefficient σ.
theorem kimuraFixation_nonneg (σ : ℝ) {y : ℝ} (hy : 0 ≤ y) : 0 ≤ kimuraFixation σ ynoncomputable def kimuraFixation (σ x : ℝ) : ℝ :=
if σ = 0 then x else (1 - exp (-2 * σ * x)) / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:98
Uses 1 · Used by 3
TheoremKimura's fixation probability is at most one#✓fully proved
Kimura's fixation probability is at most 1 at frequencies y ≤ 1, for every selection
coefficient σ.
theorem kimuraFixation_le_one (σ : ℝ) {y : ℝ} (hy : y ≤ 1) : kimuraFixation σ y ≤ 1noncomputable def kimuraFixation (σ x : ℝ) : ℝ :=
if σ = 0 then x else (1 - exp (-2 * σ * x)) / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:98
Uses 1 · Used by 3
TheoremKimura's fixation probability lies in the unit interval#✓fully proved
Kimura's fixation probability is a probability on [0, 1].
theorem kimuraFixation_mem_Icc (σ : ℝ) {x : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) :
kimuraFixation σ x ∈ Icc (0 : ℝ) 1noncomputable def kimuraFixation (σ x : ℝ) : ℝ :=
if σ = 0 then x else (1 - exp (-2 * σ * x)) / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:98
Uses 3 · Used by 3
TheoremAdvantageous alleles fix more often than their initial frequency#✓fully proved
Advantageous alleles (σ > 0) are fixed with probability strictly larger than their
initial frequency x ∈ (0, 1).
theorem lt_kimuraFixation {σ x : ℝ} (hσ : 0 < σ) (hx : x ∈ Ioo (0 : ℝ) 1) :
x < kimuraFixation σ xnoncomputable def kimuraFixation (σ x : ℝ) : ℝ :=
if σ = 0 then x else (1 - exp (-2 * σ * x)) / (1 - exp (-2 * σ))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:98
Uses 1
TheoremNeutral mean absorption time vanishes at frequency zero#✓fully proved
The neutral mean absorption time vanishes at x = 0.
@[simp]
theorem meanAbsorptionTime_zero : meanAbsorptionTime 0 = 0noncomputable def meanAbsorptionTime (x : ℝ) : ℝ :=
-2 * (x * log x + (1 - x) * log (1 - x))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:104
Uses 1 · Used by 1
TheoremNeutral mean absorption time vanishes at frequency one#✓fully proved
The neutral mean absorption time vanishes at x = 1.
@[simp]
theorem meanAbsorptionTime_one : meanAbsorptionTime 1 = 0noncomputable def meanAbsorptionTime (x : ℝ) : ℝ :=
-2 * (x * log x + (1 - x) * log (1 - x))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:104
Uses 1 · Used by 1
TheoremDerivative of the neutral mean absorption time#✓fully proved
On (0, 1), T'(x) = -2 (log x - log (1 - x)).
theorem hasDerivAt_meanAbsorptionTime {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
HasDerivAt meanAbsorptionTime (-2 * (log x - log (1 - x))) xnoncomputable def meanAbsorptionTime (x : ℝ) : ℝ :=
-2 * (x * log x + (1 - x) * log (1 - x))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:104
Uses 1 · Used by 1
TheoremKimura–Ohta (1969)#✓fully proved
The neutral mean absorption time solves L_0 T = -1 on (0, 1).
theorem generator_meanAbsorptionTime {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
generator 0 meanAbsorptionTime x = -1noncomputable def generator (σ : ℝ) (u : ℝ → ℝ) (x : ℝ) : ℝ :=
x * (1 - x) / 2 * deriv (deriv u) x + σ * x * (1 - x) * deriv u xMathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:93
noncomputable def meanAbsorptionTime (x : ℝ) : ℝ :=
-2 * (x * log x + (1 - x) * log (1 - x))MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:104
TheoremDecay of heterozygosity#✓fully proved
H(x) = 2x(1 - x) is an eigenfunction of the neutral
generator with eigenvalue -1, so E[H_t] = H_0 e^{-t} (time in units of 2N generations).
theorem generator_heterozygosity (x : ℝ) :
generator 0 (fun y => 2 * y * (1 - y)) x = -(2 * x * (1 - x))noncomputable def generator (σ : ℝ) (u : ℝ → ℝ) (x : ℝ) : ℝ :=
x * (1 - x) / 2 * deriv (deriv u) x + σ * x * (1 - x) * deriv u xMathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:93
Uses 1
TheoremMoment duality with Kingman's coalescent#✓fully proved
Moment duality with Kingman's coalescent at generator level: the neutral generator maps
y ↦ y ^ n to C(n, 2) (x ^ (n - 1) - x ^ n), which is the generator of the block-counting
process (jumps n → n - 1 at rate C(n, 2)) applied to n ↦ x ^ n.
theorem generator_pow (n : ℕ) (x : ℝ) :
generator 0 (fun y => y ^ n) x = (n.choose 2 : ℝ) * (x ^ (n - 1) - x ^ n)noncomputable def generator (σ : ℝ) (u : ℝ → ℝ) (x : ℝ) : ℝ :=
x * (1 - x) / 2 * deriv (deriv u) x + σ * x * (1 - x) * deriv u xMathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:93
Uses 1 · Used by 1
TheoremWright's stationary density (zero-flux form)#✓fully proved
On (0, 1), with infinitesimal variance
a(x) = x (1 - x) and mutation drift b(x) = α (1 - x) - β x, Wright's density
π(x) = x ^ (2α - 1) (1 - x) ^ (2β - 1) satisfies (a π)' = 2 b π, i.e. the stationary
forward (Fokker–Planck) equation ½ (a π)' - b π = 0 with zero probability flux.
theorem deriv_flux_wrightDensity (α β : ℝ) {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
deriv (fun y => y * (1 - y) * wrightDensity α β y) x =
2 * (α * (1 - x) - β * x) * wrightDensity α β xnoncomputable def wrightDensity (α β x : ℝ) : ℝ :=
x ^ (2 * α - 1) * (1 - x) ^ (2 * β - 1)MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:110
Uses 1 · Used by 1
TheoremNormalization of Wright's density#✓fully proved
For α, β > 0 the stationary density integrates to
the Beta function B(2α, 2β) = Γ(2α) Γ(2β) / Γ(2α + 2β), so
wrightDensity α β x / B(2α, 2β) is the Beta(2α, 2β) probability density on (0, 1).
theorem integral_wrightDensity {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) :
∫ x in (0 : ℝ)..1, wrightDensity α β x =
Gamma (2 * α) * Gamma (2 * β) / Gamma (2 * α + 2 * β)noncomputable def wrightDensity (α β x : ℝ) : ℝ :=
x ^ (2 * α - 1) * (1 - x) ^ (2 * β - 1)MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:110
Uses 1 · Used by 1
TheoremWright's density has finite positive total mass#✓fully proved
For α, β > 0 Wright's density has a finite, positive total mass on (0, 1).
theorem integral_wrightDensity_pos {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) :
0 < ∫ x in (0 : ℝ)..1, wrightDensity α β xnoncomputable def wrightDensity (α β x : ℝ) : ℝ :=
x ^ (2 * α - 1) * (1 - x) ^ (2 * β - 1)MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:110
Uses 2 · Used by 1
TheoremIntegrability of Wright's density on the unit interval#✓fully proved
For α, β > 0 Wright's density is integrable on [0, 1].
theorem intervalIntegrable_wrightDensity {α β : ℝ} (hα : 0 < α) (hβ : 0 < β) :
IntervalIntegrable (wrightDensity α β) MeasureTheory.volume 0 1noncomputable def wrightDensity (α β x : ℝ) : ℝ :=
x ^ (2 * α - 1) * (1 - x) ^ (2 * β - 1)MathlibExt/Biology/PopulationGenetics/Diffusion/WrightFisher.lean:110
Uses 2 · Used by 1
TheoremHeterozygosity decay in one Wright–Fisher generation#✓fully proved
If the number X of copies of an
allele among M gene copies (M = 2N for diploids) is Binomial(M, x), then the new frequency
p' = X / M satisfies E[2 p' (1 - p')] = (1 - 1/M) · 2x(1 - x).
theorem integral_binomial_heterozygosity (M : ℕ) (hM : M ≠ 0) (x : unitInterval) :
∫ k, 2 * ((k : ℝ) / M) * (1 - (k : ℝ) / M) ∂(ProbabilityTheory.binomial M x) =
(1 - 1 / (M : ℝ)) * (2 * x * (1 - x))Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.