Admixture graphs

28 fully proved

Population Genetics

StructureAdmixture graph#✓fully proved

An admixture graph on the nodes V (Patterson et al. 2012): a rooted directed acyclic graph in which every non-root node has one or two parents, with admixture proportions.

parents X are the parents of X, the root has none, every other node has one or two;
prop X Y is the probability that a lineage in X descends from parent Y: nonnegative, summing to 1 over the parents of a non-root node, and 0 off the parent set;
the parent relation is well founded, i.e. the graph is acyclic (V is finite in all results).

MathlibExt.Biology.PopulationGenetics.AdmixtureGraph · 19 lines

structure AdmixtureGraph (V : Type*) where
  /-- The root (ancestral population). -/
  root : V
  /-- The parents of each node. -/
  parents : V → Finset V
  /-- Admixture proportions: `prop X Y` is the share of ancestry of `X` from parent `Y`. -/
  prop : V → V → ℝ
  /-- The root has no parent. -/
  parents_root : parents root = ∅
  /-- Every non-root node has one parent (tree edge) or two parents (admixture node). -/
  card_parents : ∀ X, X ≠ root → (parents X).card = 1 ∨ (parents X).card = 2
  /-- Proportions are nonnegative. -/
  prop_nonneg : ∀ X Y, 0 ≤ prop X Y
  /-- Proportions vanish off the parent set. -/
  prop_eq_zero : ∀ X Y, Y ∉ parents X → prop X Y = 0
  /-- The proportions of a non-root node sum to `1`. -/
  sum_prop : ∀ X, X ≠ root → ∑ Y ∈ parents X, prop X Y = 1
  /-- The graph is acyclic: the parent relation is well founded. -/
  wf : WellFounded fun Y X => Y ∈ parents X

  parents : V → Finset V

MathlibExt/Biology/PopulationGenetics/AdmixtureGraph.lean:77

  root : V

MathlibExt/Biology/PopulationGenetics/AdmixtureGraph.lean:75

  prop : V → V → ℝ

MathlibExt/Biology/PopulationGenetics/AdmixtureGraph.lean:79

Used by 27

Used byDrift model of an admixture graph · Edges 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 · Tree-shaped admixture graph · Probability of a root-ward path in an admixture graph · Root-ward paths from a node of an admixture graph · First-step equation for root-ward paths · Admixture proportions are at most one · Probability that a lineage passes through a node · First-step equation for visit probabilities · A lineage from a parent never passes through its child · Visit probabilities on a tree are zero or one · Visit probabilities are at most one · Nonnegativity of visit probabilities · Every lineage reaches the root · A lineage visits its own node with probability one · Lineage weight of an edge in an admixture graph · Lineage weight recursion at an admixture node · First-step recursion for lineage weights · Path-sum formula for lineage weights · Lineage weights on a tree are zero or one · Lineage weights are at most one · Nonnegativity of lineage weights · Lineage weight recursion at a tree node

Admixture Graph

AbbreviationEdges of an admixture graph#✓fully proved

The edges (child, parent) of the graph.

