Skip to content

Patterson's f-statistics

40 fully proved

Definitions and model-free identities

Definitionf2 statistic#✓fully proved

The statistic f2 X Y = 𝔼[(p X - p Y) ^ 2], the expected squared allele-frequency difference between populations X and Y.

noncomputable def f2 (X Y : P) : ℝ := ∫ ω, (p X ω - p Y ω) ^ 2 ∂μ
Used by 31
Used byThree-population statistic at an admixture node · Three-population statistic at an admixture node without edge drift · f4 equals f2 for references branching off the path · Weighted 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 · Integral of a linear combination of f2 forms · Centred leaf covariance as the double centring of f2 · f2 from the centred leaf covariance · f-statistics determine exactly the centred leaf covariance · Star tree and admixture model have equal f2 · Star tree and admixture model have equal f4 · \(f_2\) in terms of expected coalescence times · Peter's formula for \(f_2\) via expected heterozygosity · \(f_3\) in terms of expected coalescence times · \(f_4\) in terms of expected coalescence times · Identifiability of the admixture proportion from f2 statistics · Admixed-branch identity for f2 statistics · Mixed drift determined by f2 statistics · Symmetry of the f2 statistic · f2 as a special case of f4 · f2 as a symmetric-difference drift length under binary loadings · f2 in the drift model · Nonnegativity of the f2 statistic · f2 of a population with itself is zero · f3 of a pure admixture · f3 of an admixture followed by drift · f3 in terms of f2 · Nondegenerate pure admixture gives negative f3 · f4 in terms of f2

Definitionf3 statistic#✓fully proved

The statistic f3 C A B = 𝔼[(p C - p A) * (p C - p B)] of a target population C against two source populations A and B.

noncomputable def f3 (C A B : P) : ℝ := ∫ ω, (p C ω - p A ω) * (p C ω - p B ω) ∂μ
Used by 15
Used byThree-population statistic at an admixture node · Three-population statistic at an admixture node without edge drift · Three-population test is nonnegative on a tree · \(f_3\) in terms of expected coalescence times · f3 statistic as shared drift on a tree · Outgroup f3 statistic · Outgroup f3 ranks populations by shared drift · f3 of a pure admixture · f3 of an admixture followed by drift · f3 in terms of f2 · f3 as a special case of f4 · f3 in the drift model · Nondegenerate pure admixture gives negative f3 · f3 is nonnegative under binary loadings · Three-population test: negative f3 rules out a tree

Definitionf4 statistic#✓fully proved

The statistic f4 A B C D = 𝔼[(p A - p B) * (p C - p D)].

noncomputable def f4 (A B C D : P) : ℝ := ∫ ω, (p A ω - p B ω) * (p C ω - p D ω) ∂μ
Used by 29
Used byqpAdm model equation · qpAdm model equation in the drift model · Linearity of the f4-statistic in its first pair · qpWave matrix of f4-statistics · The unpolarized D-statistic numerator vanishes on a tree · ABBA–BABA equals f4 · qpWave rank bound · f4 equals f2 for references branching off the path · Weighted 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 · f4 statistic as the integral of the f4 form · Star tree and admixture model have equal f4 · \(f_4\) in terms of expected coalescence times · Predicted f4 statistics are linear in the edge lengths · f2 as a special case of f4 · f2 in the drift model · f3 as a special case of f4 · f3 in the drift model · f4 of an admixed population scales with the mixture proportion · f4 is symmetric under exchanging the two pairs · f4 in terms of f2 · f4 vanishes for edge-disjoint paths · f4 in the drift model · f4-ratio estimation of the admixture proportion · f4 changes sign when the first pair is swapped · f4 changes sign when the second pair is swapped

Theoremf2 of a population with itself is zero#✓fully proved

f2 X X = 0.

@[simp] theorem f2_self (X : P) : f2 μ p X X = 0
Uses 1
Statement usesf2 statistic

TheoremSymmetry of the f2 statistic#✓fully proved

f2 is symmetric.

