Skip to content

ABBA–BABA test and f-statistic estimators

39 fully proved

Site patterns

DefinitionProbability of a derived-allele configuration#✓fully proved

Probability of the derived/ancestral configuration x when haplotype i is sampled independently and carries the derived allele with probability q i.

def configProb {n : ℕ} (q : Fin n → ℝ) (x : Fin n → Bool) : ℝ :=
  ∏ i, if x i then q i else 1 - q i
Used by 6
Used bySampling expectation is an expectation of independent indicators · Expectation under independent haplotype sampling · Additivity of the sampling expectation · Sampling expectation of a product factorizes · Sampling expectation commutes with subtraction · Configuration probabilities sum to one

DefinitionExpectation under independent haplotype sampling#✓fully proved

Expectation of a function g of the configuration under independent sampling of one haplotype per population at derived-allele frequencies q.

def sampleExpect {n : ℕ} (g : (Fin n → Bool) → ℝ) (q : Fin n → ℝ) : ℝ :=
  ∑ x, g x * configProb q x
Uses 1 · Used by 8
Statement usesProbability of a derived-allele configuration
Used bySampling expectation is an expectation of independent indicators · The unpolarized D-statistic numerator vanishes on a tree · ABBA–BABA equals f4 · Additivity of the sampling expectation · Expected polarized ABBA–BABA difference · ABBA–BABA identity · Sampling expectation of a product factorizes · Sampling expectation commutes with subtraction

DefinitionUnpolarized ABBA site-pattern indicator#✓fully proved

Unpolarized ABBA indicator for populations (P1, P2, P3, O): P1 agrees with O, P2 with P3, and P1 differs from P2 (the patterns ABBA and BAAB).

def abba (x : Fin 4 → Bool) : ℝ := if x 0 = x 3 ∧ x 1 = x 2 ∧ x 0 ≠ x 1 then 1 else 0
Used by 4
Used byABBA–BABA site-pattern identity · The unpolarized D-statistic numerator vanishes on a tree · ABBA–BABA equals f4 · ABBA–BABA identity

DefinitionUnpolarized BABA site-pattern indicator#✓fully proved

Unpolarized BABA indicator for populations (P1, P2, P3, O): P1 agrees with P3, P2 with O, and P1 differs from P2 (the patterns BABA and ABAB).

def baba (x : Fin 4 → Bool) : ℝ := if x 0 = x 2 ∧ x 1 = x 3 ∧ x 0 ≠ x 1 then 1 else 0
Used by 4
Used byABBA–BABA site-pattern identity · The unpolarized D-statistic numerator vanishes on a tree · ABBA–BABA equals f4 · ABBA–BABA identity

DefinitionPolarized ABBA site-pattern indicator#✓fully proved

Polarized ABBA indicator (Durand et al. 2011): P1 and O ancestral, P2 and P3 derived.

def abbaPol (x : Fin 4 → Bool) : ℝ :=
  if x 0 = false ∧ x 1 = true ∧ x 2 = true ∧ x 3 = false then 1 else 0
Used by 1
Used byExpected polarized ABBA–BABA difference

DefinitionPolarized BABA site-pattern indicator#✓fully proved

Polarized BABA indicator (Durand et al. 2011): P1 and P3 derived, P2 and O ancestral.

def babaPol (x : Fin 4 → Bool) : ℝ :=
  if x 0 = true ∧ x 1 = false ∧ x 2 = true ∧ x 3 = false then 1 else 0
Used by 1
Used byExpected polarized ABBA–BABA difference

TheoremConfiguration probabilities sum to one#✓fully proved

The configuration probabilities sum to 1.

theorem sum_configProb {n : ℕ} (q : Fin n → ℝ) : ∑ x, configProb q x = 1
Uses 1
Statement usesProbability of a derived-allele configuration

TheoremSampling expectation of a product factorizes#✓fully proved

sampleExpect of a product of functions of single coordinates factorizes: E[∏ i, g i (x i)] = ∏ i, (g i true * q i + g i false * (1 - q i)).

