Pedigree kinship and inbreeding

StructurePedigree#✓fully proved

A pedigree on the individuals Fin n, numbered so that parents precede their children (every finite pedigree, a finite DAG, has such a numbering). parents i = some g means that g 0 is the father and g 1 the mother of i; parents i = none means that i is a founder. Founders are unrelated and not inbred (their 2 n_F gene copies are distinct).

structure Pedigree (n : ℕ) where
  /-- The parents `(g 0, g 1)` = (father, mother) of a non-founder; `none` for a founder. -/
  parents : Fin n → Option (Fin 2 → Fin n)
  /-- Parents precede their children. -/
  parents_lt : ∀ i g, parents i = some g → ∀ k, g k < i

Used by 42

Used byAncestral paths from an individual · An ancestral path returning to its start is trivial · Ancestral path as its start followed by a tail · Kinship coefficient under gene dropping · Symmetry of gene-dropping kinship · Malécot's recursion computes gene-dropping kinship · Zero kinship with an unrelated founder · Malécot's recursion · Self-kinship under gene dropping · Ancestral paths are nonempty with the starting individual as head · Probability of identity by descent under gene dropping · Symmetry of identity by descent · Malécot's recursion step for identity by descent · A gene copy is identical by descent with itself · Inbreeding coefficient under gene dropping · Malécot's recursion computes the inbreeding coefficient · Wright's path formula · Founders are not inbred · Malécot · Ancestor relation in a pedigree · Parents are ancestors · Parent relation in a pedigree · Kinship coefficient by Malécot's recursion · Symmetry of tabular kinship · Wright's path formula · Inbreeding coefficient by Malécot's recursion · Tabular kinship when the first individual is a later founder · Tabular kinship when the first individual is a later non-founder · Tabular kinship when the second individual is a later founder · Tabular kinship when the second individual is a later non-founder · Tabular self-kinship of a founder · Tabular self-kinship of a non-founder · Individuals on an ancestral path are its start or precede it · Ancestors precede their descendants · Ancestral paths from a founder · Ancestral paths from a non-founder · Pedigree without selfing · Founder origin of a gene copy · A founder gene copy is its own origin · Origin of a gene copy of a non-founder · Ancestral paths ending at a given ancestor · Trivial ancestral path

DefinitionParent relation in a pedigree#✓fully proved

a is a parent of b.

def IsParent (a b : Fin n) : Prop := ∃ g, P.parents b = some g ∧ ∃ k, g k = a

Uses 1 · Used by 6

Statement usesPedigree

Used byZero kinship with an unrelated founder · Malécot's recursion step for identity by descent · Malécot · Ancestor relation in a pedigree · Parents are ancestors · Ancestors precede their descendants

DefinitionAncestor relation in a pedigree#✓fully proved

a is an ancestor of b (a parent, a parent of a parent, …).

def IsAncestor : Fin n → Fin n → Prop := Relation.TransGen P.IsParent

Uses 2 · Used by 7

Statement usesPedigree · Parent relation in a pedigree

Used byMalécot's recursion computes gene-dropping kinship · Zero kinship with an unrelated founder · Malécot's recursion · Malécot's recursion step for identity by descent · Malécot · Parents are ancestors · Ancestors precede their descendants

DefinitionPedigree without selfing#✓fully proved

No individual is the offspring of a selfing (father ≠ mother), as in Wright's setting of a bisexual population.

def NoSelfing : Prop := ∀ i g, P.parents i = some g → g 0 ≠ g 1

Uses 1 · Used by 2

Statement usesPedigree

Used byWright's path formula · Wright's path formula

44 fully proved

Gene dropping

AbbreviationGene-dropping outcome#✓fully proved

A gene-dropping outcome: ω i k is the Mendelian coin of the copy (i, k) (k = 0 the paternal copy, k = 1 the maternal copy), saying which copy (0 or 1) of the parent g k of i it inherits. Under gene dropping all 4 ^ n outcomes are equally likely.

