Covariance between relatives

26 fully proved

Covariance Relatives

StructureSingle-locus model under random union of gametes#✓fully proved

A single locus under random union of gametes: allele frequencies p on a finite allele set and symmetric genotypic values g a b (the mean phenotype of genotype {a, b}).

structure LocusModel (A : Type*) [Fintype A] where
  /-- Allele frequencies. -/
  p : A → ℝ
  p_nonneg : ∀ a, 0 ≤ p a
  sum_p : ∑ a, p a = 1
  /-- Genotypic values. -/
  g : A → A → ℝ
  g_symm : ∀ a b, g a b = g b a

Used by 17

Used byFisher's average effect of an allele at a single locus · Dominance deviation at a single locus · One-locus phantom heritability, unconditional · Population mean genotypic value at a single locus · Covariance between relatives · Single-locus covariance between relatives in Cockerham form · Mean product of genotypic values of two relatives · Average effects are centred · Dominance deviations are orthogonal to every allele · Single-locus model as Cockerham components · Additive variance at a single locus · Nonnegativity of the single-locus additive variance · Dominance variance at a single locus · The additive fit is least squares · Nonnegativity of the single-locus dominance variance · Genetic variance at a single locus · Fisher decomposition

Locus Model

DefinitionPopulation mean genotypic value at a single locus#✓fully proved

The population mean genotypic value μ = ∑ p_a p_b g(a, b).

def mean : ℝ := ∑ a, ∑ b, m.p a * m.p b * m.g a b

Uses 1 · Used by 6

Statement usesSingle-locus model under random union of gametes

Used byFisher's average effect of an allele at a single locus · Dominance deviation at a single locus · One-locus phantom heritability, unconditional · Covariance between relatives · Single-locus covariance between relatives in Cockerham form · Genetic variance at a single locus

DefinitionFisher's average effect of an allele at a single locus#✓fully proved

Fisher's average effect of allele a: α a = ∑_b p_b g(a, b) - μ.

def alpha (a : A) : ℝ := ∑ b, m.p b * m.g a b - m.mean

Uses 2 · Used by 5

Statement usesSingle-locus model under random union of gametes · Population mean genotypic value at a single locus

Used byDominance deviation at a single locus · Covariance between relatives · Average effects are centred · Additive variance at a single locus · Nonnegativity of the single-locus additive variance

DefinitionDominance deviation at a single locus#✓fully proved

The dominance deviation δ a b = g(a, b) - μ - α a - α b.

def delta (a b : A) : ℝ := m.g a b - m.mean - m.alpha a - m.alpha b

Uses 3 · Used by 3

Statement usesSingle-locus model under random union of gametes · Fisher's average effect of an allele at a single locus · Population mean genotypic value at a single locus

Used byDominance deviations are orthogonal to every allele · Dominance variance at a single locus · Nonnegativity of the single-locus dominance variance

DefinitionGenetic variance at a single locus#✓fully proved

The genetic variance V_G = ∑ p_a p_b (g(a, b) - μ)².

def varG : ℝ := ∑ a, ∑ b, m.p a * m.p b * (m.g a b - m.mean) ^ 2

Uses 2 · Used by 2

Statement usesSingle-locus model under random union of gametes · Population mean genotypic value at a single locus

Used byCovariance between relatives · Fisher decomposition

DefinitionAdditive variance at a single locus#✓fully proved

The additive variance V_A = 2 ∑ p_a α_a².

def varA : ℝ := 2 * ∑ a, m.p a * m.alpha a ^ 2

Uses 2 · Used by 6

Statement usesSingle-locus model under random union of gametes · Fisher's average effect of an allele at a single locus

Used byOne-locus phantom heritability, unconditional · Covariance between relatives · Single-locus covariance between relatives in Cockerham form · Single-locus model as Cockerham components · Nonnegativity of the single-locus additive variance · Fisher decomposition

DefinitionDominance variance at a single locus#✓fully proved

The dominance variance V_D = ∑ p_a p_b δ_{ab}².

def varD : ℝ := ∑ a, ∑ b, m.p a * m.p b * m.delta a b ^ 2

Uses 2 · Used by 7

Statement usesSingle-locus model under random union of gametes · Dominance deviation at a single locus

Used byOne-locus phantom heritability, unconditional · Covariance between relatives · Single-locus covariance between relatives in Cockerham form · Single-locus model as Cockerham components · The additive fit is least squares · Nonnegativity of the single-locus dominance variance · Fisher decomposition

TheoremAverage effects are centred#✓fully proved

Average effects are centred: ∑ p_a α_a = 0.

