Selective sweeps

18 fully proved

The deterministic logistic sweep

DefinitionLogistic trajectory of a selective sweep#✓fully proved

The logistic trajectory of a favourable allele with genic selection coefficient s, starting from frequency x₀: the solution of x' = s x (1 - x) with x 0 = x₀ (Maynard Smith and Haigh 1974).

noncomputable def sweepTraj (s x₀ t : ℝ) : ℝ := x₀ * exp (s * t) / (1 - x₀ + x₀ * exp (s * t))

Used by 3

Used bySweep trajectory solves the logistic equation · Sweep trajectory stays strictly between 0 and 1 · Sweep trajectory reaches its target at the sweep duration

TheoremSweep trajectory stays strictly between 0 and 1#✓fully proved

The trajectory stays strictly between 0 and 1.

theorem sweepTraj_mem_Ioo {x₀ : ℝ} (h₀ : 0 < x₀) (h₁ : x₀ < 1) (s t : ℝ) :
    sweepTraj s x₀ t ∈ Ioo (0 : ℝ) 1

Uses 1

Statement usesLogistic trajectory of a selective sweep

TheoremSweep trajectory solves the logistic equation#✓fully proved

The logistic equation: x'(t) = s x(t) (1 - x(t)).

theorem hasDerivAt_sweepTraj {x₀ : ℝ} (h₀ : 0 < x₀) (h₁ : x₀ < 1) (s t : ℝ) :
    HasDerivAt (sweepTraj s x₀) (s * sweepTraj s x₀ t * (1 - sweepTraj s x₀ t)) t

Uses 1

Statement usesLogistic trajectory of a selective sweep

DefinitionDuration of a logistic sweep between two frequencies#✓fully proved

The time the logistic trajectory with selection coefficient s takes to go from frequency a to frequency b: (1/s) log (b (1 - a) / (a (1 - b))), the difference of the logits divided by s.

noncomputable def sweepDuration (s a b : ℝ) : ℝ := (1 / s) * log (b * (1 - a) / (a * (1 - b)))

Used by 4

Used byDuration of a complete deterministic sweep · Positivity of the sweep duration · Power-law EHH after a complete sweep · Sweep trajectory reaches its target at the sweep duration

TheoremSweep trajectory reaches its target at the sweep duration#✓fully proved

sweepDuration s a b is the exact time at which the trajectory started at a reaches b.

theorem sweepTraj_sweepDuration {s a b : ℝ} (hs : s ≠ 0) (ha₀ : 0 < a) (ha₁ : a < 1)
    (hb₀ : 0 < b) (hb₁ : b < 1) : sweepTraj s a (sweepDuration s a b) = b

noncomputable def sweepTraj (s x₀ t : ℝ) : ℝ := x₀ * exp (s * t) / (1 - x₀ + x₀ * exp (s * t))

MathlibExt/Biology/PopulationGenetics/SelectionScan/SelectiveSweep.lean:90

noncomputable def sweepDuration (s a b : ℝ) : ℝ := (1 / s) * log (b * (1 - a) / (a * (1 - b)))

MathlibExt/Biology/PopulationGenetics/SelectionScan/SelectiveSweep.lean:141

Uses 2

Statement usesDuration of a logistic sweep between two frequencies · Logistic trajectory of a selective sweep

TheoremPositivity of the sweep duration#✓fully proved

The time to reach a higher frequency is positive.

theorem sweepDuration_pos {s a b : ℝ} (hs : 0 < s) (ha₀ : 0 < a) (hab : a < b) (hb₁ : b < 1) :
    0 < sweepDuration s a b

Uses 1

Statement usesDuration of a logistic sweep between two frequencies

TheoremDuration of a complete deterministic sweep#✓fully proved

A complete sweep in a population of N diploids, from a single copy 1 / (2N) to 1 - 1 / (2N), takes exactly (2 / s) log (2N - 1) generations in the deterministic logistic model. (The familiar (2 / s) log (2Ns) is the conditional expected duration of the corresponding stochastic sweep, a different quantity.)

theorem sweepDuration_full {s N : ℝ} (hs : s ≠ 0) (hN : 1 < N) :
    sweepDuration s (1 / (2 * N)) (1 - 1 / (2 * N)) = (2 / s) * log (2 * N - 1)

Uses 1 · Used by 1

Statement usesDuration of a logistic sweep between two frequencies

Used byPower-law EHH after a complete sweep

Extended haplotype homozygosity under a star-shaped sweep genealogy

DefinitionEHH in the star-genealogy sweep model#✓fully proved

The probability that two carriers of a swept allele are identical over a window of genetic length d, in the star-genealogy model of Voight et al. (2006): all carriers coalesce at the start of the sweep, a time T ago, and the pair is identical exactly when neither of its two lineages recombined, each at rate r * d per unit time.

noncomputable def sweepEhh (r T d : ℝ) : ℝ := exp (-2 * (r * d) * T)

Used by 5

Used byOne-sided integrated haplotype homozygosity · One-sided iHH in the star-genealogy model · Star-genealogy EHH decays with window length · Star-genealogy EHH as a squared Poisson zero probability · Power-law EHH after a complete sweep

TheoremStar-genealogy EHH as a squared Poisson zero probability#✓fully proved

The star-genealogy EHH is the square of the probability that a Poisson number of recombination events with mean r d T on one lineage is zero.

theorem sweepEhh_eq_poisson_sq (r T d : ℝ≥0) :
    sweepEhh r T d = ((poissonMeasure (r * d * T)).real {0}) ^ 2

Uses 1

Statement usesEHH in the star-genealogy sweep model

TheoremStar-genealogy EHH decays with window length#✓fully proved