abbrev Coins (n : ℕ) : Type := Fin n → Fin 2 → Fin 2

Used by 10

Used byZero kinship with an unrelated founder · Probability of identity by descent under gene dropping · Symmetry of identity by descent · Malécot's recursion step for identity by descent · A gene copy is identical by descent with itself · Founders are not inbred · Malécot · Founder origin of a gene copy · A founder gene copy is its own origin · Origin of a gene copy of a non-founder

DefinitionFounder origin of a gene copy#✓fully proved

The founder copy from which the gene copy c = (i, k) descends under the gene-dropping outcome ω: a founder copy is its own origin; a copy of a non-founder descends from the copy ω i k of its parent g k.

def origin (ω : Coins n) (c : Fin n × Fin 2) : Fin n × Fin 2 :=
  match _h : P.parents c.1 with
  | none => c
  | some g => origin ω (g c.2, ω c.1 c.2)
termination_by c.1.val
decreasing_by exact P.parents_lt c.1 g _h c.2

Uses 2 · Used by 9

Statement usesPedigree · Gene-dropping outcome

Used byZero kinship with an unrelated founder · Probability of identity by descent under gene dropping · Symmetry of identity by descent · Malécot's recursion step for identity by descent · A gene copy is identical by descent with itself · Founders are not inbred · Malécot · A founder gene copy is its own origin · Origin of a gene copy of a non-founder

DefinitionProbability of identity by descent under gene dropping#✓fully proved

The probability, under gene dropping (independent fair Mendelian coins), that the gene copies c and d are identical by descent, i.e. descend from the same founder copy.

noncomputable def ibd (c d : Fin n × Fin 2) : ℝ :=
  ((Finset.univ.filter fun ω : Coins n => P.origin ω c = P.origin ω d).card : ℝ) / 4 ^ n

Uses 3 · Used by 10

Statement usesPedigree · Gene-dropping outcome · Founder origin of a gene copy

Used byKinship coefficient under gene dropping · Symmetry of gene-dropping kinship · Zero kinship with an unrelated founder · Malécot's recursion · Self-kinship under gene dropping · Symmetry of identity by descent · Malécot's recursion step for identity by descent · A gene copy is identical by descent with itself · Inbreeding coefficient under gene dropping · Malécot

DefinitionKinship coefficient under gene dropping#✓fully proved

The kinship (coancestry) coefficient under gene dropping: the probability that a copy drawn at random from i and a copy drawn at random from j are identical by descent.

noncomputable def geneDropKinship (i j : Fin n) : ℝ :=
  (∑ a : Fin 2, ∑ b : Fin 2, P.ibd (i, a) (j, b)) / 4

Uses 2 · Used by 7

Statement usesPedigree · Probability of identity by descent under gene dropping

Used bySymmetry of gene-dropping kinship · Malécot's recursion computes gene-dropping kinship · Zero kinship with an unrelated founder · Malécot's recursion · Self-kinship under gene dropping · Malécot's recursion computes the inbreeding coefficient · Malécot

DefinitionInbreeding coefficient under gene dropping#✓fully proved

The inbreeding coefficient under gene dropping: the probability that the two copies of i are identical by descent.

noncomputable def inbreeding (i : Fin n) : ℝ := P.ibd (i, 0) (i, 1)

Uses 2 · Used by 6

Statement usesPedigree · Probability of identity by descent under gene dropping

Used byMalécot's recursion computes gene-dropping kinship · Self-kinship under gene dropping · Malécot's recursion computes the inbreeding coefficient · Wright's path formula · Founders are not inbred · Malécot

Malécot's recursion (the tabular method)

DefinitionKinship coefficient by Malécot's recursion#✓fully proved

The kinship coefficient by Malécot's recursion, computed in the order of the numbering (the tabular method): for i < j, φ i j = (φ i f + φ i m) / 2 with f, m the parents of j and φ i j = 0 if j is a founder; φ i i = (1 + φ f m) / 2 with f, m the parents of i and φ i i = 1 / 2 for a founder; symmetric for j < i.