theorem sampleExpect_prod {n : ℕ} (g : Fin n → Bool → ℝ) (q : Fin n → ℝ) :
    sampleExpect (fun x => ∏ i, g i (x i)) q =
      ∏ i, (g i true * q i + g i false * (1 - q i))
Uses 2 · Used by 2
Statement usesExpectation under independent haplotype sampling
Proof usesProbability of a derived-allele configuration
Used byExpected polarized ABBA–BABA difference · ABBA–BABA identity

TheoremAdditivity of the sampling expectation#✓fully proved

sampleExpect is additive in the function.

theorem sampleExpect_add {n : ℕ} (f g : (Fin n → Bool) → ℝ) (q : Fin n → ℝ) :
    sampleExpect (fun x => f x + g x) q = sampleExpect f q + sampleExpect g q
Uses 2 · Used by 1
Statement usesExpectation under independent haplotype sampling
Proof usesProbability of a derived-allele configuration
Used byABBA–BABA identity

TheoremSampling expectation commutes with subtraction#✓fully proved

sampleExpect commutes with subtraction of functions.

theorem sampleExpect_sub {n : ℕ} (f g : (Fin n → Bool) → ℝ) (q : Fin n → ℝ) :
    sampleExpect (fun x => f x - g x) q = sampleExpect f q - sampleExpect g q
Uses 2 · Used by 3
Statement usesExpectation under independent haplotype sampling
Proof usesProbability of a derived-allele configuration
Used byThe unpolarized D-statistic numerator vanishes on a tree · Expected polarized ABBA–BABA difference · ABBA–BABA identity

TheoremSampling expectation is an expectation of independent indicators#✓fully proved

sampleExpect is the expectation under independent sampling: if the derived-allele indicators X i are independent random variables with P(X i = true) = q i, then E[g (X 0, …, X (n - 1))] = sampleExpect g q.

theorem integral_eq_sampleExpect {Ω : Type*} {mΩ : MeasurableSpace Ω} {ν : Measure Ω}
    [IsProbabilityMeasure ν] {n : ℕ} {X : Fin n → Ω → Bool} (hX : ∀ i, Measurable (X i))
    (hind : iIndepFun X ν) {q : Fin n → ℝ} (hq : ∀ i, ν.real {ω | X i ω = true} = q i)
    (g : (Fin n → Bool) → ℝ) :
    ∫ ω, g (fun i => X i ω) ∂ν = sampleExpect g q
Uses 2
Statement usesExpectation under independent haplotype sampling
Proof usesProbability of a derived-allele configuration

TheoremABBA–BABA site-pattern identity#✓fully proved

The site-pattern identity: 1[BABA] - 1[ABBA] = (x₁ - x₂) (x₃ - x₄) for every configuration of derived-allele indicators.

theorem baba_sub_abba (x : Fin 4 → Bool) :
    baba x - abba x =
      (((x 0).toNat : ℝ) - (x 1).toNat) * (((x 2).toNat : ℝ) - (x 3).toNat)
Uses 2 · Used by 1
Statement usesUnpolarized ABBA site-pattern indicator · Unpolarized BABA site-pattern indicator
Used byABBA–BABA identity

TheoremABBA–BABA identity#✓fully proved

ABBA–BABA identity (Patterson et al. 2012; Durand et al. 2011): under independent sampling of one haplotype per population at derived-allele frequencies q (any reals; frequencies in [0, 1] in the biological model), E[BABA - ABBA] = (q₁ - q₂) (q₃ - q₄).

theorem sampleExpect_baba_sub_abba (q : Fin 4 → ℝ) :
    sampleExpect (fun x => baba x - abba x) q = (q 0 - q 1) * (q 2 - q 3)
Uses 7 · Used by 1
Statement usesUnpolarized ABBA site-pattern indicator · Unpolarized BABA site-pattern indicator · Expectation under independent haplotype sampling
Proof usesABBA–BABA site-pattern identity · Additivity of the sampling expectation · Sampling expectation of a product factorizes · Sampling expectation commutes with subtraction
Used byABBA–BABA equals f4