Haplotype homozygosity decays with the window length.

theorem sweepEhh_antitone {r T : ℝ} (hr : 0 ≤ r) (hT : 0 ≤ T) {d d' : ℝ} (hd : d ≤ d') :
    sweepEhh r T d' ≤ sweepEhh r T d

Uses 1

Statement usesEHH in the star-genealogy sweep model

DefinitionOne-sided integrated haplotype homozygosity#✓fully proved

The one-sided integrated haplotype homozygosity: the area under the EHH decay curve in one direction from the focal site. Voight et al.'s iHH integrates in both directions; see ihh_twoSided.

noncomputable def ihh (r T : ℝ) : ℝ := ∫ d in Ioi (0 : ℝ), sweepEhh r T d

Uses 1 · Used by 6

Statement usesEHH in the star-genealogy sweep model

Used byXP-EHH in star-genealogy sweep models · One-sided iHH in the star-genealogy model · Two-sided integrated haplotype homozygosity · Two-sided iHH in the star-genealogy model · Integrated haplotype score (iHS) · iHS as the log ratio of genealogy ages

DefinitionTwo-sided integrated haplotype homozygosity#✓fully proved

The two-sided integrated haplotype homozygosity of Voight et al.: the sum of the one-sided integrals in the two chromosome directions.

noncomputable def ihh_twoSided (r T : ℝ) : ℝ := 2 * ihh r T

Uses 1 · Used by 1

Statement usesOne-sided integrated haplotype homozygosity

Used byTwo-sided iHH in the star-genealogy model

TheoremOne-sided iHH in the star-genealogy model#✓fully proved

In the star-genealogy model the one-sided integrated haplotype homozygosity is 1 / (2 r T).

theorem ihh_eq {r T : ℝ} (hr : 0 < r) (hT : 0 < T) : ihh r T = (2 * r * T)⁻¹

Uses 2 · Used by 3

Statement usesOne-sided integrated haplotype homozygosity

Proof usesEHH in the star-genealogy sweep model

Used byXP-EHH in star-genealogy sweep models · Two-sided iHH in the star-genealogy model · iHS as the log ratio of genealogy ages

TheoremTwo-sided iHH in the star-genealogy model#✓fully proved

In the star-genealogy model the two-sided integrated haplotype homozygosity is 1 / (r T).

theorem ihh_twoSided_eq {r T : ℝ} (hr : 0 < r) (hT : 0 < T) : ihh_twoSided r T = (r * T)⁻¹

Uses 3

Statement usesTwo-sided integrated haplotype homozygosity

Proof usesOne-sided integrated haplotype homozygosity · One-sided iHH in the star-genealogy model

DefinitionIntegrated haplotype score (iHS)#✓fully proved

The integrated haplotype score of Voight et al. (2006): the log ratio of the integrated haplotype homozygosities of the ancestral and the derived allele, whose star genealogies have ages T_A and T_D. The factor of two between the one-sided and two-sided integrals cancels in this ratio.

noncomputable def ihs (r T_A T_D : ℝ) : ℝ := log (ihh r T_A / ihh r T_D)

Uses 1 · Used by 2

Statement usesOne-sided integrated haplotype homozygosity

Used byiHS as the log ratio of genealogy ages · iHS is negative exactly when the derived allele is younger

TheoremiHS as the log ratio of genealogy ages#✓fully proved

In the star-genealogy model the integrated haplotype score is the log ratio of the two ages, so the recombination rate cancels.

theorem ihs_eq_log_div {r T_A T_D : ℝ} (hr : 0 < r) (hA : 0 < T_A) (hD : 0 < T_D) :
    ihs r T_A T_D = log (T_D / T_A)

Uses 3 · Used by 1

Statement usesIntegrated haplotype score (iHS)

Proof usesOne-sided integrated haplotype homozygosity · One-sided iHH in the star-genealogy model

Used byiHS is negative exactly when the derived allele is younger

TheoremiHS is negative exactly when the derived allele is younger#✓fully proved

The integrated haplotype score is negative exactly when the derived allele's star genealogy is the younger one, i.e. when the derived allele swept faster.

theorem ihs_neg_iff {r T_A T_D : ℝ} (hr : 0 < r) (hA : 0 < T_A) (hD : 0 < T_D) :
    ihs r T_A T_D < 0 ↔ T_D < T_A

Uses 2

Statement usesIntegrated haplotype score (iHS)

Proof usesiHS as the log ratio of genealogy ages

TheoremPower-law EHH after a complete sweep#✓fully proved

Combining the exact sweep duration with the star-genealogy decay: after a complete sweep of a favourable allele with selection coefficient s in a population of N diploids, the extended haplotype homozygosity at genetic distance d is the power law (2N - 1) ^ (-(4 r d / s)).

theorem sweepEhh_sweepDuration_full {r s N d : ℝ} (hs : 0 < s) (hN : 1 < N) :
    sweepEhh r (sweepDuration s (1 / (2 * N)) (1 - 1 / (2 * N))) d
      = (2 * N - 1) ^ (-(4 * r * d / s))

noncomputable def sweepEhh (r T d : ℝ) : ℝ := exp (-2 * (r * d) * T)

MathlibExt/Biology/PopulationGenetics/SelectionScan/SelectiveSweep.lean:189

noncomputable def sweepDuration (s a b : ℝ) : ℝ := (1 / s) * log (b * (1 - a) / (a * (1 - b)))

MathlibExt/Biology/PopulationGenetics/SelectionScan/SelectiveSweep.lean:141

Uses 3

Statement usesDuration of a logistic sweep between two frequencies · EHH in the star-genealogy sweep model

Proof usesDuration of a complete deterministic sweep

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.