abbrev Edge : Type _ := {e : V × V // e.2 ∈ G.parents e.1}

Uses 1 · Used by 13

Statement usesAdmixture graph

Used byDrift 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 · Lineage weight of an edge in an admixture graph · Lineage weight recursion at an admixture node · First-step recursion for lineage weights · Path-sum formula for lineage weights · Lineage weights on a tree are zero or one · Lineage weights are at most one · Nonnegativity of lineage weights · Lineage weight recursion at a tree node

DefinitionProbability that a lineage passes through a node#✓fully proved

visit X c is the probability that the lineage of a gene sampled in X, traced toward the root with parents chosen according to the admixture proportions, passes through c.

noncomputable def visit (X c : V) : ℝ :=
  G.wf.fix (C := fun _ => ℝ)
    (fun X ih => if X = c then 1 else ∑ Y ∈ (G.parents X).attach, G.prop X Y * ih Y Y.2) X

Uses 1 · Used by 13

Statement usesAdmixture graph

Used byThree-population statistic at an admixture node · First-step equation for visit probabilities · A lineage from a parent never passes through its child · Visit probabilities on a tree are zero or one · Visit probabilities are at most one · Nonnegativity of visit probabilities · Every lineage reaches the root · A lineage visits its own node with probability one · Lineage weight of an edge in an admixture graph · First-step recursion for lineage weights · Lineage weights on a tree are zero or one · Lineage weights are at most one · Nonnegativity of lineage weights

DefinitionLineage weight of an edge in an admixture graph#✓fully proved

weight X e is the probability that the lineage of a gene sampled in X traverses the edge e = (c, p): it reaches c and then descends from p.

noncomputable def weight (X : V) (e : G.Edge) : ℝ := G.visit X e.1.1 * G.prop e.1.1 e.1.2

Uses 3 · Used by 12

Statement usesAdmixture graph · Edges of an admixture graph · Probability that a lineage passes through a node

Used byDrift 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 · Lineage weight recursion at an admixture node · First-step recursion for lineage weights · Path-sum formula for lineage weights · Lineage weights on a tree are zero or one · Lineage weights are at most one · Nonnegativity of lineage weights · Lineage weight recursion at a tree node

DefinitionProbability of a root-ward path in an admixture graph#✓fully proved

The probability of a root-ward path [v₀, v₁, …, v_k]: the product of the proportions prop vᵢ vᵢ₊₁.

def pathProb : List V → ℝ
  | a :: b :: l => G.prop a b * pathProb (b :: l)
  | _ => 1

Uses 1 · Used by 1

Statement usesAdmixture graph

Used byPath-sum formula for lineage weights

DefinitionRoot-ward paths from a node of an admixture graph#✓fully proved

The root-ward paths from X: the lists [X = v₀, v₁, …, v_k = root] with each vᵢ₊₁ a parent of vᵢ.

noncomputable def paths (X : V) : Finset (List V) :=
  G.wf.fix (C := fun _ => Finset (List V))
    (fun X ih => if G.parents X = ∅ then {[X]} else
      (G.parents X).attach.biUnion fun Y => (ih Y Y.2).image (List.cons X)) X

Uses 1 · Used by 2

Statement usesAdmixture graph

Used byFirst-step equation for root-ward paths · Path-sum formula for lineage weights

TheoremFirst-step equation for visit probabilities#✓fully proved

First-step equation for visit.

theorem visit_eq (X c : V) :
    G.visit X c = if X = c then 1 else ∑ Y ∈ G.parents X, G.prop X Y * G.visit Y c

Uses 2 · Used by 7

Statement usesAdmixture graph · Probability that a lineage passes through a node

Used byA lineage from a parent never passes through its child · Visit probabilities on a tree are zero or one · Visit probabilities are at most one · Nonnegativity of visit probabilities · Every lineage reaches the root · A lineage visits its own node with probability one · First-step recursion for lineage weights

TheoremA lineage visits its own node with probability one#✓fully proved

A lineage passes through its own node with probability 1.

@[simp] theorem visit_self (X : V) : G.visit X X = 1

Uses 3 · Used by 1

Statement usesAdmixture graph · Probability that a lineage passes through a node

Proof usesFirst-step equation for visit probabilities

Used byFirst-step recursion for lineage weights

TheoremNonnegativity of visit probabilities#✓fully proved

Visit probabilities are nonnegative.

theorem visit_nonneg (X c : V) : 0 ≤ G.visit X c

Uses 3 · Used by 1

Statement usesAdmixture graph · Probability that a lineage passes through a node

Proof usesFirst-step equation for visit probabilities

Used byNonnegativity of lineage weights

TheoremVisit probabilities are at most one#✓fully proved

Visit probabilities are at most 1.

theorem visit_le_one (X c : V) : G.visit X c ≤ 1

Uses 3 · Used by 1

Statement usesAdmixture graph · Probability that a lineage passes through a node

Proof usesFirst-step equation for visit probabilities

Used byLineage weights are at most one

TheoremEvery lineage reaches the root#✓fully proved

Every lineage reaches the root.

theorem visit_root (X : V) : G.visit X G.root = 1

Uses 3

Statement usesAdmixture graph · Probability that a lineage passes through a node

Proof usesFirst-step equation for visit probabilities

TheoremFirst-step equation for root-ward paths#✓fully proved

First-step equation for paths.

theorem paths_eq (X : V) :
    G.paths X = if G.parents X = ∅ then {[X]} else
      (G.parents X).biUnion fun Y => (G.paths Y).image (List.cons X)

Uses 2 · Used by 1

Statement usesAdmixture graph · Root-ward paths from a node of an admixture graph

Used byPath-sum formula for lineage weights

TheoremAdmixture proportions are at most one#✓fully proved

Admixture proportions are at most 1.

theorem prop_le_one (X Y : V) : G.prop X Y ≤ 1

Uses 1 · Used by 1

Statement usesAdmixture graph

Used byLineage weights are at most one

TheoremA lineage from a parent never passes through its child#✓fully proved

Acyclicity: a lineage from a parent Y of X never passes through X.

theorem visit_eq_zero_of_mem_parents {X Y : V} (h : Y ∈ G.parents X) : G.visit Y X = 0

Uses 3 · Used by 2

Statement usesAdmixture graph · Probability that a lineage passes through a node

Proof usesFirst-step equation for visit probabilities

Used byThree-population statistic at an admixture node · First-step recursion for lineage weights

TheoremNonnegativity of lineage weights#✓fully proved

Lineage weights are nonnegative.

theorem weight_nonneg (X : V) (e : G.Edge) : 0 ≤ G.weight X e

Uses 5

Statement usesAdmixture graph · Edges of an admixture graph · Lineage weight of an edge in an admixture graph

Proof usesProbability that a lineage passes through a node · Nonnegativity of visit probabilities

TheoremLineage weights are at most one#✓fully proved

Lineage weights are at most 1.

theorem weight_le_one (X : V) (e : G.Edge) : G.weight X e ≤ 1

Uses 6

Statement usesAdmixture graph · Edges of an admixture graph · Lineage weight of an edge in an admixture graph

Proof usesAdmixture proportions are at most one · Probability that a lineage passes through a node · Visit probabilities are at most one

TheoremFirst-step recursion for lineage weights#✓fully proved

First-step recursion for lineage weights: a lineage from X traverses e either as its first step (if e starts at X) or after moving to a parent Y, chosen with probability prop X Y.

theorem weight_eq (X : V) (e : G.Edge) :
    G.weight X e = ∑ Y ∈ G.parents X, G.prop X Y * G.weight Y e +
      if e.1.1 = X then G.prop X e.1.2 else 0

Uses 7 · Used by 3

Statement usesAdmixture graph · Edges of an admixture graph · Lineage weight of an edge in an admixture graph

Proof usesProbability that a lineage passes through a node · First-step equation for visit probabilities · A lineage from a parent never passes through its child · A lineage visits its own node with probability one

Used byLineage weight recursion at an admixture node · Path-sum formula for lineage weights · Lineage weight recursion at a tree node

TheoremLineage weight recursion at an admixture node#✓fully proved

The recursion at an admixture node X with parents A ≠ B: with α = prop X A, w X = α w A + (1 - α) w B + w₀, where w₀ puts weight α on the edge (X, A), 1 - α on (X, B) and 0 elsewhere.

theorem weight_admixture {X A B : V} (hX : G.parents X = {A, B}) (hAB : A ≠ B) :
    G.weight X = G.prop X A • G.weight A + (1 - G.prop X A) • G.weight B +
      fun e => if e.1.1 = X then G.prop X e.1.2 else 0

Uses 4 · Used by 1

Statement usesAdmixture graph · Edges of an admixture graph · Lineage weight of an edge in an admixture graph

Proof usesFirst-step recursion for lineage weights

Used byThree-population statistic at an admixture node

TheoremLineage weight recursion at a tree node#✓fully proved

The recursion at a tree node X with the single parent Y: w X = w Y + 1_{(X, Y)}.

theorem weight_tree {X Y : V} (hX : G.parents X = {Y}) :
    G.weight X = G.weight Y + fun e => if e.1.1 = X then 1 else 0

Uses 4

Statement usesAdmixture graph · Edges of an admixture graph · Lineage weight of an edge in an admixture graph

Proof usesFirst-step recursion for lineage weights

TheoremPath-sum formula for lineage weights#✓fully proved

Path-sum form of the lineage weights (Patterson et al. 2012): weight X e is the sum, over the root-ward paths from X that traverse e, of the products of the admixture proportions along the path.

theorem weight_eq_sum_paths (X : V) (e : G.Edge) :
    G.weight X e = ∑ π ∈ G.paths X, if e.1 ∈ π.zip π.tail then G.pathProb π else 0

Uses 7

Statement usesAdmixture graph · Edges of an admixture graph · Probability of a root-ward path in an admixture graph · Root-ward paths from a node of an admixture graph · Lineage weight of an edge in an admixture graph

Proof usesFirst-step equation for root-ward paths · First-step recursion for lineage weights

DefinitionTree-shaped admixture graph#✓fully proved

The graph is a tree: no node has two parents.

def IsTree : Prop := ∀ X, (G.parents X).card ≤ 1

Uses 1 · Used by 4

Statement usesAdmixture graph

Used byThree-population test is nonnegative on a tree · A tree-shaped admixture graph has binary loadings · Visit probabilities on a tree are zero or one · Lineage weights on a tree are zero or one

TheoremVisit probabilities on a tree are zero or one#✓fully proved

On a tree every visit probability is 0 or 1.

theorem visit_eq_zero_or_one (hG : G.IsTree) (X c : V) :
    G.visit X c = 0 ∨ G.visit X c = 1

Uses 4 · Used by 1

Statement usesAdmixture graph · Tree-shaped admixture graph · Probability that a lineage passes through a node

Proof usesFirst-step equation for visit probabilities

Used byLineage weights on a tree are zero or one

TheoremLineage weights on a tree are zero or one#✓fully proved

On a tree every lineage weight is 0 or 1.

theorem weight_eq_zero_or_one (hG : G.IsTree) (X : V) (e : G.Edge) :
    G.weight X e = 0 ∨ G.weight X e = 1

Uses 6 · Used by 1

Statement usesAdmixture graph · Edges of an admixture graph · Tree-shaped admixture graph · Lineage weight of an edge in an admixture graph

Proof usesProbability that a lineage passes through a node · Visit probabilities on a tree are zero or one

Used byA tree-shaped admixture graph has binary loadings

DefinitionDrift model of an admixture graph#✓fully proved

The drift model of an admixture graph: the populations are the nodes, the root frequency is root, the edge increments are incr (square integrable and pairwise uncorrelated), the drift length of an edge is the second moment of its increment, and the weights are the lineage weights of the graph.

noncomputable def driftModel (root : Ω → ℝ) (incr : G.Edge → Ω → ℝ) (hroot : MemLp root 2 μ)
    (hincr : ∀ e, MemLp (incr e) 2 μ)
    (hinner : ∀ e f, e ≠ f → ∫ ω, incr e ω * incr f ω ∂μ = 0) : DriftModel μ G.Edge V where
  root := root
  incr := incr
  len e := ∫ ω, incr e ω ^ 2 ∂μ
  weight := G.weight
  memLp_root := hroot
  memLp_incr := hincr
  inner_incr := hinner
  sq_incr _ := rfl

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. -/
  ⋯

MathlibExt/Biology/PopulationGenetics/FStatistics.lean:188

  len : E → ℝ

MathlibExt/Biology/PopulationGenetics/FStatistics.lean:194

  sq_incr : ∀ e, ∫ ω, incr e ω ^ 2 ∂μ = len e

MathlibExt/Biology/PopulationGenetics/FStatistics.lean:204

Uses 4

Statement usesAdmixture graph · Edges of an admixture graph · Lineage weight of an edge in an admixture graph · Admixture-graph drift model

TheoremA tree-shaped admixture graph has binary loadings#✓fully proved

A tree-shaped admixture graph induces a drift model with binary loadings (all weights 0 or 1).

theorem hasBinaryLoadings_of_isTree (hG : G.IsTree) {M : DriftModel μ G.Edge V}
    (hM : M.weight = G.weight) : M.HasBinaryLoadings

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. -/
  ⋯

MathlibExt/Biology/PopulationGenetics/FStatistics.lean:188

Uses 7 · Used by 1

Statement usesAdmixture graph · Edges of an admixture graph · Tree-shaped admixture graph · Lineage weight of an edge in an admixture graph · Admixture-graph drift model · Binary loadings of a drift model

Proof usesLineage weights on a tree are zero or one

Used byThree-population test is nonnegative on a tree

TheoremThree-population test is nonnegative on a tree#✓fully proved

The three-population test on a tree-shaped admixture graph: f3 C A B ≥ 0.

theorem f3_nonneg_of_isTree (hG : G.IsTree) {M : DriftModel μ G.Edge V}
    (hM : M.weight = G.weight) (C A B : V) : 0 ≤ f3 μ M.freq C A B

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. -/
  ⋯

MathlibExt/Biology/PopulationGenetics/FStatistics.lean:188

noncomputable def f3 (C A B : P) : ℝ := ∫ ω, (p C ω - p A ω) * (p C ω - p B ω) ∂μ

MathlibExt/Biology/PopulationGenetics/FStatistics.lean:89

Uses 9

Statement usesAdmixture graph · Edges of an admixture graph · Tree-shaped admixture graph · Lineage weight of an edge in an admixture graph · Admixture-graph drift model · Allele frequency of a population in the drift model · f3 statistic

Proof usesA tree-shaped admixture graph has binary loadings · f3 is nonnegative under binary loadings

TheoremThree-population statistic at an admixture node#✓fully proved

The three-population statistic at an admixture node X with parents A ≠ B, proportions α = prop X A and β = prop X B (α + β = 1), in a drift model with the graph's weights: f3 X A B = α² ℓ_{XA} + β² ℓ_{XB} - α β f2 A B, where ℓ_{XA}, ℓ_{XB} are the drift lengths of the two admixture edges.

theorem f3_admixture {M : DriftModel μ G.Edge V} (hM : M.weight = G.weight) {X A B : V}
    (hX : G.parents X = {A, B}) (hAB : A ≠ B) :
    f3 μ M.freq X A B =
      G.prop X A ^ 2 * M.len ⟨(X, A), by simp [hX]⟩ +
        G.prop X B ^ 2 * M.len ⟨(X, B), by simp [hX]⟩ -
        G.prop X A * G.prop X B * f2 μ M.freq A B

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. -/
  ⋯

MathlibExt/Biology/PopulationGenetics/FStatistics.lean:188

noncomputable def f3 (C A B : P) : ℝ := ∫ ω, (p C ω - p A ω) * (p C ω - p B ω) ∂μ

MathlibExt/Biology/PopulationGenetics/FStatistics.lean:89

Uses 12 · Used by 1

Statement usesAdmixture graph · Edges of an admixture graph · Lineage weight of an edge in an admixture graph · Admixture-graph drift model · Allele frequency of a population in the drift model · f2 statistic · f3 statistic

Proof usesProbability that a lineage passes through a node · A lineage from a parent never passes through its child · Lineage weight recursion at an admixture node · f2 in the drift model · f3 in the drift model

Used byThree-population statistic at an admixture node without edge drift

TheoremThree-population statistic at an admixture node without edge drift#✓fully proved

With no drift on the admixture edges, an admixture node X with parents A ≠ B and proportion α = prop X A has f3 X A B = -α (1 - α) f2 A B (the hypothesis of the seed's DriftModel.f3_admixture, here derived from the graph).

theorem f3_admixture_of_len_eq_zero {M : DriftModel μ G.Edge V} (hM : M.weight = G.weight)
    {X A B : V} (hX : G.parents X = {A, B}) (hAB : A ≠ B)
    (hA : M.len ⟨(X, A), by simp [hX]⟩ = 0) (hB : M.len ⟨(X, B), by simp [hX]⟩ = 0) :
    f3 μ M.freq X A B = -(G.prop X A * (1 - G.prop X A)) * f2 μ M.freq A B

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. -/
  ⋯

MathlibExt/Biology/PopulationGenetics/FStatistics.lean:188

Uses 8

Statement usesAdmixture graph · Edges of an admixture graph · Lineage weight of an edge in an admixture graph · Admixture-graph drift model · Allele frequency of a population in the drift model · f2 statistic · f3 statistic

Proof usesThree-population statistic at an admixture node

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.