Genomic relationship matrices
Relatedness
StructureMalécot's identity-by-descent model#✓fully proved
Malécot's identity-by-descent model at one biallelic locus, at the level of second
moments. The individuals are ι; individual i carries the gene copies (i, 0) (paternal) and
(i, 1) (maternal), and allele c ∈ {0, 1} indicates the reference allele on copy c. The
reference allele has frequency p ∈ (0, 1) (a polymorphic locus), and ibd c d is the
probability that the copies c and d are identical by descent: IBD copies carry the same
allele and non-IBD copies are independent draws with frequency p (Malécot 1948), which gives
the second moments 𝔼[a_c a_d] = p² + p (1 - p) ibd c d. Only these first and second moments
are assumed. ibd is determined by the moments (p (1 - p) ≠ 0), and ibd c c = 1
(IBDModel.ibd_self). In Malécot's model ibd c d ∈ [0, 1]; the structure does not require
this, and the identities below hold for any real ibd (for example a correlation relative to a
reference population, which can be negative). A monomorphic locus (p ∈ {0, 1}) is excluded:
there the GRM denominator 2p(1 - p) vanishes.
MathlibExt.Biology.StatisticalGenetics.Relatedness.IBDModel · 19 lines
structure IBDModel (μ : Measure Ω) (ι : Type*) where
/-- The reference-allele frequency. -/
p : ℝ
/-- The locus is polymorphic: `0 < p`. -/
p_pos : 0 < p
/-- The locus is polymorphic: `p < 1`. -/
p_lt_one : p < 1
/-- The reference-allele indicator of each gene copy. -/
allele : ι × Fin 2 → Ω → ℝ
/-- The allele indicators are random variables. -/
measurable_allele : ∀ c, Measurable (allele c)
/-- The allele indicators take the values `0` and `1`. -/
allele_mem : ∀ c ω, allele c ω = 0 ∨ allele c ω = 1
/-- The probability that two gene copies are identical by descent. -/
ibd : ι × Fin 2 → ι × Fin 2 → ℝ
/-- Every copy carries the reference allele with probability `p`. -/
integral_allele : ∀ c, ∫ ω, allele c ω ∂μ = p
/-- Malécot's second moments: `𝔼[a_c a_d] = p² + p (1 - p) ibd c d`. -/
integral_allele_mul : ∀ c d, ∫ ω, allele c ω * allele d ω ∂μ = p ^ 2 + p * (1 - p) * ibd c d p : ℝMathlibExt/Biology/StatisticalGenetics/Relatedness.lean:79
allele : ι × Fin 2 → Ω → ℝMathlibExt/Biology/StatisticalGenetics/Relatedness.lean:85
ibd : ι × Fin 2 → ι × Fin 2 → ℝMathlibExt/Biology/StatisticalGenetics/Relatedness.lean:91
Used by 21
1 + F_i · Diagonal GRM entry is unbiased for \(1 + F_i\) · The KING moment · The KING moment · Kinship coefficient · Symmetry of kinship · Self-kinship equals \((1 + F_i)/2\)Identity by descent
DefinitionGenotype of an individual at a biallelic locus#✓fully proved
The genotype (reference-allele count) x_i ∈ {0, 1, 2} of individual i.
def genotype (i : ι) (ω : Ω) : ℝ := D.allele (i, 0) ω + D.allele (i, 1) ωUses 1 · Used by 11
1 + F_i · The KING moment · The KING momentDefinitionKinship coefficient#✓fully proved
The kinship coefficient φ_ij: the probability that a copy drawn at random from i and a
copy drawn at random from j are identical by descent.
Uses 1 · Used by 9
1 + F_i · Diagonal GRM entry is unbiased for \(1 + F_i\) · The KING moment · The KING moment · Symmetry of kinship · Self-kinship equals \((1 + F_i)/2\)DefinitionInbreeding coefficient#✓fully proved
The inbreeding coefficient F_i: the probability that the two copies of i are identical
by descent.
def inbreeding (i : ι) : ℝ := D.ibd (i, 0) (i, 1)Uses 1 · Used by 5
DefinitionGenetic relationship matrix entry#✓fully proved
The genetic relationship matrix entry of Yang et al. (2010) at one locus,
A_ij = (x_i - 2p)(x_j - 2p) / (2p(1 - p)).
noncomputable def grm (i j : ι) (ω : Ω) : ℝ :=
(D.genotype i ω - 2 * D.p) * (D.genotype j ω - 2 * D.p) / (2 * D.p * (1 - D.p))Uses 2 · Used by 2
DefinitionGCTA diagonal relationship estimator#✓fully proved
The diagonal estimator of GCTA (Yang et al. 2011) at one locus,
A_ii = 1 + (x_i² - (1 + 2p) x_i + 2p²) / (2p(1 - p)).
noncomputable def grmDiag (i : ι) (ω : Ω) : ℝ :=
1 + (D.genotype i ω ^ 2 - (1 + 2 * D.p) * D.genotype i ω + 2 * D.p ^ 2) /
(2 * D.p * (1 - D.p))Uses 2 · Used by 1
TheoremIntegrability of allele indicators#✓fully proved
The allele indicators are integrable.
theorem integrable_allele (c : ι × Fin 2) : Integrable (D.allele c) μUses 1 · Used by 3
TheoremIntegrability of products of allele indicators#✓fully proved
Products of allele indicators are integrable.
theorem integrable_allele_mul (c d : ι × Fin 2) :
Integrable (fun ω => D.allele c ω * D.allele d ω) μUses 2 · Used by 2
TheoremA gene copy is identical by descent with itself#✓fully proved
A gene copy is identical by descent with itself: ibd c c = 1.
theorem ibd_self (c : ι × Fin 2) : D.ibd c c = 1Uses 1 · Used by 1
TheoremSymmetry of identity by descent#✓fully proved
Identity by descent is symmetric.
theorem ibd_comm (c d : ι × Fin 2) : D.ibd c d = D.ibd d cUses 1 · Used by 2
TheoremSelf-kinship equals \((1 + F_i)/2\)#✓fully proved
φ_ii = (1 + F_i) / 2.
theorem kinship_self (i : ι) : D.kinship i i = (1 + D.inbreeding i) / 2Uses 5 · Used by 3
TheoremSymmetry of kinship#✓fully proved
Kinship is symmetric.
theorem kinship_comm (i j : ι) : D.kinship i j = D.kinship j iUses 3
TheoremIntegrability of genotypes#✓fully proved
Genotypes are integrable.
theorem integrable_genotype (i : ι) : Integrable (D.genotype i) μUses 3 · Used by 2
TheoremIntegrability of products of genotypes#✓fully proved
Products of genotypes are integrable.
theorem integrable_genotype_mul (i j : ι) :
Integrable (fun ω => D.genotype i ω * D.genotype j ω) μUses 3 · Used by 3
TheoremExpected genotype equals \(2p\)#✓fully proved
𝔼[x_i] = 2p.
theorem integral_genotype (i : ι) : ∫ ω, D.genotype i ω ∂μ = 2 * D.pUses 3 · Used by 2
TheoremSecond moment of genotypes in terms of kinship#✓fully proved
𝔼[x_i x_j] = 4p² + 4p(1 - p) φ_ij.
theorem integral_genotype_mul (i j : ι) :
∫ ω, D.genotype i ω * D.genotype j ω ∂μ =
4 * D.p ^ 2 + 4 * D.p * (1 - D.p) * D.kinship i jUses 4 · Used by 3
TheoremThe genetic relationship covariance#✓fully proved
The genetic relationship covariance (Yang et al. 2010):
𝔼[(x_i - 2p)(x_j - 2p)] = 2p(1 - p) · 2 φ_ij.
theorem integral_centered_mul (i j : ι) :
∫ ω, (D.genotype i ω - 2 * D.p) * (D.genotype j ω - 2 * D.p) ∂μ =
2 * D.p * (1 - D.p) * (2 * D.kinship i j)Uses 7 · Used by 1
TheoremThe GRM is unbiased for twice the kinship#✓fully proved
The GRM is unbiased for twice the kinship (Yang et al. 2010):
𝔼[A_ij] = 2 φ_ij, for every pair i, j (including i = j, where 2 φ_ii = 1 + F_i).
theorem integral_grm (i j : ι) : ∫ ω, D.grm i j ω ∂μ = 2 * D.kinship i jUses 5 · Used by 1
TheoremDiagonal GRM entry is unbiased for \(1 + F_i\)#✓fully proved
The diagonal GRM entry is unbiased for 1 + F_i: 𝔼[A_ii] = 1 + F_i.
theorem integral_grm_self (i : ι) : ∫ ω, D.grm i i ω ∂μ = 1 + D.inbreeding iTheoremThe KING moment#✓fully proved
The KING moment (Manichaikul et al. 2010), general form:
𝔼[(x_i - x_j)²] = 2p(1 - p)(1 + F_i) + 2p(1 - p)(1 + F_j) - 8p(1 - p) φ_ij.
theorem integral_sub_sq (i j : ι) :
∫ ω, (D.genotype i ω - D.genotype j ω) ^ 2 ∂μ =
2 * D.p * (1 - D.p) * (1 + D.inbreeding i) + 2 * D.p * (1 - D.p) * (1 + D.inbreeding j) -
8 * D.p * (1 - D.p) * D.kinship i jUses 7 · Used by 1
TheoremThe KING moment#✓fully proved
The KING moment (Manichaikul et al. 2010) for two non-inbred individuals:
𝔼[(x_i - x_j)²] = 4p(1 - p)(1 - 2φ_ij).
theorem integral_sub_sq_of_inbreeding_eq_zero {i j : ι} (hi : D.inbreeding i = 0)
(hj : D.inbreeding j = 0) :
∫ ω, (D.genotype i ω - D.genotype j ω) ^ 2 ∂μ =
4 * D.p * (1 - D.p) * (1 - 2 * D.kinship i j)Uses 5
TheoremThe GCTA diagonal estimator is unbiased for 1 + F_i#✓fully proved
The GCTA diagonal estimator is unbiased for 1 + F_i (Yang et al. 2011):
𝔼[1 + (x_i² - (1 + 2p) x_i + 2p²) / (2p(1 - p))] = 1 + F_i.
theorem integral_grmDiag (i : ι) : ∫ ω, D.grmDiag i ω ∂μ = 1 + D.inbreeding iUses 10
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.