Allele age and the Maruyama effect

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

The slope constant of Kimura's formula is positive.

TheoremKimura's fixation probability is strictly increasing#●ready to state

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

TheoremPositivity of Kimura's fixation probability#✓fully proved

An allele present at positive frequency has positive fixation probability.

theorem kimuraFixation_pos (σ : ℝ) {x : ℝ} (hx : 0 < x) : 0 < kimuraFixation σ x
Uses 4 · Used by 3
Statement usesKimura's fixation probability
Proof usesDerivative of Kimura's fixation probability as a function · Kimura's fixation probability vanishes at frequency zero · Slope constant of Kimura's fixation probability
Used byClosed form above the current frequency · Closed form below the current frequency · Mean age as the limit of conditional sojourn times

TheoremKimura's fixation probability is less than one#✓fully proved

An allele at frequency below 1 is lost with positive probability.

theorem kimuraFixation_lt_one (σ : ℝ) {x : ℝ} (hx : x < 1) : kimuraFixation σ x < 1
Uses 4 · Used by 3
Statement usesKimura's fixation probability
Proof usesDerivative of Kimura's fixation probability as a function · Kimura's fixation probability equals one at frequency one · Slope constant of Kimura's fixation probability
Used byClosed form above the current frequency · Closed form below the current frequency · Mean age as the limit of conditional sojourn times

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

