Admixture linkage disequilibrium

25 fully proved

Haplotype and genotype covariances

DefinitionAllele count of a gamete at one locus#✓fully proved

The 0/1 count of the '1' allele carried by a gamete at one locus.

def alleleCount (b : Bool) : ℝ := if b then 1 else 0

Used by 4

Used byCovariance of allele counts within a gamete · Gamete allele covariance equals linkage disequilibrium · Covariance of unphased diploid genotypes · Diploid genotype covariance is twice the linkage disequilibrium

DefinitionCovariance of allele counts within a gamete#✓fully proved

The covariance of the allele counts at the two loci of one gamete drawn from the gamete frequencies x: ∑ g, x g a(g.1) a(g.2) - (∑ g, x g a(g.1)) (∑ g, x g a(g.2)).

def alleleCov (x : Bool × Bool → ℝ) : ℝ :=
  ∑ g, x g * (alleleCount g.1 * alleleCount g.2) -
    (∑ g, x g * alleleCount g.1) * ∑ g, x g * alleleCount g.2

Uses 1 · Used by 3

Statement usesAllele count of a gamete at one locus

Used byCovariance of local-ancestry indicators after pulse admixture · Local-ancestry covariance in Morgans · Gamete allele covariance equals linkage disequilibrium

DefinitionCovariance of unphased diploid genotypes#✓fully proved

The covariance of the unphased diploid genotypes X = X₁ + X₂ ∈ {0, 1, 2} at the first locus and Y = Y₁ + Y₂ at the second, for an individual made of two gametes g, h drawn independently from x (random union of gametes). This is z(x, y) of Loh et al. (2013), Eq. 1.

def genotypeCov (x : Bool × Bool → ℝ) : ℝ :=
  (∑ g, ∑ h, x g * x h * ((alleleCount g.1 + alleleCount h.1) *
      (alleleCount g.2 + alleleCount h.2))) -
    (∑ g, ∑ h, x g * x h * (alleleCount g.1 + alleleCount h.1)) *
      ∑ g, ∑ h, x g * x h * (alleleCount g.2 + alleleCount h.2)

Uses 1 · Used by 4

Statement usesAllele count of a gamete at one locus

Used byDiploid genotype covariance in an admixed population · Diploid genotype covariance is twice the linkage disequilibrium · Expected ALDER weighted linkage disequilibrium · Weighted linkage disequilibrium in terms of the f4 statistic

TheoremGamete allele covariance equals linkage disequilibrium#✓fully proved

The covariance of the allele counts of one gamete is the linkage disequilibrium D = x_AB x_ab - x_Ab x_aB (frequencies summing to 1).

theorem alleleCov_eq_linkageDiseq {x : Bool × Bool → ℝ} (hx : ∑ g, x g = 1) :
    alleleCov x = linkageDiseq x

Uses 3 · Used by 1

Statement usesCovariance of allele counts within a gamete · Linkage disequilibrium of a two-locus gamete law

Proof usesAllele count of a gamete at one locus

Used byCovariance of local-ancestry indicators after pulse admixture

TheoremDiploid genotype covariance is twice the linkage disequilibrium#✓fully proved

The diploid genotype covariance is twice the haplotype one, z = 2 D: the two same-gamete terms each contribute D and the two cross-gamete terms vanish by independence (Loh et al. 2013, Eqs. 2–3).

theorem genotypeCov_eq_two_mul {x : Bool × Bool → ℝ} (hx : ∑ g, x g = 1) :
    genotypeCov x = 2 * linkageDiseq x

Uses 3 · Used by 1

Statement usesCovariance of unphased diploid genotypes · Linkage disequilibrium of a two-locus gamete law

Proof usesAllele count of a gamete at one locus

Used byDiploid genotype covariance in an admixed population

Pulse admixture of two source populations

DefinitionBernoulli allele frequency#✓fully proved

The frequency p of the '1' allele (b = true) or 1 - p of the '0' allele.

def bernFreq (p : ℝ) (b : Bool) : ℝ := if b then p else 1 - p

Used by 2

Used byAdmixture linkage disequilibrium right after the pulse · Gamete frequencies after an admixture pulse

DefinitionGamete frequencies after an admixture pulse#✓fully proved

Gamete frequencies right after the pulse: with probability α the gamete comes from A, where the loci are in linkage equilibrium with '1' frequencies pA and qA, and otherwise from B (frequencies pB, qB). The biological domain is α, pA, qA, pB, qB ∈ [0, 1]; the identities below hold for all reals.