TheoremExpected polarized ABBA–BABA difference#✓fully proved

Polarized form (Durand et al. 2011, with q 3 the derived-allele frequency in the outgroup): E[BABA_pol - ABBA_pol] = (q₁ - q₂) q₃ (1 - q₄). When the outgroup is fixed for the ancestral allele (q 3 = 0) this is (q₁ - q₂) (q₃ - q₄), as in the unpolarized identity.

theorem sampleExpect_babaPol_sub_abbaPol (q : Fin 4 → ℝ) :
    sampleExpect (fun x => babaPol x - abbaPol x) q = (q 0 - q 1) * q 2 * (1 - q 3)
Uses 5
Statement usesPolarized ABBA site-pattern indicator · Polarized BABA site-pattern indicator · Expectation under independent haplotype sampling
Proof usesSampling expectation of a product factorizes · Sampling expectation commutes with subtraction

TheoremABBA–BABA equals f4#✓fully proved

When the frequencies p X ω are themselves random (drift, and the choice of locus) and one haplotype is sampled from each population independently given the frequencies, the expected BABA - ABBA difference is f4 P1 P2 P3 O.

theorem integral_sampleExpect_baba_sub_abba (P1 P2 P3 O : P) :
    ∫ ω, sampleExpect (fun x => baba x - abba x) ![p P1 ω, p P2 ω, p P3 ω, p O ω] ∂μ =
      f4 μ p P1 P2 P3 O
Uses 5 · Used by 1
Statement usesUnpolarized ABBA site-pattern indicator · Unpolarized BABA site-pattern indicator · Expectation under independent haplotype sampling · f4 statistic
Proof usesABBA–BABA identity
Used byThe unpolarized D-statistic numerator vanishes on a tree

The qpAdm model equation

TheoremLinearity of the f4-statistic in its first pair#✓fully proved

Linearity of f4 in its first pair: if p A - p B = ∑ l, c l * (p (C l) - p (D l)) pointwise, then f4 A B Y Z = ∑ l, c l * f4 (C l) (D l) Y Z.

theorem f4_eq_sum_of_sub_eq_sum (hp : ∀ X, MemLp (p X) 2 μ) {ι : Type*} [Fintype ι]
    {A B Y Z : P} (C D : ι → P) (c : ι → ℝ)
    (h : ∀ ω, p A ω - p B ω = ∑ l, c l * (p (C l) ω - p (D l) ω)) :
    f4 μ p A B Y Z = ∑ l, c l * f4 μ p (C l) (D l) Y Z
Uses 1 · Used by 2
Statement usesf4 statistic
Used byqpAdm model equation · qpWave rank bound

TheoremqpAdm model equation#✓fully proved

qpAdm model equation (Haak et al. 2015, Supplementary Information): if the target T is an admixture of sources S k with weights w k summing to 1 (p T = ∑ k, w k * p (S k) pointwise; the weights may be negative, as in fitted qpAdm models), then for all X, Y, Z, f4 T X Y Z = ∑ k, w k * f4 (S k) X Y Z. The merged DriftModel.f4_admixture_right is a two-source drift-model instance (mixture in the second pair, one source as fourth argument).

theorem f4_affine_combination (hp : ∀ X, MemLp (p X) 2 μ) {ι : Type*} [Fintype ι]
    {T X Y Z : P} (S : ι → P) (w : ι → ℝ) (hw : ∑ k, w k = 1)
    (hT : ∀ ω, p T ω = ∑ k, w k * p (S k) ω) :
    f4 μ p T X Y Z = ∑ k, w k * f4 μ p (S k) X Y Z
Uses 2
Statement usesf4 statistic
Proof usesLinearity of the f4-statistic in its first pair

The qpWave rank bound

DefinitionqpWave matrix of f4-statistics#✓fully proved

