Coalescence times, f-statistics and PCA

17 fully proved

f-statistics from heterozygosities and coalescence times

DefinitionProbability that two genes differ at a biallelic site#✓fully proved

The probability a (1 - b) + b (1 - a) that a gene from a population with allele frequency a and a gene from a population with allele frequency b differ at a biallelic site.

def hetPair (a b : ℝ) : ℝ := a * (1 - b) + b * (1 - a)

Used by 4

Used byPeter's formula for \(f_2\) via expected heterozygosity · Integrability of pairwise heterozygosity · Expected heterozygosity between populations · Squared frequency difference via pairwise heterozygosity

TheoremSquared frequency difference via pairwise heterozygosity#✓fully proved

(a - b) ^ 2 = hetPair a b - (hetPair a a + hetPair b b) / 2.

theorem sq_sub_eq_hetPair (a b : ℝ) :
    (a - b) ^ 2 = hetPair a b - (hetPair a a + hetPair b b) / 2

Uses 1 · Used by 1

Statement usesProbability that two genes differ at a biallelic site

Used byPeter's formula for \(f_2\) via expected heterozygosity

DefinitionExpected heterozygosity between populations#✓fully proved

The expected heterozygosity π X Y = 𝔼[hetPair (p X) (p Y)] between populations X and Y (within population X when Y = X).

noncomputable def meanHet (μ : Measure Ω) (p : P → Ω → ℝ) (X Y : P) : ℝ :=
  ∫ ω, hetPair (p X ω) (p Y ω) ∂μ

Uses 1 · Used by 3

Statement usesProbability that two genes differ at a biallelic site

Used byCoalescent model linking heterozygosity and coalescence times · \(f_2\) in terms of expected coalescence times · Peter's formula for \(f_2\) via expected heterozygosity

TheoremIntegrability of pairwise heterozygosity#✓fully proved

hetPair of square-integrable frequencies is integrable on a finite measure space.

theorem integrable_hetPair {μ : Measure Ω} [IsFiniteMeasure μ] {p : P → Ω → ℝ}
    (hp : ∀ X, MemLp (p X) 2 μ) (X Y : P) :
    Integrable (fun ω => hetPair (p X ω) (p Y ω)) μ

Uses 1 · Used by 1

Statement usesProbability that two genes differ at a biallelic site

Used byPeter's formula for \(f_2\) via expected heterozygosity

TheoremPeter's formula for \(f_2\) via expected heterozygosity#✓fully proved

Peter (2016): f2 A B = π A B - (π A A + π B B) / 2.

theorem f2_eq_meanHet {μ : Measure Ω} [IsFiniteMeasure μ] {p : P → Ω → ℝ}
    (hp : ∀ X, MemLp (p X) 2 μ) (A B : P) :
    f2 μ p A B = meanHet μ p A B - (meanHet μ p A A + meanHet μ p B B) / 2

Uses 5 · Used by 1

Statement usesExpected heterozygosity between populations · f2 statistic

Proof usesProbability that two genes differ at a biallelic site · Integrability of pairwise heterozygosity · Squared frequency difference via pairwise heterozygosity

Used by\(f_2\) in terms of expected coalescence times

StructureCoalescent model linking heterozygosity and coalescence times#✓fully proved

The relation between allele frequencies and coalescence times under neutral infinite-sites mutation, taken as the model assumption: the expected heterozygosity between populations X and Y is θ times the expected coalescence time coalTime X Y of a gene from X and a gene from Y (two genes drawn independently, so with replacement, when X = Y). Time is in units of 2N generations and θ = 4Nu. The measure μ is finite: it ranges over the evolutionary randomness and, in practice, over a finite set of loci. For θ = 0 the coalescence times are not determined by the frequencies, and the identities below then say that the f-statistics vanish.