def sourceMix (α pA qA pB qB : ℝ) (g : Bool × Bool) : ℝ :=
  α * (bernFreq pA g.1 * bernFreq qA g.2) + (1 - α) * (bernFreq pB g.1 * bernFreq qB g.2)

Uses 1 · Used by 8

Statement usesBernoulli allele frequency

Used byCovariance of local-ancestry indicators after pulse admixture · Joint law of local ancestry after an admixture pulse · Diploid genotype covariance in an admixed population · Decay of admixture linkage disequilibrium over generations · Admixture linkage disequilibrium right after the pulse · Pulse gamete frequencies sum to one · Expected ALDER weighted linkage disequilibrium · Weighted linkage disequilibrium in terms of the f4 statistic

TheoremPulse gamete frequencies sum to one#✓fully proved

The pulse gamete frequencies sum to 1.

theorem sum_sourceMix (α pA qA pB qB : ℝ) : ∑ g, sourceMix α pA qA pB qB g = 1

Uses 1 · Used by 3

Statement usesGamete frequencies after an admixture pulse

Used byCovariance of local-ancestry indicators after pulse admixture · Diploid genotype covariance in an admixed population · Decay of admixture linkage disequilibrium over generations

TheoremAdmixture linkage disequilibrium right after the pulse#✓fully proved

Admixture LD right after the pulse: D₀ = α (1 - α) δ(x) δ(y), with δ(x) = pA - pB, δ(y) = qA - qB (Chakraborty and Weiss 1988).

theorem linkageDiseq_sourceMix (α pA qA pB qB : ℝ) :
    linkageDiseq (sourceMix α pA qA pB qB) = α * (1 - α) * ((pA - pB) * (qA - qB))

Uses 3 · Used by 1

Statement usesGamete frequencies after an admixture pulse · Linkage disequilibrium of a two-locus gamete law

Proof usesBernoulli allele frequency

Used byDecay of admixture linkage disequilibrium over generations

TheoremDecay of admixture linkage disequilibrium over generations#✓fully proved

Admixture LD after n generations of random mating with recombination fraction r: D_n = (1 - r)^n α (1 - α) δ(x) δ(y).

theorem linkageDiseq_admixed (α pA qA pB qB r : ℝ) (n : ℕ) :
    linkageDiseq ((recombine r)^[n] (sourceMix α pA qA pB qB)) =
      (1 - r) ^ n * (α * (1 - α) * ((pA - pB) * (qA - qB)))

Uses 6 · Used by 2

Statement usesGamete frequencies after an admixture pulse · Linkage disequilibrium of a two-locus gamete law · Random mating with recombination

Proof usesAdmixture linkage disequilibrium right after the pulse · Pulse gamete frequencies sum to one · Linkage disequilibrium after \(t\) generations

Used byCovariance of local-ancestry indicators after pulse admixture · Diploid genotype covariance in an admixed population

TheoremRecombination preserves total gamete frequency#✓fully proved

Recombination keeps gamete frequencies summing to 1 over any number of generations.

theorem sum_iterate_recombine {x : Bool × Bool → ℝ} (hx : ∑ g, x g = 1) (r : ℝ) (n : ℕ) :
    ∑ g, (recombine r)^[n] x g = 1

Uses 2 · Used by 2

Statement usesRandom mating with recombination

Proof usesRecombination preserves total gamete frequency

Used byCovariance of local-ancestry indicators after pulse admixture · Diploid genotype covariance in an admixed population

TheoremDiploid genotype covariance in an admixed population#✓fully proved

The diploid genotype covariance in the admixed population n generations after the pulse: z(x, y) = 2 α (1 - α) (1 - r)^n δ(x) δ(y) (Loh et al. 2013, Eq. 3, with the exact discrete-generation factor (1 - r)^n in place of e^{-n d}).

theorem genotypeCov_admixed (α pA qA pB qB r : ℝ) (n : ℕ) :
    genotypeCov ((recombine r)^[n] (sourceMix α pA qA pB qB)) =
      2 * (α * (1 - α)) * (1 - r) ^ n * ((pA - pB) * (qA - qB))

Uses 8 · Used by 1

Statement usesCovariance of unphased diploid genotypes · Gamete frequencies after an admixture pulse · Random mating with recombination

Proof usesDiploid genotype covariance is twice the linkage disequilibrium · Decay of admixture linkage disequilibrium over generations · Recombination preserves total gamete frequency · Pulse gamete frequencies sum to one · Linkage disequilibrium of a two-locus gamete law

