Dominance linkage disequilibrium

21 fully proved

Dominance LD

StructureTwo-locus diploid genotype under random union of gametes#✓fully proved

A diploid two-locus genotype under random union of gametes: the haplotypes (X₁, Y₁) and (X₂, Y₂) are independent and identically distributed, with square-integrable allele codings.

MathlibExt.Biology.StatisticalGenetics.DominanceLD.RandomUnion · 17 lines

structure RandomUnion (P : Measure Ω) where
  /-- The allele coding of haplotype 1 at locus `A`. -/
  x1 : Ω → ℝ
  /-- The allele coding of haplotype 1 at locus `B`. -/
  y1 : Ω → ℝ
  /-- The allele coding of haplotype 2 at locus `A`. -/
  x2 : Ω → ℝ
  /-- The allele coding of haplotype 2 at locus `B`. -/
  y2 : Ω → ℝ
  memLp_x1 : MemLp x1 2 P
  memLp_y1 : MemLp y1 2 P
  memLp_x2 : MemLp x2 2 P
  memLp_y2 : MemLp y2 2 P
  /-- The two haplotypes are independent. -/
  indep : IndepFun (fun ω => (x1 ω, y1 ω)) (fun ω => (x2 ω, y2 ω)) P
  /-- The two haplotypes are identically distributed. -/
  ident : IdentDistrib (fun ω => (x1 ω, y1 ω)) (fun ω => (x2 ω, y2 ω)) P P

Used by 18

Used byAdditive coding at the first locus · Additive coding at the second locus · Correlation of additive codings equals the gametic correlation · Dominance coding at the first locus · Dominance coding at the second locus · Dominance LD is the square of additive LD · Allele frequency at the first locus · Allele frequency at the second locus · Additive linkage disequilibrium is twice the gametic one · Additive and dominance codings at different loci are uncorrelated · Second moment of the additive coding at the first locus · Second moment of the additive coding at the second locus · Dominance linkage disequilibrium is the square of the gametic one · Second moment of the dominance coding at the first locus · Second moment of the dominance coding at the second locus · Gametic linkage disequilibrium · Haplotype variance at the first locus · Haplotype variance at the second locus

Random Union

DefinitionAllele frequency at the first locus#✓fully proved

The allele frequency (mean coding) p = E X₁ at locus A.

noncomputable def freqA : ℝ := ∫ ω, G.x1 ω ∂P

Uses 1 · Used by 10

Statement usesTwo-locus diploid genotype under random union of gametes

Used byAdditive coding at the first locus · Dominance coding at the first locus · Dominance LD is the square of additive LD · Additive linkage disequilibrium is twice the gametic one · Additive and dominance codings at different loci are uncorrelated · Second moment of the additive coding at the first locus · Dominance linkage disequilibrium is the square of the gametic one · Second moment of the dominance coding at the first locus · Gametic linkage disequilibrium · Haplotype variance at the first locus

DefinitionAllele frequency at the second locus#✓fully proved

The allele frequency (mean coding) q = E Y₁ at locus B.

noncomputable def freqB : ℝ := ∫ ω, G.y1 ω ∂P

Uses 1 · Used by 10

Statement usesTwo-locus diploid genotype under random union of gametes

Used byAdditive coding at the second locus · Dominance coding at the second locus · Dominance LD is the square of additive LD · Additive linkage disequilibrium is twice the gametic one · Additive and dominance codings at different loci are uncorrelated · Second moment of the additive coding at the second locus · Dominance linkage disequilibrium is the square of the gametic one · Second moment of the dominance coding at the second locus · Gametic linkage disequilibrium · Haplotype variance at the second locus

DefinitionHaplotype variance at the first locus#✓fully proved

The haplotype variance V_A = E (X₁ - p)² at locus A.

noncomputable def varA : ℝ := ∫ ω, (G.x1 ω - G.freqA) ^ 2 ∂P

Uses 2 · Used by 4

Statement usesTwo-locus diploid genotype under random union of gametes · Allele frequency at the first locus

Used byCorrelation of additive codings equals the gametic correlation · Dominance LD is the square of additive LD · Second moment of the additive coding at the first locus · Second moment of the dominance coding at the first locus

DefinitionHaplotype variance at the second locus#✓fully proved

The haplotype variance V_B = E (Y₁ - q)² at locus B.

noncomputable def varB : ℝ := ∫ ω, (G.y1 ω - G.freqB) ^ 2 ∂P

Uses 2 · Used by 4

Statement usesTwo-locus diploid genotype under random union of gametes · Allele frequency at the second locus

Used byCorrelation of additive codings equals the gametic correlation · Dominance LD is the square of additive LD · Second moment of the additive coding at the second locus · Second moment of the dominance coding at the second locus

DefinitionGametic linkage disequilibrium#✓fully proved

The gametic linkage disequilibrium D = E (X₁ - p) (Y₁ - q).

noncomputable def ldD : ℝ := ∫ ω, (G.x1 ω - G.freqA) * (G.y1 ω - G.freqB) ∂P

