Fisher's decomposition of genetic variance

DefinitionMean genotypic value under Hardy–Weinberg proportions#✓fully proved

The mean genotypic value μ = ∑ i ∑ j p i p j G i j under Hardy–Weinberg proportions.

noncomputable def meanValue (p : A → ℝ) (G : A → A → ℝ) : ℝ := ∑ i, ∑ j, p i * p j * G i j

Used by 17

Used byAdditive variance at a biallelic locus (Falconer & Mackay 1996, ch. 8) · Average effect of an allele · Full-sib covariance of genotypic values · Full sibs (Fisher 1918) · Half-sib covariance of genotypic values · Half sibs (Fisher 1918) · Parent–offspring covariance of genotypic values · Parent and offspring (Fisher 1918) · Dominance deviation of a genotype · Dominance variance at a biallelic locus (Falconer & Mackay 1996, ch. 8) · Least squares (Fisher 1918) · Genetic variance under Hardy–Weinberg proportions · Fisher's variance decomposition · Decomposition of the genotypic value · Average effects have mean zero · Orthogonality of dominance deviations in the first allele · Orthogonality of dominance deviations in the second allele

DefinitionAverage effect of an allele#✓fully proved

The average effect of allele i, α i = ∑ j p j G i j - μ: the mean value of the genotypes carrying i (the other gene drawn from the population) minus the population mean. This is the average excess; under Hardy–Weinberg proportions it is Fisher's average effect, the coefficient of the least-squares additive fit (domVar_le_sum_sq).

noncomputable def avgEffect (p : A → ℝ) (G : A → A → ℝ) (i : A) : ℝ :=
  ∑ j, p j * G i j - meanValue p G

Uses 1 · Used by 13

Statement usesMean genotypic value under Hardy–Weinberg proportions

Used byAdditive genetic variance · Additive variance at a biallelic locus (Falconer & Mackay 1996, ch. 8) · Full sibs (Fisher 1918) · Half sibs (Fisher 1918) · Parent and offspring (Fisher 1918) · Dominance deviation of a genotype · Dominance variance at a biallelic locus (Falconer & Mackay 1996, ch. 8) · Least squares (Fisher 1918) · Fisher's variance decomposition · Decomposition of the genotypic value · Average effects have mean zero · Orthogonality of dominance deviations in the first allele · Orthogonality of dominance deviations in the second allele

DefinitionDominance deviation of a genotype#✓fully proved

The dominance deviation δ i j = G i j - μ - α i - α j.

noncomputable def domDev (p : A → ℝ) (G : A → A → ℝ) (i j : A) : ℝ :=
  G i j - meanValue p G - avgEffect p G i - avgEffect p G j

Uses 2 · Used by 7

Statement usesAverage effect of an allele · Mean genotypic value under Hardy–Weinberg proportions

Used byDominance variance · Dominance variance at a biallelic locus (Falconer & Mackay 1996, ch. 8) · Least squares (Fisher 1918) · Fisher's variance decomposition · Decomposition of the genotypic value · Orthogonality of dominance deviations in the first allele · Orthogonality of dominance deviations in the second allele

DefinitionGenetic variance under Hardy–Weinberg proportions#✓fully proved

The genetic variance V_G = ∑ i ∑ j p i p j (G i j - μ) ².

noncomputable def genVar (p : A → ℝ) (G : A → A → ℝ) : ℝ :=
  ∑ i, ∑ j, p i * p j * (G i j - meanValue p G) ^ 2

Uses 1 · Used by 2

Statement usesMean genotypic value under Hardy–Weinberg proportions

Used byFull sibs (Fisher 1918) · Fisher's variance decomposition

DefinitionAdditive genetic variance#✓fully proved

The additive genetic variance V_A = 2 ∑ i p i α i ², the variance of the breeding value α i + α j.

noncomputable def addVar (p : A → ℝ) (G : A → A → ℝ) : ℝ :=
  2 * ∑ i, p i * avgEffect p G i ^ 2

Uses 1 · Used by 5