structure CoalescentModel (μ : Measure Ω) (P : Type*) where
  /-- Allele frequencies of the populations. -/
  freq : P → Ω → ℝ
  /-- The scaled mutation rate `θ = 4Nu`. -/
  theta : ℝ
  /-- Expected pairwise coalescence times `𝔼[T X Y]`. -/
  coalTime : P → P → ℝ
  /-- Frequencies are square integrable. -/
  memLp_freq : ∀ X, MemLp (freq X) 2 μ
  /-- Infinite sites: `π X Y = θ 𝔼[T X Y]`. -/
  meanHet_eq : ∀ X Y, meanHet μ freq X Y = theta * coalTime X Y

Uses 1 · Used by 3

Statement usesExpected heterozygosity between populations

Used by\(f_2\) in terms of expected coalescence times · \(f_3\) in terms of expected coalescence times · \(f_4\) in terms of expected coalescence times

Theorem\(f_2\) in terms of expected coalescence times#✓fully proved

f2 A B = θ (𝔼 T_AB - (𝔼 T_AA + 𝔼 T_BB) / 2).

theorem f2_eq (A B : P) :
    f2 μ M.freq A B =
      M.theta * (M.coalTime A B - (M.coalTime A A + M.coalTime B B) / 2)

Uses 4 · Used by 2

Statement usesCoalescent model linking heterozygosity and coalescence times · f2 statistic

Proof usesPeter's formula for \(f_2\) via expected heterozygosity · Expected heterozygosity between populations

Used by\(f_3\) in terms of expected coalescence times · \(f_4\) in terms of expected coalescence times

Theorem\(f_3\) in terms of expected coalescence times#✓fully proved

f3 C A B = θ / 2 * (𝔼 T_CA + 𝔼 T_CB - 𝔼 T_AB - 𝔼 T_CC).

theorem f3_eq (C A B : P) :
    f3 μ M.freq C A B =
      M.theta / 2 * (M.coalTime C A + M.coalTime C B - M.coalTime A B - M.coalTime C C)

Uses 5

Statement usesCoalescent model linking heterozygosity and coalescence times · f3 statistic

Proof uses\(f_2\) in terms of expected coalescence times · f2 statistic · f3 in terms of f2

Theorem\(f_4\) in terms of expected coalescence times#✓fully proved

f4 A B C D = θ / 2 * (𝔼 T_AD + 𝔼 T_BC - 𝔼 T_AC - 𝔼 T_BD).

theorem f4_eq (A B C D : P) :
    f4 μ M.freq A B C D =
      M.theta / 2 * (M.coalTime A D + M.coalTime B C - M.coalTime A C - M.coalTime B D)

Uses 5

Statement usesCoalescent model linking heterozygosity and coalescence times · f4 statistic

Proof uses\(f_2\) in terms of expected coalescence times · f2 statistic · f4 in terms of f2

PCA from coalescence times (McVean 2009)

DefinitionColumn mean of a genotype matrix#✓fully proved

The column mean (1 / n) ∑ i, Z i s of locus s over the n samples.

noncomputable def colMean (Z : ι → S → ℝ) (s : S) : ℝ := (∑ i, Z i s) / Fintype.card ι

Used by 1

Used byColumn-centred genotype matrix

DefinitionColumn-centred genotype matrix#✓fully proved

The genotype matrix with columns centred over the samples.

noncomputable def centered (Z : ι → S → ℝ) (i : ι) (s : S) : ℝ := Z i s - colMean Z s

Uses 1 · Used by 2

Statement usesColumn mean of a genotype matrix

Used bySample covariance of the centred genotype matrix · Genotype covariance as double-centred pairwise differences

DefinitionSample covariance of the centred genotype matrix#✓fully proved

The sample covariance C i j = (1 / L) ∑ s, X i s * X j s of the centred genotype matrix X over the L loci.

noncomputable def genCov (Z : ι → S → ℝ) (i j : ι) : ℝ :=
  (∑ s, centered Z i s * centered Z j s) / Fintype.card S

Uses 1 · Used by 2

Statement usesColumn-centred genotype matrix

Used byGenotype covariance as double-centred pairwise differences · McVean's theorem on expected genotype covariance

