Segregating sites and pairwise differences

DefinitionTajima's constant \(a_1\)#✓fully proved

a₁ = ∑_{i=1}^{n-1} 1/i (Tajima 1989).

def tajimaA1 (n : ℕ) : ℝ := ∑ i ∈ Ico 1 n, (i : ℝ)⁻¹

Used by 28

Used byCovariance of π and S · Pair coalescence time against the total branch length · Tajima's numerator has mean zero · Unbiased estimator of Tajima's variance term · Tajima's \(a_1\) is a harmonic number · Tajima's constant \(c_1\) · Tajima's constant \(c_2\) · Tajima's constant \(e_1\) · Tajima's constant \(e_2\) · Variance of the number of segregating sites · Tajima's variance identity · Numerator of Fu and Li's D · Numerator of Fu and Li's D has mean zero at constant size · HKA's estimating equations · True parameters solve the HKA estimating equations · HKA expected number of segregating sites · HKA variance of the number of segregating sites · Positivity of the HKA polymorphism variance · Level of the Chebyshev test · Positivity of Tajima's \(c_1\) for at least four genes · Tajima's \(c_1\) vanishes for three genes · Tajima's \(c_1\) vanishes for two genes · Positivity of Tajima's \(c_2\) for at least four genes · Tajima's \(c_2\) vanishes for three genes · Tajima's \(c_2\) vanishes for two genes · Chebyshev test of neutrality · Tajima's D · Positivity of the denominator of Tajima's D

DefinitionTajima's constant \(a_2\)#✓fully proved

a₂ = ∑_{i=1}^{n-1} 1/i² (Tajima 1989).

def tajimaA2 (n : ℕ) : ℝ := ∑ i ∈ Ico 1 n, ((i : ℝ) ^ 2)⁻¹

Used by 12

Used byUnbiased estimator of Tajima's variance term · Tajima's constant \(c_2\) · Tajima's constant \(e_2\) · Variance of the number of segregating sites · Tajima's variance identity · Variance of the total branch length · HKA variance of the number of segregating sites · Positivity of the HKA polymorphism variance · Positivity of Tajima's \(c_2\) for at least four genes · Tajima's \(c_2\) vanishes for three genes · Tajima's \(c_2\) vanishes for two genes · Positivity of the denominator of Tajima's D

DefinitionTajima's constant \(b_1\)#✓fully proved

b₁ = (n + 1) / (3 (n - 1)) (Tajima 1989), for n ≥ 2.

def tajimaB1 (n : ℕ) : ℝ := ((n : ℝ) + 1) / (3 * ((n : ℝ) - 1))

Used by 4

Used byTajima's constant \(c_1\) · Variance of the mean number of pairwise differences · Tajima's variance identity · Positivity of Tajima's \(c_1\) for at least four genes

DefinitionTajima's constant \(b_2\)#✓fully proved

b₂ = 2 (n² + n + 3) / (9 n (n - 1)) (Tajima 1989), for n ≥ 2.

def tajimaB2 (n : ℕ) : ℝ := 2 * ((n : ℝ) ^ 2 + n + 3) / (9 * n * ((n : ℝ) - 1))

Used by 6

Used byTajima's constant \(c_2\) · Variance of the mean number of pairwise differences · Tajima's variance identity · Positivity of Tajima's \(c_2\) for at least four genes · Tajima's \(c_2\) vanishes for three genes · Tajima's \(c_2\) vanishes for two genes

DefinitionTajima's constant \(c_1\)#✓fully proved

c₁ = b₁ - 1/a₁ (Tajima 1989), for n ≥ 2.

def tajimaC1 (n : ℕ) : ℝ := tajimaB1 n - 1 / tajimaA1 n

Uses 2 · Used by 9

Statement usesTajima's constant \(a_1\) · Tajima's constant \(b_1\)

Used byUnbiased estimator of Tajima's variance term · Tajima's constant \(e_1\) · Tajima's variance identity · Level of the Chebyshev test · Positivity of Tajima's \(c_1\) for at least four genes · Tajima's \(c_1\) vanishes for three genes · Tajima's \(c_1\) vanishes for two genes · Chebyshev test of neutrality · Positivity of the denominator of Tajima's D

