Linkage disequilibrium and Haldane's map function

20 fully proved

Two-locus random mating

DefinitionAllele frequency at the first locus#✓fully proved

The frequency ∑ b, x (a, b) of allele a at the first locus.

def alleleFreqFst (x : Bool × Bool → ℝ) (a : Bool) : ℝ := ∑ b, x (a, b)

Used by 10

Used byOhta–Kimura σ_d² · Hill–Robertson / Ohta–Kimura, first row · Hill–Robertson / Ohta–Kimura, second row · Hill–Robertson / Ohta–Kimura, third row · Recombination preserves first-locus allele frequencies · Recombination preserves second-locus allele frequencies · Random mating with recombination · Classical form of the recombination recursion · Recombination preserves nonnegativity of gamete frequencies · Recombination preserves total gamete frequency

DefinitionAllele frequency at the second locus#✓fully proved

The frequency ∑ a, x (a, b) of allele b at the second locus.

def alleleFreqSnd (x : Bool × Bool → ℝ) (b : Bool) : ℝ := ∑ a, x (a, b)

Used by 10

Used byOhta–Kimura σ_d² · Hill–Robertson / Ohta–Kimura, first row · Hill–Robertson / Ohta–Kimura, second row · Hill–Robertson / Ohta–Kimura, third row · Recombination preserves first-locus allele frequencies · Recombination preserves second-locus allele frequencies · Random mating with recombination · Classical form of the recombination recursion · Recombination preserves nonnegativity of gamete frequencies · Recombination preserves total gamete frequency

DefinitionLinkage disequilibrium of a two-locus gamete law#✓fully proved

The linkage disequilibrium D = x_AB x_ab - x_Ab x_aB.

def linkageDiseq (x : Bool × Bool → ℝ) : ℝ :=
  x (true, true) * x (false, false) - x (true, false) * x (false, true)

Used by 15

Used byOhta–Kimura σ_d² · Hill–Robertson / Ohta–Kimura, first row · Hill–Robertson / Ohta–Kimura, second row · Hill–Robertson / Ohta–Kimura, third row · Drift of gamete frequencies matches recombination · Linkage disequilibrium after \(t\) generations · Linkage disequilibrium decays by the factor \(1 - r\) · Classical form of the recombination recursion · Linkage disequilibrium tends to zero · Covariance of local-ancestry indicators after pulse admixture · Gamete allele covariance equals linkage disequilibrium · Diploid genotype covariance in an admixed population · Diploid genotype covariance is twice the linkage disequilibrium · Decay of admixture linkage disequilibrium over generations · Admixture linkage disequilibrium right after the pulse

DefinitionRandom mating with recombination#✓fully proved

One generation of random mating with recombination fraction r: recombine r x g = (1 - r) x_g + r p_{g.1} q_{g.2}.

def recombine (r : ℝ) (x : Bool × Bool → ℝ) (g : Bool × Bool) : ℝ :=
  (1 - r) * x g + r * (alleleFreqFst x g.1 * alleleFreqSnd x g.2)

Uses 2 · Used by 16

Statement usesAllele frequency at the first locus · Allele frequency at the second locus

Used byDrift of gamete frequencies matches recombination · Recombination preserves first-locus allele frequencies · Recombination preserves second-locus allele frequencies · Linkage disequilibrium after \(t\) generations · Linkage disequilibrium decays by the factor \(1 - r\) · Classical form of the recombination recursion · Recombination preserves nonnegativity of gamete frequencies · Recombination preserves total gamete frequency · Linkage disequilibrium tends to zero · Covariance of local-ancestry indicators after pulse admixture · Local-ancestry covariance in Morgans · Diploid genotype covariance in an admixed population · Decay of admixture linkage disequilibrium over generations · Recombination preserves total gamete frequency · Expected ALDER weighted linkage disequilibrium · Weighted linkage disequilibrium in terms of the f4 statistic

TheoremClassical form of the recombination recursion#✓fully proved

The classical form of the recursion: coupling gametes (AB, ab) lose r D and repulsion gametes (Ab, aB) gain r D. This identity holds for every real r; the biological domain is 0 ≤ r ≤ 1/2.