The qpWave matrix of left populations L 0, …, L n and right populations R 0, …, R r: entry (i, j) is f4 (L (i + 1)) (L 0) (R (j + 1)) (R 0).

noncomputable def f4Matrix {n r : ℕ} (L : Fin (n + 1) → P) (R : Fin (r + 1) → P) :
    Matrix (Fin n) (Fin r) ℝ :=
  Matrix.of fun i j => f4 μ p (L i.succ) (L 0) (R j.succ) (R 0)
Uses 1 · Used by 1
Statement usesf4 statistic
Used byqpWave rank bound

TheoremqpWave rank bound#✓fully proved

qpWave rank bound (Reich et al. 2012, Supplementary Information; Patterson et al. 2012): if the frequency of every left population L i is an affine combination ∑ l, a i l * p (S l) (∑ l, a i l = 1, coefficients of any sign) of the frequencies of k + 1 source populations, then the matrix f4 (L i) (L 0) (R j) (R 0) (i, j ≥ 1) has rank at most k; with k sources, at most k - 1. The right populations are arbitrary. The converse (rank k forces k + 1 streams) and the statistical rank test are not covered.

theorem rank_f4Matrix_le (hp : ∀ X, MemLp (p X) 2 μ) {n r k : ℕ} (L : Fin (n + 1) → P)
    (R : Fin (r + 1) → P) (S : Fin (k + 1) → P) (a : Fin (n + 1) → Fin (k + 1) → ℝ)
    (ha : ∀ i, ∑ l, a i l = 1) (hL : ∀ i ω, p (L i) ω = ∑ l, a i l * p (S l) ω) :
    (f4Matrix μ p L R).rank ≤ k
Uses 3
Statement usesqpWave matrix of f4-statistics
Proof usesLinearity of the f4-statistic in its first pair · f4 statistic

Unbiased estimators under binomial sampling

DefinitionUnbiased heterozygosity estimator#✓fully proved

Unbiased estimator of p (1 - p) from x derived copies among m sampled copies: x (m - x) / (m (m - 1)) (meaningful for m ≥ 2).

noncomputable def hetHat (m : ℕ) (x : ℝ) : ℝ := x * (m - x) / (m * (m - 1))
Used by 6
Used byUnbiased f2 estimator · Unbiased f3 estimator · Unbiased f2 · Unbiased f3 · Unbiased heterozygosity · Unbiasedness of the summed f2 estimator

DefinitionUnbiased f2 estimator#✓fully proved

The unbiased f2 estimator of Patterson et al. (2012), Appendix: (â - b̂)² - â (1 - â) / (m_A - 1) - b̂ (1 - b̂) / (m_B - 1) with â = x_A / m_A, written as (x_A / m_A - x_B / m_B)² - x_A (m_A - x_A) / (m_A² (m_A - 1)) - ….

noncomputable def f2Hat (mA mB : ℕ) (xA xB : ℝ) : ℝ :=
  (xA / mA - xB / mB) ^ 2 - hetHat mA xA / mA - hetHat mB xB / mB
Uses 1 · Used by 3
Statement usesUnbiased heterozygosity estimator
Used byUnbiased f2 · Hudson's F_ST, ratio of averages · Unbiasedness of the summed f2 estimator

DefinitionUnbiased f3 estimator#✓fully proved

The unbiased f3 estimator of Patterson et al. (2012), Appendix: (ĉ - â) (ĉ - b̂) - ĉ (1 - ĉ) / (m_C - 1).

noncomputable def f3Hat (mC mA mB : ℕ) (xC xA xB : ℝ) : ℝ :=
  (xC / mC - xA / mA) * (xC / mC - xB / mB) - hetHat mC xC / mC
Uses 1 · Used by 1
Statement usesUnbiased heterozygosity estimator
Used byUnbiased f3

Definitionf4 estimator#✓fully proved

The f4 estimator (â - b̂) (ĉ - d̂); it needs no correction for four distinct populations.