DefinitionTajima's constant \(c_2\)#✓fully proved

c₂ = b₂ - (n + 2)/(a₁ n) + a₂/a₁² (Tajima 1989), for n ≥ 2.

def tajimaC2 (n : ℕ) : ℝ :=
  tajimaB2 n - ((n : ℝ) + 2) / (tajimaA1 n * n) + tajimaA2 n / tajimaA1 n ^ 2

Uses 3 · Used by 9

Statement usesTajima's constant \(a_1\) · Tajima's constant \(a_2\) · Tajima's constant \(b_2\)

Used byUnbiased estimator of Tajima's variance term · Tajima's constant \(e_2\) · Tajima's variance identity · Level of the Chebyshev test · Positivity of Tajima's \(c_2\) for at least four genes · Tajima's \(c_2\) vanishes for three genes · Tajima's \(c_2\) vanishes for two genes · Chebyshev test of neutrality · Positivity of the denominator of Tajima's D

DefinitionTajima's constant \(e_1\)#✓fully proved

e₁ = c₁ / a₁ (Tajima 1989), for n ≥ 2.

def tajimaE1 (n : ℕ) : ℝ := tajimaC1 n / tajimaA1 n

Uses 2 · Used by 3

Statement usesTajima's constant \(a_1\) · Tajima's constant \(c_1\)

Used byUnbiased estimator of Tajima's variance term · Tajima's D · Positivity of the denominator of Tajima's D

DefinitionTajima's constant \(e_2\)#✓fully proved

e₂ = c₂ / (a₁² + a₂) (Tajima 1989), for n ≥ 2.

def tajimaE2 (n : ℕ) : ℝ := tajimaC2 n / (tajimaA1 n ^ 2 + tajimaA2 n)

Uses 3 · Used by 3

Statement usesTajima's constant \(a_1\) · Tajima's constant \(a_2\) · Tajima's constant \(c_2\)

Used byUnbiased estimator of Tajima's variance term · Tajima's D · Positivity of the denominator of Tajima's D

TheoremTajima's \(a_1\) is a harmonic number#✓fully proved

a₁ is the harmonic number H_{n-1}.

theorem tajimaA1_eq_harmonic (n : ℕ) : tajimaA1 n = (harmonic (n - 1) : ℝ)

Uses 1 · Used by 8

Statement usesTajima's constant \(a_1\)

Used byCovariance of π and S · Pair coalescence time against the total branch length · Tajima's numerator has mean zero · Unbiased estimator of Tajima's variance term · Variance of the number of segregating sites · Tajima's variance identity · Positivity of the HKA polymorphism variance · Positivity of the denominator of Tajima's D

TheoremVariance of the total branch length#✓fully proved

Variance of the total branch length (Watterson 1975): Var L = ∑_{k=2}^n k² Var T_k = 4 ∑_{j=1}^{n-1} 1/j² (uses independence of the holding times).

theorem variance_totalLength : Var[K.totalLength; μ] = 4 * tajimaA2 n

Uses 6 · Used by 1

Statement usesHolding times of Kingman's coalescent · Total branch length of a coalescent genealogy · Tajima's constant \(a_2\)

Proof usesPositivity of the number of pairs · Variance of an exponentially distributed random variable · Finiteness of all moments of the exponential law

Used byVariance of the number of segregating sites

TheoremVariance of the number of segregating sites#✓fully proved

Variance of the number of segregating sites (Watterson 1975; Tajima 1989): if, given the genealogy σ-algebra m, the number S of segregating sites has conditional mean and conditional variance (θ/2) L (as for a Poisson count with mean θ L / 2), then Var S = θ a₁ + θ² a₂.

