Poisson random field model

DefinitionSawyer–Hartl Poisson random field density#✓fully proved

The Sawyer–Hartl (1992) Poisson-random-field density: the expected number of sites per unit frequency at which the derived allele has frequency x, for scaled mutation rate θ = 4Nu and scaled genic selection σ = 2Ns: θ · u_σ(1 - x) / (x (1 - x)) with u_σ = kimuraFixation σ, i.e. θ (1 - e^{-2σ(1 - x)}) / ((1 - e^{-2σ}) x (1 - x)), and θ / x when σ = 0. The model domain is θ > 0 and x ∈ (0, 1); at x = 0, 1 Lean's a / 0 = 0 gives the junk value 0.

noncomputable def prfDensity (θ σ x : ℝ) : ℝ :=
  θ * kimuraFixation σ (1 - x) / (x * (1 - x))

Uses 1 · Used by 15

Statement usesKimura's fixation probability

Used byUniform bound on the expected site-frequency spectrum · Frequency density averaged over a distribution of fitness effects · Mixture identity · Integrability of the expected spectrum in the selection coefficient · Probability current · ODE characterization of the Poisson-random-field density · Expected site frequency spectrum under the Poisson random field · Neutral site-frequency spectrum (Fu 1995) · Expected number of sites derived in the whole neutral sample · Stationary forward equation (Sawyer–Hartl 1992) · Closed form of the Poisson random field density with selection · Neutral Poisson random field density · The neutral density from the Green's function · Boundary normalization at 1 · Boundary normalization at 0

TheoremClosed form of the Poisson random field density with selection#✓fully proved

The Poisson-random-field density with selection, explicitly: θ (1 - e^{-2σ(1 - x)}) / ((1 - e^{-2σ}) x (1 - x)) for σ ≠ 0.

theorem prfDensity_of_ne_zero (θ : ℝ) {σ : ℝ} (hσ : σ ≠ 0) (x : ℝ) :
    prfDensity θ σ x = θ * (1 - exp (-2 * σ * (1 - x))) / ((1 - exp (-2 * σ)) * x * (1 - x))

Uses 2

Statement usesSawyer–Hartl Poisson random field density

Proof usesKimura's fixation probability

TheoremNeutral Poisson random field density#✓fully proved

The neutral Poisson-random-field density is θ / x (for x ≠ 1).

theorem prfDensity_zero (θ : ℝ) {x : ℝ} (hx : x ≠ 1) : prfDensity θ 0 x = θ / x

Uses 3 · Used by 1

Statement usesSawyer–Hartl Poisson random field density

Proof usesKimura's fixation probability · Neutral fixation probability equals the initial frequency

Used byThe neutral density from the Green's function

TheoremThe neutral density from the Green's function#✓fully proved

A new neutral mutation enters at a small frequency p; with mutations arriving at rate θ / (2p) per unit time (so that the mutational input of frequency is θ / 2), the expected sojourn density at x ≥ p is θ / (2p) · G(p, x) = θ / x, the neutral Poisson-random-field density.

theorem prfDensity_zero_eq_neutralGreen (θ : ℝ) {p x : ℝ} (hp : 0 < p) (hpx : p ≤ x)
    (hx : x < 1) : prfDensity θ 0 x = θ / (2 * p) * neutralGreen p x

Uses 3

Statement usesNeutral Wright–Fisher Green's function · Sawyer–Hartl Poisson random field density

Proof usesNeutral Poisson random field density

TheoremStationary forward equation (Sawyer–Hartl 1992)#✓fully proved

On (0, 1) the weighted density F(x) = x (1 - x) φ(x) of the Poisson-random-field density solves the stationary Fokker–Planck equation ½ F'' - σ F' = 0 of the Wright–Fisher diffusion with genic selection σ (the forward equation ½ (x (1 - x) φ)'' - (σ x (1 - x) φ)' = 0).