Uses 3 · Used by 4

Statement usesTwo-locus diploid genotype under random union of gametes · Allele frequency at the first locus · Allele frequency at the second locus

Used byCorrelation of additive codings equals the gametic correlation · Dominance LD is the square of additive LD · Additive linkage disequilibrium is twice the gametic one · Dominance linkage disequilibrium is the square of the gametic one

DefinitionAdditive coding at the first locus#✓fully proved

The additive coding a_A = (X₁ - p) + (X₂ - p) (centred allele count) at locus A.

noncomputable def addA (ω : Ω) : ℝ := (G.x1 ω - G.freqA) + (G.x2 ω - G.freqA)

Uses 2 · Used by 5

Statement usesTwo-locus diploid genotype under random union of gametes · Allele frequency at the first locus

Used byCorrelation of additive codings equals the gametic correlation · Dominance LD is the square of additive LD · Additive linkage disequilibrium is twice the gametic one · Additive and dominance codings at different loci are uncorrelated · Second moment of the additive coding at the first locus

DefinitionAdditive coding at the second locus#✓fully proved

The additive coding a_B = (Y₁ - q) + (Y₂ - q) at locus B.

noncomputable def addB (ω : Ω) : ℝ := (G.y1 ω - G.freqB) + (G.y2 ω - G.freqB)

Uses 2 · Used by 4

Statement usesTwo-locus diploid genotype under random union of gametes · Allele frequency at the second locus

Used byCorrelation of additive codings equals the gametic correlation · Dominance LD is the square of additive LD · Additive linkage disequilibrium is twice the gametic one · Second moment of the additive coding at the second locus

DefinitionDominance coding at the first locus#✓fully proved

The dominance coding d_A = (X₁ - p) (X₂ - p) at locus A.

noncomputable def domA (ω : Ω) : ℝ := (G.x1 ω - G.freqA) * (G.x2 ω - G.freqA)

Uses 2 · Used by 3

Statement usesTwo-locus diploid genotype under random union of gametes · Allele frequency at the first locus

Used byDominance LD is the square of additive LD · Dominance linkage disequilibrium is the square of the gametic one · Second moment of the dominance coding at the first locus

DefinitionDominance coding at the second locus#✓fully proved

The dominance coding d_B = (Y₁ - q) (Y₂ - q) at locus B.

noncomputable def domB (ω : Ω) : ℝ := (G.y1 ω - G.freqB) * (G.y2 ω - G.freqB)

Uses 2 · Used by 4

Statement usesTwo-locus diploid genotype under random union of gametes · Allele frequency at the second locus

Used byDominance LD is the square of additive LD · Additive and dominance codings at different loci are uncorrelated · Dominance linkage disequilibrium is the square of the gametic one · Second moment of the dominance coding at the second locus

TheoremAdditive linkage disequilibrium is twice the gametic one#✓fully proved

Additive LD: E(a_A a_B) = 2 D.

theorem integral_addA_mul_addB : ∫ ω, G.addA ω * G.addB ω ∂P = 2 * G.ldD

Uses 6 · Used by 1

Statement usesTwo-locus diploid genotype under random union of gametes · Additive coding at the first locus · Additive coding at the second locus · Gametic linkage disequilibrium

Proof usesAllele frequency at the first locus · Allele frequency at the second locus

Used byCorrelation of additive codings equals the gametic correlation

TheoremSecond moment of the additive coding at the first locus#✓fully proved

The additive coding has second moment E(a_A²) = 2 V_A.

theorem integral_addA_sq : ∫ ω, G.addA ω ^ 2 ∂P = 2 * G.varA

Uses 4 · Used by 1

Statement usesTwo-locus diploid genotype under random union of gametes · Additive coding at the first locus · Haplotype variance at the first locus

Proof usesAllele frequency at the first locus

Used byCorrelation of additive codings equals the gametic correlation

TheoremSecond moment of the additive coding at the second locus#✓fully proved

The additive coding has second moment E(a_B²) = 2 V_B.

theorem integral_addB_sq : ∫ ω, G.addB ω ^ 2 ∂P = 2 * G.varB

Uses 4 · Used by 1

Statement usesTwo-locus diploid genotype under random union of gametes · Additive coding at the second locus · Haplotype variance at the second locus

Proof usesAllele frequency at the second locus

Used byCorrelation of additive codings equals the gametic correlation

TheoremDominance linkage disequilibrium is the square of the gametic one#✓fully proved

Dominance LD: E(d_A d_B) = D².

theorem integral_domA_mul_domB : ∫ ω, G.domA ω * G.domB ω ∂P = G.ldD ^ 2

Uses 6 · Used by 1

Statement usesTwo-locus diploid genotype under random union of gametes · Dominance coding at the first locus · Dominance coding at the second locus · Gametic linkage disequilibrium

Proof usesAllele frequency at the first locus · Allele frequency at the second locus

Used byDominance LD is the square of additive LD

