Permutation tests

DefinitionPermutation p-value#✓fully proved

The permutation (group-invariance) p-value of the statistic T at ω: the fraction of group elements g with T (g • ω) ≥ T ω.

noncomputable def permutationPValue (T : Ω → ℝ) (ω : Ω) : ℝ :=
  ((Finset.univ.filter fun g : G => T ω ≤ T (g • ω)).card : ℝ) / Fintype.card G

Used by 1

Used byValidity of permutation p-values

TheoremCounting lemma for rank counts#✓fully proved

Counting lemma: for any family of reals t indexed by G and any k, at most k elements h have rank count #{g | t h ≤ t g} at most k.

theorem card_filter_rankCount_le (t : G → ℝ) (k : ℕ) :
    (Finset.univ.filter fun h : G =>
        (Finset.univ.filter fun g : G => t h ≤ t g).card ≤ k).card ≤ k

Used by 2

Used byValidity of Monte Carlo permutation p-values · Validity of permutation p-values

TheoremValidity of permutation p-values#✓fully proved

Lehmann and Romano (2005), §15.2; Hemerik and Goeman (2018): if the law μ is invariant under the action of a finite group G, the permutation p-value of any measurable statistic is valid.

theorem isValidPValue_permutationPValue (μ : Measure Ω) [IsProbabilityMeasure μ]
    [SMulInvariantMeasure G Ω μ] (hsmul : ∀ g : G, Measurable fun ω : Ω => g • ω)
    {T : Ω → ℝ} (hT : Measurable T) :
    IsValidPValue μ (permutationPValue G T)

Uses 3

Statement usesValid p-value · Permutation p-value

Proof usesCounting lemma for rank counts

DefinitionMonte Carlo permutation p-value#✓fully proved

The Monte Carlo permutation p-value (1 + #{b | T(g_b • ω) ≥ T(ω)}) / (B + 1) of the statistic T at the data ω with the B drawn group elements g.

noncomputable def monteCarloPermutationPValue {B : ℕ} (T : Ω → ℝ) (ω : Ω) (g : Fin B → G) :
    ℝ :=
  (1 + ((Finset.univ.filter fun b => T ω ≤ T (g b • ω)).card : ℝ)) / (B + 1)

Used by 1

Used byValidity of Monte Carlo permutation p-values

TheoremValidity of Monte Carlo permutation p-values#✓fully proved

Phipson and Smyth (2010); Hemerik and Goeman (2018): if the null law μ is invariant under a finite group G and g₁, …, g_B are drawn independently and uniformly from G, independently of the data, then (1 + #{b | T(g_b • ω) ≥ T(ω)}) / (B + 1) is a valid p-value under the joint law.

theorem isValidPValue_monteCarloPermutationPValue [Finite G] [MeasurableSpace G]
    [DiscreteMeasurableSpace G] (B : ℕ) (μ : Measure Ω) [IsProbabilityMeasure μ]
    [SMulInvariantMeasure G Ω μ] (hsmul : ∀ g : G, Measurable fun ω : Ω => g • ω) {T : Ω → ℝ}
    (hT : Measurable T) :
    IsValidPValue (μ.prod (Measure.pi fun _ : Fin B => uniformOn (Set.univ : Set G)))
      (fun x => monteCarloPermutationPValue T x.1 x.2)

Uses 3

Statement usesValid p-value · Monte Carlo permutation p-value

Proof usesCounting lemma for rank counts

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.