MathlibExt.Biology.StatisticalGenetics.Kinship.Pedigree.kinship · 20 lines

noncomputable def kinship (i j : Fin n) : ℝ :=
  if _hji : j < i then
    match h : P.parents i with
    | none => 0
    | some g => (kinship (g 0) j + kinship (g 1) j) / 2
  else if _hij : i < j then
    match h : P.parents j with
    | none => 0
    | some g => (kinship i (g 0) + kinship i (g 1)) / 2
  else
    match h : P.parents i with
    | none => 1 / 2
    | some g => (1 + kinship (g 0) (g 1)) / 2
termination_by i.val + j.val
decreasing_by
  all_goals
    have h0 := P.parents_lt _ g h 0
    have h1 := P.parents_lt _ g h 1
    simp only [Fin.lt_def, not_lt] at *
    omega

Uses 1 · Used by 12

Statement usesPedigree

Used byMalécot's recursion computes gene-dropping kinship · Malécot's recursion computes the inbreeding coefficient · Wright's path formula · Symmetry of tabular kinship · Wright's path formula · Inbreeding coefficient by Malécot's recursion · Tabular kinship when the first individual is a later founder · Tabular kinship when the first individual is a later non-founder · Tabular kinship when the second individual is a later founder · Tabular kinship when the second individual is a later non-founder · Tabular self-kinship of a founder · Tabular self-kinship of a non-founder

DefinitionInbreeding coefficient by Malécot's recursion#✓fully proved

The inbreeding coefficient by Malécot's recursion: F i = φ f m for the parents f, m of i, and F i = 0 for a founder.

noncomputable def kinshipInbreeding (i : Fin n) : ℝ :=
  match P.parents i with
  | none => 0
  | some g => P.kinship (g 0) (g 1)

Uses 2 · Used by 3

Statement usesPedigree · Kinship coefficient by Malécot's recursion

Used byMalécot's recursion computes the inbreeding coefficient · Wright's path formula · Wright's path formula

TheoremTabular kinship when the second individual is a later non-founder#✓fully proved

The tabular recursion for i < j with j a non-founder.

theorem kinship_of_lt_of_parents_eq_some {i j : Fin n} {g : Fin 2 → Fin n} (hij : i < j)
    (h : P.parents j = some g) :
    P.kinship i j = (P.kinship i (g 0) + P.kinship i (g 1)) / 2

Uses 2 · Used by 3

Statement usesPedigree · Kinship coefficient by Malécot's recursion

Used byMalécot's recursion computes gene-dropping kinship · Symmetry of tabular kinship · Wright's path formula

TheoremTabular kinship when the second individual is a later founder#✓fully proved

The tabular recursion for i < j with j a founder.

theorem kinship_of_lt_of_parents_eq_none {i j : Fin n} (hij : i < j)
    (h : P.parents j = none) : P.kinship i j = 0

Uses 2 · Used by 3

Statement usesPedigree · Kinship coefficient by Malécot's recursion

Used byMalécot's recursion computes gene-dropping kinship · Symmetry of tabular kinship · Wright's path formula

TheoremTabular self-kinship of a non-founder#✓fully proved

The tabular recursion on the diagonal for a non-founder: φ i i = (1 + φ f m) / 2.

theorem kinship_self_of_parents_eq_some {i : Fin n} {g : Fin 2 → Fin n}
    (h : P.parents i = some g) : P.kinship i i = (1 + P.kinship (g 0) (g 1)) / 2

Uses 2 · Used by 2

Statement usesPedigree · Kinship coefficient by Malécot's recursion

Used byMalécot's recursion computes gene-dropping kinship · Wright's path formula

TheoremTabular self-kinship of a founder#✓fully proved

The tabular recursion on the diagonal for a founder: φ i i = 1 / 2.

