Ewens–Watterson test

DefinitionNumber of permutations with a given cycle type#✓fully proved

The number of permutations of n letters with cycle type π, w(π) = n! / ∏ j, j ^ (a j) * (a j)! with a j = π.parts.count j (Cauchy's formula).

def cycleTypeWeight (π : n.Partition) : ℝ :=
  (n.factorial : ℝ) /
    ∏ j ∈ π.parts.toFinset, ((j : ℝ) ^ π.parts.count j * ((π.parts.count j).factorial : ℝ))

Used by 9

Used byConditional upper-tail p-value of the Ewens–Watterson test · Positivity of the cycle-type weight · K is sufficient for θ · The Ewens–Watterson conditional law · Factorization of the Ewens sampling formula · Law of the number of alleles · Validity of the Ewens–Watterson test · Conditional validity of the Ewens–Watterson test · Cauchy's count by number of cycles

DefinitionProbability of a given number of alleles under the Ewens formula#✓fully proved

The probability P_θ(K = k) that a sample of n genes carries exactly k distinct alleles under the Ewens sampling formula.

def numAllelesProb (θ : ℝ) (n k : ℕ) : ℝ :=
  ∑ π : n.Partition with π.parts.card = k, ewensProb θ π

Uses 1 · Used by 4

Statement usesEwens sampling formula

Used byEwens conditional probability given the number of alleles · K is sufficient for θ · Law of the number of alleles · Validity of the Ewens–Watterson test

DefinitionEwens conditional probability given the number of alleles#✓fully proved

The conditional probability of the allelic partition π given that the number of alleles is K = K(π) = π.parts.card, under the Ewens sampling formula with parameter θ.

def ewensCondProb (θ : ℝ) (π : n.Partition) : ℝ :=
  ewensProb θ π / numAllelesProb θ n π.parts.card

Uses 2 · Used by 4

Statement usesEwens sampling formula · Probability of a given number of alleles under the Ewens formula

Used byK is sufficient for θ · The Ewens–Watterson conditional law · Validity of the Ewens–Watterson test · Conditional validity of the Ewens–Watterson test

DefinitionConditional upper-tail p-value of the Ewens–Watterson test#✓fully proved

The conditional upper-tail p-value of a statistic T of the allelic partition: the conditional probability, given the observed number of alleles K(π), that T is at least its observed value T π. It is written with the cycle-type weights and so does not involve θ (by ewensCondProb_eq it is the conditional tail probability for every θ > 0).

def condUpperPValue (T : n.Partition → ℝ) (π : n.Partition) : ℝ :=
  (∑ π' : n.Partition with π'.parts.card = π.parts.card ∧ T π ≤ T π', cycleTypeWeight π') /
    ∑ π' : n.Partition with π'.parts.card = π.parts.card, cycleTypeWeight π'

Uses 1 · Used by 2

Statement usesNumber of permutations with a given cycle type

Used byValidity of the Ewens–Watterson test · Conditional validity of the Ewens–Watterson test

DefinitionSample homozygosity of an allelic partition#✓fully proved

The sample homozygosity F(π) = ∑_i (n_i / n)², the sum over the alleles of the squared sample frequencies (Watterson 1978); n_i ranges over the parts of π.

def homozygosity (π : n.Partition) : ℝ :=
  (π.parts.map fun j : ℕ => ((j : ℝ) / n) ^ 2).sum

TheoremPositivity of the cycle-type weight#✓fully proved

The cycle-type weight is positive.

theorem cycleTypeWeight_pos (π : n.Partition) : 0 < cycleTypeWeight π

Uses 1 · Used by 2

Statement usesNumber of permutations with a given cycle type

Used byValidity of the Ewens–Watterson test · Conditional validity of the Ewens–Watterson test

TheoremFactorization of the Ewens sampling formula#✓fully proved

Factorization of the Ewens sampling formula (Ewens 1972): P_θ(π) = θ ^ K(π) / θ^{(n)} * w(π), with K(π) = π.parts.card the number of alleles.

theorem ewensProb_eq_mul_cycleTypeWeight (θ : ℝ) (π : n.Partition) :
    ewensProb θ π = θ ^ π.parts.card / (ascPochhammer ℝ n).eval θ * cycleTypeWeight π

Uses 2 · Used by 4

Statement usesNumber of permutations with a given cycle type · Ewens sampling formula

Used byK is sufficient for θ · Law of the number of alleles · Validity of the Ewens–Watterson test · Cauchy's count by number of cycles

TheoremK is sufficient for θ#✓fully proved

K is sufficient for θ (Ewens 1972): for θ > 0, the conditional law of the allelic partition given the number of alleles is w(π) / ∑_{K(π') = K(π)} w(π'), which does not depend on θ.

theorem ewensCondProb_eq {θ : ℝ} (hθ : 0 < θ) (π : n.Partition) :
    ewensCondProb θ π =
      cycleTypeWeight π /
        ∑ π' : n.Partition with π'.parts.card = π.parts.card, cycleTypeWeight π'

Uses 5 · Used by 2

Statement usesNumber of permutations with a given cycle type · Ewens conditional probability given the number of alleles

Proof usesEwens sampling formula · Factorization of the Ewens sampling formula · Probability of a given number of alleles under the Ewens formula

Used byThe Ewens–Watterson conditional law · Conditional validity of the Ewens–Watterson test

TheoremCauchy's count by number of cycles#✓fully proved

The cycle-type weights of the partitions of n into k parts sum to the unsigned Stirling number of the first kind |s(n, k)|.

theorem sum_cycleTypeWeight_eq_stirlingFirst (n k : ℕ) :
    ∑ π : n.Partition with π.parts.card = k, cycleTypeWeight π = (n.stirlingFirst k : ℝ)

Uses 4 · Used by 2

Statement usesNumber of permutations with a given cycle type

Proof usesEwens sampling formula · Factorization of the Ewens sampling formula · The Ewens sampling formula is a probability distribution

Used byThe Ewens–Watterson conditional law · Law of the number of alleles

TheoremLaw of the number of alleles#✓fully proved

Law of the number of alleles (Ewens 1972): P_θ(K = k) = |s(n, k)| θ ^ k / θ^{(n)}. As an identity between the defining sums it holds for every real θ; it is a probability for θ > 0.

theorem numAllelesProb_eq (θ : ℝ) (n k : ℕ) :
    numAllelesProb θ n k = (n.stirlingFirst k : ℝ) * θ ^ k / (ascPochhammer ℝ n).eval θ

Uses 5

Statement usesProbability of a given number of alleles under the Ewens formula

Proof usesNumber of permutations with a given cycle type · Ewens sampling formula · Factorization of the Ewens sampling formula · Cauchy's count by number of cycles

TheoremThe Ewens–Watterson conditional law#✓fully proved

The Ewens–Watterson conditional law (Ewens 1972; Watterson 1978): for θ > 0, P(π | K = K(π)) = w(π) / |s(n, K(π))| = n! / (|s(n, k)| ∏ j, j ^ (a j) (a j)!).

theorem ewensCondProb_eq_stirlingFirst {θ : ℝ} (hθ : 0 < θ) (π : n.Partition) :
    ewensCondProb θ π = cycleTypeWeight π / (n.stirlingFirst π.parts.card : ℝ)

Uses 4

Statement usesNumber of permutations with a given cycle type · Ewens conditional probability given the number of alleles

Proof usesK is sufficient for θ · Cauchy's count by number of cycles

TheoremValidity of a discrete upper-tail p-value#✓fully proved

For nonnegative masses q on a finite set s and a statistic T, the upper-tail p-value p x = ∑_{y ∈ s, T x ≤ T y} q y satisfies ∑_{x ∈ s, p x ≤ t} q x ≤ t for every t ≥ 0.

theorem sum_upperTail_le {ι : Type*} (s : Finset ι) (q T : ι → ℝ) (hq : ∀ i ∈ s, 0 ≤ q i)
    {t : ℝ} (ht : 0 ≤ t) :
    ∑ x ∈ s with ∑ y ∈ s with T x ≤ T y, q y ≤ t, q x ≤ t

Used by 1

Used byConditional validity of the Ewens–Watterson test

TheoremConditional validity of the Ewens–Watterson test#✓fully proved

For θ > 0, every number of alleles k and every level t ≥ 0, the conditional probability given K = k that the conditional upper-tail p-value of T is at most t is at most t.

theorem sum_condUpperPValue_le_cond {θ : ℝ} (hθ : 0 < θ) (T : n.Partition → ℝ) (k : ℕ)
    {t : ℝ} (ht : 0 ≤ t) :
    ∑ π : n.Partition with π.parts.card = k ∧ condUpperPValue T π ≤ t, ewensCondProb θ π ≤ t

Uses 6 · Used by 1

Statement usesConditional upper-tail p-value of the Ewens–Watterson test · Ewens conditional probability given the number of alleles

Proof usesNumber of permutations with a given cycle type · Positivity of the cycle-type weight · K is sufficient for θ · Validity of a discrete upper-tail p-value

Used byValidity of the Ewens–Watterson test

TheoremValidity of the Ewens–Watterson test#✓fully proved

Validity of the Ewens–Watterson test (Watterson 1978): for every θ > 0 and every level t ≥ 0, the Ewens probability that the conditional upper-tail p-value of T is at most t is at most t. With T = homozygosity this is the test against excess homozygosity, with T = -homozygosity the test against a deficit of homozygosity.

theorem sum_condUpperPValue_le {θ : ℝ} (hθ : 0 < θ) (T : n.Partition → ℝ) {t : ℝ}
    (ht : 0 ≤ t) :
    ∑ π : n.Partition with condUpperPValue T π ≤ t, ewensProb θ π ≤ t

Uses 9

Statement usesConditional upper-tail p-value of the Ewens–Watterson test · Ewens sampling formula

Proof usesNumber of permutations with a given cycle type · Positivity of the cycle-type weight · Ewens conditional probability given the number of alleles · Factorization of the Ewens sampling formula · Probability of a given number of alleles under the Ewens formula · Conditional validity of the Ewens–Watterson test · The Ewens sampling formula is a probability distribution

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.