theorem sum_p_alpha : ∑ a, m.p a * m.alpha a = 0

Uses 3 · Used by 1

Statement usesSingle-locus model under random union of gametes · Fisher's average effect of an allele at a single locus

Proof usesAverage effects have mean zero

Used byCovariance between relatives

TheoremDominance deviations are orthogonal to every allele#✓fully proved

Dominance deviations are orthogonal to every allele: ∑_b p_b δ_{ab} = 0.

theorem sum_p_delta (a : A) : ∑ b, m.p b * m.delta a b = 0

Uses 3

Statement usesSingle-locus model under random union of gametes · Dominance deviation at a single locus

Proof usesOrthogonality of dominance deviations in the second allele

TheoremFisher decomposition#✓fully proved

Fisher decomposition of the genetic variance: V_G = V_A + V_D.

theorem varG_eq : m.varG = m.varA + m.varD

Uses 5 · Used by 1

Statement usesSingle-locus model under random union of gametes · Additive variance at a single locus · Dominance variance at a single locus · Genetic variance at a single locus

Proof usesFisher's variance decomposition

Used byCovariance between relatives

TheoremNonnegativity of the single-locus additive variance#✓fully proved

The additive variance is nonnegative.

theorem varA_nonneg : 0 ≤ m.varA

Uses 3 · Used by 2

Statement usesSingle-locus model under random union of gametes · Additive variance at a single locus

Proof usesFisher's average effect of an allele at a single locus

Used bySingle-locus covariance between relatives in Cockerham form · Single-locus model as Cockerham components

TheoremNonnegativity of the single-locus dominance variance#✓fully proved

The dominance variance is nonnegative.

theorem varD_nonneg : 0 ≤ m.varD

Uses 3 · Used by 2

Statement usesSingle-locus model under random union of gametes · Dominance variance at a single locus

Proof usesDominance deviation at a single locus

Used bySingle-locus covariance between relatives in Cockerham form · Single-locus model as Cockerham components

TheoremThe additive fit is least squares#✓fully proved

The additive fit is least squares (Fisher definition of average effects): every additive fit c + h a + h b has mean squared error at least V_D, the error of μ + α a + α b.

theorem varD_le (c : ℝ) (h : A → ℝ) :
    m.varD ≤ ∑ a, ∑ b, m.p a * m.p b * (m.g a b - c - h a - h b) ^ 2

Uses 3

Statement usesSingle-locus model under random union of gametes · Dominance variance at a single locus

Proof usesLeast squares (Fisher 1918)

DefinitionMean product of genotypic values of two relatives#✓fully proved

The mean product of genotypic values of two non-inbred relatives that share 0, 1, 2 alleles identical by descent with probabilities k₀, k₁, k₂: given the IBD state, the non-shared alleles are independent draws from p.

def relProd (k₀ k₁ k₂ : ℝ) : ℝ :=
  k₀ * (∑ a, ∑ b, ∑ c, ∑ d, m.p a * m.p b * m.p c * m.p d * (m.g a b * m.g c d)) +
  k₁ * (∑ a, ∑ b, ∑ c, m.p a * m.p b * m.p c * (m.g a b * m.g a c)) +
  k₂ * (∑ a, ∑ b, m.p a * m.p b * (m.g a b * m.g a b))

Uses 1 · Used by 3

Statement usesSingle-locus model under random union of gametes

Used byOne-locus phantom heritability, unconditional · Covariance between relatives · Single-locus covariance between relatives in Cockerham form

TheoremCovariance between relatives#✓fully proved

Covariance between relatives at one locus (Fisher 1918; in the IBD form of Falconer and Mackay ch. 9): for IBD probabilities summing to one, E[G_X G_Y] - μ² = (k₁ / 2 + k₂) V_A + k₂ V_D, i.e. 2φ V_A + Δ V_D with kinship φ = k₁ / 4 + k₂ / 2 and Δ = k₂.

theorem relCov_eq {k₀ k₁ k₂ : ℝ} (hk : k₀ + k₁ + k₂ = 1) :
    m.relProd k₀ k₁ k₂ - m.mean ^ 2 = (k₁ / 2 + k₂) * m.varA + k₂ * m.varD

Uses 9 · Used by 2

Statement usesSingle-locus model under random union of gametes · Population mean genotypic value at a single locus · Mean product of genotypic values of two relatives · Additive variance at a single locus · Dominance variance at a single locus

Proof usesFisher's average effect of an allele at a single locus · Average effects are centred · Genetic variance at a single locus · Fisher decomposition