theorem kinship_self_of_parents_eq_none {i : Fin n} (h : P.parents i = none) :
    P.kinship i i = 1 / 2

Uses 2 · Used by 2

Statement usesPedigree · Kinship coefficient by Malécot's recursion

Used byMalécot's recursion computes gene-dropping kinship · Wright's path formula

TheoremTabular kinship when the first individual is a later non-founder#✓fully proved

The tabular recursion for j < i with i a non-founder.

theorem kinship_of_gt_of_parents_eq_some {i j : Fin n} {g : Fin 2 → Fin n} (hji : j < i)
    (h : P.parents i = some g) :
    P.kinship i j = (P.kinship (g 0) j + P.kinship (g 1) j) / 2

Uses 2 · Used by 3

Statement usesPedigree · Kinship coefficient by Malécot's recursion

Used byMalécot's recursion computes gene-dropping kinship · Symmetry of tabular kinship · Wright's path formula

TheoremTabular kinship when the first individual is a later founder#✓fully proved

The tabular recursion for j < i with i a founder.

theorem kinship_of_gt_of_parents_eq_none {i j : Fin n} (hji : j < i)
    (h : P.parents i = none) : P.kinship i j = 0

Uses 2 · Used by 3

Statement usesPedigree · Kinship coefficient by Malécot's recursion

Used byMalécot's recursion computes gene-dropping kinship · Symmetry of tabular kinship · Wright's path formula

TheoremSymmetry of tabular kinship#✓fully proved

The tabular kinship is symmetric.

theorem kinship_comm (i j : Fin n) : P.kinship i j = P.kinship j i

Uses 6

Statement usesPedigree · Kinship coefficient by Malécot's recursion

Proof usesTabular kinship when the first individual is a later founder · Tabular kinship when the first individual is a later non-founder · Tabular kinship when the second individual is a later founder · Tabular kinship when the second individual is a later non-founder

Wright's path formula

DefinitionAncestral paths from an individual#✓fully proved

The ancestral paths from i: the lists [i = v₀, v₁, …, v_k] with each v_{t+1} a parent of v_t (k ≥ 0; the path [i] has no edge).

noncomputable def ancPaths (i : Fin n) : Finset (List (Fin n)) :=
  match h : P.parents i with
  | none => {[i]}
  | some g => insert [i] (Finset.univ.biUnion fun k : Fin 2 =>
      (ancPaths (g k)).image (List.cons i))
termination_by i.val
decreasing_by exact P.parents_lt i g h k

Uses 1 · Used by 9

Statement usesPedigree

Used byAn ancestral path returning to its start is trivial · Ancestral path as its start followed by a tail · Ancestral paths are nonempty with the starting individual as head · Wright's path formula · Individuals on an ancestral path are its start or precede it · Ancestral paths from a founder · Ancestral paths from a non-founder · Ancestral paths ending at a given ancestor · Trivial ancestral path

DefinitionAncestral paths ending at a given ancestor#✓fully proved

The ancestral paths from i that end at A.

noncomputable def pathsTo (i A : Fin n) : Finset (List (Fin n)) :=
  (P.ancPaths i).filter fun p => p.getLast? = some A

Uses 2 · Used by 2

Statement usesPedigree · Ancestral paths from an individual

Used byWright's path formula · Wright's path formula

TheoremAncestral paths are nonempty with the starting individual as head#✓fully proved

Every path in ancPaths i starts at i and is nonempty.

theorem head?_of_mem_ancPaths {i : Fin n} {p : List (Fin n)} (hp : p ∈ P.ancPaths i) :
    p.head? = some i

Uses 2 · Used by 2

Statement usesPedigree · Ancestral paths from an individual

Used byAncestral path as its start followed by a tail · Wright's path formula

Gene dropping: basic facts

TheoremA founder gene copy is its own origin#✓fully proved

A founder copy is its own origin.

theorem origin_of_parents_eq_none {c : Fin n × Fin 2} (h : P.parents c.1 = none) (ω : Coins n) :
    P.origin ω c = c