theorem recombine_eq_sub {x : Bool × Bool → ℝ} (hx : ∑ g, x g = 1) (r : ℝ) (g : Bool × Bool) :
    recombine r x g = x g - (if g.1 = g.2 then 1 else -1) * r * linkageDiseq x

Uses 4 · Used by 2

Statement usesLinkage disequilibrium of a two-locus gamete law · Random mating with recombination

Proof usesAllele frequency at the first locus · Allele frequency at the second locus

Used byDrift of gamete frequencies matches recombination · Linkage disequilibrium decays by the factor \(1 - r\)

TheoremRecombination preserves total gamete frequency#✓fully proved

Recombination keeps gamete frequencies summing to 1.

theorem sum_recombine {x : Bool × Bool → ℝ} (hx : ∑ g, x g = 1) (r : ℝ) :
    ∑ g, recombine r x g = 1

Uses 3 · Used by 2

Statement usesRandom mating with recombination

Proof usesAllele frequency at the first locus · Allele frequency at the second locus

Used byLinkage disequilibrium after \(t\) generations · Recombination preserves total gamete frequency

TheoremRecombination preserves nonnegativity of gamete frequencies#✓fully proved

Recombination keeps gamete frequencies nonnegative for 0 ≤ r ≤ 1.

theorem recombine_nonneg {x : Bool × Bool → ℝ} (hx : ∀ g, 0 ≤ x g) {r : ℝ} (hr0 : 0 ≤ r)
    (hr1 : r ≤ 1) (g : Bool × Bool) : 0 ≤ recombine r x g

Uses 3

Statement usesRandom mating with recombination

Proof usesAllele frequency at the first locus · Allele frequency at the second locus

TheoremRecombination preserves first-locus allele frequencies#✓fully proved

Allele frequencies at the first locus are unchanged by random mating (for every real r).

theorem alleleFreqFst_recombine {x : Bool × Bool → ℝ} (hx : ∑ g, x g = 1) (r : ℝ) (a : Bool) :
    alleleFreqFst (recombine r x) a = alleleFreqFst x a

Uses 3

Statement usesAllele frequency at the first locus · Random mating with recombination

Proof usesAllele frequency at the second locus

TheoremRecombination preserves second-locus allele frequencies#✓fully proved

Allele frequencies at the second locus are unchanged by random mating (for every real r).

theorem alleleFreqSnd_recombine {x : Bool × Bool → ℝ} (hx : ∑ g, x g = 1) (r : ℝ) (b : Bool) :
    alleleFreqSnd (recombine r x) b = alleleFreqSnd x b

Uses 3

Statement usesAllele frequency at the second locus · Random mating with recombination

Proof usesAllele frequency at the first locus

TheoremLinkage disequilibrium decays by the factor \(1 - r\)#✓fully proved

Linkage disequilibrium decays by the factor 1 - r per generation: D' = (1 - r) D (for every real r).

theorem linkageDiseq_recombine {x : Bool × Bool → ℝ} (hx : ∑ g, x g = 1) (r : ℝ) :
    linkageDiseq (recombine r x) = (1 - r) * linkageDiseq x

Uses 3 · Used by 1

Statement usesLinkage disequilibrium of a two-locus gamete law · Random mating with recombination

Proof usesClassical form of the recombination recursion

Used byLinkage disequilibrium after \(t\) generations

TheoremLinkage disequilibrium after \(t\) generations#✓fully proved

After t generations, D_t = (1 - r)^t D_0.

theorem linkageDiseq_iterate {x : Bool × Bool → ℝ} (hx : ∑ g, x g = 1) (r : ℝ) (t : ℕ) :
    linkageDiseq ((recombine r)^[t] x) = (1 - r) ^ t * linkageDiseq x

Uses 4 · Used by 2

Statement usesLinkage disequilibrium of a two-locus gamete law · Random mating with recombination

Proof usesLinkage disequilibrium decays by the factor \(1 - r\) · Recombination preserves total gamete frequency

Used byLinkage disequilibrium tends to zero · Decay of admixture linkage disequilibrium over generations

TheoremLinkage disequilibrium tends to zero#✓fully proved

Linkage disequilibrium tends to 0 whenever 0 < r ≤ 1; this contains the biological range 0 < r ≤ 1/2. For r = 0 (complete linkage) D is constant.