Used byWeighted linkage disequilibrium in terms of the f4 statistic

Local-ancestry covariance after a pulse

DefinitionJoint law of local ancestry after an admixture pulse#✓fully proved

Joint law of the local-ancestry labels at the two loci right after the pulse (true = descends from A): every gamete is entirely from A (probability α) or entirely from B. This is sourceMix with perfectly differentiated markers (pA = qA = 1, pB = qB = 0).

def ancestryPulse (α : ℝ) : Bool × Bool → ℝ := sourceMix α 1 1 0 0

Uses 1 · Used by 2

Statement usesGamete frequencies after an admixture pulse

Used byCovariance of local-ancestry indicators after pulse admixture · Local-ancestry covariance in Morgans

TheoremCovariance of local-ancestry indicators after pulse admixture#✓fully proved

Pulse admixture: after n generations of random mating the local-ancestry indicators at two loci with recombination fraction r have covariance Cov(I_x, I_y) = α (1 - α) (1 - r)^n (for every real α, r; the biological domain is 0 ≤ α ≤ 1, 0 ≤ r ≤ 1/2). The ancestry labels obey the two-locus random-mating recursion of Linkage.recombine (Chakraborty and Weiss 1988).

theorem alleleCov_ancestryPulse (α r : ℝ) (n : ℕ) :
    alleleCov ((recombine r)^[n] (ancestryPulse α)) = α * (1 - α) * (1 - r) ^ n

Uses 9 · Used by 1

Statement usesCovariance of allele counts within a gamete · Joint law of local ancestry after an admixture pulse · Random mating with recombination

Proof usesGamete allele covariance equals linkage disequilibrium · Decay of admixture linkage disequilibrium over generations · Gamete frequencies after an admixture pulse · Recombination preserves total gamete frequency · Pulse gamete frequencies sum to one · Linkage disequilibrium of a two-locus gamete law

Used byLocal-ancestry covariance in Morgans

Relation to the continuous form e^{-n d}

TheoremHaldane's map function: \(1 - r = e^{-d}\cosh d\)#✓fully proved

With Haldane's map function, 1 - r = e^{-d} cosh d for map length d.

theorem one_sub_haldane (d : ℝ) : 1 - haldane d = exp (-d) * cosh d

Uses 1 · Used by 1

Statement usesHaldane's map function

Used byExact decay factor under Haldane's map function

TheoremExact decay factor under Haldane's map function#✓fully proved

Exact decay in Morgans: (1 - r)^n = e^{-n d} (cosh d)^n when r = haldane d.

theorem pow_one_sub_haldane (d : ℝ) (n : ℕ) :
    (1 - haldane d) ^ n = exp (-(n * d)) * cosh d ^ n

Uses 2 · Used by 2

Statement usesHaldane's map function

Proof usesHaldane's map function: \(1 - r = e^{-d}\cosh d\)

Used byLocal-ancestry covariance in Morgans · Continuous decay is a lower bound for the exact factor under Haldane's map

TheoremContinuous decay is a lower bound for the exact factor under Haldane's map#✓fully proved

The continuous decay e^{-n d} used by Chakraborty and Weiss (1988) and Loh et al. (2013) is a lower bound for the exact factor (1 - r)^n under Haldane's map (all real d; the biological domain is 0 ≤ d).

theorem exp_neg_mul_le_pow_one_sub_haldane (d : ℝ) (n : ℕ) :
    exp (-(n * d)) ≤ (1 - haldane d) ^ n

Uses 2

Statement usesHaldane's map function

Proof usesExact decay factor under Haldane's map function

TheoremLocal-ancestry covariance in Morgans#✓fully proved

Local-ancestry covariance in Morgans: Cov(I_x, I_y) = α (1 - α) e^{-n d} (cosh d)^n for loci d Morgans apart.

theorem alleleCov_ancestryPulse_haldane (α d : ℝ) (n : ℕ) :
    alleleCov ((recombine (haldane d))^[n] (ancestryPulse α)) =
      α * (1 - α) * (exp (-(n * d)) * cosh d ^ n)

Uses 6

Statement usesCovariance of allele counts within a gamete · Joint law of local ancestry after an admixture pulse · Haldane's map function · Random mating with recombination

Proof usesCovariance of local-ancestry indicators after pulse admixture · Exact decay factor under Haldane's map function