theorem variance_segSites [IsProbabilityMeasure μ] {m : MeasurableSpace Ω} (hm : m ≤ mΩ)
    {S : Ω → ℝ} {θ : ℝ} (hS2 : MemLp S 2 μ)
    (hmean : μ[S | m] =ᵐ[μ] fun ω => θ / 2 * K.totalLength ω)
    (hvar : Var[S; μ | m] =ᵐ[μ] fun ω => θ / 2 * K.totalLength ω) :
    Var[S; μ] = θ * tajimaA1 n + θ ^ 2 * tajimaA2 n

Uses 7 · Used by 2

Statement usesHolding times of Kingman's coalescent · Total branch length of a coalescent genealogy · Tajima's constant \(a_1\) · Tajima's constant \(a_2\)

Proof usesExpected total branch length of the coalescent · Variance of the total branch length · Tajima's \(a_1\) is a harmonic number

Used byUnbiased estimator of Tajima's variance term · Tajima's variance identity

AbbreviationPairs of genes in a sample#✓fully proved

The pairs of genes in a sample of size n.

abbrev samplePairs (n : ℕ) : Finset (Finset (Fin n)) := (univ : Finset (Fin n)).powersetCard 2

Used by 7

Used byCovariance of π and S · Expected pairwise differences · Tajima's numerator has mean zero · Mean number of pairwise differences · Counting sample pairs by overlap with a given pair · Variance of the mean number of pairwise differences · Tajima's variance identity

DefinitionMean number of pairwise differences#✓fully proved

The mean number of pairwise differences π = C(n, 2)⁻¹ ∑_{i<j} D_{ij} (Tajima 1983), where D s is the number of sites at which the two sequences of the pair s differ.

def meanPairDiff (n : ℕ) (D : Finset (Fin n) → Ω → ℝ) : Ω → ℝ :=
  fun ω => ((n.choose 2 : ℕ) : ℝ)⁻¹ * ∑ s ∈ samplePairs n, D s ω

Uses 1 · Used by 5

Statement usesPairs of genes in a sample

Used byCovariance of π and S · Expected pairwise differences · Tajima's numerator has mean zero · Variance of the mean number of pairwise differences · Tajima's variance identity

TheoremExpected pairwise differences#✓fully proved

Expected pairwise differences (Tajima 1983): if, for each pair s of sampled genes, the coalescence time τ s of the pair is exponential with rate 1 and the number D s of differences has conditional mean θ τ s given the genealogy σ-algebra m (mutations at rate θ / 2 on each of the two branches of length τ s), then E π = θ.

theorem integral_meanPairDiff {m : MeasurableSpace Ω} (hm : m ≤ mΩ) [SigmaFinite (μ.trim hm)]
    {D τ : Finset (Fin n) → Ω → ℝ} {θ : ℝ} (hn : 2 ≤ n)
    (hτ : ∀ s ∈ samplePairs n, HasLaw (τ s) (expMeasure 1) μ)
    (hDint : ∀ s ∈ samplePairs n, Integrable (D s) μ)
    (hD : ∀ s ∈ samplePairs n, μ[D s | m] =ᵐ[μ] fun ω => θ * τ s ω) :
    μ[meanPairDiff n D] = θ

Uses 3 · Used by 1

Statement usesMean number of pairwise differences · Pairs of genes in a sample

Proof usesMean of an exponentially distributed random variable

Used byTajima's numerator has mean zero

TheoremTajima's numerator has mean zero#✓fully proved

Tajima's numerator has mean zero (Tajima 1989): under the hypotheses of integral_meanPairDiff and Watterson's (E[S | m] = (θ/2) L), E[π - S / a₁] = 0 for a sample of size n ≥ 2.

theorem integral_tajimaNumerator {Ω : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω}
    {n : ℕ} (K : KingmanTimes μ n) {m : MeasurableSpace Ω} (hm : m ≤ mΩ)
    [SigmaFinite (μ.trim hm)] {S : Ω → ℝ} {D τ : Finset (Fin n) → Ω → ℝ} {θ : ℝ} (hn : 2 ≤ n)
    (hSint : Integrable S μ) (hS : μ[S | m] =ᵐ[μ] fun ω => θ / 2 * K.totalLength ω)
    (hτ : ∀ s ∈ samplePairs n, HasLaw (τ s) (expMeasure 1) μ)
    (hDint : ∀ s ∈ samplePairs n, Integrable (D s) μ)
    (hD : ∀ s ∈ samplePairs n, μ[D s | m] =ᵐ[μ] fun ω => θ * τ s ω) :
    μ[fun ω => meanPairDiff n D ω - S ω / tajimaA1 n] = 0