Used byOne-locus phantom heritability, unconditional · Single-locus covariance between relatives in Cockerham form

Covariance Relatives

StructureCockerham–Kempthorne variance components#✓fully proved

Cockerham–Kempthorne variance components up to order n: V i j = V_{A^i D^j} is the component of i additive and j dominance factors (V 1 0 = V_A, V 0 1 = V_D, V 2 0 = V_AA, …). They are nonnegative, there is no (0, 0) component, and the genetic covariance of relatives with 2φ and Δ is ∑_{i, j ≤ n} (2φ)^i Δ^j V i j. This structure is the stated representation; it is proved for one locus by LocusModel.relCov_eq.

structure CockerhamComponents where
  /-- Highest order kept. -/
  n : ℕ
  /-- The components `V_{A^i D^j}`. -/
  V : ℕ → ℕ → ℝ
  V_nonneg : ∀ i j, 0 ≤ V i j
  V_zero_zero : V 0 0 = 0
  /-- Finite support: components above order `n` vanish. `V` is total only as a function;
  there are no unconstrained ignored components outside the summation range of `cov`, which
  sums exactly over `i, j ≤ n`. -/
  V_supported : ∀ i j, n < i ∨ n < j → V i j = 0

Used by 9

Used byGenetic covariance of relatives in Cockerham form · Falconer's estimator · Falconer's estimator in terms of Cockerham components · Equality case of the phantom heritability inequality · Phantom heritability · Single-locus covariance between relatives in Cockerham form · Single-locus model as Cockerham components · Additive variance of the Cockerham components · Phantom heritability inequality

Cockerham Components

DefinitionGenetic covariance of relatives in Cockerham form#✓fully proved

The genetic covariance of relatives with coefficients 2φ = twoPhi and Δ = Δ.

def cov (twoPhi Δ : ℝ) : ℝ :=
  ∑ i ∈ range (c.n + 1), ∑ j ∈ range (c.n + 1), twoPhi ^ i * Δ ^ j * c.V i j

Uses 1 · Used by 4

Statement usesCockerham–Kempthorne variance components

Used byFalconer's estimator · Falconer's estimator in terms of Cockerham components · Phantom heritability · Single-locus covariance between relatives in Cockerham form

DefinitionAdditive variance of the Cockerham components#✓fully proved

The additive variance V_A = V 1 0 (zero if n = 0).

def varA : ℝ := if 1 ≤ c.n then c.V 1 0 else 0

Uses 1 · Used by 4

Statement usesCockerham–Kempthorne variance components

Used byFalconer's estimator in terms of Cockerham components · Equality case of the phantom heritability inequality · Phantom heritability · Phantom heritability inequality

DefinitionFalconer's estimator#✓fully proved

Falconer's estimator under the ACE model, in covariance form: monozygotic twins have 2φ = Δ = 1, dizygotic twins (full sibs) 2φ = 1/2, Δ = 1/4, and both share the same common-environment covariance C; the estimator is 2 (Cov_MZ - Cov_DZ).

noncomputable def falconer (C : ℝ) : ℝ := 2 * ((c.cov 1 1 + C) - (c.cov (1 / 2) (1 / 4) + C))

Uses 2 · Used by 4

Statement usesCockerham–Kempthorne variance components · Genetic covariance of relatives in Cockerham form

Used byFalconer's estimator in terms of Cockerham components · Equality case of the phantom heritability inequality · Phantom heritability · Phantom heritability inequality

TheoremFalconer's estimator in terms of Cockerham components#✓fully proved

Falconer's estimator is V_A plus the non-additive components weighted by 2 (1 - 2^{-i} 4^{-j}) (derived from Cockerham's coefficients).

theorem falconer_eq (C : ℝ) :
    c.falconer C = c.varA + ∑ i ∈ range (c.n + 1), ∑ j ∈ range (c.n + 1),
      (if (i, j) = (1, 0) then 0 else 2 * (1 - (1 / 2) ^ i * (1 / 4) ^ j) * c.V i j)

Uses 4 · Used by 2

Statement usesCockerham–Kempthorne variance components · Falconer's estimator · Additive variance of the Cockerham components

Proof usesGenetic covariance of relatives in Cockerham form

Used byEquality case of the phantom heritability inequality · Phantom heritability inequality

TheoremPhantom heritability inequality#✓fully proved

The phantom-heritability inequality in covariance form: V_A ≤ 2 (Cov_MZ - Cov_DZ).

theorem varA_le_falconer (C : ℝ) : c.varA ≤ c.falconer C

Uses 4 · Used by 1