noncomputable def f4Hat (mA mB mC mD : ℕ) (xA xB xC xD : ℝ) : ℝ :=
  (xA / mA - xB / mB) * (xC / mC - xD / mD)
Used by 1
Used byUnbiased f4

DefinitionEstimator of Hudson's F_ST denominator#✓fully proved

Hudson's F_ST denominator estimator â (1 - b̂) + b̂ (1 - â) (Bhatia et al. 2013); the numerator estimator is f2Hat.

noncomputable def hudsonDenHat (mA mB : ℕ) (xA xB : ℝ) : ℝ :=
  xA / mA * (1 - xB / mB) + xB / mB * (1 - xA / mA)
Used by 3
Used byHudson's denominator is unbiased · Hudson's F_ST, ratio of averages · Unbiasedness of the summed Hudson denominator estimator

DefinitionHudson's F_ST denominator at one site#✓fully proved

Hudson's F_ST denominator at one site: p_A (1 - p_B) + p_B (1 - p_A), the probability that two copies, one from each population, differ. The numerator is (p_A - p_B) ^ 2.

def hudsonDen (pA pB : ℝ) : ℝ := pA * (1 - pB) + pB * (1 - pA)
Used by 6
Used byHudson's F_ST (ratio of averages) · Hudson's F_ST lies between 0 and 1 · Hudson's denominator is unbiased · Hudson's F_ST, ratio of averages · Unbiasedness of the summed Hudson denominator estimator · Hudson's numerator is at most the denominator

DefinitionHudson's F_ST (ratio of averages)#✓fully proved

Hudson's F_ST over sites s in the ratio-of-averages form of Bhatia et al. (2013): ∑ s, (p_A s - p_B s) ^ 2 / ∑ s, hudsonDen (p_A s) (p_B s). It is defined when the denominator is positive (it vanishes only if every site is fixed for the same allele in both populations); otherwise Lean's value 0 is a junk value.

noncomputable def hudsonFst {ι : Type*} (s : Finset ι) (pA pB : ι → ℝ) : ℝ :=
  (∑ i ∈ s, (pA i - pB i) ^ 2) / ∑ i ∈ s, hudsonDen (pA i) (pB i)
Uses 1 · Used by 2
Statement usesHudson's F_ST denominator at one site
Used byHudson's F_ST lies between 0 and 1 · Hudson's F_ST, ratio of averages

TheoremHudson's numerator is at most the denominator#✓fully proved

At each site Hudson's numerator is at most the denominator for frequencies in [0, 1]: the difference is p_A (1 - p_A) + p_B (1 - p_B) ≥ 0.

theorem sq_sub_le_hudsonDen {pA pB : ℝ} (hA0 : 0 ≤ pA) (hA1 : pA ≤ 1) (hB0 : 0 ≤ pB)
    (hB1 : pB ≤ 1) : (pA - pB) ^ 2 ≤ hudsonDen pA pB
Uses 1 · Used by 1
Statement usesHudson's F_ST denominator at one site
Used byHudson's F_ST lies between 0 and 1

TheoremHudson's F_ST lies between 0 and 1#✓fully proved

Hudson's F_ST lies in [0, 1] for frequencies in [0, 1]. (When the denominator vanishes the junk value 0 also lies in [0, 1], so no positivity hypothesis is needed.)

theorem hudsonFst_mem_Icc {ι : Type*} (s : Finset ι) (pA pB : ι → ℝ)
    (hA : ∀ i ∈ s, pA i ∈ Set.Icc (0 : ℝ) 1) (hB : ∀ i ∈ s, pB i ∈ Set.Icc (0 : ℝ) 1) :
    hudsonFst s pA pB ∈ Set.Icc (0 : ℝ) 1
Uses 3
Statement usesHudson's F_ST (ratio of averages)
Proof usesHudson's F_ST denominator at one site · Hudson's numerator is at most the denominator

TheoremSample allele frequency is unbiased#✓fully proved

The sample frequency is unbiased: for X ~ Bin(m, p) with m ≥ 1, E[X / m] = p. (For m = 0, X / 0 = 0 is a junk value, hence m ≥ 1.)