theorem tendsto_linkageDiseq_iterate {x : Bool × Bool → ℝ} (hx : ∑ g, x g = 1) {r : ℝ}
    (hr0 : 0 < r) (hr1 : r ≤ 1) :
    Tendsto (fun t : ℕ => linkageDiseq ((recombine r)^[t] x)) atTop (𝓝 0)

Uses 3

Statement usesLinkage disequilibrium of a two-locus gamete law · Random mating with recombination

Proof usesLinkage disequilibrium after \(t\) generations

Haldane's map function

DefinitionHaldane's map function#✓fully proved

Haldane's map function r(d) = (1 - e^{-2d}) / 2: the recombination fraction between two loci at map distance d Morgans when crossovers form a Poisson process (no interference).

noncomputable def haldane (d : ℝ) : ℝ := (1 - exp (-2 * d)) / 2

Used by 11

Used byHaldane's recombination fraction is below one half · Every recombination fraction below one half is attained · Nonnegativity of Haldane's map function · Series for the probability of an odd Poisson count · Inverse Haldane map function recovers map distance · Haldane's map function from Poisson crossovers · Distant loci are unlinked in the limit · Local-ancestry covariance in Morgans · Continuous decay is a lower bound for the exact factor under Haldane's map · Haldane's map function: \(1 - r = e^{-d}\cosh d\) · Exact decay factor under Haldane's map function

TheoremSeries for the probability of an odd Poisson count#✓fully proved

The probability that a Poisson count of mean d is odd, as a series: ∑_{k odd} e^{-d} d^k / k! = (1 - e^{-2d}) / 2 (Haldane 1919). The series identity holds for every real d; it is a probability for 0 ≤ d.

theorem hasSum_poisson_odd (d : ℝ) :
    HasSum (fun k : ℕ => if Odd k then exp (-d) * d ^ k / k ! else 0) (haldane d)

Uses 1 · Used by 1

Statement usesHaldane's map function

Used byHaldane's map function from Poisson crossovers

TheoremHaldane's map function from Poisson crossovers#✓fully proved

Haldane's map function (Haldane 1919): if the number of crossovers in an interval of map length d Morgans is Poisson with mean d, the probability of an odd number of crossovers, i.e. of recombination between the ends of the interval, is (1 - e^{-2d}) / 2.

theorem poissonMeasure_real_odd (d : ℝ≥0) :
    (poissonMeasure d).real {k | Odd k} = haldane d

Uses 2

Statement usesHaldane's map function

Proof usesSeries for the probability of an odd Poisson count

TheoremNonnegativity of Haldane's map function#✓fully proved

Haldane's map function is nonnegative at nonnegative distances.

theorem haldane_nonneg {d : ℝ} (hd : 0 ≤ d) : 0 ≤ haldane d

Uses 1

Statement usesHaldane's map function

TheoremHaldane's recombination fraction is below one half#✓fully proved

The recombination fraction is always below 1/2 (for every real d).

theorem haldane_lt_half (d : ℝ) : haldane d < 1 / 2

Uses 1

Statement usesHaldane's map function

TheoremDistant loci are unlinked in the limit#✓fully proved

Loci far apart are unlinked in the limit: r → 1/2 as d → ∞.

theorem tendsto_haldane_atTop : Tendsto haldane atTop (𝓝 (1 / 2))

Uses 1

Statement usesHaldane's map function

TheoremInverse Haldane map function recovers map distance#✓fully proved

The inverse map function d = -½ log(1 - 2r) recovers the map distance.

theorem neg_half_log_haldane (d : ℝ) : -(1 / 2) * log (1 - 2 * haldane d) = d

Uses 1

Statement usesHaldane's map function

TheoremEvery recombination fraction below one half is attained#✓fully proved

Every r < 1/2 is the recombination fraction at the distance -½ log(1 - 2r). The hypothesis keeps log on positive arguments: at r = 1/2 the right side would use the junk value log 0 = 0. The distance is nonnegative exactly when 0 ≤ r.

theorem haldane_neg_half_log {r : ℝ} (hr : r < 1 / 2) :
    haldane (-(1 / 2) * log (1 - 2 * r)) = r

Uses 1

Statement usesHaldane's map function

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.