Hudson–Kreitman–Aguadé test

DefinitionHKA expected number of segregating sites#✓fully proved

HKA's expected number of segregating sites θ C(n) in a sample of n genes with scaled mutation rate θ (use f θ for species B).

def hkaPolyMean (θ : ℝ) (n : ℕ) : ℝ := θ * tajimaA1 n

Uses 1 · Used by 3

Statement usesTajima's constant \(a_1\)

Used byTrue parameters solve the HKA estimating equations · Hudson–Kreitman–Aguadé statistic · The HKA statistic has mean 3 L at the true parameters

DefinitionHKA variance of the number of segregating sites#✓fully proved

HKA's variance of the number of segregating sites, θ C(n) + θ² C₂(n).

def hkaPolyVar (θ : ℝ) (n : ℕ) : ℝ := θ * tajimaA1 n + θ ^ 2 * tajimaA2 n

Uses 2 · Used by 3

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

Used byPositivity of the HKA polymorphism variance · Hudson–Kreitman–Aguadé statistic · The HKA statistic has mean 3 L at the true parameters

DefinitionHKA expected divergence#✓fully proved

HKA's expected divergence θ (T + (1 + f) / 2).

def hkaDivMean (θ T f : ℝ) : ℝ := θ * (T + (1 + f) / 2)

Used by 7

Used byHKA variance of the divergence · Positivity of the HKA divergence variance · True parameters solve the HKA estimating equations · Hudson–Kreitman–Aguadé statistic · Expected divergence · The HKA statistic has mean 3 L at the true parameters · Variance of the divergence

DefinitionHKA variance of the divergence#✓fully proved

HKA's variance of the divergence, θ (T + (1 + f) / 2) + (θ (1 + f) / 2)².

def hkaDivVar (θ T f : ℝ) : ℝ := hkaDivMean θ T f + (θ * (1 + f) / 2) ^ 2

Uses 1 · Used by 4

Statement usesHKA expected divergence

Used byPositivity of the HKA divergence variance · Hudson–Kreitman–Aguadé statistic · The HKA statistic has mean 3 L at the true parameters · Variance of the divergence

TheoremExpected divergence#✓fully proved