theorem integral_div_of_hasLaw_binomial {X : Ω → ℝ} {m : ℕ} {q : I}
    (hX : HasLaw X Bin(ℝ, m, q) μ) (hm : 1 ≤ m) : μ[fun ω => X ω / m] = (q : ℝ)
Used by 5
Used byUnbiased f2 · Unbiased f3 · Unbiased f4 · Unbiased heterozygosity · Hudson's denominator is unbiased

TheoremUnbiased heterozygosity#✓fully proved

For X ~ Bin(m, p) with m ≥ 2, E[X (m - X) / (m (m - 1))] = p (1 - p).

theorem integral_hetHat {X : Ω → ℝ} {m : ℕ} {q : I} (hX : HasLaw X Bin(ℝ, m, q) μ)
    (hm : 2 ≤ m) : μ[fun ω => hetHat m (X ω)] = q * (1 - (q : ℝ))
Uses 3
Statement usesUnbiased heterozygosity estimator
Proof usesSample allele frequency is unbiased · Second factorial moment of a binomial random variable

TheoremUnbiased f2#✓fully proved

Unbiased f2 (Patterson et al. 2012, Appendix): with independent binomial samples X_A ~ Bin(m_A, p_A), X_B ~ Bin(m_B, p_B), m_A, m_B ≥ 2, E[f2Hat] = (p_A - p_B) ^ 2, the population f2 at the site.

theorem integral_f2Hat {XA XB : Ω → ℝ} {mA mB : ℕ} {qA qB : I}
    (hA : HasLaw XA Bin(ℝ, mA, qA) μ) (hB : HasLaw XB Bin(ℝ, mB, qB) μ) (hAB : IndepFun XA XB μ)
    (hmA : 2 ≤ mA) (hmB : 2 ≤ mB) :
    μ[fun ω => f2Hat mA mB (XA ω) (XB ω)] = ((qA : ℝ) - qB) ^ 2
Uses 4 · Used by 1
Statement usesUnbiased f2 estimator
Proof usesUnbiased heterozygosity estimator · Sample allele frequency is unbiased · Second factorial moment of a binomial random variable
Used byUnbiasedness of the summed f2 estimator

TheoremUnbiased f3#✓fully proved

Unbiased f3 (Patterson et al. 2012, Appendix): with pairwise independent binomial samples, m_C ≥ 2 and m_A, m_B ≥ 1, E[f3Hat] = (p_C - p_A) (p_C - p_B).

theorem integral_f3Hat {XC XA XB : Ω → ℝ} {mC mA mB : ℕ} {qC qA qB : I}
    (hC : HasLaw XC Bin(ℝ, mC, qC) μ) (hA : HasLaw XA Bin(ℝ, mA, qA) μ)
    (hB : HasLaw XB Bin(ℝ, mB, qB) μ) (hCA : IndepFun XC XA μ) (hCB : IndepFun XC XB μ)
    (hAB : IndepFun XA XB μ) (hmC : 2 ≤ mC) (hmA : 1 ≤ mA) (hmB : 1 ≤ mB) :
    μ[fun ω => f3Hat mC mA mB (XC ω) (XA ω) (XB ω)] = ((qC : ℝ) - qA) * ((qC : ℝ) - qB)
Uses 4
Statement usesUnbiased f3 estimator
Proof usesUnbiased heterozygosity estimator · Sample allele frequency is unbiased · Second factorial moment of a binomial random variable

TheoremUnbiased f4#✓fully proved

For four populations sampled independently across the two pairs (m ≥ 1 each), E[f4Hat] = (p_A - p_B) (p_C - p_D); no correction is needed.