theorem f2_comm (X Y : P) : f2 μ p X Y = f2 μ p Y X
Uses 1
Statement usesf2 statistic

TheoremNonnegativity of the f2 statistic#✓fully proved

f2 is nonnegative.

theorem f2_nonneg (X Y : P) : 0 ≤ f2 μ p X Y
Uses 1
Statement usesf2 statistic

Theoremf4 is symmetric under exchanging the two pairs#✓fully proved

f4 is symmetric under exchanging the two pairs.

theorem f4_comm_pairs (A B C D : P) : f4 μ p A B C D = f4 μ p C D A B
Uses 1 · Used by 1
Statement usesf4 statistic
Used byf4 changes sign when the second pair is swapped

Theoremf4 changes sign when the first pair is swapped#✓fully proved

f4 changes sign when the first pair is swapped.

theorem f4_swap_left (A B C D : P) : f4 μ p A B C D = -f4 μ p B A C D
Uses 1 · Used by 1
Statement usesf4 statistic
Used byf4 changes sign when the second pair is swapped

Theoremf4 changes sign when the second pair is swapped#✓fully proved

f4 changes sign when the second pair is swapped.

theorem f4_swap_right (A B C D : P) : f4 μ p A B C D = -f4 μ p A B D C
Uses 3
Statement usesf4 statistic
Proof usesf4 is symmetric under exchanging the two pairs · f4 changes sign when the first pair is swapped

Theoremf2 as a special case of f4#✓fully proved

f2 is the special case f4 A B A B.

theorem f2_eq_f4 (A B : P) : f2 μ p A B = f4 μ p A B A B
Uses 2 · Used by 2
Statement usesf2 statistic · f4 statistic
Used byWeighted LD amplitude with the true source populations · f2 in the drift model

Theoremf3 as a special case of f4#✓fully proved

f3 is the special case f4 C A C B.

theorem f3_eq_f4 (C A B : P) : f3 μ p C A B = f4 μ p C A C B
Uses 2 · Used by 1
Statement usesf3 statistic · f4 statistic
Used byf3 in the drift model

TheoremSquare of a difference of square-integrable frequencies is integrable#✓fully proved

A difference of square-integrable frequencies has integrable square.

theorem integrable_sub_sq (hp : ∀ X, MemLp (p X) 2 μ) (X Y : P) :
    Integrable (fun ω => (p X ω - p Y ω) ^ 2) μ
Used by 3
Used byIntegral of a linear combination of f2 forms · f3 in terms of f2 · f4 in terms of f2

Theoremf3 in terms of f2#✓fully proved

f3 in terms of f2: f3 C A B = (f2 C A + f2 C B - f2 A B) / 2.

theorem f3_eq_f2 (hp : ∀ X, MemLp (p X) 2 μ) (C A B : P) :
    f3 μ p C A B = (f2 μ p C A + f2 μ p C B - f2 μ p A B) / 2
Uses 3 · Used by 1
Statement usesf2 statistic · f3 statistic
Proof usesSquare of a difference of square-integrable frequencies is integrable
Used by\(f_3\) in terms of expected coalescence times

Theoremf4 in terms of f2#✓fully proved

f4 in terms of f2: f4 A B C D = (f2 A D + f2 B C - f2 A C - f2 B D) / 2.

theorem f4_eq_f2 (hp : ∀ X, MemLp (p X) 2 μ) (A B C D : P) :
    f4 μ p A B C D = (f2 μ p A D + f2 μ p B C - f2 μ p A C - f2 μ p B D) / 2
Uses 3 · Used by 2
Statement usesf2 statistic · f4 statistic
Proof usesSquare of a difference of square-integrable frequencies is integrable
Used byStar tree and admixture model have equal f4 · \(f_4\) in terms of expected coalescence times

The drift (admixture-graph) model

StructureAdmixture-graph drift model#✓fully proved

The admixture-graph drift model, stated at the level of second moments.