ALDER weighted LD

DefinitionExpected ALDER weighted linkage disequilibrium#✓fully proved

The expected ALDER two-site weighted-LD statistic 𝔼[z(x, y) w(x) w(y)] (Loh et al. 2013, Appendix A, without distance binning). The loci x and y drift independently: ω.1 and ω.2 are independent draws from μ, and p X ω is the frequency of the '1' allele in population X. The covariance z(x, y) is that of the population formed n generations ago as an α : 1 - α mixture of A and B (genotypeCov_admixed), and the weights are the frequency differences w = p R - p S between two reference populations R and S.

noncomputable def weightedLD (α r : ℝ) (n : ℕ) (A B R S : P) : ℝ :=
  ∫ ω, genotypeCov ((recombine r)^[n] (sourceMix α (p A ω.1) (p A ω.2) (p B ω.1) (p B ω.2))) *
      ((p R ω.1 - p S ω.1) * (p R ω.2 - p S ω.2)) ∂μ.prod μ

Uses 3 · Used by 5

Statement usesCovariance of unphased diploid genotypes · Gamete frequencies after an admixture pulse · Random mating with recombination

Used byWeighted LD amplitude with the admixed population as reference · Weighted LD amplitude with two diverged references · Weighted linkage disequilibrium in terms of the f4 statistic · Weighted LD amplitude with one diverged reference · Weighted LD amplitude with the true source populations

TheoremWeighted linkage disequilibrium in terms of the f4 statistic#✓fully proved

The expected weighted LD factors as 2 α (1 - α) (1 - r)^n (f4 A B R S)^2: by independence of the loci, 𝔼[δ(x) w(x) δ(y) w(y)] = 𝔼[δ w]^2 and 𝔼[δ w] = f4 A B R S. The identity holds with the Bochner-integral conventions as stated; it is meaningful when the frequencies are square integrable, as in every DriftModel.

theorem weightedLD_eq [SFinite μ] (α r : ℝ) (n : ℕ) (A B R S : P) :
    weightedLD μ p α r n A B R S = 2 * (α * (1 - α)) * (1 - r) ^ n * f4 μ p A B R S ^ 2

Uses 6 · Used by 4

Statement usesExpected ALDER weighted linkage disequilibrium · f4 statistic

Proof usesCovariance of unphased diploid genotypes · Diploid genotype covariance in an admixed population · Gamete frequencies after an admixture pulse · Random mating with recombination

Used byWeighted LD amplitude with the admixed population as reference · Weighted LD amplitude with two diverged references · Weighted LD amplitude with one diverged reference · Weighted LD amplitude with the true source populations

TheoremWeighted LD amplitude with the true source populations#✓fully proved

Weights from the true mixing populations (R = A, S = B): the amplitude is 2 α β F2(A, B)^2 (Loh et al. 2013, Eq. 4).

theorem weightedLD_sources [SFinite μ] (α r : ℝ) (n : ℕ) (A B : P) :
    weightedLD μ M.freq α r n A B A B =
      2 * (α * (1 - α)) * (1 - r) ^ n * f2 μ M.freq A B ^ 2

Uses 7

Statement usesExpected ALDER weighted linkage disequilibrium · Admixture-graph drift model · Allele frequency of a population in the drift model · f2 statistic

Proof usesWeighted linkage disequilibrium in terms of the f4 statistic · f2 as a special case of f4 · f4 statistic

Theoremf4 equals f2 for references branching off the path#✓fully proved

Branch points on the A–B path. Suppose that A = A″ + uA, A′ = A″ + uA', B = B″ + uB, B′ = B″ + uB' at the level of lineage weights, where w A″ - w B″ is disjoint in support from each of uA, uB, uA', uB', and each of uA, uB is disjoint from each of uA', uB'. On a tree this says that the paths A″–B″, A″–A, B″–B, A″–A′, B″–B′ share no edge (the vectors may be signed, so every rooting is allowed). Then f4 A B A′ B′ = f2 A″ B″.

theorem f4_eq_f2_of_branch {A B A' B' A'' B'' : P} {uA uB uA' uB' : E → ℝ}
    (hA : M.weight A = M.weight A'' + uA) (hB : M.weight B = M.weight B'' + uB)
    (hA' : M.weight A' = M.weight A'' + uA') (hB' : M.weight B' = M.weight B'' + uB')
    (hdisj : ∀ e, ∀ u ∈ [uA, uB], ∀ v ∈ [uA', uB'], u e * v e = 0)
    (hpath : ∀ e, ∀ u ∈ [uA, uB, uA', uB'], (M.weight A'' e - M.weight B'' e) * u e = 0) :
    f4 μ M.freq A B A' B' = f2 μ M.freq A'' B''