theorem integral_f4Hat {XA XB XC XD : Ω → ℝ} {mA mB mC mD : ℕ} {qA qB qC qD : I}
    (hA : HasLaw XA Bin(ℝ, mA, qA) μ) (hB : HasLaw XB Bin(ℝ, mB, qB) μ)
    (hC : HasLaw XC Bin(ℝ, mC, qC) μ) (hD : HasLaw XD Bin(ℝ, mD, qD) μ)
    (hAC : IndepFun XA XC μ) (hAD : IndepFun XA XD μ) (hBC : IndepFun XB XC μ)
    (hBD : IndepFun XB XD μ) (hmA : 1 ≤ mA) (hmB : 1 ≤ mB) (hmC : 1 ≤ mC) (hmD : 1 ≤ mD) :
    μ[fun ω => f4Hat mA mB mC mD (XA ω) (XB ω) (XC ω) (XD ω)] =
      ((qA : ℝ) - qB) * ((qC : ℝ) - qD)
Uses 2
Statement usesf4 estimator
Proof usesSample allele frequency is unbiased

TheoremHudson's denominator is unbiased#✓fully proved

Hudson's denominator is unbiased (Bhatia et al. 2013): with independent binomial samples (m ≥ 1 each), E[hudsonDenHat] = hudsonDen p_A p_B.

theorem integral_hudsonDenHat {XA XB : Ω → ℝ} {mA mB : ℕ} {qA qB : I}
    (hA : HasLaw XA Bin(ℝ, mA, qA) μ) (hB : HasLaw XB Bin(ℝ, mB, qB) μ) (hAB : IndepFun XA XB μ)
    (hmA : 1 ≤ mA) (hmB : 1 ≤ mB) :
    μ[fun ω => hudsonDenHat mA mB (XA ω) (XB ω)] = hudsonDen qA qB
Uses 3 · Used by 1
Statement usesHudson's F_ST denominator at one site · Estimator of Hudson's F_ST denominator
Proof usesSample allele frequency is unbiased
Used byUnbiasedness of the summed Hudson denominator estimator

TheoremUnbiasedness of the summed f2 estimator#✓fully proved

Summed over sites, Hudson's numerator estimator ∑ s, f2Hat is unbiased for ∑ s, (p_A s - p_B s) ^ 2 (independence is needed only within each site).

theorem integral_sum_f2Hat (hA : ∀ i ∈ s, HasLaw (XA i) Bin(ℝ, mA i, qA i) μ)
    (hB : ∀ i ∈ s, HasLaw (XB i) Bin(ℝ, mB i, qB i) μ)
    (hAB : ∀ i ∈ s, IndepFun (XA i) (XB i) μ) (hmA : ∀ i ∈ s, 2 ≤ mA i)
    (hmB : ∀ i ∈ s, 2 ≤ mB i) :
    μ[fun ω => ∑ i ∈ s, f2Hat (mA i) (mB i) (XA i ω) (XB i ω)] =
      ∑ i ∈ s, ((qA i : ℝ) - qB i) ^ 2
Uses 3 · Used by 1
Statement usesUnbiased f2 estimator
Proof usesUnbiased heterozygosity estimator · Unbiased f2
Used byHudson's F_ST, ratio of averages

TheoremUnbiasedness of the summed Hudson denominator estimator#✓fully proved

Summed over sites, Hudson's denominator estimator is unbiased for ∑ s, hudsonDen (p_A s) (p_B s).

theorem integral_sum_hudsonDenHat (hA : ∀ i ∈ s, HasLaw (XA i) Bin(ℝ, mA i, qA i) μ)
    (hB : ∀ i ∈ s, HasLaw (XB i) Bin(ℝ, mB i, qB i) μ)
    (hAB : ∀ i ∈ s, IndepFun (XA i) (XB i) μ) (hmA : ∀ i ∈ s, 1 ≤ mA i)
    (hmB : ∀ i ∈ s, 1 ≤ mB i) :
    μ[fun ω => ∑ i ∈ s, hudsonDenHat (mA i) (mB i) (XA i ω) (XB i ω)] =
      ∑ i ∈ s, hudsonDen (qA i) (qB i)
Uses 3 · Used by 1
Statement usesHudson's F_ST denominator at one site · Estimator of Hudson's F_ST denominator
Proof usesHudson's denominator is unbiased
Used byHudson's F_ST, ratio of averages