DefinitionNumber of pairwise differences between samples#✓fully proved

The number of pairwise differences d i j = ∑ s, (Z i s - Z j s) ^ 2 (for 0/1 haplotypes, the number of loci at which samples i and j differ).

def pairDiff (Z : ι → S → ℝ) (i j : ι) : ℝ := ∑ s, (Z i s - Z j s) ^ 2

Used by 3

Used byGenotype covariance as double-centred pairwise differences · McVean's theorem on expected genotype covariance · McVean's genealogical model for PCA

DefinitionDouble centring of a square matrix#✓fully proved

The double centring t̄ i· + t̄ ·j - t i j - t̄ ·· of a square matrix t (row, column and grand means over the n indices).

noncomputable def doubleCenter (t : ι → ι → ℝ) (i j : ι) : ℝ :=
  (∑ k, t i k) / Fintype.card ι + (∑ k, t k j) / Fintype.card ι - t i j -
    (∑ k, ∑ l, t k l) / (Fintype.card ι : ℝ) ^ 2

Used by 4

Used byCentred leaf covariance as the double centring of f2 · f-statistics determine exactly the centred leaf covariance · Genotype covariance as double-centred pairwise differences · McVean's theorem on expected genotype covariance

TheoremGenotype covariance as double-centred pairwise differences#✓fully proved

McVean (2009), deterministic form: the covariance of the centred genotype matrix is the double centring of the pairwise-difference matrix, divided by 2 L.

theorem genCov_eq_doubleCenter (Z : ι → S → ℝ) (i j : ι) :
    genCov Z i j = doubleCenter (pairDiff Z) i j / (2 * Fintype.card S)

Uses 4 · Used by 1

Statement usesDouble centring of a square matrix · Sample covariance of the centred genotype matrix · Number of pairwise differences between samples

Proof usesColumn-centred genotype matrix

Used byMcVean's theorem on expected genotype covariance

StructureMcVean's genealogical model for PCA#✓fully proved

McVean's genealogical setting for PCA, taken as the model assumption: random genotypes Z i s (sample i, locus s), square integrable, whose expected numbers of pairwise differences are θ times the expected pairwise coalescence times coalTime i j (neutral infinite sites, time in units of 2N generations, θ the total scaled mutation rate of the L loci). For θ = 0 the coalescence times are not determined by the genotypes.

structure McVeanModel (μ : Measure Ω) (ι S : Type*) [Fintype ι] [Fintype S] where
  /-- Random genotypes. -/
  geno : ι → S → Ω → ℝ
  /-- The scaled mutation rate. -/
  theta : ℝ
  /-- Expected pairwise coalescence times of the samples. -/
  coalTime : ι → ι → ℝ
  /-- Genotypes are square integrable. -/
  memLp_geno : ∀ i s, MemLp (geno i s) 2 μ
  /-- Infinite sites: `𝔼[d i j] = θ t i j`. -/
  integral_pairDiff : ∀ i j, ∫ ω, pairDiff (fun k s => geno k s ω) i j ∂μ = theta * coalTime i j

Uses 1 · Used by 1

Statement usesNumber of pairwise differences between samples

Used byMcVean's theorem on expected genotype covariance

TheoremMcVean's theorem on expected genotype covariance#✓fully proved

McVean (2009): the expected genotype covariance is θ / (2 L) times the double centring of the expected pairwise coalescence times, 𝔼[C i j] = θ / (2 L) * (t̄ i· + t̄ ·j - t i j - t̄ ··).

theorem McVeanModel.integral_genCov {μ : Measure Ω} (M : McVeanModel μ ι S) (i j : ι) :
    ∫ ω, genCov (fun k s => M.geno k s ω) i j ∂μ =
      M.theta / (2 * Fintype.card S) * doubleCenter M.coalTime i j

Uses 5

Statement usesMcVean's genealogical model for PCA · Double centring of a square matrix · Sample covariance of the centred genotype matrix

Proof usesGenotype covariance as double-centred pairwise differences · Number of pairwise differences between samples

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.