theorem forward_prfDensity (θ σ : ℝ) {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
    deriv (deriv fun y => y * (1 - y) * prfDensity θ σ y) x / 2 -
      σ * deriv (fun y => y * (1 - y) * prfDensity θ σ y) x = 0

Uses 4

Statement usesSawyer–Hartl Poisson random field density

Proof usesDerivative of Kimura's fixation probability at a point · Kimura's fixation probability · Slope constant of Kimura's fixation probability

TheoremProbability current#✓fully proved

On (0, 1) the current J = σ F - F' / 2 of the stationary forward equation, for the weighted density F(x) = x (1 - x) φ(x), is the constant θ · u_σ'(0) / 2 (u_σ'(0) = kimuraSlope σ = 2σ / (1 - e^{-2σ}), and 1 for σ = 0), so J = θ σ / (1 - e^{-2σ}), and J = θ / 2 in the neutral case: the mutational input of frequency at 0, carried through (0, 1) to fixation at 1.

theorem current_prfDensity (θ σ : ℝ) {x : ℝ} (hx : x ∈ Ioo (0 : ℝ) 1) :
    σ * (x * (1 - x) * prfDensity θ σ x) -
      deriv (fun y => y * (1 - y) * prfDensity θ σ y) x / 2 = θ * kimuraSlope σ / 2

Uses 6

Statement usesSlope constant of Kimura's fixation probability · Sawyer–Hartl Poisson random field density

Proof usesDerivative of Kimura's fixation probability at a point · Kimura's fixation probability · Neutral fixation probability equals the initial frequency · Denominator of Kimura's formula is nonzero

TheoremBoundary normalization at 0#✓fully proved

As x → 0⁺ the weighted density x (1 - x) φ(x) tends to θ. (This is not the probability current, which is current_prfDensity.)

theorem tendsto_weighted_prfDensity_zero (θ σ : ℝ) :
    Tendsto (fun y => y * (1 - y) * prfDensity θ σ y) (𝓝[>] 0) (𝓝 θ)

Uses 4

Statement usesSawyer–Hartl Poisson random field density

Proof usesContinuity of Kimura's fixation probability · Kimura's fixation probability · Kimura's fixation probability equals one at frequency one

TheoremBoundary normalization at 1#✓fully proved

As x → 1⁻ the weighted density x (1 - x) φ(x) tends to 0.

theorem tendsto_weighted_prfDensity_one (θ σ : ℝ) :
    Tendsto (fun y => y * (1 - y) * prfDensity θ σ y) (𝓝[<] 1) (𝓝 0)

Uses 4

Statement usesSawyer–Hartl Poisson random field density

Proof usesContinuity of Kimura's fixation probability · Kimura's fixation probability · Kimura's fixation probability vanishes at frequency zero

TheoremODE characterization of the Poisson-random-field density#✓fully proved

Let θ ≠ 0 and let φ be a density on (0, 1) whose weighted density x (1 - x) φ(x) extends to a function F continuous on [0, 1], twice differentiable on (0, 1), solving the stationary forward equation ½ F'' - σ F' = 0 there, with boundary normalizations F(0) = θ and F(1) = 0. Then φ is the Sawyer–Hartl density on (0, 1).

theorem eq_prfDensity_of_forward {θ σ : ℝ} (hθ : θ ≠ 0) {φ F : ℝ → ℝ}
    (hF : ∀ x ∈ Ioo (0 : ℝ) 1, F x = x * (1 - x) * φ x) (hcont : ContinuousOn F (Icc 0 1))
    (hdiff : DifferentiableOn ℝ F (Ioo 0 1)) (hdiff' : DifferentiableOn ℝ (deriv F) (Ioo 0 1))
    (hfwd : ∀ x ∈ Ioo (0 : ℝ) 1, deriv (deriv F) x / 2 - σ * deriv F x = 0)
    (h0 : F 0 = θ) (h1 : F 1 = 0) :
    ∀ x ∈ Ioo (0 : ℝ) 1, φ x = prfDensity θ σ x

Uses 4

Statement usesSawyer–Hartl Poisson random field density

Proof usesUniqueness of the fixation probability (Kimura 1962) · Backward generator of the Wright–Fisher diffusion with selection · Kimura's fixation probability

DefinitionExpected site frequency spectrum under the Poisson random field#✓fully proved

The expected unfolded site-frequency spectrum of a sample of n gene copies under the Poisson random field: the expected number of sites where exactly i of the n sampled copies carry the derived allele, E ξ_i = ∫ x in 0..1, C(n, i) x ^ i (1 - x) ^ (n - i) φ(x). The site-frequency spectrum consists of the segregating classes 1 ≤ i < n. The value at i = n is the expected number of sites at which every sampled copy is derived (monomorphic in the sample, expectedSFS_neutral_self); for i = 0 the integrand is not integrable at 0 (the expected number of ancestral-monomorphic sites is infinite) and Lean's integral returns its junk value 0.

noncomputable def expectedSFS (θ σ : ℝ) (n i : ℕ) : ℝ :=
  ∫ x in (0 : ℝ)..1, (n.choose i : ℝ) * x ^ i * (1 - x) ^ (n - i) * prfDensity θ σ x

Uses 1 · Used by 10

Statement usesSawyer–Hartl Poisson random field density

Used byUniform bound on the expected site-frequency spectrum · Site-frequency spectrum under a distribution of fitness effects · DFE spectrum is additive in the measure · Spectrum under a point-mass DFE is the single-selection spectrum · Mixture identity · Site-frequency spectrum under the gamma DFE · DFE spectrum is homogeneous in the measure · Integrability of the expected spectrum in the selection coefficient · Neutral site-frequency spectrum (Fu 1995) · Expected number of sites derived in the whole neutral sample

TheoremNeutral site-frequency spectrum (Fu 1995)#✓fully proved

With σ = 0, for the segregating classes 1 ≤ i < n the expected number of sites with i derived copies in a sample of n is θ / i.

theorem expectedSFS_neutral (θ : ℝ) {n i : ℕ} (hi : 0 < i) (hin : i < n) :
    expectedSFS θ 0 n i = θ / i

Uses 3

Statement usesExpected site frequency spectrum under the Poisson random field

Proof usesKimura's fixation probability · Sawyer–Hartl Poisson random field density

TheoremExpected number of sites derived in the whole neutral sample#✓fully proved

With σ = 0 the expected number of sites at which all n ≥ 1 sampled copies carry the derived allele is θ / n. These sites are monomorphic in the sample, so this is not a class of the site-frequency spectrum.

theorem expectedSFS_neutral_self (θ : ℝ) {n : ℕ} (hn : 0 < n) :
    expectedSFS θ 0 n n = θ / n

Uses 3

Statement usesExpected site frequency spectrum under the Poisson random field

Proof usesKimura's fixation probability · Sawyer–Hartl Poisson random field density

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.