The allele frequency of population X is root + ∑ e, weight X e * incr e (see DriftModel.freq), where E is the (finite) set of edges of the graph.

  • root is the ancestral (root) allele frequency;
  • incr e is the drift increment (frequency change) along edge e;
  • len e is the drift length of edge e, i.e. the second moment 𝔼[incr e ^ 2];
  • weight X e is the probability that a lineage sampled in X traverses e: on an admixture graph it is the sum, over root-to-X paths through e, of the product of the admixture proportions on the path; on a tree it is the 0/1 indicator that e lies on the root-to-X lineage.

f-statistics depend only on second moments of frequency differences, in which the root cancels, so only these are assumed: the increments are square integrable, pairwise uncorrelated (the mixed second moments 𝔼[incr e * incr f], e ≠ f, vanish, as they do for independent mean-zero drift on distinct edges), and 𝔼[incr e ^ 2] = len e.

MathlibExt.Biology.PopulationGenetics.FStatistics.DriftModel · 17 lines 
structure DriftModel (μ : Measure Ω) (E P : Type*) [Fintype E] where
  /-- Ancestral (root) allele frequency. -/
  root : Ω → ℝ
  /-- Drift increment along edge `e`. -/
  incr : E → Ω → ℝ
  /-- Drift length of edge `e`. -/
  len : E → ℝ
  /-- Probability that a lineage sampled in population `X` traverses edge `e`. -/
  weight : P → E → ℝ
  /-- The root frequency is square integrable. -/
  memLp_root : MemLp root 2 μ
  /-- Each drift increment is square integrable. -/
  memLp_incr : ∀ e, MemLp (incr e) 2 μ
  /-- Increments on distinct edges are uncorrelated. -/
  inner_incr : ∀ e f, e ≠ f → ∫ ω, incr e ω * incr f ω ∂μ = 0
  /-- The drift length of an edge is the second moment of its increment. -/
  sq_incr : ∀ e, ∫ ω, incr e ω ^ 2 ∂μ = len e
Used by 42
Used byqpAdm model equation in the drift model · The unpolarized D-statistic numerator vanishes on a tree · Drift model of an admixture graph · Three-population statistic at an admixture node · Three-population statistic at an admixture node without edge drift · Three-population test is nonnegative on a tree · A tree-shaped admixture graph has binary loadings · f4 equals f2 for references branching off the path · Weighted 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 · Star tree and admixture model have equal f2 · Star tree and admixture model have equal f4 · Star-tree model has binary loadings · Admixture model lacks binary loadings · Predicted f4 statistics are linear in the edge lengths · Identifiability of the admixture proportion from f2 statistics · Admixed-branch identity for f2 statistics · f3 statistic as shared drift on a tree · Outgroup f3 statistic · Outgroup f3 ranks populations by shared drift · Mixed drift determined by f2 statistics · f2 as a symmetric-difference drift length under binary loadings · f2 in the drift model · f3 of a pure admixture · f3 of an admixture followed by drift · f3 in the drift model · Nondegenerate pure admixture gives negative f3 · f3 is nonnegative under binary loadings · f4 of an admixed population scales with the mixture proportion · f4 vanishes for edge-disjoint paths · f4 in the drift model · f4-ratio estimation of the admixture proportion · Allele frequency of a population in the drift model · Binary loadings of a drift model · Bilinearity of the second moment of drift increments · Drift lengths are nonnegative · Lineage of a population in the drift model · Population frequencies are square integrable · Weighted sum of drift increments is square integrable · Three-population test: negative f3 rules out a tree

DefinitionAllele frequency of a population in the drift model#✓fully proved

The allele frequency of population X: the root frequency plus the weighted sum of the drift increments of the edges traversed by lineages from X.