Uses 8

Statement usesHolding times of Kingman's coalescent · Total branch length of a coalescent genealogy · Mean number of pairwise differences · Pairs of genes in a sample · Tajima's constant \(a_1\)

Proof usesWatterson's estimator is unbiased · Expected pairwise differences · Tajima's \(a_1\) is a harmonic number

TheoremUnbiased estimator of Tajima's variance term#✓fully proved

Unbiased estimator of Tajima's variance term (Tajima 1989): with S as in variance_segSites, E[e₁ S + e₂ S (S - 1)] = c₁ θ + c₂ θ² for n ≥ 2. (By Tajima's analysis c₁ θ + c₂ θ² is Var(π - S / a₁).)

theorem integral_tajimaVarEstimator {Ω : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω}
    {n : ℕ} (K : KingmanTimes μ n) [IsProbabilityMeasure μ] {m : MeasurableSpace Ω}
    (hm : m ≤ mΩ) {S : Ω → ℝ} {θ : ℝ} (hn : 2 ≤ n) (hS2 : MemLp S 2 μ)
    (hmean : μ[S | m] =ᵐ[μ] fun ω => θ / 2 * K.totalLength ω)
    (hvar : Var[S; μ | m] =ᵐ[μ] fun ω => θ / 2 * K.totalLength ω) :
    μ[fun ω => tajimaE1 n * S ω + tajimaE2 n * (S ω * (S ω - 1))] =
      tajimaC1 n * θ + tajimaC2 n * θ ^ 2

Uses 11

Statement usesHolding times of Kingman's coalescent · Total branch length of a coalescent genealogy · Tajima's constant \(c_1\) · Tajima's constant \(c_2\) · Tajima's constant \(e_1\) · Tajima's constant \(e_2\)

Proof usesExpected number of segregating sites · Variance of the number of segregating sites · Tajima's constant \(a_1\) · Tajima's \(a_1\) is a harmonic number · Tajima's constant \(a_2\)

TheoremCounting sample pairs by overlap with a given pair#✓fully proved

Among the pairs of a sample of size n, one equals a given pair s, 2 (n - 2) share exactly one gene with it and C(n - 2, 2) are disjoint from it.

theorem sum_samplePairs_card_inter {n : ℕ} {s : Finset (Fin n)} (hs : s ∈ samplePairs n)
    (f : ℕ → ℝ) :
    ∑ t ∈ samplePairs n, f #(s ∩ t) =
      f 2 + 2 * ((n - 2 : ℕ) : ℝ) * f 1 + (((n - 2).choose 2 : ℕ) : ℝ) * f 0

Uses 1 · Used by 1

Statement usesPairs of genes in a sample

Used byVariance of the mean number of pairwise differences

TheoremVariance of the mean number of pairwise differences#✓fully proved

Variance of the mean number of pairwise differences (Tajima 1983): Var π = b₁ θ + b₂ θ² for a sample of size n ≥ 2, under the conditional-moment model of the module docstring: τ s ~ Exp(1), E[τ s τ t] = 4/3 (one shared gene), 11/9 (disjoint pairs); the shared path lengths ℓ; E[D s | m] = θ τ s and E[D s D t | m] = θ² τ s τ t + (θ / 2) ℓ s t.

MathlibExt.Biology.PopulationGenetics.Coalescent.variance_meanPairDiff · 18 lines