Statement usesAverage effect of an allele

Used byAdditive variance at a biallelic locus (Falconer & Mackay 1996, ch. 8) · Full sibs (Fisher 1918) · Half sibs (Fisher 1918) · Parent and offspring (Fisher 1918) · Fisher's variance decomposition

DefinitionDominance variance#✓fully proved

The dominance variance V_D = ∑ i ∑ j p i p j δ i j ².

noncomputable def domVar (p : A → ℝ) (G : A → A → ℝ) : ℝ :=
  ∑ i, ∑ j, p i * p j * domDev p G i j ^ 2

Uses 1 · Used by 4

Statement usesDominance deviation of a genotype

Used byFull sibs (Fisher 1918) · Dominance variance at a biallelic locus (Falconer & Mackay 1996, ch. 8) · Least squares (Fisher 1918) · Fisher's variance decomposition

TheoremDecomposition of the genotypic value#✓fully proved

The decomposition G i j = μ + α i + α j + δ i j (an identity by definition of δ).

theorem genotypicValue_eq (p : A → ℝ) (G : A → A → ℝ) (i j : A) :
    G i j = meanValue p G + avgEffect p G i + avgEffect p G j + domDev p G i j

Uses 3

Statement usesAverage effect of an allele · Dominance deviation of a genotype · Mean genotypic value under Hardy–Weinberg proportions

TheoremAverage effects have mean zero#✓fully proved

The average effects have mean zero: ∑ i p i α i = 0.

theorem sum_mul_avgEffect {p : A → ℝ} (hp : ∑ i, p i = 1) (G : A → A → ℝ) :
    ∑ i, p i * avgEffect p G i = 0

Uses 2 · Used by 5

Statement usesAverage effect of an allele

Proof usesMean genotypic value under Hardy–Weinberg proportions

Used byAverage effects are centred · Full sibs (Fisher 1918) · Half sibs (Fisher 1918) · Fisher's variance decomposition · Orthogonality of dominance deviations in the second allele

TheoremOrthogonality of dominance deviations in the second allele#✓fully proved

Orthogonality of the dominance deviations: ∑ j p j δ i j = 0 for every i.

theorem sum_mul_domDev_right {p : A → ℝ} (hp : ∑ i, p i = 1) (G : A → A → ℝ) (i : A) :
    ∑ j, p j * domDev p G i j = 0

Uses 4 · Used by 4

Statement usesDominance deviation of a genotype

Proof usesAverage effect of an allele · Mean genotypic value under Hardy–Weinberg proportions · Average effects have mean zero

Used byDominance deviations are orthogonal to every allele · Least squares (Fisher 1918) · Fisher's variance decomposition · Orthogonality of dominance deviations in the first allele

TheoremOrthogonality of dominance deviations in the first allele#✓fully proved

Orthogonality of the dominance deviations for a symmetric genotypic value: ∑ i p i δ i j = 0 for every j.

theorem sum_mul_domDev_left {p : A → ℝ} (hp : ∑ i, p i = 1) {G : A → A → ℝ}
    (hG : ∀ i j, G i j = G j i) (j : A) : ∑ i, p i * domDev p G i j = 0

Uses 4 · Used by 2

Statement usesDominance deviation of a genotype

Proof usesAverage effect of an allele · Mean genotypic value under Hardy–Weinberg proportions · Orthogonality of dominance deviations in the second allele

Used byLeast squares (Fisher 1918) · Fisher's variance decomposition

TheoremLeast squares (Fisher 1918)#✓fully proved

Among all fits c + a i + a j of the genotypic value by a function additive over the two genes, the additive fitted genotypic value μ + α i + α j minimizes the weighted squared error ∑ p i p j (G i j - c - a i - a j) ²; its error is V_D.

theorem domVar_le_sum_sq {p : A → ℝ} (hp0 : ∀ i, 0 ≤ p i) (hp : ∑ i, p i = 1)
    {G : A → A → ℝ} (hG : ∀ i j, G i j = G j i) (c : ℝ) (a : A → ℝ) :
    domVar p G ≤ ∑ i, ∑ j, p i * p j * (G i j - c - a i - a j) ^ 2