Uses 3 · Used by 4

Statement usesPedigree · Gene-dropping outcome · Founder origin of a gene copy

Used byZero kinship with an unrelated founder · Malécot's recursion step for identity by descent · Founders are not inbred · Malécot

TheoremOrigin of a gene copy of a non-founder#✓fully proved

A copy of a non-founder descends from the chosen copy of the corresponding parent.

theorem origin_of_parents_eq_some {c : Fin n × Fin 2} {g : Fin 2 → Fin n}
    (h : P.parents c.1 = some g) (ω : Coins n) :
    P.origin ω c = P.origin ω (g c.2, ω c.1 c.2)

Uses 3 · Used by 3

Statement usesPedigree · Gene-dropping outcome · Founder origin of a gene copy

Used byZero kinship with an unrelated founder · Malécot's recursion step for identity by descent · Malécot

TheoremAncestors precede their descendants#✓fully proved

Ancestors precede their descendants.

theorem IsAncestor.lt {a b : Fin n} (h : P.IsAncestor a b) : a < b

Uses 3 · Used by 3

Statement usesPedigree · Ancestor relation in a pedigree

Proof usesParent relation in a pedigree

Used byMalécot's recursion computes gene-dropping kinship · Malécot's recursion step for identity by descent · Malécot

TheoremParents are ancestors#✓fully proved

A parent is an ancestor.

theorem isAncestor_of_parents_eq_some {i : Fin n} {g : Fin 2 → Fin n}
    (h : P.parents i = some g) (k : Fin 2) : P.IsAncestor (g k) i

Uses 3 · Used by 3

Statement usesPedigree · Ancestor relation in a pedigree

Proof usesParent relation in a pedigree

Used byZero kinship with an unrelated founder · Malécot's recursion step for identity by descent · Malécot

Gene dropping satisfies Malécot's recursion

TheoremA gene copy is identical by descent with itself#✓fully proved

Two copies are identical by descent of themselves with probability 1.

theorem ibd_self (c : Fin n × Fin 2) : P.ibd c c = 1

Uses 4 · Used by 1

Statement usesPedigree · Probability of identity by descent under gene dropping

Proof usesGene-dropping outcome · Founder origin of a gene copy

Used bySelf-kinship under gene dropping

TheoremSymmetry of identity by descent#✓fully proved

Identity by descent is symmetric.

theorem ibd_comm (c d : Fin n × Fin 2) : P.ibd c d = P.ibd d c

Uses 4 · Used by 2

Statement usesPedigree · Probability of identity by descent under gene dropping

Proof usesGene-dropping outcome · Founder origin of a gene copy

Used bySymmetry of gene-dropping kinship · Self-kinship under gene dropping

TheoremMalécot's recursion step for identity by descent#✓fully proved

One step of Malécot's recursion for identity by descent.

theorem ibd_of_parents_eq_some {i j : Fin n} {g : Fin 2 → Fin n} (hij : j ≠ i)
    (hanc : ¬ P.IsAncestor j i) (h : P.parents j = some g) (a b : Fin 2) :
    P.ibd (i, a) (j, b) = (P.ibd (i, a) (g b, 0) + P.ibd (i, a) (g b, 1)) / 2

Uses 10 · Used by 1

Statement usesPedigree · Ancestor relation in a pedigree · Probability of identity by descent under gene dropping

Proof usesGene-dropping outcome · Ancestors precede their descendants · Parent relation in a pedigree · Parents are ancestors · Founder origin of a gene copy · A founder gene copy is its own origin · Origin of a gene copy of a non-founder

Used byMalécot's recursion

TheoremSelf-kinship under gene dropping#✓fully proved

φ i i = (1 + F i) / 2 under gene dropping.

theorem geneDropKinship_self (i : Fin n) :
    P.geneDropKinship i i = (1 + P.inbreeding i) / 2

Uses 6 · Used by 1

