Tajima's D

DefinitionTajima's D#✓fully proved

Tajima's D (Tajima 1989) for a sample of n genes with mean number of pairwise differences π and S segregating sites: D = (π - S / a₁) / √(e₁ S + e₂ S (S - 1)). It is meaningful for n ≥ 4 and S ≥ 1 (tajimaVarEstimator_pos); otherwise Lean's junk values for x / 0 and √ of a nonpositive number apply.

def tajimaD (n : ℕ) (π S : ℝ) : ℝ :=
  (π - S / tajimaA1 n) / Real.sqrt (tajimaE1 n * S + tajimaE2 n * (S * (S - 1)))

Uses 3

Statement usesTajima's constant \(a_1\) · Tajima's constant \(e_1\) · Tajima's constant \(e_2\)

TheoremTajima's \(c_1\) vanishes for two genes#✓fully proved

For two genes c₁ = 0.

theorem tajimaC1_two : tajimaC1 2 = 0

Uses 2

Statement usesTajima's constant \(c_1\)

Proof usesTajima's constant \(a_1\)

TheoremTajima's \(c_2\) vanishes for two genes#✓fully proved

For two genes c₂ = 0.

theorem tajimaC2_two : tajimaC2 2 = 0

Uses 4

Statement usesTajima's constant \(c_2\)

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

TheoremTajima's \(c_1\) vanishes for three genes#✓fully proved

For three genes c₁ = 0.

theorem tajimaC1_three : tajimaC1 3 = 0

Uses 2

Statement usesTajima's constant \(c_1\)

Proof usesTajima's constant \(a_1\)

TheoremTajima's \(c_2\) vanishes for three genes#✓fully proved

For three genes c₂ = 0.

theorem tajimaC2_three : tajimaC2 3 = 0

Uses 4

Statement usesTajima's constant \(c_2\)

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

TheoremPositivity of Tajima's \(c_1\) for at least four genes#✓fully proved

c₁ = (n + 1) / (3 (n - 1)) - 1 / a₁ > 0 for n ≥ 4.

theorem tajimaC1_pos {n : ℕ} (hn : 4 ≤ n) : 0 < tajimaC1 n

Uses 3 · Used by 1

Statement usesTajima's constant \(c_1\)

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

Used byPositivity of the denominator of Tajima's D

TheoremPositivity of Tajima's \(c_2\) for at least four genes#✓fully proved

c₂ = b₂ - (n + 2) / (a₁ n) + a₂ / a₁² > 0 for n ≥ 4.

theorem tajimaC2_pos {n : ℕ} (hn : 4 ≤ n) : 0 < tajimaC2 n

Uses 4 · Used by 1

Statement usesTajima's constant \(c_2\)

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

Used byPositivity of the denominator of Tajima's D

TheoremPositivity of the denominator of Tajima's D#✓fully proved

The denominator of Tajima's D is well defined: e₁ S + e₂ S (S - 1) > 0 for n ≥ 4 and S ≥ 1.

theorem tajimaVarEstimator_pos {n : ℕ} (hn : 4 ≤ n) {S : ℝ} (hS : 1 ≤ S) :
    0 < tajimaE1 n * S + tajimaE2 n * (S * (S - 1))

Uses 9

Statement usesTajima's constant \(e_1\) · Tajima's constant \(e_2\)

Proof usesTajima's constant \(a_1\) · Tajima's \(a_1\) is a harmonic number · Tajima's constant \(a_2\) · Tajima's constant \(c_1\) · Positivity of Tajima's \(c_1\) for at least four genes · Tajima's constant \(c_2\) · Positivity of Tajima's \(c_2\) for at least four genes

DefinitionChebyshev test of neutrality#✓fully proved

The rejection region of the Chebyshev test of neutrality at level α and hypothesized θ₀: |π - S / a₁| ≥ √((c₁ θ₀ + c₂ θ₀²) / α).

def tajimaChebyshevTest (n : ℕ) (θ₀ α π S : ℝ) : Prop :=
  Real.sqrt ((tajimaC1 n * θ₀ + tajimaC2 n * θ₀ ^ 2) / α) ≤ |π - S / tajimaA1 n|

Uses 3 · Used by 1

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

Used byLevel of the Chebyshev test

TheoremLevel of the Chebyshev test#✓fully proved

If Tajima's numerator π - S / a₁ is square integrable with mean 0 and variance c₁ θ₀ + c₂ θ₀² > 0 (as under the standard neutral model, by KingmanTimes.integral_tajimaNumerator and KingmanTimes.variance_tajimaNumerator), then for every α > 0 the test rejects with probability at most α.

theorem measure_tajimaChebyshevTest_le {Ω : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω}
    [IsProbabilityMeasure μ] {n : ℕ} {π S : Ω → ℝ} {θ₀ α : ℝ} (hα : 0 < α)
    (hmem : MemLp (fun ω => π ω - S ω / tajimaA1 n) 2 μ)
    (hmean : μ[fun ω => π ω - S ω / tajimaA1 n] = 0)
    (hvar : Var[fun ω => π ω - S ω / tajimaA1 n; μ] = tajimaC1 n * θ₀ + tajimaC2 n * θ₀ ^ 2)
    (hpos : 0 < tajimaC1 n * θ₀ + tajimaC2 n * θ₀ ^ 2) :
    μ {ω | tajimaChebyshevTest n θ₀ α (π ω) (S ω)} ≤ ENNReal.ofReal α

Uses 4

Statement usesTajima's constant \(a_1\) · Tajima's constant \(c_1\) · Tajima's constant \(c_2\) · Chebyshev test of neutrality

10 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.