theorem variance_meanPairDiff [IsProbabilityMeasure μ] {m : MeasurableSpace Ω} (hm : m ≤ mΩ)
    {D τ : Finset (Fin n) → Ω → ℝ} {ℓ : Finset (Fin n) → Finset (Fin n) → Ω → ℝ} {θ : ℝ}
    (hn : 2 ≤ n)
    (hτ : ∀ s ∈ samplePairs n, HasLaw (τ s) (expMeasure 1) μ)
    (hτ₁ : ∀ s ∈ samplePairs n, ∀ t ∈ samplePairs n, #(s ∩ t) = 1 →
      μ[fun ω => τ s ω * τ t ω] = 4 / 3)
    (hτ₀ : ∀ s ∈ samplePairs n, ∀ t ∈ samplePairs n, Disjoint s t →
      μ[fun ω => τ s ω * τ t ω] = 11 / 9)
    (hℓ₂ : ∀ s ∈ samplePairs n, ℓ s s =ᵐ[μ] fun ω => 2 * τ s ω)
    (hℓ₁ : ∀ s ∈ samplePairs n, ∀ t ∈ samplePairs n, #(s ∩ t) = 1 →
      ℓ s t =ᵐ[μ] fun ω => τ s ω + τ t ω - τ (symmDiff s t) ω)
    (hℓ₀ : ∀ s ∈ samplePairs n, ∀ t ∈ samplePairs n, Disjoint s t → μ[ℓ s t] = 2 / 3)
    (hD2 : ∀ s ∈ samplePairs n, MemLp (D s) 2 μ)
    (hD : ∀ s ∈ samplePairs n, μ[D s | m] =ᵐ[μ] fun ω => θ * τ s ω)
    (hDD : ∀ s ∈ samplePairs n, ∀ t ∈ samplePairs n,
      μ[fun ω => D s ω * D t ω | m] =ᵐ[μ]
        fun ω => θ ^ 2 * (τ s ω * τ t ω) + θ / 2 * ℓ s t ω) :
    Var[meanPairDiff n D; μ] = tajimaB1 n * θ + tajimaB2 n * θ ^ 2

Uses 8 · Used by 1

Statement usesMean number of pairwise differences · Pairs of genes in a sample · Tajima's constant \(b_1\) · Tajima's constant \(b_2\)

Proof usesCounting sample pairs by overlap with a given pair · Mean of an exponentially distributed random variable · Variance of an exponentially distributed random variable · Finiteness of all moments of the exponential law

Used byTajima's variance identity

DefinitionProbability that a pair lies in separate lineages#✓fully proved

The probability (k - 1) (n + 1) / ((n - 1) (k + 1)) that a given pair of a sample of size n is still in two distinct lineages while the genealogy has k lineages (2 ≤ k ≤ n, n ≥ 2; at n = 1 the definition divides by zero and returns 0).

def pairSeparateProb (n k : ℕ) : ℝ :=
  ((k : ℝ) - 1) * ((n : ℝ) + 1) / (((n : ℝ) - 1) * ((k : ℝ) + 1))

Used by 3

Used byPair coalescence time against the total branch length · Sum of pair-separation probabilities over squared pair counts · Mean coalescence time of a pair is one

TheoremMean coalescence time of a pair is one#✓fully proved

∑_{k=2}^n p_k / C(k, 2) = 1: the mean coalescence time of a pair is 1.

theorem sum_pairSeparateProb_div_choose {n : ℕ} (hn : 2 ≤ n) :
    ∑ k ∈ Icc 2 n, pairSeparateProb n k * ((k.choose 2 : ℕ) : ℝ)⁻¹ = 1

Uses 1 · Used by 1

Statement usesProbability that a pair lies in separate lineages

Used byPair coalescence time against the total branch length

TheoremSum of pair-separation probabilities over squared pair counts#✓fully proved

∑_{k=2}^n k p_k / C(k, 2)² = (n + 2) / n.

theorem sum_mul_pairSeparateProb_div_choose_sq {n : ℕ} (hn : 2 ≤ n) :
    ∑ k ∈ Icc 2 n, (k : ℝ) * pairSeparateProb n k * (((k.choose 2 : ℕ) : ℝ)⁻¹) ^ 2 =
      ((n : ℝ) + 2) / n

Uses 1 · Used by 1

Statement usesProbability that a pair lies in separate lineages

Used byPair coalescence time against the total branch length

TheoremCovariance of π and S#✓fully proved