Statement usesPedigree · Kinship coefficient under gene dropping · Inbreeding coefficient under gene dropping

Proof usesProbability of identity by descent under gene dropping · Symmetry of identity by descent · A gene copy is identical by descent with itself

Used byMalécot's recursion computes gene-dropping kinship

TheoremFounders are not inbred#✓fully proved

The inbreeding coefficient of a founder is 0.

theorem inbreeding_of_parents_eq_none {i : Fin n} (h : P.parents i = none) :
    P.inbreeding i = 0

Uses 5 · Used by 2

Statement usesPedigree · Inbreeding coefficient under gene dropping

Proof usesGene-dropping outcome · Founder origin of a gene copy · A founder gene copy is its own origin

Used byMalécot's recursion computes gene-dropping kinship · Malécot's recursion computes the inbreeding coefficient

TheoremMalécot#✓fully proved

The inbreeding coefficient of i is the kinship of its parents, F i = φ f m, under gene dropping.

theorem inbreeding_of_parents_eq_some {i : Fin n} {g : Fin 2 → Fin n}
    (h : P.parents i = some g) : P.inbreeding i = P.geneDropKinship (g 0) (g 1)

Uses 12 · Used by 2

Statement usesPedigree · Kinship coefficient under gene dropping · Inbreeding coefficient under gene dropping

Proof usesGene-dropping outcome · Ancestor relation in a pedigree · Ancestors precede their descendants · Parent relation in a pedigree · Probability of identity by descent under gene dropping · Parents are ancestors · Founder origin of a gene copy · A founder gene copy is its own origin · Origin of a gene copy of a non-founder

Used byMalécot's recursion computes gene-dropping kinship · Malécot's recursion computes the inbreeding coefficient

TheoremMalécot's recursion#✓fully proved

Malécot's recursion under gene dropping: if j ≠ i is not an ancestor of i and has parents f, m, then φ i j = (φ i f + φ i m) / 2.

theorem geneDropKinship_of_parents_eq_some {i j : Fin n} {g : Fin 2 → Fin n} (hij : j ≠ i)
    (hanc : ¬ P.IsAncestor j i) (h : P.parents j = some g) :
    P.geneDropKinship i j = (P.geneDropKinship i (g 0) + P.geneDropKinship i (g 1)) / 2

Uses 5 · Used by 1

Statement usesPedigree · Ancestor relation in a pedigree · Kinship coefficient under gene dropping

Proof usesProbability of identity by descent under gene dropping · Malécot's recursion step for identity by descent

Used byMalécot's recursion computes gene-dropping kinship

TheoremZero kinship with an unrelated founder#✓fully proved

A founder j ≠ i that is not an ancestor of i has kinship 0 with i.

theorem geneDropKinship_of_parents_eq_none {i j : Fin n} (hij : j ≠ i)
    (hanc : ¬ P.IsAncestor j i) (h : P.parents j = none) : P.geneDropKinship i j = 0

Uses 10 · Used by 1

Statement usesPedigree · Ancestor relation in a pedigree · Kinship coefficient under gene dropping

Proof usesGene-dropping outcome · Parent relation in a pedigree · Probability of identity by descent under gene dropping · Parents are ancestors · Founder origin of a gene copy · A founder gene copy is its own origin · Origin of a gene copy of a non-founder

Used byMalécot's recursion computes gene-dropping kinship

TheoremSymmetry of gene-dropping kinship#✓fully proved

Gene-dropping kinship is symmetric.

theorem geneDropKinship_comm (i j : Fin n) : P.geneDropKinship i j = P.geneDropKinship j i

Uses 4 · Used by 1

Statement usesPedigree · Kinship coefficient under gene dropping

Proof usesProbability of identity by descent under gene dropping · Symmetry of identity by descent

Used byMalécot's recursion computes gene-dropping kinship

TheoremMalécot's recursion computes gene-dropping kinship#✓fully proved

The kinship coefficient computed by Malécot's recursion is the probability of identity by descent under gene dropping.