def freq (X : P) : Ω → ℝ := fun ω => M.root ω + ∑ e, M.weight X e * M.incr e ω
Uses 1 · Used by 32
Statement usesAdmixture-graph drift model
Used byqpAdm model equation in the drift model · The unpolarized D-statistic numerator vanishes on a tree · Three-population statistic at an admixture node · Three-population statistic at an admixture node without edge drift · Three-population test is nonnegative on a tree · f4 equals f2 for references branching off the path · Weighted 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 · Star tree and admixture model have equal f2 · Star tree and admixture model have equal f4 · Predicted f4 statistics are linear in the edge lengths · Identifiability of the admixture proportion from f2 statistics · Admixed-branch identity for f2 statistics · f3 statistic as shared drift on a tree · Outgroup f3 statistic · Outgroup f3 ranks populations by shared drift · Mixed drift determined by f2 statistics · f2 as a symmetric-difference drift length under binary loadings · f2 in the drift model · f3 of a pure admixture · f3 of an admixture followed by drift · f3 in the drift model · Nondegenerate pure admixture gives negative f3 · f3 is nonnegative under binary loadings · f4 of an admixed population scales with the mixture proportion · f4 vanishes for edge-disjoint paths · f4 in the drift model · f4-ratio estimation of the admixture proportion · Population frequencies are square integrable · Three-population test: negative f3 rules out a tree

TheoremDrift lengths are nonnegative#✓fully proved

Drift lengths are nonnegative.

theorem len_nonneg (e : E) : 0 ≤ M.len e
Uses 1 · Used by 1
Statement usesAdmixture-graph drift model
Used byf3 is nonnegative under binary loadings

TheoremWeighted sum of drift increments is square integrable#✓fully proved

A weighted sum of increments is square integrable.

theorem memLp_sum_incr (a : E → ℝ) : MemLp (fun ω => ∑ e, a e * M.incr e ω) 2 μ
Uses 1 · Used by 1
Statement usesAdmixture-graph drift model
Used byPopulation frequencies are square integrable

TheoremPopulation frequencies are square integrable#✓fully proved

Population frequencies are square integrable.

theorem memLp_freq (X : P) : MemLp (M.freq X) 2 μ
Uses 3 · Used by 1
Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model
Proof usesWeighted sum of drift increments is square integrable
Used byStar tree and admixture model have equal f4

TheoremBilinearity of the second moment of drift increments#✓fully proved

Bilinearity of the second moment of increments: 𝔼[(∑ e, a e * incr e) * (∑ f, b f * incr f)] = ∑ e, a e * b e * len e.

theorem integral_sum_mul_sum (a b : E → ℝ) :
    ∫ ω, (∑ e, a e * M.incr e ω) * (∑ f, b f * M.incr f ω) ∂μ = ∑ e, a e * b e * M.len e
Uses 1 · Used by 1
Statement usesAdmixture-graph drift model
Used byf4 in the drift model

Theoremf4 in the drift model#✓fully proved

f4 in the drift model: the root cancels, and f4 A B C D is the drift length shared by the paths A–B and C–D, weighted by (w A e - w B e) * (w C e - w D e).

theorem f4_freq (A B C D : P) :
    f4 μ M.freq A B C D =
      ∑ e, (M.weight A e - M.weight B e) * (M.weight C e - M.weight D e) * M.len e
Uses 4 · Used by 9
Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f4 statistic
Proof usesBilinearity of the second moment of drift increments
Used byqpAdm model equation in the drift model · f4 equals f2 for references branching off the path · Weighted LD amplitude with the admixed population as reference · Weighted LD amplitude with one diverged reference · Predicted f4 statistics are linear in the edge lengths · f2 in the drift model · f3 in the drift model · f4 of an admixed population scales with the mixture proportion · f4 vanishes for edge-disjoint paths

Theoremf2 in the drift model#✓fully proved

f2 in the drift model: f2 X Y = ∑ e, (w X e - w Y e) ^ 2 * len e.

theorem f2_freq (X Y : P) :
    f2 μ M.freq X Y = ∑ e, (M.weight X e - M.weight Y e) ^ 2 * M.len e