Uses 6 · Used by 1

Statement usesDominance variance

Proof usesAverage effect of an allele · Dominance deviation of a genotype · Mean genotypic value under Hardy–Weinberg proportions · Orthogonality of dominance deviations in the first allele · Orthogonality of dominance deviations in the second allele

Used byThe additive fit is least squares

TheoremFisher's variance decomposition#✓fully proved

V_G = V_A + V_D.

theorem genVar_eq_addVar_add_domVar {p : A → ℝ} (hp : ∑ i, p i = 1) {G : A → A → ℝ}
    (hG : ∀ i j, G i j = G j i) : genVar p G = addVar p G + domVar p G

Uses 9 · Used by 2

Statement usesAdditive genetic variance · Dominance variance · Genetic variance under Hardy–Weinberg proportions

Proof usesAverage effect of an allele · Dominance deviation of a genotype · Mean genotypic value under Hardy–Weinberg proportions · Average effects have mean zero · Orthogonality of dominance deviations in the first allele · Orthogonality of dominance deviations in the second allele

Used byFisher decomposition · Full sibs (Fisher 1918)

22 fully proved

Covariances between relatives

DefinitionParent–offspring covariance of genotypic values#✓fully proved

The covariance of the genotypic values of a parent and its offspring: the parent has genotype (i, j) (frequency p i p j) and transmits cond b i j (each with probability 1/2), and the offspring's other gene k comes from an unrelated mate (frequency p k).

noncomputable def covParentOffspring (p : A → ℝ) (G : A → A → ℝ) : ℝ :=
  ∑ i, ∑ j, ∑ k, ∑ b : Bool, p i * p j * p k / 2 *
    ((G i j - meanValue p G) * (G (cond b i j) k - meanValue p G))

Uses 1 · Used by 1

Statement usesMean genotypic value under Hardy–Weinberg proportions

Used byParent and offspring (Fisher 1918)

DefinitionHalf-sib covariance of genotypic values#✓fully proved

The covariance of the genotypic values of half sibs: the common parent has genotype (i, j) and transmits cond b i j to one offspring and, independently, cond b' i j to the other; the second genes k, l come from two unrelated mates.