Expected divergence (Hudson, Kreitman & Aguadé 1987): if the ancestral coalescence time τ is exponential with rate 2 / (1 + f) and, given the genealogy σ-algebra m, the divergence D has conditional mean θ (T + τ), then E D = θ (T + (1 + f) / 2) (for f > -1). No integrability hypothesis on D is needed: if D were not integrable its conditional expectation would be 0 (Mathlib's convention), and the hypothesis would force θ = 0, where the identity reads 0 = 0.

theorem integral_hkaDivergence {Ω : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω}
    [IsProbabilityMeasure μ] {m : MeasurableSpace Ω} (hm : m ≤ mΩ) {D τ : Ω → ℝ}
    {θ T f : ℝ} (hf : -1 < f) (hτ : HasLaw τ (expMeasure (2 / (1 + f))) μ)
    (hmean : μ[D | m] =ᵐ[μ] fun ω => θ * (T + τ ω)) :
    μ[D] = hkaDivMean θ T f

Uses 3

Statement usesHKA expected divergence

Proof usesExponentially distributed random variables are integrable · Mean of an exponentially distributed random variable

TheoremVariance of the divergence#✓fully proved

Variance of the divergence (Hudson, Kreitman & Aguadé 1987): under the hypotheses of integral_hkaDivergence, if moreover D is square integrable with conditional variance θ (T + τ) given m (as for a Poisson count), then Var D = θ (T + (1 + f) / 2) + (θ (1 + f) / 2)².

theorem variance_hkaDivergence {Ω : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω}
    [IsProbabilityMeasure μ] {m : MeasurableSpace Ω} (hm : m ≤ mΩ) {D τ : Ω → ℝ}
    {θ T f : ℝ} (hf : -1 < f) (hτ : HasLaw τ (expMeasure (2 / (1 + f))) μ)
    (hD : MemLp D 2 μ) (hmean : μ[D | m] =ᵐ[μ] fun ω => θ * (T + τ ω))
    (hvar : Var[D; μ | m] =ᵐ[μ] fun ω => θ * (T + τ ω)) :
    Var[D; μ] = hkaDivVar θ T f

Uses 5

Statement usesHKA variance of the divergence

Proof usesHKA expected divergence · Exponentially distributed random variables are integrable · Mean of an exponentially distributed random variable · Variance of an exponentially distributed random variable

DefinitionHudson–Kreitman–Aguadé statistic#✓fully proved

The HKA statistic for L loci with polymorphism counts SA i, SB i, divergences D i, parameters θ i, T, f and sample sizes nA, nB: the sum over loci of the squared standardized deviations of the three counts from their HKA expectations.

def hkaStatistic {L : ℕ} (nA nB : ℕ) (θ : Fin L → ℝ) (T f : ℝ) (SA SB D : Fin L → ℝ) : ℝ :=
  ∑ i, ((SA i - hkaPolyMean (θ i) nA) ^ 2 / hkaPolyVar (θ i) nA +
    (SB i - hkaPolyMean (f * θ i) nB) ^ 2 / hkaPolyVar (f * θ i) nB +
    (D i - hkaDivMean (θ i) T f) ^ 2 / hkaDivVar (θ i) T f)

Uses 4 · Used by 1

Statement usesHKA expected divergence · HKA variance of the divergence · HKA expected number of segregating sites · HKA variance of the number of segregating sites

Used byThe HKA statistic has mean 3 L at the true parameters

TheoremPositivity of the HKA polymorphism variance#✓fully proved

HKA's variances are positive in the biological domain: θ > 0, n ≥ 2.

theorem hkaPolyVar_pos {θ : ℝ} (hθ : 0 < θ) {n : ℕ} (hn : 2 ≤ n) : 0 < hkaPolyVar θ n

Uses 4 · Used by 1

Statement usesHKA variance of the number of segregating sites

Proof usesTajima's constant \(a_1\) · Tajima's \(a_1\) is a harmonic number · Tajima's constant \(a_2\)

Used byThe HKA statistic has mean 3 L at the true parameters

TheoremPositivity of the HKA divergence variance#✓fully proved

HKA's divergence variance is positive for θ > 0, T ≥ 0, f > -1.

theorem hkaDivVar_pos {θ T f : ℝ} (hθ : 0 < θ) (hT : 0 ≤ T) (hf : -1 < f) :
    0 < hkaDivVar θ T f

Uses 2 · Used by 1

Statement usesHKA variance of the divergence

Proof usesHKA expected divergence

Used byThe HKA statistic has mean 3 L at the true parameters

TheoremThe HKA statistic has mean 3 L at the true parameters#✓fully proved

If every count is square integrable with the HKA mean and variance (as derived above under the neutral model), with θ i > 0, T ≥ 0, f > 0 and nA, nB ≥ 2, then E X² = 3 L.

theorem integral_hkaStatistic {Ω : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω}
    [IsProbabilityMeasure μ] {L nA nB : ℕ} {θ : Fin L → ℝ} {T f : ℝ}
    (hθ : ∀ i, 0 < θ i) (hT : 0 ≤ T) (hf : 0 < f) (hnA : 2 ≤ nA) (hnB : 2 ≤ nB)
    {SA SB D : Fin L → Ω → ℝ} (hSA : ∀ i, MemLp (SA i) 2 μ) (hSB : ∀ i, MemLp (SB i) 2 μ)
    (hD : ∀ i, MemLp (D i) 2 μ)
    (eSA : ∀ i, μ[SA i] = hkaPolyMean (θ i) nA)
    (eSB : ∀ i, μ[SB i] = hkaPolyMean (f * θ i) nB)
    (eD : ∀ i, μ[D i] = hkaDivMean (θ i) T f)
    (vSA : ∀ i, Var[SA i; μ] = hkaPolyVar (θ i) nA)
    (vSB : ∀ i, Var[SB i; μ] = hkaPolyVar (f * θ i) nB)
    (vD : ∀ i, Var[D i; μ] = hkaDivVar (θ i) T f) :
    μ[fun ω => hkaStatistic nA nB θ T f (fun i => SA i ω) (fun i => SB i ω)
      (fun i => D i ω)] = 3 * (L : ℝ)

Uses 7

Statement usesHKA expected divergence · HKA variance of the divergence · HKA expected number of segregating sites · HKA variance of the number of segregating sites · Hudson–Kreitman–Aguadé statistic

Proof usesPositivity of the HKA divergence variance · Positivity of the HKA polymorphism variance

DefinitionHKA's estimating equations#✓fully proved

HKA's estimating equations (Hudson, Kreitman & Aguadé 1987) for parameters θ i, T, f given the counts: the totals over loci of polymorphism in A, in B and of divergence match their expectations, and at each locus the total of the three counts matches its expectation. (Only L - 1 of the per-locus equations are independent of the totals.)

def hkaEquations {L : ℕ} (nA nB : ℕ) (θ : Fin L → ℝ) (T f : ℝ) (SA SB D : Fin L → ℝ) :
    Prop :=
  (∑ i, SA i = tajimaA1 nA * ∑ i, θ i) ∧ (∑ i, SB i = f * tajimaA1 nB * ∑ i, θ i) ∧
    (∑ i, D i = (T + (1 + f) / 2) * ∑ i, θ i) ∧
    ∀ i, SA i + SB i + D i = θ i * (T + (1 + f) / 2 + tajimaA1 nA + f * tajimaA1 nB)

Uses 1 · Used by 1

Statement usesTajima's constant \(a_1\)

Used byTrue parameters solve the HKA estimating equations

TheoremTrue parameters solve the HKA estimating equations#✓fully proved

The true parameters solve HKA's estimating equations at the expected counts.

theorem hkaEquations_expected {L : ℕ} (nA nB : ℕ) (θ : Fin L → ℝ) (T f : ℝ) :
    hkaEquations nA nB θ T f (fun i => hkaPolyMean (θ i) nA)
      (fun i => hkaPolyMean (f * θ i) nB) (fun i => hkaDivMean (θ i) T f)

Uses 4

Statement usesHKA expected divergence · HKA's estimating equations · HKA expected number of segregating sites

Proof usesTajima's constant \(a_1\)

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.