Uses 6 · Used by 9
Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f2 statistic
Proof usesf4 in the drift model · f2 as a special case of f4 · f4 statistic
Used byThree-population statistic at an admixture node · f4 equals f2 for references branching off the path · Weighted LD amplitude with the admixed population as reference · Weighted LD amplitude with one diverged reference · Star tree and admixture model have equal f2 · Admixed-branch identity for f2 statistics · f2 as a symmetric-difference drift length under binary loadings · f3 of a pure admixture · f3 of an admixture followed by drift

Theoremf3 in the drift model#✓fully proved

f3 in the drift model: f3 C A B = ∑ e, (w C e - w A e) * (w C e - w B e) * len e.

theorem f3_freq (C A B : P) :
    f3 μ M.freq C A B =
      ∑ e, (M.weight C e - M.weight A e) * (M.weight C e - M.weight B e) * M.len e
Uses 6 · Used by 6
Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f3 statistic
Proof usesf4 in the drift model · f3 as a special case of f4 · f4 statistic
Used byThree-population statistic at an admixture node · f3 statistic as shared drift on a tree · Outgroup f3 statistic · f3 of a pure admixture · f3 of an admixture followed by drift · f3 is nonnegative under binary loadings

Theoremf4 vanishes for edge-disjoint paths#✓fully proved

f4 A B C D = 0 when no edge contributes to both the A–B and the C–D path. On a tree with split AB | CD the paths A–B and C–D share no edge, so this hypothesis holds.

theorem f4_eq_zero_of_disjoint {A B C D : P}
    (h : ∀ e, (M.weight A e - M.weight B e) * (M.weight C e - M.weight D e) = 0) :
    f4 μ M.freq A B C D = 0
Uses 4 · Used by 1
Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f4 statistic
Proof usesf4 in the drift model
Used byThe unpolarized D-statistic numerator vanishes on a tree

DefinitionBinary loadings of a drift model#✓fully proved

The model has binary loadings if every lineage weight is 0 or 1.

Every tree model has binary loadings: there weight X e is the indicator of e lying on the root-to-X path. The converse fails, since nothing forces the weight-1 edge sets to be compatible root-to-leaf paths: two edges of length 1 and four populations with weight vectors 00, 10, 01, 11 have binary loadings, but their f2 distances form a square, which violates the four-point condition of tree metrics. The results below use only the binary values, so they apply to every tree.

def HasBinaryLoadings : Prop := ∀ X e, M.weight X e = 0 ∨ M.weight X e = 1
Uses 1 · Used by 9
Statement usesAdmixture-graph drift model
Used byA tree-shaped admixture graph has binary loadings · Star-tree model has binary loadings · Admixture model lacks binary loadings · f3 statistic as shared drift on a tree · Outgroup f3 statistic · Outgroup f3 ranks populations by shared drift · f2 as a symmetric-difference drift length under binary loadings · f3 is nonnegative under binary loadings · Three-population test: negative f3 rules out a tree

DefinitionLineage of a population in the drift model#✓fully proved

The edges of weight 1 for population X; on a tree, the root-to-X lineage.

noncomputable def lineage (X : P) : Finset E :=
  haveI := Classical.decEq ℝ
  {e | M.weight X e = 1}
Uses 1 · Used by 4
Statement usesAdmixture-graph drift model
Used byf3 statistic as shared drift on a tree · Outgroup f3 statistic · Outgroup f3 ranks populations by shared drift · f2 as a symmetric-difference drift length under binary loadings

Theoremf3 is nonnegative under binary loadings#✓fully proved

With binary loadings f3 is nonnegative; on a tree it is the drift length of the path from C to the A–B path.

theorem f3_nonneg_of_hasBinaryLoadings (hM : M.HasBinaryLoadings) (C A B : P) :
    0 ≤ f3 μ M.freq C A B
Uses 6 · Used by 2
Statement usesAdmixture-graph drift model · Binary loadings of a drift model · Allele frequency of a population in the drift model · f3 statistic
Proof usesf3 in the drift model · Drift lengths are nonnegative
Used byThree-population test is nonnegative on a tree · Three-population test: negative f3 rules out a tree