The sojourn density (Green's function) of the Wright–Fisher diffusion with genic selection, time in units of 2N generations, σ = 2Ns. With u = kimuraFixation σ and u'(x) = kimuraSlope σ · e^{-2σx},

Ψ(p, x) = 2 u(min p x) (1 - u(max p x)) / (x (1 - x) u'(x)),

which is 2 S(min p x) (S(1) - S(max p x)) / (S(1) x (1 - x) e^{-2σx}) in terms of the scale function S(y) = (1 - e^{-2σy}) / (2σ) (S(y) = y if σ = 0). The neutral case is handled by the neutral branches of kimuraFixation and kimuraSlope (selectionGreen_zero). It is meaningful for 0 < x < 1; at x = 0, 1 the denominator vanishes and division by 0 gives 0 (a null set for integrals in x). In the diffusion reading, Ψ(p, x) dx is the expected time an allele started at frequency p spends in (x, x + dx) before loss or fixation (Ewens 2004, Chapter 4; the paper's Ψ(p, x) divided by 2N).

noncomputable def selectionGreen (σ p x : ℝ) : ℝ :=
  2 * kimuraFixation σ (min p x) * (1 - kimuraFixation σ (max p x)) /
    (x * (1 - x) * (kimuraSlope σ * exp (-2 * σ * x)))
Uses 2 · Used by 14
Statement usesKimura's fixation probability · Slope constant of Kimura's fixation probability
Used byMaruyama–Kimura conditional sojourn density · Closed form above the current frequency · Closed form below the current frequency · Continuity of the sojourn density in the starting frequency · Green's representation with selection · Sojourn density solves the backward equation above the target · Sojourn density solves the backward equation below the target · The general Green kernel specializes to Kimura's sojourn density · Right derivative of the sojourn density at the diagonal · Left derivative of the sojourn density at the diagonal · Sojourn density from frequency zero vanishes · Sojourn density from frequency one vanishes · Neutral case of the sojourn density · Mean age as the limit of conditional sojourn times

TheoremNeutral case of the sojourn density#✓fully proved

For σ = 0 and 0 < x < 1 the sojourn density is the neutral Green's function.

theorem selectionGreen_zero {p x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
    selectionGreen 0 p x = neutralGreen p x
Uses 5
Statement usesNeutral Wright–Fisher Green's function · Sojourn density of the Wright–Fisher diffusion with selection
Proof usesKimura's fixation probability · Neutral fixation probability equals the initial frequency · Slope constant of Kimura's fixation probability

TheoremThe general Green kernel specializes to Kimura's sojourn density#✓fully proved

For genic selection b x = σ x (1 - x), a x = x (1 - x), the general Green's function greenFunction is selectionGreen σ on [0, 1] × (0, 1). The scale function is S(y) = u(y) / u'(0) with u = kimuraFixation σ and u'(0) = kimuraSlope σ, since both have derivative ψ(y) = e^{-2σy} and vanish at 0; substituting that and S(1) = 1 / u'(0) into greenFunction gives selectionGreen.

theorem greenFunction_eq_selectionGreen (σ : ℝ) {p : ℝ} (hp : p ∈ Icc (0 : ℝ) 1)
    {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
    greenFunction (fun x => σ * x * (1 - x)) (fun x => x * (1 - x)) p x =
      selectionGreen σ p x
Uses 11
Statement usesDirichlet Green's function of a one-dimensional diffusion · Sojourn density of the Wright–Fisher diffusion with selection
Proof usesContinuity of Kimura's fixation probability · Derivative of Kimura's fixation probability at a point · Kimura's fixation probability · Kimura's fixation probability equals one at frequency one · Kimura's fixation probability vanishes at frequency zero · Slope constant of Kimura's fixation probability · Scale density of a one-dimensional diffusion · Scale density of the Wright–Fisher diffusion with genic selection · Scale function of a one-dimensional diffusion

TheoremGreen's representation with selection#✓fully proved

Green's representation with selection (Ewens 2004, Chapter 4; the integrated form of the paper's -δ(x - p) = s p (1 - p) ∂Ψ/∂p + p (1 - p) / (4N) ∂²Ψ/∂p²). For continuous g and p ∈ (0, 1), v(q) = ∫₀¹ Ψ(q, x) g(x) dx solves L_σ v = -g at p; with integral_selectionGreen_left and integral_selectionGreen_right (v(0) = v(1) = 0) this generalizes generator_integral_neutralGreen to σ ≠ 0. In the diffusion reading, v(p) is the expected value of ∫₀^T g(X_t) dt up to absorption.

theorem generator_integral_selectionGreen (σ : ℝ) {g : ℝ → ℝ} (hg : Continuous g) {p : ℝ}
    (hp : p ∈ Ioo (0 : ℝ) 1) :
    generator σ (fun q => ∫ x in (0 : ℝ)..1, selectionGreen σ q x * g x) p = -g p
Uses 9
Statement usesBackward generator of the Wright–Fisher diffusion with selection · Sojourn density of the Wright–Fisher diffusion with selection
Proof usesContinuity of Kimura's fixation probability · Derivative of Kimura's fixation probability at a point · Kimura's fixation probability · Kimura's fixation probability equals one at frequency one · Kimura's fixation probability vanishes at frequency zero · Slope constant of Kimura's fixation probability · Slope constant of Kimura's formula is nonzero

TheoremSojourn density from frequency zero vanishes#✓fully proved

Boundary value at 0: an absent allele spends no time in (0, 1), so ∫₀¹ Ψ(0, x) g(x) dx = 0 for every g.

theorem integral_selectionGreen_left (σ : ℝ) (g : ℝ → ℝ) :
    ∫ x in (0 : ℝ)..1, selectionGreen σ 0 x * g x = 0
Uses 4
Statement usesSojourn density of the Wright–Fisher diffusion with selection
Proof usesKimura's fixation probability · Kimura's fixation probability vanishes at frequency zero · Slope constant of Kimura's fixation probability

TheoremSojourn density from frequency one vanishes#✓fully proved

Boundary value at 1: a fixed allele spends no time in (0, 1), so ∫₀¹ Ψ(1, x) g(x) dx = 0 for every g.

theorem integral_selectionGreen_right (σ : ℝ) (g : ℝ → ℝ) :
    ∫ x in (0 : ℝ)..1, selectionGreen σ 1 x * g x = 0
Uses 4
Statement usesSojourn density of the Wright–Fisher diffusion with selection
Proof usesKimura's fixation probability · Kimura's fixation probability equals one at frequency one · Slope constant of Kimura's fixation probability

TheoremSojourn density solves the backward equation below the target#✓fully proved

Below the target frequency the sojourn density solves the homogeneous backward equation in its first argument: L_σ Ψ(·, x) = 0 at every p < x (pointwise form of the paper's -δ(x - p) = L_σ Ψ(·, x)).

theorem generator_selectionGreen_of_lt (σ : ℝ) {p x : ℝ} (hpx : p < x) :
    generator σ (fun q => selectionGreen σ q x) p = 0
Uses 5
Statement usesBackward generator of the Wright–Fisher diffusion with selection · Sojourn density of the Wright–Fisher diffusion with selection
Proof usesDerivative of Kimura's fixation probability at a point · Kimura's fixation probability · Slope constant of Kimura's fixation probability

TheoremSojourn density solves the backward equation above the target#✓fully proved

Above the target frequency: L_σ Ψ(·, x) = 0 at every p > x.

theorem generator_selectionGreen_of_gt (σ : ℝ) {p x : ℝ} (hxp : x < p) :
    generator σ (fun q => selectionGreen σ q x) p = 0
Uses 5
Statement usesBackward generator of the Wright–Fisher diffusion with selection · Sojourn density of the Wright–Fisher diffusion with selection
Proof usesDerivative of Kimura's fixation probability at a point · Kimura's fixation probability · Slope constant of Kimura's fixation probability

TheoremContinuity of the sojourn density in the starting frequency#✓fully proved

The sojourn density is continuous in the starting frequency (in particular at p = x).

theorem continuous_selectionGreen_left (σ x : ℝ) : Continuous fun p => selectionGreen σ p x
Uses 4
Statement usesSojourn density of the Wright–Fisher diffusion with selection
Proof usesContinuity of Kimura's fixation probability · Kimura's fixation probability · Slope constant of Kimura's fixation probability

TheoremLeft derivative of the sojourn density at the diagonal#✓fully proved

Left derivative at the diagonal: ∂_p Ψ(x⁻, x) = 2 (1 - u(x)) / (x (1 - x)). Together with hasDerivWithinAt_selectionGreen_Ici this gives the jump -2 / (x (1 - x)) of ∂_p Ψ at p = x, i.e. L_σ Ψ(·, x) = -δ_x in the distributional sense.

theorem hasDerivWithinAt_selectionGreen_Iic (σ : ℝ) {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
    HasDerivWithinAt (fun p => selectionGreen σ p x)
      (2 * (1 - kimuraFixation σ x) / (x * (1 - x))) (Iic x) x
Uses 4
Statement usesKimura's fixation probability · Sojourn density of the Wright–Fisher diffusion with selection
Proof usesDerivative of Kimura's fixation probability at a point · Slope constant of Kimura's fixation probability

TheoremRight derivative of the sojourn density at the diagonal#✓fully proved

Right derivative at the diagonal: ∂_p Ψ(x⁺, x) = -2 u(x) / (x (1 - x)).

theorem hasDerivWithinAt_selectionGreen_Ici (σ : ℝ) {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
    HasDerivWithinAt (fun p => selectionGreen σ p x)
      (-(2 * kimuraFixation σ x / (x * (1 - x)))) (Ici x) x
Uses 4
Statement usesKimura's fixation probability · Sojourn density of the Wright–Fisher diffusion with selection
Proof usesDerivative of Kimura's fixation probability at a point · Slope constant of Kimura's fixation probability

DefinitionMaruyama–Kimura conditional sojourn density#✓fully proved

The Maruyama–Kimura conditional sojourn density (the paper's Ψ_z(p, z)): given the initial frequency p and the current frequency x, the density of mean time spent at frequency z along the path, Ψ(p, z) Ψ(z, x) / Ψ(p, x) (Maruyama and Kimura 1975; Kiezun et al. 2013, Methods). Time in units of 2N generations.

noncomputable def ageDensity (σ p x z : ℝ) : ℝ :=
  selectionGreen σ p z * selectionGreen σ z x / selectionGreen σ p x
Uses 1 · Used by 3
Statement usesSojourn density of the Wright–Fisher diffusion with selection
Used byClosed form above the current frequency · Closed form below the current frequency · Mean age as the limit of conditional sojourn times

DefinitionClosed-form sojourn density below the current frequency#✓fully proved

The paper's closed form Ψ₁(z) for 0 < z < x (Kiezun et al. 2013, Methods), in units of 2N generations with σ = 2Ns: (e^{-2σ(1-z)} - 1)(e^{-2σz} - 1) / (σ z (1 - z) (1 - e^{-2σ})), and its continuous extension 2 for σ = 0. It does not depend on the current frequency x.

noncomputable def maruyamaBelow (σ z : ℝ) : ℝ :=
  if σ = 0 then 2 else
    (exp (-2 * σ * (1 - z)) - 1) * (exp (-2 * σ * z) - 1) /
      (σ * z * (1 - z) * (1 - exp (-2 * σ)))
Used by 15
Used byClosed form below the current frequency · Integrability of the sojourn density below the current frequency · Sojourn density below the current frequency via fixation probability · Hyperbolic form of the sojourn density below the current frequency · Paper units · Maruyama effect, below the current frequency · Stronger selection, smaller Ψ₁ · Symmetry · Positivity of the sojourn density below the current frequency · Mean age of an allele at a given frequency · The Maruyama effect (Kiezun et al. 2013) · Stronger selection, younger alleles · Symmetry · Kimura and Ohta (1973) · Mean age as the limit of conditional sojourn times

DefinitionClosed-form sojourn density above the current frequency#✓fully proved

The paper's closed form Ψ₂(z) for x < z < 1 (Kiezun et al. 2013, Methods), in units of 2N generations with σ = 2Ns: (e^{-2σ(1-z)} - 1)(e^{2σ(1-z)} - 1)(1 - e^{2σx}) / (σ z (1 - z)(e^{-2σ(1-x)} - 1)(1 - e^{2σ})), and its continuous extension 2 x (1 - z) / ((1 - x) z) for σ = 0.

noncomputable def maruyamaAbove (σ x z : ℝ) : ℝ :=
  if σ = 0 then 2 * x * (1 - z) / ((1 - x) * z) else
    (exp (-2 * σ * (1 - z)) - 1) * (exp (2 * σ * (1 - z)) - 1) * (1 - exp (2 * σ * x)) /
      (σ * z * (1 - z) * (exp (-2 * σ * (1 - x)) - 1) * (1 - exp (2 * σ)))
Used by 16
Used byClosed form above the current frequency · Integrability of the sojourn density above the current frequency · Sojourn density above the current frequency via fixation probability · Hyperbolic form of the sojourn density above the current frequency · Paper units · Maruyama effect, above the current frequency · Stronger selection, smaller Ψ₂ · Symmetry · Sojourn density above the current frequency vanishes at one · Positivity of the sojourn density above the current frequency · Mean age of an allele at a given frequency · The Maruyama effect (Kiezun et al. 2013) · Stronger selection, younger alleles · Symmetry · Kimura and Ohta (1973) · Mean age as the limit of conditional sojourn times

DefinitionMean age of an allele at a given frequency#✓fully proved

The mean age of an allele at current frequency x (the paper's a(x)), in units of 2N generations: ∫₀^x Ψ₁(z) dz + ∫_x^1 Ψ₂(z) dz.

noncomputable def meanAge (σ x : ℝ) : ℝ :=
  (∫ z in (0 : ℝ)..x, maruyamaBelow σ z) + ∫ z in x..1, maruyamaAbove σ x z
Uses 2 · Used by 6
Statement usesClosed-form sojourn density above the current frequency · Closed-form sojourn density below the current frequency
Used byThe Maruyama effect (Kiezun et al. 2013) · Stronger selection, younger alleles · Stronger selection, younger alleles · Symmetry · Kimura and Ohta (1973) · Mean age as the limit of conditional sojourn times

TheoremSojourn density below the current frequency via fixation probability#✓fully proved

Ψ₁ through Kimura's fixation probability: Ψ₁(z) = 2 u(z)(1 - u(z)) / (z (1 - z) u'(z)) on (0, 1).

theorem maruyamaBelow_eq {σ z : ℝ} (hz : z ∈ Ioo (0 : ℝ) 1) :
    maruyamaBelow σ z = 2 * kimuraFixation σ z * (1 - kimuraFixation σ z) /
      (z * (1 - z) * (kimuraSlope σ * exp (-2 * σ * z)))
Uses 5 · Used by 1
Statement usesKimura's fixation probability · Slope constant of Kimura's fixation probability · Closed-form sojourn density below the current frequency
Proof usesNeutral fixation probability equals the initial frequency · Denominator of Kimura's formula is nonzero
Used byClosed form below the current frequency

TheoremSojourn density above the current frequency via fixation probability#✓fully proved

Ψ₂ through Kimura's fixation probability: Ψ₂(z) = 2 u(x)(1 - u(z))² / ((1 - u(x)) z (1 - z) u'(z)) on (0, 1).

theorem maruyamaAbove_eq {σ x z : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) (hz : z ∈ Ioo (0 : ℝ) 1) :
    maruyamaAbove σ x z = 2 * kimuraFixation σ x * (1 - kimuraFixation σ z) ^ 2 /
      ((1 - kimuraFixation σ x) * z * (1 - z) * (kimuraSlope σ * exp (-2 * σ * z)))
Uses 5 · Used by 1
Statement usesKimura's fixation probability · Slope constant of Kimura's fixation probability · Closed-form sojourn density above the current frequency
Proof usesNeutral fixation probability equals the initial frequency · Denominator of Kimura's formula is nonzero
Used byClosed form above the current frequency

TheoremClosed form below the current frequency#✓fully proved

For 0 < p ≤ z ≤ x < 1 the conditional sojourn density is the paper's Ψ₁(z); it depends neither on p nor on x.

theorem ageDensity_of_le_of_le (σ : ℝ) {p x z : ℝ} (hp : 0 < p) (hpz : p ≤ z) (hzx : z ≤ x)
    (hx : x < 1) : ageDensity σ p x z = maruyamaBelow σ z
Uses 8 · Used by 1
Statement usesMaruyama–Kimura conditional sojourn density · Closed-form sojourn density below the current frequency
Proof usesKimura's fixation probability · Kimura's fixation probability is less than one · Positivity of Kimura's fixation probability · Slope constant of Kimura's fixation probability · Sojourn density below the current frequency via fixation probability · Sojourn density of the Wright–Fisher diffusion with selection
Used byMean age as the limit of conditional sojourn times

TheoremClosed form above the current frequency#✓fully proved

For 0 < p ≤ x ≤ z < 1 the conditional sojourn density is the paper's Ψ₂(z); it does not depend on p.

theorem ageDensity_of_le_of_ge (σ : ℝ) {p x z : ℝ} (hp : 0 < p) (hpx : p ≤ x) (hxz : x ≤ z)
    (hz : z < 1) : ageDensity σ p x z = maruyamaAbove σ x z
Uses 8 · Used by 1
Statement usesMaruyama–Kimura conditional sojourn density · Closed-form sojourn density above the current frequency
Proof usesKimura's fixation probability · Kimura's fixation probability is less than one · Positivity of Kimura's fixation probability · Slope constant of Kimura's fixation probability · Sojourn density above the current frequency via fixation probability · Sojourn density of the Wright–Fisher diffusion with selection
Used byMean age as the limit of conditional sojourn times

TheoremPaper units#✓fully proved

With N diploid individuals, selection coefficient s ≠ 0 and time in generations, the paper prints Ψ₁(z) = (e^{-γ(1-z)} - 1)(e^{-γz} - 1) / (s z (1 - z)(1 - e^{-γ})) with γ = 4Ns; it equals 2N · maruyamaBelow (2Ns) z.

theorem maruyamaBelow_generations {N s : ℝ} (hN : 0 < N) (hs : s ≠ 0) (z : ℝ) :
    2 * N * maruyamaBelow (2 * N * s) z =
      (exp (-(4 * N * s) * (1 - z)) - 1) * (exp (-(4 * N * s) * z) - 1) /
        (s * z * (1 - z) * (1 - exp (-(4 * N * s))))
Uses 1
Statement usesClosed-form sojourn density below the current frequency

TheoremPaper units#✓fully proved

The paper's Ψ₂(z) = (e^{-γ(1-z)} - 1)(e^{γ(1-z)} - 1)(1 - e^{γx}) / (s z (1 - z)(e^{-γ(1-x)} - 1)(1 - e^{γ})), γ = 4Ns, equals 2N · maruyamaAbove (2Ns) x z.

theorem maruyamaAbove_generations {N s : ℝ} (hN : 0 < N) (hs : s ≠ 0) (x z : ℝ) :
    2 * N * maruyamaAbove (2 * N * s) x z =
      (exp (-(4 * N * s) * (1 - z)) - 1) * (exp (4 * N * s * (1 - z)) - 1) *
          (1 - exp (4 * N * s * x)) /
        (s * z * (1 - z) * (exp (-(4 * N * s) * (1 - x)) - 1) * (1 - exp (4 * N * s)))
Uses 1
Statement usesClosed-form sojourn density above the current frequency

TheoremKimura and Ohta (1973)#✓fully proved

The mean age of a neutral allele at frequency x ∈ (0, 1) is -2 x log x / (1 - x) in units of 2N generations (-4N x ln x / (1 - x) generations).

theorem meanAge_zero {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
    meanAge 0 x = -2 * x * log x / (1 - x)
Uses 3
Statement usesMean age of an allele at a given frequency
Proof usesClosed-form sojourn density above the current frequency · Closed-form sojourn density below the current frequency

TheoremHyperbolic form of the sojourn density below the current frequency#✓fully proved

Ψ₁ in hyperbolic form: 2 sinh(σz) sinh(σ(1 - z)) / (σ z (1 - z) sinh σ) for σ ≠ 0.

theorem maruyamaBelow_eq_sinh {σ z : ℝ} (hσ : σ ≠ 0) (hz : z ∈ Ioo (0 : ℝ) 1) :
    maruyamaBelow σ z = 2 * sinh (σ * z) * sinh (σ * (1 - z)) / (σ * z * (1 - z) * sinh σ)
Uses 1 · Used by 4
Statement usesClosed-form sojourn density below the current frequency
Used byMaruyama effect, below the current frequency · Stronger selection, smaller Ψ₁ · Symmetry · Positivity of the sojourn density below the current frequency

TheoremHyperbolic form of the sojourn density above the current frequency#✓fully proved

Ψ₂ in hyperbolic form: 2 sinh(σ(1 - z))² sinh(σx) / (σ sinh σ sinh(σ(1 - x)) z (1 - z)) for σ ≠ 0.

theorem maruyamaAbove_eq_sinh {σ x z : ℝ} (hσ : σ ≠ 0) (hx : x ∈ Ioo (0 : ℝ) 1)
    (hz : z ∈ Ioo (0 : ℝ) 1) :
    maruyamaAbove σ x z = 2 * sinh (σ * (1 - z)) ^ 2 * sinh (σ * x) /
      (σ * sinh σ * sinh (σ * (1 - x)) * z * (1 - z))
Uses 1 · Used by 4
Statement usesClosed-form sojourn density above the current frequency
Used byMaruyama effect, above the current frequency · Stronger selection, smaller Ψ₂ · Symmetry · Positivity of the sojourn density above the current frequency

TheoremSymmetry#✓fully proved

Ψ₁ is the same for σ and -σ.

theorem maruyamaBelow_neg (σ : ℝ) {z : ℝ} (hz : z ∈ Ioo (0 : ℝ) 1) :
    maruyamaBelow (-σ) z = maruyamaBelow σ z
Uses 2 · Used by 3
Statement usesClosed-form sojourn density below the current frequency
Proof usesHyperbolic form of the sojourn density below the current frequency
Used byMaruyama effect, below the current frequency · Positivity of the sojourn density below the current frequency · Symmetry

TheoremSymmetry#✓fully proved

Ψ₂ is the same for σ and -σ.

theorem maruyamaAbove_neg (σ : ℝ) {x z : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) (hz : z ∈ Ioo (0 : ℝ) 1) :
    maruyamaAbove (-σ) x z = maruyamaAbove σ x z
Uses 2 · Used by 3
Statement usesClosed-form sojourn density above the current frequency
Proof usesHyperbolic form of the sojourn density above the current frequency
Used byMaruyama effect, above the current frequency · Positivity of the sojourn density above the current frequency · Symmetry

TheoremPositivity of the sojourn density below the current frequency#✓fully proved

Ψ₁ is positive on (0, 1).

theorem maruyamaBelow_pos (σ : ℝ) {z : ℝ} (hz : z ∈ Ioo (0 : ℝ) 1) : 0 < maruyamaBelow σ z
Uses 3 · Used by 2
Statement usesClosed-form sojourn density below the current frequency
Proof usesHyperbolic form of the sojourn density below the current frequency · Symmetry
Used byIntegrability of the sojourn density below the current frequency · Mean age as the limit of conditional sojourn times

TheoremMaruyama effect, below the current frequency#✓fully proved

For σ ≠ 0, Ψ₁(z) < 2, its neutral value, for every z ∈ (0, 1).

theorem maruyamaBelow_lt {σ z : ℝ} (hσ : σ ≠ 0) (hz : z ∈ Ioo (0 : ℝ) 1) :
    maruyamaBelow σ z < maruyamaBelow 0 z
Uses 3 · Used by 4
Statement usesClosed-form sojourn density below the current frequency
Proof usesHyperbolic form of the sojourn density below the current frequency · Symmetry
Used byIntegrability of the sojourn density below the current frequency · Stronger selection, smaller Ψ₁ · The Maruyama effect (Kiezun et al. 2013) · Mean age as the limit of conditional sojourn times

TheoremMaruyama effect, above the current frequency#✓fully proved

For σ ≠ 0 and 0 < x < z < 1, Ψ₂(z) is strictly below its neutral value 2 x (1 - z) / ((1 - x) z).

theorem maruyamaAbove_lt {σ x z : ℝ} (hσ : σ ≠ 0) (hx : 0 < x) (hxz : x < z) (hz : z < 1) :
    maruyamaAbove σ x z < maruyamaAbove 0 x z
Uses 3 · Used by 3
Statement usesClosed-form sojourn density above the current frequency
Proof usesHyperbolic form of the sojourn density above the current frequency · Symmetry
Used byIntegrability of the sojourn density above the current frequency · Stronger selection, smaller Ψ₂ · The Maruyama effect (Kiezun et al. 2013)

TheoremPositivity of the sojourn density above the current frequency#✓fully proved

Ψ₂ is positive for 0 < x < z < 1.

theorem maruyamaAbove_pos (σ : ℝ) {x z : ℝ} (hx : 0 < x) (hxz : x < z) (hz : z < 1) :
    0 < maruyamaAbove σ x z
Uses 3 · Used by 1
Statement usesClosed-form sojourn density above the current frequency
Proof usesHyperbolic form of the sojourn density above the current frequency · Symmetry
Used byIntegrability of the sojourn density above the current frequency

TheoremSojourn density above the current frequency vanishes at one#✓fully proved

At z = 1 the closed form Ψ₂ vanishes (a null set for the integral).

@[simp]
theorem maruyamaAbove_one_right (σ x : ℝ) : maruyamaAbove σ x 1 = 0
Uses 1 · Used by 2
Statement usesClosed-form sojourn density above the current frequency
Used byIntegrability of the sojourn density above the current frequency · Symmetry

TheoremIntegrability of the sojourn density below the current frequency#✓fully proved

Ψ₁ is integrable on [0, x] (it is bounded by 2).

theorem intervalIntegrable_maruyamaBelow (σ : ℝ) {x : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) :
    IntervalIntegrable (maruyamaBelow σ) volume 0 x
Uses 3 · Used by 3
Statement usesClosed-form sojourn density below the current frequency
Proof usesMaruyama effect, below the current frequency · Positivity of the sojourn density below the current frequency
Used byThe Maruyama effect (Kiezun et al. 2013) · Stronger selection, younger alleles · Mean age as the limit of conditional sojourn times

TheoremIntegrability of the sojourn density above the current frequency#✓fully proved

Ψ₂ is integrable on [x, 1] for x ∈ (0, 1) (it is bounded by 2 / (1 - x)).

theorem intervalIntegrable_maruyamaAbove (σ : ℝ) {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
    IntervalIntegrable (maruyamaAbove σ x) volume x 1
Uses 4 · Used by 3
Statement usesClosed-form sojourn density above the current frequency
Proof usesMaruyama effect, above the current frequency · Sojourn density above the current frequency vanishes at one · Positivity of the sojourn density above the current frequency
Used byThe Maruyama effect (Kiezun et al. 2013) · Stronger selection, younger alleles · Mean age as the limit of conditional sojourn times

TheoremSymmetry#✓fully proved

The mean age is the same for σ and -σ.

theorem meanAge_neg (σ : ℝ) {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) : meanAge (-σ) x = meanAge σ x
Uses 6 · Used by 1
Statement usesMean age of an allele at a given frequency
Proof usesClosed-form sojourn density above the current frequency · Symmetry · Sojourn density above the current frequency vanishes at one · Closed-form sojourn density below the current frequency · Symmetry
Used byStronger selection, younger alleles

TheoremThe Maruyama effect (Kiezun et al. 2013)#✓fully proved

For σ ≠ 0 and x ∈ (0, 1), an allele under selection, advantageous or deleterious, is on average strictly younger than a neutral allele at the same frequency.

theorem meanAge_lt {σ x : ℝ} (hσ : σ ≠ 0) (hx : x ∈ Ioo (0 : ℝ) 1) :
    meanAge σ x < meanAge 0 x
Uses 7
Statement usesMean age of an allele at a given frequency
Proof usesIntegrability of the sojourn density above the current frequency · Integrability of the sojourn density below the current frequency · Closed-form sojourn density above the current frequency · Maruyama effect, above the current frequency · Closed-form sojourn density below the current frequency · Maruyama effect, below the current frequency

TheoremMean age as the limit of conditional sojourn times#✓fully proved

Mean age as the limit of conditional sojourn times (Maruyama 1974; Kiezun et al. 2013, Methods): for x ∈ (0, 1), the total conditional sojourn time ∫₀¹ Ψ_z(p, z) dz of a path from initial frequency p to current frequency x tends to the mean age a(x) as p → 0⁺ (an allele arises at frequency close to 0).

theorem tendsto_integral_ageDensity (σ : ℝ) {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
    Tendsto (fun p => ∫ z in (0 : ℝ)..1, ageDensity σ p x z) (𝓝[>] 0) (𝓝 (meanAge σ x))
Uses 19
Statement usesMaruyama–Kimura conditional sojourn density · Mean age of an allele at a given frequency
Proof usesClosed form above the current frequency · Closed form below the current frequency · Continuity of Kimura's fixation probability · Derivative of Kimura's fixation probability as a function · Derivative of Kimura's fixation probability at a point · Integrability of the sojourn density above the current frequency · Integrability of the sojourn density below the current frequency · Kimura's fixation probability · Kimura's fixation probability is less than one · Positivity of Kimura's fixation probability · Kimura's fixation probability vanishes at frequency zero · Slope constant of Kimura's fixation probability · Closed-form sojourn density above the current frequency · Closed-form sojourn density below the current frequency · Maruyama effect, below the current frequency · Positivity of the sojourn density below the current frequency · Sojourn density of the Wright–Fisher diffusion with selection

TheoremStronger selection, smaller Ψ₁#✓fully proved

For 0 ≤ σ < τ and z ∈ (0, 1), Ψ₁ at τ is strictly below Ψ₁ at σ.

theorem maruyamaBelow_lt_of_lt {σ τ z : ℝ} (hσ : 0 ≤ σ) (hστ : σ < τ)
    (hz : z ∈ Ioo (0 : ℝ) 1) : maruyamaBelow τ z < maruyamaBelow σ z
Uses 3 · Used by 1
Statement usesClosed-form sojourn density below the current frequency
Proof usesHyperbolic form of the sojourn density below the current frequency · Maruyama effect, below the current frequency
Used byStronger selection, younger alleles

TheoremStronger selection, smaller Ψ₂#✓fully proved

For 0 ≤ σ < τ and 0 < x < z < 1, Ψ₂ at τ is strictly below Ψ₂ at σ.

theorem maruyamaAbove_lt_of_lt {σ τ x z : ℝ} (hσ : 0 ≤ σ) (hστ : σ < τ) (hx : 0 < x)
    (hxz : x < z) (hz : z < 1) : maruyamaAbove τ x z < maruyamaAbove σ x z
Uses 3 · Used by 1
Statement usesClosed-form sojourn density above the current frequency
Proof usesHyperbolic form of the sojourn density above the current frequency · Maruyama effect, above the current frequency
Used byStronger selection, younger alleles

TheoremStronger selection, younger alleles#✓fully proved

At a fixed frequency x ∈ (0, 1), the mean age is strictly decreasing in σ ≥ 0. Kiezun et al. (2013, Figure 1b) show this numerically from the closed forms; here it is proved.

theorem meanAge_lt_meanAge_of_lt {σ τ x : ℝ} (hσ : 0 ≤ σ) (hστ : σ < τ)
    (hx : x ∈ Ioo (0 : ℝ) 1) : meanAge τ x < meanAge σ x
Uses 7 · Used by 1
Statement usesMean age of an allele at a given frequency
Proof usesIntegrability of the sojourn density above the current frequency · Integrability of the sojourn density below the current frequency · Closed-form sojourn density above the current frequency · Stronger selection, smaller Ψ₂ · Closed-form sojourn density below the current frequency · Stronger selection, smaller Ψ₁
Used byStronger selection, younger alleles

TheoremStronger selection, younger alleles#✓fully proved

Stronger selection, younger alleles, for either sign of selection: if |σ| < |τ| then an allele at frequency x ∈ (0, 1) under selection τ is on average strictly younger than one under selection σ.

theorem meanAge_lt_meanAge_of_abs_lt {σ τ x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) (h : |σ| < |τ|) :
    meanAge τ x < meanAge σ x
Uses 3
Statement usesMean age of an allele at a given frequency
Proof usesStronger selection, younger alleles · Symmetry

TheoremMean time as a sum of sojourn times#✓fully proved

Mean time as a sum of sojourn times (the identity behind Maruyama and Kimura 1975). For a jointly measurable family of transition densities w p x t ≥ 0 on (0, 1) satisfying the Chapman–Kolmogorov equation for positive times, ∫₀^∞ t w(p, x, t) dt = ∫₀¹ Ψ(p, y) Ψ(y, x) dy with Ψ(p, x) = ∫₀^∞ w(p, x, t) dt, in ℝ≥0∞. Dividing by Ψ(p, x) reads ∫₀¹ Ψ(p, y) Ψ(y, x) / Ψ(p, x) dy (the integral of ageDensity when Ψ = selectionGreen σ) as a mean time. The statement is abstract: no diffusion is constructed, and w is not required to be the Wright–Fisher transition density.

theorem lintegral_mul_eq_lintegral_sojourn_mul (w : ℝ → ℝ → ℝ → ℝ≥0∞)
    (hw : Measurable fun q : ℝ × ℝ × ℝ => w q.1 q.2.1 q.2.2)
    (hck : ∀ p x s t, 0 < s → 0 < t →
      w p x (s + t) = ∫⁻ y in Ioo (0 : ℝ) 1, w p y s * w y x t)
    (p x : ℝ) :
    ∫⁻ t in Ioi (0 : ℝ), ENNReal.ofReal t * w p x t =
      ∫⁻ y in Ioo (0 : ℝ) 1, (∫⁻ s in Ioi (0 : ℝ), w p y s) * ∫⁻ t in Ioi (0 : ℝ), w y x t
43 fully proved2 ready to state

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.