Statement usesCockerham–Kempthorne variance components · Falconer's estimator · Additive variance of the Cockerham components

Proof usesFalconer's estimator in terms of Cockerham components

Used byPhantom heritability

TheoremEquality case of the phantom heritability inequality#✓fully proved

Equality holds iff every non-additive component of order ≤ n vanishes.

theorem falconer_eq_varA_iff (C : ℝ) :
    c.falconer C = c.varA ↔
      ∀ i ∈ range (c.n + 1), ∀ j ∈ range (c.n + 1), (i, j) ≠ (1, 0) → c.V i j = 0

Uses 4

Statement usesCockerham–Kempthorne variance components · Falconer's estimator · Additive variance of the Cockerham components

Proof usesFalconer's estimator in terms of Cockerham components

TheoremPhantom heritability#✓fully proved

Phantom heritability on the correlation scale (Zuk et al. 2012): with phenotypic variance V_P > 0, the narrow-sense heritability V_A / V_P is at most the ACE estimate 2 (r_MZ - r_DZ), where r = Cov / V_P.

theorem narrow_le_falconerHeritability (C : ℝ) {VP : ℝ} (hVP : 0 < VP) :
    c.varA / VP ≤ 2 * ((c.cov 1 1 + C) / VP - (c.cov (1 / 2) (1 / 4) + C) / VP)

Uses 5

Statement usesCockerham–Kempthorne variance components · Genetic covariance of relatives in Cockerham form · Additive variance of the Cockerham components

Proof usesFalconer's estimator · Phantom heritability inequality

Locus Model

DefinitionSingle-locus model as Cockerham components#✓fully proved

The one-locus model as Cockerham components of order 1: V 1 0 = V_A, V 0 1 = V_D, V 1 1 = 0.

MathlibExt.Biology.StatisticalGenetics.CovarianceRelatives.LocusModel.toComponents · 15 lines

def toComponents : CockerhamComponents where
  n := 1
  V i j := if (i, j) = (1, 0) then m.varA else if (i, j) = (0, 1) then m.varD else 0
  V_nonneg i j := by
    split_ifs
    · exact m.varA_nonneg
    · exact m.varD_nonneg
    · exact le_refl 0
  V_zero_zero := by simp
  V_supported i j h := by
    rcases h with hi | hj <;> split_ifs with h1 h2 <;>
      (first
        | (obtain ⟨rfl, rfl⟩ := Prod.mk.inj h1; omega)
        | (obtain ⟨rfl, rfl⟩ := Prod.mk.inj h2; omega)
        | rfl)

Uses 6 · Used by 1

Statement usesCockerham–Kempthorne variance components · Single-locus model under random union of gametes · Additive variance at a single locus · Nonnegativity of the single-locus additive variance · Dominance variance at a single locus · Nonnegativity of the single-locus dominance variance

Used bySingle-locus covariance between relatives in Cockerham form

TheoremSingle-locus covariance between relatives in Cockerham form#✓fully proved

The one-locus covariance between relatives is the Cockerham form of toComponents.

theorem relCov_eq_cov {k₀ k₁ k₂ : ℝ} (hk : k₀ + k₁ + k₂ = 1) :
    m.relProd k₀ k₁ k₂ - m.mean ^ 2 = m.toComponents.cov (k₁ / 2 + k₂) k₂

Uses 11

Statement usesGenetic covariance of relatives in Cockerham form · Single-locus model under random union of gametes · Population mean genotypic value at a single locus · Mean product of genotypic values of two relatives · Single-locus model as Cockerham components

Proof usesCockerham–Kempthorne variance components · Covariance between relatives · Additive variance at a single locus · Nonnegativity of the single-locus additive variance · Dominance variance at a single locus · Nonnegativity of the single-locus dominance variance

TheoremOne-locus phantom heritability, unconditional#✓fully proved

With monozygotic twins (k₂ = 1), dizygotic twins (k = (1/4, 1/2, 1/4)) and a common environment C, 2 (Cov_MZ - Cov_DZ) = V_A + (3/2) V_D.

theorem falconer_eq_of_locus (C : ℝ) :
    2 * ((m.relProd 0 0 1 - m.mean ^ 2 + C) - (m.relProd (1 / 4) (1 / 2) (1 / 4) -
      m.mean ^ 2 + C)) = m.varA + 3 / 2 * m.varD

Uses 6

Statement usesSingle-locus model under random union of gametes · Population mean genotypic value at a single locus · Mean product of genotypic values of two relatives · Additive variance at a single locus · Dominance variance at a single locus

Proof usesCovariance between relatives

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.