TheoremHudson's F_ST, ratio of averages#✓fully proved

Hudson's F_ST, ratio of averages (Bhatia et al. 2013): the ratio of the expected summed numerator and denominator estimators is the population hudsonFst. This is a statement about the ratio of expectations; the expectation of the ratio of the estimated sums is in general not hudsonFst.

theorem integral_sum_div_integral_sum (hA : ∀ i ∈ s, HasLaw (XA i) Bin(ℝ, mA i, qA i) μ)
    (hB : ∀ i ∈ s, HasLaw (XB i) Bin(ℝ, mB i, qB i) μ)
    (hAB : ∀ i ∈ s, IndepFun (XA i) (XB i) μ) (hmA : ∀ i ∈ s, 2 ≤ mA i)
    (hmB : ∀ i ∈ s, 2 ≤ mB i) :
    μ[fun ω => ∑ i ∈ s, f2Hat (mA i) (mB i) (XA i ω) (XB i ω)] /
        μ[fun ω => ∑ i ∈ s, hudsonDenHat (mA i) (mB i) (XA i ω) (XB i ω)] =
      hudsonFst s (fun i => qA i) (fun i => qB i)
Uses 6
Statement usesUnbiased f2 estimator · Estimator of Hudson's F_ST denominator · Hudson's F_ST (ratio of averages)
Proof usesHudson's F_ST denominator at one site · Unbiasedness of the summed f2 estimator · Unbiasedness of the summed Hudson denominator estimator

Drift-model corollaries

TheoremThe unpolarized D-statistic numerator vanishes on a tree#✓fully proved

In the drift model, if no edge lies on both the P1–P2 and the P3–O path (as on the tree ((P1, P2), P3), O), then the expected unpolarized ABBA and BABA counts are equal. Thus BABA - ABBA and its sign reversal have expectation 0. The integrability hypotheses make both expectations meaningful.

theorem integral_sampleExpect_abba_eq_baba {P1 P2 P3 O : P}
    (h : ∀ e, (M.weight P1 e - M.weight P2 e) * (M.weight P3 e - M.weight O e) = 0)
    (habba : Integrable
      (fun ω => sampleExpect abba ![M.freq P1 ω, M.freq P2 ω, M.freq P3 ω, M.freq O ω]) μ)
    (hbaba : Integrable
      (fun ω => sampleExpect baba ![M.freq P1 ω, M.freq P2 ω, M.freq P3 ω, M.freq O ω]) μ) :
    ∫ ω, sampleExpect abba ![M.freq P1 ω, M.freq P2 ω, M.freq P3 ω, M.freq O ω] ∂μ =
      ∫ ω, sampleExpect baba ![M.freq P1 ω, M.freq P2 ω, M.freq P3 ω, M.freq O ω] ∂μ
Uses 9
Statement usesUnpolarized ABBA site-pattern indicator · Unpolarized BABA site-pattern indicator · Expectation under independent haplotype sampling · Admixture-graph drift model · Allele frequency of a population in the drift model
Proof usesABBA–BABA equals f4 · Sampling expectation commutes with subtraction · f4 vanishes for edge-disjoint paths · f4 statistic

TheoremqpAdm model equation in the drift model#✓fully proved

If the lineage weights of T are an affine combination ∑ k, w k • weight (S k) of those of the sources (∑ k, w k = 1, weights of any sign), then f4 T X Y Z = ∑ k, w k * f4 (S k) X Y Z.

theorem f4_affine_combination {ι : Type*} [Fintype ι] {T X Y Z : P} (S : ι → P) (w : ι → ℝ)
    (hT : M.weight T = ∑ k, w k • M.weight (S k)) (hw : ∑ k, w k = 1) :
    f4 μ M.freq T X Y Z = ∑ k, w k * f4 μ M.freq (S k) X Y Z
Uses 4
Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f4 statistic
Proof usesf4 in the drift model

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.