Theoremf2 as a symmetric-difference drift length under binary loadings#✓fully proved

With binary loadings f2 X Y is the total drift length of the edges in exactly one of the weight-1 edge sets of X and Y. On a tree, where these sets are the root-to-X and root-to-Y paths, this is the additive tree distance between X and Y.

theorem f2_eq_sum_symmDiff [DecidableEq E] (hM : M.HasBinaryLoadings) (X Y : P) :
    f2 μ M.freq X Y = ∑ e ∈ M.lineage X ∆ M.lineage Y, M.len e
Uses 6
Statement usesAdmixture-graph drift model · Binary loadings of a drift model · Allele frequency of a population in the drift model · Lineage of a population in the drift model · f2 statistic
Proof usesf2 in the drift model

TheoremThree-population test: negative f3 rules out a tree#✓fully proved

Three-population test: a negative f3 C A B is incompatible with binary loadings, hence with every tree model.

theorem not_hasBinaryLoadings_of_f3_neg {C A B : P} (h : f3 μ M.freq C A B < 0) :
    ¬ M.HasBinaryLoadings
Uses 5
Statement usesAdmixture-graph drift model · Binary loadings of a drift model · Allele frequency of a population in the drift model · f3 statistic
Proof usesf3 is nonnegative under binary loadings

Theoremf3 of a pure admixture#✓fully proved

If C is a mixture of A and B in proportions α : 1 - α (with no subsequent drift), then f3 C A B = -α (1 - α) f2 A B.

theorem f3_admixture {A B C : P} {α : ℝ}
    (h : M.weight C = α • M.weight A + (1 - α) • M.weight B) :
    f3 μ M.freq C A B = -(α * (1 - α)) * 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 · f3 statistic
Proof usesf2 in the drift model · f3 in the drift model
Used byNondegenerate pure admixture gives negative f3

Theoremf3 of an admixture followed by drift#✓fully proved

Admixture followed by drift: if C is an α : 1 - α mixture of A and B that then drifts along a private edge c (not traversed by A or B), then f3 C A B = len c - α (1 - α) f2 A B; post-admixture drift can mask the admixture signal.

theorem f3_admixture_drift [DecidableEq E] {A B C : P} {α : ℝ} {c : E}
    (h : M.weight C = α • M.weight A + (1 - α) • M.weight B + Pi.single c 1)
    (hA : M.weight A c = 0) (hB : M.weight B c = 0) :
    f3 μ M.freq C A B = M.len c - α * (1 - α) * f2 μ M.freq A B
Uses 6
Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f2 statistic · f3 statistic
Proof usesf2 in the drift model · f3 in the drift model

TheoremNondegenerate pure admixture gives negative f3#✓fully proved

Three-population test, converse direction: a nondegenerate pure admixture (0 < α < 1, f2 A B > 0) yields a negative f3 C A B.

theorem f3_neg_of_admixture {A B C : P} {α : ℝ} (hα0 : 0 < α) (hα1 : α < 1)
    (hAB : 0 < f2 μ M.freq A B) (h : M.weight C = α • M.weight A + (1 - α) • M.weight B) :
    f3 μ M.freq C A B < 0
Uses 5
Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f2 statistic · f3 statistic
Proof usesf3 of a pure admixture

Theoremf4 of an admixed population scales with the mixture proportion#✓fully proved

If X is an α : 1 - α mixture of Y and C, then f4 A O X C = α * f4 A O Y C (bilinearity of f4, together with f4 A O C C = 0).

theorem f4_admixture_right {A O X Y C : P} {α : ℝ}
    (h : M.weight X = α • M.weight Y + (1 - α) • M.weight C) :
    f4 μ M.freq A O X C = α * f4 μ M.freq A O Y C
Uses 4 · Used by 1
Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f4 statistic
Proof usesf4 in the drift model
Used byf4-ratio estimation of the admixture proportion

Theoremf4-ratio estimation of the admixture proportion#✓fully proved

