Skip to content

Outgroup f3 and admixed branches

7 fully proved

Outgroup f3

Theoremf3 statistic as shared drift on a tree#✓fully proved

With binary loadings, f3 O A B is the total drift length of the edges shared by the paths O–A and O–B (on a tree, the path from O to the A–B path).

theorem f3_eq_sum_inter_symmDiff [DecidableEq E] (hM : M.HasBinaryLoadings) (O A B : P) :
    f3 μ M.freq O A B =
      ∑ e ∈ (M.lineage O ∆ M.lineage A) ∩ (M.lineage O ∆ M.lineage B), 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 · f3 statistic
Proof usesf3 in the drift model

TheoremOutgroup f3 statistic#✓fully proved

Outgroup f3 (Raghavan et al. 2014): with binary loadings, if the lineage of O shares no edge with the lineages of A and B, then f3 O A B is the drift from the outgroup to the root plus the drift shared by A and B.

theorem f3_outgroup [DecidableEq E] (hM : M.HasBinaryLoadings) {O A B : P}
    (hA : Disjoint (M.lineage O) (M.lineage A)) (hB : Disjoint (M.lineage O) (M.lineage B)) :
    f3 μ M.freq O A B = ∑ e ∈ M.lineage O, M.len e + ∑ e ∈ M.lineage A ∩ M.lineage B, M.len e
Uses 6 · Used by 1
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 · f3 statistic
Proof usesf3 in the drift model
Used byOutgroup f3 ranks populations by shared drift

TheoremOutgroup f3 ranks populations by shared drift#✓fully proved

For a fixed outgroup O and population A, the outgroup f3 ranks candidates B by the drift they share with A.

theorem f3_outgroup_le_iff [DecidableEq E] (hM : M.HasBinaryLoadings) {O A B B' : P}
    (hA : Disjoint (M.lineage O) (M.lineage A)) (hB : Disjoint (M.lineage O) (M.lineage B))
    (hB' : Disjoint (M.lineage O) (M.lineage B')) :
    f3 μ M.freq O A B ≤ f3 μ M.freq O A B' ↔
      ∑ e ∈ M.lineage A ∩ M.lineage B, M.len e ≤ ∑ e ∈ M.lineage A ∩ M.lineage B', 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 · f3 statistic
Proof usesOutgroup f3 statistic

Admixed branches

DefinitionMixMapper mixed drift#✓fully proved

MixMapper's mixed drift α² ℓ_a + (1 - α)² ℓ_b + ℓ_c: the only combination of the terminal drift lengths that enters the f2 statistics of an admixed population.

def mixedDrift (α la lb lc : ℝ) : ℝ := α ^ 2 * la + (1 - α) ^ 2 * lb + lc
Used by 3
Used byIdentifiability of the admixture proportion from f2 statistics · Admixed-branch identity for f2 statistics · Mixed drift determined by f2 statistics

TheoremAdmixed-branch identity for f2 statistics#✓fully proved

The admixed-branch identity (Lipson et al. 2013): if Mx is an α : 1 - α mixture of the endpoints of the edges a (below A) and b (below B), followed by drift on c, and A, B, X do not use a, b, c, then f2 Mx X = α f2 A X + (1 - α) f2 B X - α (1 - α) f2 A B + mixedDrift α ℓ_a ℓ_b ℓ_c.

theorem f2_admixedBranch [DecidableEq E] {Mx A B X : P} {a b c : E} {α : ℝ} (hab : a ≠ b)
    (hac : a ≠ c) (hbc : b ≠ c)
    (hw : M.weight Mx = α • (M.weight A + Pi.single a 1) +
      (1 - α) • (M.weight B + Pi.single b 1) + Pi.single c 1)
    (hA : ∀ e ∈ ({a, b, c} : Finset E), M.weight A e = 0)
    (hB : ∀ e ∈ ({a, b, c} : Finset E), M.weight B e = 0)
    (hX : ∀ e ∈ ({a, b, c} : Finset E), M.weight X e = 0) :
    f2 μ M.freq Mx X = α * f2 μ M.freq A X + (1 - α) * f2 μ M.freq B X -
      α * (1 - α) * f2 μ M.freq A B + mixedDrift α (M.len a) (M.len b) (M.len c)
Uses 5 · Used by 2
Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f2 statistic · MixMapper mixed drift
Proof usesf2 in the drift model
Used byIdentifiability of the admixture proportion from f2 statistics · Mixed drift determined by f2 statistics

TheoremIdentifiability of the admixture proportion from f2 statistics#✓fully proved

Identifiability of the mixture proportion (our formulation): with the split points A, B given, two references X₁, X₂ satisfying the hypotheses of f2_admixedBranch and with different contrasts f2 A Xᵢ - f2 B Xᵢ determine α from f2 statistics.

theorem alpha_eq_of_f2 [DecidableEq E] {Mx A B X₁ X₂ : P} {a b c : E} {α : ℝ} (hab : a ≠ b)
    (hac : a ≠ c) (hbc : b ≠ c)
    (hw : M.weight Mx = α • (M.weight A + Pi.single a 1) +
      (1 - α) • (M.weight B + Pi.single b 1) + Pi.single c 1)
    (hA : ∀ e ∈ ({a, b, c} : Finset E), M.weight A e = 0)
    (hB : ∀ e ∈ ({a, b, c} : Finset E), M.weight B e = 0)
    (hX₁ : ∀ e ∈ ({a, b, c} : Finset E), M.weight X₁ e = 0)
    (hX₂ : ∀ e ∈ ({a, b, c} : Finset E), M.weight X₂ e = 0)
    (hD : f2 μ M.freq A X₁ - f2 μ M.freq B X₁ ≠ f2 μ M.freq A X₂ - f2 μ M.freq B X₂) :
    α = (f2 μ M.freq Mx X₁ - f2 μ M.freq Mx X₂ - (f2 μ M.freq B X₁ - f2 μ M.freq B X₂)) /
      (f2 μ M.freq A X₁ - f2 μ M.freq B X₁ - (f2 μ M.freq A X₂ - f2 μ M.freq B X₂))
Uses 5
Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f2 statistic
Proof usesAdmixed-branch identity for f2 statistics · MixMapper mixed drift

TheoremMixed drift determined by f2 statistics#✓fully proved

Given α, the mixed drift is determined by the f2 statistics of one reference X.

theorem mixedDrift_eq [DecidableEq E] {Mx A B X : P} {a b c : E} {α : ℝ} (hab : a ≠ b)
    (hac : a ≠ c) (hbc : b ≠ c)
    (hw : M.weight Mx = α • (M.weight A + Pi.single a 1) +
      (1 - α) • (M.weight B + Pi.single b 1) + Pi.single c 1)
    (hA : ∀ e ∈ ({a, b, c} : Finset E), M.weight A e = 0)
    (hB : ∀ e ∈ ({a, b, c} : Finset E), M.weight B e = 0)
    (hX : ∀ e ∈ ({a, b, c} : Finset E), M.weight X e = 0) :
    mixedDrift α (M.len a) (M.len b) (M.len c) = f2 μ M.freq Mx X - α * f2 μ M.freq A X -
      (1 - α) * f2 μ M.freq B X + α * (1 - α) * f2 μ M.freq A B
Uses 5
Statement usesAdmixture-graph drift model · Allele frequency of a population in the drift model · f2 statistic · MixMapper mixed drift
Proof usesAdmixed-branch identity for f2 statistics

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.