theorem geneDropKinship_eq_kinship (i j : Fin n) :
    P.geneDropKinship i j = P.kinship i j

Uses 18 · Used by 1

Statement usesPedigree · Kinship coefficient under gene dropping · Kinship coefficient by Malécot's recursion

Proof usesAncestor relation in a pedigree · Ancestors precede their descendants · Symmetry of gene-dropping kinship · Zero kinship with an unrelated founder · Malécot's recursion · Self-kinship under gene dropping · Inbreeding coefficient under gene dropping · Founders are not inbred · Malécot · Tabular kinship when the first individual is a later founder · Tabular kinship when the first individual is a later non-founder · Tabular kinship when the second individual is a later founder · Tabular kinship when the second individual is a later non-founder · Tabular self-kinship of a founder · Tabular self-kinship of a non-founder

Used byMalécot's recursion computes the inbreeding coefficient

TheoremMalécot's recursion computes the inbreeding coefficient#✓fully proved

The inbreeding coefficient computed by Malécot's recursion is the probability of identity by descent of the two copies of i under gene dropping.

theorem inbreeding_eq_kinshipInbreeding (i : Fin n) :
    P.inbreeding i = P.kinshipInbreeding i

Uses 8 · Used by 1

Statement usesPedigree · Inbreeding coefficient under gene dropping · Inbreeding coefficient by Malécot's recursion

Proof usesKinship coefficient under gene dropping · Malécot's recursion computes gene-dropping kinship · Founders are not inbred · Malécot · Kinship coefficient by Malécot's recursion

Used byWright's path formula

Wright's path formula: proof

TheoremAncestral paths from a founder#✓fully proved

The only ancestral path from a founder is [i].

theorem mem_ancPaths_of_parents_eq_none {i : Fin n} (h : P.parents i = none)
    {p : List (Fin n)} : p ∈ P.ancPaths i ↔ p = [i]

Uses 2 · Used by 4

Statement usesPedigree · Ancestral paths from an individual

Used byAn ancestral path returning to its start is trivial · Wright's path formula · Individuals on an ancestral path are its start or precede it · Trivial ancestral path

TheoremAncestral paths from a non-founder#✓fully proved

The ancestral paths from a non-founder: [i] and i :: q for a path q from a parent.

theorem mem_ancPaths_of_parents_eq_some {i : Fin n} {g : Fin 2 → Fin n}
    (h : P.parents i = some g) {p : List (Fin n)} :
    p ∈ P.ancPaths i ↔ p = [i] ∨ ∃ k, ∃ q ∈ P.ancPaths (g k), p = i :: q

Uses 2 · Used by 4

Statement usesPedigree · Ancestral paths from an individual

Used byAn ancestral path returning to its start is trivial · Wright's path formula · Individuals on an ancestral path are its start or precede it · Trivial ancestral path

TheoremIndividuals on an ancestral path are its start or precede it#✓fully proved

Every individual on an ancestral path from i is i or precedes it.

theorem le_of_mem_ancPaths {i : Fin n} {p : List (Fin n)} (hp : p ∈ P.ancPaths i) :
    ∀ v ∈ p, v ≤ i

Uses 4 · Used by 2

Statement usesPedigree · Ancestral paths from an individual

Proof usesAncestral paths from a founder · Ancestral paths from a non-founder

Used byAn ancestral path returning to its start is trivial · Wright's path formula

TheoremAncestral path as its start followed by a tail#✓fully proved

Every ancestral path from i starts with i.

theorem exists_eq_cons_of_mem_ancPaths {i : Fin n} {p : List (Fin n)}
    (hp : p ∈ P.ancPaths i) : ∃ q, p = i :: q

Uses 3 · Used by 2

Statement usesPedigree · Ancestral paths from an individual

Proof usesAncestral paths are nonempty with the starting individual as head

Used byAn ancestral path returning to its start is trivial · Wright's path formula