Cov(π, S) = θ + (n + 2) θ² / (2 n) for n ≥ 2, if τ s ~ Exp(1), E[τ s L] = 2 a₁ + (n + 2) / n (L the total branch length), E[D s | m] = θ τ s, E[S | m] = (θ / 2) L and E[D s S | m] = (θ² / 2) τ s L + θ τ s (the path of each pair lies in the tree). This is the covariance behind Tajima's (1989) c₁, c₂.

theorem covariance_meanPairDiff_segSites [IsProbabilityMeasure μ] {m : MeasurableSpace Ω}
    (hm : m ≤ mΩ) {S : Ω → ℝ} {D τ : Finset (Fin n) → Ω → ℝ} {θ : ℝ} (hn : 2 ≤ n)
    (hS2 : MemLp S 2 μ) (hS : μ[S | m] =ᵐ[μ] fun ω => θ / 2 * K.totalLength ω)
    (hτ : ∀ s ∈ samplePairs n, HasLaw (τ s) (expMeasure 1) μ)
    (hτL : ∀ s ∈ samplePairs n,
      μ[fun ω => τ s ω * K.totalLength ω] = 2 * tajimaA1 n + ((n : ℝ) + 2) / n)
    (hD2 : ∀ s ∈ samplePairs n, MemLp (D s) 2 μ)
    (hD : ∀ s ∈ samplePairs n, μ[D s | m] =ᵐ[μ] fun ω => θ * τ s ω)
    (hDS : ∀ s ∈ samplePairs n, μ[fun ω => D s ω * S ω | m] =ᵐ[μ]
      fun ω => θ ^ 2 / 2 * (τ s ω * K.totalLength ω) + θ * τ s ω) :
    cov[meanPairDiff n D, S; μ] = θ + ((n : ℝ) + 2) / (2 * n) * θ ^ 2

Uses 11 · Used by 1

Statement usesHolding times of Kingman's coalescent · Total branch length of a coalescent genealogy · Mean number of pairwise differences · Pairs of genes in a sample · Tajima's constant \(a_1\)

Proof usesIntegrability of the total branch length · Expected total branch length of the coalescent · Tajima's \(a_1\) is a harmonic number · Mean of an exponentially distributed random variable · Variance of an exponentially distributed random variable · Finiteness of all moments of the exponential law

Used byTajima's variance identity

TheoremTajima's variance identity#✓fully proved

Tajima's variance identity (Tajima 1989): Var(π - S / a₁) = c₁ θ + c₂ θ² for a sample of size n ≥ 2, under the hypotheses of variance_meanPairDiff, covariance_meanPairDiff_segSites and variance_segSites.

MathlibExt.Biology.PopulationGenetics.Coalescent.KingmanTimes.variance_tajimaNumerator · 25 lines