TheoremSecond moment of the dominance coding at the first locus#✓fully proved

The dominance coding has second moment E(d_A²) = V_A².

theorem integral_domA_sq : ∫ ω, G.domA ω ^ 2 ∂P = G.varA ^ 2

Uses 4 · Used by 1

Statement usesTwo-locus diploid genotype under random union of gametes · Dominance coding at the first locus · Haplotype variance at the first locus

Proof usesAllele frequency at the first locus

Used byDominance LD is the square of additive LD

TheoremSecond moment of the dominance coding at the second locus#✓fully proved

The dominance coding has second moment E(d_B²) = V_B².

theorem integral_domB_sq : ∫ ω, G.domB ω ^ 2 ∂P = G.varB ^ 2

Uses 4 · Used by 1

Statement usesTwo-locus diploid genotype under random union of gametes · Dominance coding at the second locus · Haplotype variance at the second locus

Proof usesAllele frequency at the second locus

Used byDominance LD is the square of additive LD

TheoremAdditive and dominance codings at different loci are uncorrelated#✓fully proved

The additive coding at A and the dominance coding at B are uncorrelated: E(a_A d_B) = 0.

theorem integral_addA_mul_domB : ∫ ω, G.addA ω * G.domB ω ∂P = 0

Uses 5

Statement usesTwo-locus diploid genotype under random union of gametes · Additive coding at the first locus · Dominance coding at the second locus

Proof usesAllele frequency at the first locus · Allele frequency at the second locus

TheoremCorrelation of additive codings equals the gametic correlation#✓fully proved

The correlation of the additive codings is the gametic correlation r = D / √(V_A V_B).

theorem addCorr_eq :
    (∫ ω, G.addA ω * G.addB ω ∂P) /
        Real.sqrt ((∫ ω, G.addA ω ^ 2 ∂P) * ∫ ω, G.addB ω ^ 2 ∂P) =
      G.ldD / Real.sqrt (G.varA * G.varB)

Uses 9 · Used by 1

Statement usesTwo-locus diploid genotype under random union of gametes · Additive coding at the first locus · Additive coding at the second locus · Gametic linkage disequilibrium · Haplotype variance at the first locus · Haplotype variance at the second locus

Proof usesAdditive linkage disequilibrium is twice the gametic one · Second moment of the additive coding at the first locus · Second moment of the additive coding at the second locus

Used byDominance LD is the square of additive LD

TheoremDominance LD is the square of additive LD#✓fully proved

Dominance LD is the square of additive LD (Palmer et al. 2023, graphical abstract): the correlation of the dominance codings at two loci is the square of the correlation of their additive codings.

theorem domCorr_eq_addCorr_sq :
    (∫ ω, G.domA ω * G.domB ω ∂P) /
        Real.sqrt ((∫ ω, G.domA ω ^ 2 ∂P) * ∫ ω, G.domB ω ^ 2 ∂P) =
      ((∫ ω, G.addA ω * G.addB ω ∂P) /
        Real.sqrt ((∫ ω, G.addA ω ^ 2 ∂P) * ∫ ω, G.addB ω ^ 2 ∂P)) ^ 2

Uses 14

Statement usesTwo-locus diploid genotype under random union of gametes · Additive coding at the first locus · Additive coding at the second locus · Dominance coding at the first locus · Dominance coding at the second locus

Proof usesCorrelation of additive codings equals the gametic correlation · Allele frequency at the first locus · Allele frequency at the second locus · Dominance linkage disequilibrium is the square of the gametic one · Second moment of the dominance coding at the first locus · Second moment of the dominance coding at the second locus · Gametic linkage disequilibrium · Haplotype variance at the first locus · Haplotype variance at the second locus

Dominance LD

DefinitionDominance encoding of a biallelic genotype#✓fully proved

The dominance encoding of a biallelic genotype g ∈ {0, 1, 2} (count of the allele with frequency p): p², -p (1 - p), (1 - p)². Dividing by -p (1 - p) gives the encoding -p / (1 - p), 1, -(1 - p) / p of Palmer et al. (2023).

noncomputable def dominanceEncoding (p g : ℝ) : ℝ :=
  if g = 0 then p ^ 2 else if g = 1 then -(p * (1 - p)) else (1 - p) ^ 2

Used by 1

Used byDominance coding of allele indicators equals the dominance encoding

TheoremDominance coding of allele indicators equals the dominance encoding#✓fully proved

For 0/1 allele indicators the dominance coding (X₁ - p) (X₂ - p) depends only on the genotype X₁ + X₂ and equals its dominance encoding.

theorem domCode_eq_dominanceEncoding {x1 x2 : ℝ} (h1 : x1 = 0 ∨ x1 = 1) (h2 : x2 = 0 ∨ x2 = 1)
    (p : ℝ) : (x1 - p) * (x2 - p) = dominanceEncoding p (x1 + x2)

Uses 1

Statement usesDominance encoding of a biallelic genotype

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.