TheoremAn ancestral path returning to its start is trivial#✓fully proved

A path from i ending at i is [i].

theorem eq_singleton_of_mem_ancPaths {i : Fin n} {p : List (Fin n)} (hp : p ∈ P.ancPaths i)
    (hl : p.getLast? = some i) : p = [i]

Uses 6 · Used by 1

Statement usesPedigree · Ancestral paths from an individual

Proof usesAncestral path as its start followed by a tail · Individuals on an ancestral path are its start or precede it · Ancestral paths from a founder · Ancestral paths from a non-founder

Used byWright's path formula

TheoremTrivial ancestral path#✓fully proved

[i] is an ancestral path from i.

theorem singleton_mem_ancPaths (i : Fin n) : [i] ∈ P.ancPaths i

Uses 4 · Used by 1

Statement usesPedigree · Ancestral paths from an individual

Proof usesAncestral paths from a founder · Ancestral paths from a non-founder

Used byWright's path formula

TheoremWright's path formula#✓fully proved

Wright's path formula in kinship form: φ i j is the sum, over common ancestors A (including i or j themselves) and pairs of ancestral paths p from i to A and p' from j to A that share no individual other than A, of (1/2) ^ (n₁ + n₂ + 1) * (1 + F A), where n₁ + n₂ + 1 = p.length + p'.length - 1 is the number of individuals on the loop.

theorem kinship_eq_sum_paths (hP : P.NoSelfing) (i j : Fin n) :
    P.kinship i j = ∑ A, ∑ p ∈ P.pathsTo i A, ∑ p' ∈ P.pathsTo j A,
      if ∀ v ∈ p, v ∈ p' → v = A then
        (1 / 2 : ℝ) ^ (p.length + p'.length - 1) * (1 + P.kinshipInbreeding A)
      else 0

Uses 19 · Used by 1

Statement usesPedigree · Pedigree without selfing · Kinship coefficient by Malécot's recursion · Inbreeding coefficient by Malécot's recursion · Ancestral paths ending at a given ancestor

Proof usesAncestral paths from an individual · An ancestral path returning to its start is trivial · Ancestral path as its start followed by a tail · Ancestral paths are nonempty with the starting individual as head · Tabular kinship when the first individual is a later founder · Tabular kinship when the first individual is a later non-founder · Tabular kinship when the second individual is a later founder · Tabular kinship when the second individual is a later non-founder · Tabular self-kinship of a founder · Tabular self-kinship of a non-founder · Individuals on an ancestral path are its start or precede it · Ancestral paths from a founder · Ancestral paths from a non-founder · Trivial ancestral path

Used byWright's path formula

TheoremWright's path formula#✓fully proved

Wright's path formula for the inbreeding coefficient (Wright 1922): if i has parents f = g 0 and m = g 1, then F_i = Σ (1/2) ^ (n₁ + n₂ + 1) (1 + F_A) over common ancestors A of f and m (including f or m themselves) and pairs of ancestral paths from f and m to A (with n₁ and n₂ edges) that share only A. Here F is the gene-dropping inbreeding coefficient.

theorem inbreeding_eq_sum_paths (hP : P.NoSelfing) {i : Fin n} {g : Fin 2 → Fin n}
    (h : P.parents i = some g) :
    P.inbreeding i = ∑ A, ∑ p ∈ P.pathsTo (g 0) A, ∑ p' ∈ P.pathsTo (g 1) A,
      if ∀ v ∈ p, v ∈ p' → v = A then
        (1 / 2 : ℝ) ^ (p.length + p'.length - 1) * (1 + P.inbreeding A)
      else 0

Uses 8

Statement usesPedigree · Pedigree without selfing · Inbreeding coefficient under gene dropping · Ancestral paths ending at a given ancestor

Proof usesMalécot's recursion computes the inbreeding coefficient · Kinship coefficient by Malécot's recursion · Inbreeding coefficient by Malécot's recursion · Wright's path formula

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.