theorem variance_tajimaNumerator [IsProbabilityMeasure μ] {m : MeasurableSpace Ω}
    (hm : m ≤ mΩ) {S : Ω → ℝ} {D τ : Finset (Fin n) → Ω → ℝ}
    {ℓ : Finset (Fin n) → Finset (Fin n) → Ω → ℝ} {θ : ℝ} (hn : 2 ≤ n)
    (hS2 : MemLp S 2 μ) (hS : μ[S | m] =ᵐ[μ] fun ω => θ / 2 * K.totalLength ω)
    (hSvar : Var[S; μ | m] =ᵐ[μ] fun ω => θ / 2 * K.totalLength ω)
    (hτ : ∀ s ∈ samplePairs n, HasLaw (τ s) (expMeasure 1) μ)
    (hτ₁ : ∀ s ∈ samplePairs n, ∀ t ∈ samplePairs n, #(s ∩ t) = 1 →
      μ[fun ω => τ s ω * τ t ω] = 4 / 3)
    (hτ₀ : ∀ s ∈ samplePairs n, ∀ t ∈ samplePairs n, Disjoint s t →
      μ[fun ω => τ s ω * τ t ω] = 11 / 9)
    (hτL : ∀ s ∈ samplePairs n,
      μ[fun ω => τ s ω * K.totalLength ω] = 2 * tajimaA1 n + ((n : ℝ) + 2) / n)
    (hℓ₂ : ∀ s ∈ samplePairs n, ℓ s s =ᵐ[μ] fun ω => 2 * τ s ω)
    (hℓ₁ : ∀ s ∈ samplePairs n, ∀ t ∈ samplePairs n, #(s ∩ t) = 1 →
      ℓ s t =ᵐ[μ] fun ω => τ s ω + τ t ω - τ (symmDiff s t) ω)
    (hℓ₀ : ∀ s ∈ samplePairs n, ∀ t ∈ samplePairs n, Disjoint s t → μ[ℓ s t] = 2 / 3)
    (hD2 : ∀ s ∈ samplePairs n, MemLp (D s) 2 μ)
    (hD : ∀ s ∈ samplePairs n, μ[D s | m] =ᵐ[μ] fun ω => θ * τ s ω)
    (hDD : ∀ s ∈ samplePairs n, ∀ t ∈ samplePairs n,
      μ[fun ω => D s ω * D t ω | m] =ᵐ[μ]
        fun ω => θ ^ 2 * (τ s ω * τ t ω) + θ / 2 * ℓ s t ω)
    (hDS : ∀ s ∈ samplePairs n, μ[fun ω => D s ω * S ω | m] =ᵐ[μ]
      fun ω => θ ^ 2 / 2 * (τ s ω * K.totalLength ω) + θ * τ s ω) :
    Var[fun ω => meanPairDiff n D ω - S ω / tajimaA1 n; μ] =
      tajimaC1 n * θ + tajimaC2 n * θ ^ 2

Uses 14

Statement usesHolding times of Kingman's coalescent · Total branch length of a coalescent genealogy · Mean number of pairwise differences · Pairs of genes in a sample · Tajima's constant \(a_1\) · Tajima's constant \(c_1\) · Tajima's constant \(c_2\)

Proof usesCovariance of π and S · Variance of the number of segregating sites · Tajima's \(a_1\) is a harmonic number · Tajima's constant \(a_2\) · Tajima's constant \(b_1\) · Tajima's constant \(b_2\) · Variance of the mean number of pairwise differences

TheoremPair coalescence time against the total branch length#✓fully proved

If the coalescence time of a pair is τ = ∑_{k=2}^n χ k T k, where χ k indicates that the pair is still in two distinct lineages while there are k lineages, and the topology is independent of the holding times in the sense E[χ k T k T k'] = p k E[T k T k'] with p k = pairSeparateProb n k, then E[τ L] = 2 a₁ + (n + 2) / n for n ≥ 2. Only this factorization is used, so χ k need not be an indicator in the statement.

theorem integral_pairTime_mul_totalLength [IsProbabilityMeasure μ] {χ : ℕ → Ω → ℝ}
    {τ : Ω → ℝ} (hn : 2 ≤ n) (hτ : τ = fun ω => ∑ k ∈ Icc 2 n, χ k ω * K.T k ω)
    (hχ : ∀ k ∈ Icc 2 n, ∀ k' ∈ Icc 2 n,
      μ[fun ω => χ k ω * (K.T k ω * K.T k' ω)] =
        pairSeparateProb n k * μ[fun ω => K.T k ω * K.T k' ω]) :
    μ[fun ω => τ ω * K.totalLength ω] = 2 * tajimaA1 n + ((n : ℝ) + 2) / n

Uses 13

Statement usesHolding times of Kingman's coalescent · Total branch length of a coalescent genealogy · Probability that a pair lies in separate lineages · Tajima's constant \(a_1\)

Proof usesPositivity of the number of pairs · Integrability of coalescent holding times · Expected coalescent holding time · Weighted sum of reciprocals of \(\binom{k}{2}\) is twice a harmonic number · Sum of pair-separation probabilities over squared pair counts · Mean coalescence time of a pair is one · Tajima's \(a_1\) is a harmonic number · Variance of an exponentially distributed random variable · Finiteness of all moments of the exponential law

24 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.