noncomputable def covHalfSibs (p : A → ℝ) (G : A → A → ℝ) : ℝ :=
  ∑ i, ∑ j, ∑ k, ∑ l, ∑ b : Bool, ∑ b' : Bool, p i * p j * p k * p l / 4 *
    ((G (cond b i j) k - meanValue p G) * (G (cond b' i j) l - meanValue p G))

Uses 1 · Used by 1

Statement usesMean genotypic value under Hardy–Weinberg proportions

Used byHalf sibs (Fisher 1918)

DefinitionFull-sib covariance of genotypic values#✓fully proved

The covariance of the genotypic values of full sibs: the sire (i, j) and the dam (k, l) are unrelated; the first offspring receives cond b i j and cond e k l, the second, independently, cond b' i j and cond e' k l.

noncomputable def covFullSibs (p : A → ℝ) (G : A → A → ℝ) : ℝ :=
  ∑ i, ∑ j, ∑ k, ∑ l, ∑ b : Bool, ∑ b' : Bool, ∑ e : Bool, ∑ e' : Bool,
    p i * p j * p k * p l / 16 *
      ((G (cond b i j) (cond e k l) - meanValue p G) *
        (G (cond b' i j) (cond e' k l) - meanValue p G))

Uses 1 · Used by 1

Statement usesMean genotypic value under Hardy–Weinberg proportions

Used byFull sibs (Fisher 1918)

TheoremParent and offspring (Fisher 1918)#✓fully proved

Cov(P, O) = V_A / 2.

theorem covParentOffspring_eq {p : A → ℝ} (hp : ∑ i, p i = 1) {G : A → A → ℝ}
    (hG : ∀ i j, G i j = G j i) : covParentOffspring p G = addVar p G / 2

Uses 4

Statement usesAdditive genetic variance · Parent–offspring covariance of genotypic values

Proof usesAverage effect of an allele · Mean genotypic value under Hardy–Weinberg proportions

TheoremHalf sibs (Fisher 1918)#✓fully proved

Cov(HS) = V_A / 4.

theorem covHalfSibs_eq {p : A → ℝ} (hp : ∑ i, p i = 1) (G : A → A → ℝ) :
    covHalfSibs p G = addVar p G / 4

Uses 5

Statement usesAdditive genetic variance · Half-sib covariance of genotypic values

Proof usesAverage effect of an allele · Mean genotypic value under Hardy–Weinberg proportions · Average effects have mean zero

TheoremFull sibs (Fisher 1918)#✓fully proved

Cov(FS) = V_A / 2 + V_D / 4.

theorem covFullSibs_eq {p : A → ℝ} (hp : ∑ i, p i = 1) {G : A → A → ℝ}
    (hG : ∀ i j, G i j = G j i) : covFullSibs p G = addVar p G / 2 + domVar p G / 4

Uses 8

Statement usesAdditive genetic variance · Full-sib covariance of genotypic values · Dominance variance

Proof usesAverage effect of an allele · Genetic variance under Hardy–Weinberg proportions · Fisher's variance decomposition · Mean genotypic value under Hardy–Weinberg proportions · Average effects have mean zero

Two alleles

DefinitionAllele frequencies at a biallelic locus#✓fully proved

Allele frequencies at a biallelic locus: A₁ (true) has frequency q₁ and A₂ (false) has frequency 1 - q₁.

def biallelicFreq (q₁ : ℝ) : Bool → ℝ := fun b => if b then q₁ else 1 - q₁

Used by 2

Used byAdditive variance at a biallelic locus (Falconer & Mackay 1996, ch. 8) · Dominance variance at a biallelic locus (Falconer & Mackay 1996, ch. 8)

DefinitionGenotypic values at a biallelic locus on Falconer's scale#✓fully proved

Genotypic values at a biallelic locus on Falconer's scale: A₁A₁ ↦ a, A₁A₂ ↦ d, A₂A₂ ↦ -a (the origin is the midpoint of the homozygotes).

def biallelicValue (a d : ℝ) : Bool → Bool → ℝ := fun b c =>
  if b then (if c then a else d) else (if c then d else -a)

Used by 2

Used byAdditive variance at a biallelic locus (Falconer & Mackay 1996, ch. 8) · Dominance variance at a biallelic locus (Falconer & Mackay 1996, ch. 8)

TheoremAdditive variance at a biallelic locus (Falconer & Mackay 1996, ch. 8)#✓fully proved

With p = q₁ and q = 1 - q₁, V_A = 2pq (a + d (q - p)) ². An algebraic identity, valid for every real q₁; it is a variance for 0 ≤ q₁ ≤ 1.

theorem addVar_biallelic (q₁ a d : ℝ) :
    addVar (biallelicFreq q₁) (biallelicValue a d) =
      2 * q₁ * (1 - q₁) * (a + d * ((1 - q₁) - q₁)) ^ 2

Uses 5

Statement usesAdditive genetic variance · Allele frequencies at a biallelic locus · Genotypic values at a biallelic locus on Falconer's scale

Proof usesAverage effect of an allele · Mean genotypic value under Hardy–Weinberg proportions

TheoremDominance variance at a biallelic locus (Falconer & Mackay 1996, ch. 8)#✓fully proved

V_D = (2pqd) ², for every real q₁.

theorem domVar_biallelic (q₁ a d : ℝ) :
    domVar (biallelicFreq q₁) (biallelicValue a d) = (2 * q₁ * (1 - q₁) * d) ^ 2

Uses 6

Statement usesAllele frequencies at a biallelic locus · Genotypic values at a biallelic locus on Falconer's scale · Dominance variance

Proof usesAverage effect of an allele · Dominance deviation of a genotype · Mean genotypic value under Hardy–Weinberg proportions

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.