f4-ratio estimation of the admixture proportion. f4-ratio estimation (Patterson et al. 2012). Let X be an α : 1 - α mixture of a source lineage Y and of C, where Y is unsampled but sister to the sampled population B relative to the A–O path, so that f4 A O Y C = f4 A O B C. If this value is nonzero, the ratio f4 A O X C / f4 A O B C of two estimable statistics recovers the admixture proportion α.

theorem f4_ratio {A O X Y B C : P} {α : ℝ}
    (h : M.weight X = α • M.weight Y + (1 - α) • M.weight C)
    (hYB : f4 μ M.freq A O Y C = f4 μ M.freq A O B C) (hB : f4 μ M.freq A O B C ≠ 0) :
    f4 μ M.freq A O X C / f4 μ M.freq A O B C = α
Uses 4
Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f4 statistic
Proof usesf4 of an admixed population scales with the mixture proportion

The Wahlund effect

DefinitionMean allele frequency of a subdivided population#✓fully proved

Mean allele frequency q̄ = ∑ i, c i * q i of a population made of subpopulations with weights c i and allele frequencies q i.

def meanFreq : ℝ := ∑ i, c i * q i
Used by 3
Used byWahlund effect · Total heterozygosity of the pooled population · Wahlund identity

DefinitionMean within-subpopulation heterozygosity#✓fully proved

Mean within-subpopulation (Hardy–Weinberg) heterozygosity H_S = ∑ i, c i * 2 q i (1 - q i).

def hetSub : ℝ := ∑ i, c i * (2 * q i * (1 - q i))
Used by 3
Used byNonnegativity of the fixation index \(F_{ST}\) · Wahlund effect · Wahlund identity

DefinitionTotal heterozygosity of the pooled population#✓fully proved

Total heterozygosity H_T = 2 q̄ (1 - q̄) expected under random mating of the pooled population.

def hetTotal : ℝ := 2 * meanFreq c q * (1 - meanFreq c q)
Uses 1 · Used by 3
Statement usesMean allele frequency of a subdivided population
Used byNonnegativity of the fixation index \(F_{ST}\) · Wahlund effect · Wahlund identity

TheoremWahlund identity#✓fully proved

Wahlund identity: for weights summing to 1, H_T - H_S = 2 ∑ i, c i * (q i - q̄) ^ 2, twice the weighted variance of subpopulation frequencies.

theorem wahlund (hc : ∑ i, c i = 1) :
    hetTotal c q - hetSub c q = 2 * ∑ i, c i * (q i - meanFreq c q) ^ 2
Uses 3 · Used by 1
Statement usesMean within-subpopulation heterozygosity · Total heterozygosity of the pooled population · Mean allele frequency of a subdivided population
Used byWahlund effect

TheoremWahlund effect#✓fully proved

The Wahlund effect: with nonnegative weights summing to 1, subdivision lowers heterozygosity, H_S ≤ H_T.

theorem hetSub_le_hetTotal (hc0 : ∀ i, 0 ≤ c i) (hc : ∑ i, c i = 1) :
    hetSub c q ≤ hetTotal c q
Uses 4 · Used by 1
Statement usesMean within-subpopulation heterozygosity · Total heterozygosity of the pooled population
Proof usesMean allele frequency of a subdivided population · Wahlund identity
Used byNonnegativity of the fixation index \(F_{ST}\)

TheoremNonnegativity of the fixation index \(F_{ST}\)#✓fully proved

F_ST = (H_T - H_S) / H_T is nonnegative for nonnegative weights summing to 1. The ratio is defined only when H_T > 0 (at a fixed allele H_T = H_S = 0), so that is assumed.

theorem fst_nonneg (hc0 : ∀ i, 0 ≤ c i) (hc : ∑ i, c i = 1) (hT : 0 < hetTotal c q) :
    0 ≤ (hetTotal c q - hetSub c q) / hetTotal c q
Uses 3
Statement usesMean within-subpopulation heterozygosity · Total heterozygosity of the pooled population
Proof usesWahlund effect

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.