Uses 6 · Used by 1

Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f2 statistic · f4 statistic

Proof usesf2 in the drift model · f4 in the drift model

Used byWeighted LD amplitude with two diverged references

TheoremWeighted LD amplitude with two diverged references#✓fully proved

Two diverged references A′, B′ branching off the A–B path at A″ and B″: the amplitude is 2 α β F2(A″, B″)^2 (Loh et al. 2013, Eq. 6).

theorem weightedLD_branch [SFinite μ] (α r : ℝ) (n : ℕ) {A B A' B' A'' B'' : P}
    {uA uB uA' uB' : E → ℝ}
    (hA : M.weight A = M.weight A'' + uA) (hB : M.weight B = M.weight B'' + uB)
    (hA' : M.weight A' = M.weight A'' + uA') (hB' : M.weight B' = M.weight B'' + uB')
    (hdisj : ∀ e, ∀ u ∈ [uA, uB], ∀ v ∈ [uA', uB'], u e * v e = 0)
    (hpath : ∀ e, ∀ u ∈ [uA, uB, uA', uB'], (M.weight A'' e - M.weight B'' e) * u e = 0) :
    weightedLD μ M.freq α r n A B A' B' =
      2 * (α * (1 - α)) * (1 - r) ^ n * f2 μ M.freq A'' B'' ^ 2

Uses 7

Statement usesExpected ALDER weighted linkage disequilibrium · Admixture-graph drift model · Allele frequency of a population in the drift model · f2 statistic

Proof usesf4 equals f2 for references branching off the path · Weighted linkage disequilibrium in terms of the f4 statistic · f4 statistic

TheoremWeighted LD amplitude with the admixed population as reference#✓fully proved

One reference A and the admixed population C itself, with no drift in C after the pulse (w C = α w A + (1 - α) w B): the weights are p A - p C = β δ and the amplitude is 2 α β^3 F2(A, B)^2 (Loh et al. 2013, Eq. 7).

theorem weightedLD_admixedRef [SFinite μ] (α r : ℝ) (n : ℕ) {A B C : P}
    (hC : M.weight C = α • M.weight A + (1 - α) • M.weight B) :
    weightedLD μ M.freq α r n A B A C =
      2 * (α * (1 - α) ^ 3) * (1 - r) ^ n * f2 μ M.freq A B ^ 2

Uses 8

Statement usesExpected ALDER weighted linkage disequilibrium · Admixture-graph drift model · Allele frequency of a population in the drift model · f2 statistic

Proof usesWeighted linkage disequilibrium in terms of the f4 statistic · f2 in the drift model · f4 in the drift model · f4 statistic

TheoremWeighted LD amplitude with one diverged reference#✓fully proved

One diverged reference R′ branching off the A–B path at R″ (so A = R″ + uA, B = R″ + uB, R′ = R″ + uR with pairwise disjoint supports) and the admixed population C with no post-pulse drift: the weights p R′ - p C give the amplitude 2 α β (α F2(A, R″) - β F2(B, R″))^2 (Loh et al. 2013, Eq. 8).

theorem weightedLD_oneRef [SFinite μ] (α r : ℝ) (n : ℕ) {A B C R' R'' : P}
    {uA uB uR : E → ℝ}
    (hA : M.weight A = M.weight R'' + uA) (hB : M.weight B = M.weight R'' + uB)
    (hR : M.weight R' = M.weight R'' + uR)
    (hAB : ∀ e, uA e * uB e = 0) (hAR : ∀ e, uA e * uR e = 0) (hBR : ∀ e, uB e * uR e = 0)
    (hC : M.weight C = α • M.weight A + (1 - α) • M.weight B) :
    weightedLD μ M.freq α r n A B R' C =
      2 * (α * (1 - α)) * (1 - r) ^ n *
        (α * f2 μ M.freq A R'' - (1 - α) * f2 μ M.freq B R'') ^ 2

Uses 8

Statement usesExpected ALDER weighted linkage disequilibrium · Admixture-graph drift model · Allele frequency of a population in the drift model · f2 statistic

Proof usesWeighted linkage disequilibrium in terms of the f4 statistic · f2 in the drift model · f4 in the drift model · f4 statistic

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.