Principal-component correction for stratification

34 fully proved

Residualization on a span of axes

DefinitionResidualized vector after adjustment for a subspace#✓fully proved

The adjusted (residualized) y: the residual of the least-squares regression of y on the subspace V (y minus its orthogonal projection onto V).

noncomputable def adjusted (V : Submodule ℝ E) (y : E) : E :=
  y - V.starProjection y

Used by 15

Used byAdditivity of residualization · Stratification within the axis span does not change the residual · Residual as projection onto the orthogonal complement · Residual vanishes exactly on the subspace · Residuals lie in the orthogonal complement · Vectors orthogonal to the subspace are their own residuals · Homogeneity of residualization · Residual with respect to an orthonormal family of axes · EIGENSTRAT association statistic · Stratification in the axis span is removed · Nonnegativity of the EIGENSTRAT statistic · Genotypes in the axis span carry no signal after adjustment · Frisch–Waugh–Lovell theorem, existence · Frisch–Waugh–Lovell theorem, uniqueness · Residuals are orthogonal to every axis

TheoremResiduals lie in the orthogonal complement#✓fully proved

Residuals are orthogonal to the adjustment subspace.

theorem adjusted_mem_orthogonal (V : Submodule ℝ E) (y : E) : adjusted V y ∈ Vᗮ

Uses 1 · Used by 1

Statement usesResidualized vector after adjustment for a subspace

Used byResiduals are orthogonal to every axis

TheoremResiduals are orthogonal to every axis#✓fully proved

Residuals are orthogonal to every vector of the subspace, in particular to every axis.

theorem inner_adjusted_eq_zero (V : Submodule ℝ E) {v : E} (hv : v ∈ V) (y : E) :
    ⟪v, adjusted V y⟫_ℝ = 0

Uses 2

Statement usesResidualized vector after adjustment for a subspace

Proof usesResiduals lie in the orthogonal complement

TheoremResidual as projection onto the orthogonal complement#✓fully proved

The residual is the orthogonal projection onto Vᗮ.

theorem adjusted_eq_starProjection_orthogonal (V : Submodule ℝ E) (y : E) :
    adjusted V y = Vᗮ.starProjection y

Uses 1 · Used by 3

Statement usesResidualized vector after adjustment for a subspace

Used byAdditivity of residualization · Vectors orthogonal to the subspace are their own residuals · Homogeneity of residualization

TheoremAdditivity of residualization#✓fully proved

Residualization is additive.

theorem adjusted_add (V : Submodule ℝ E) (y z : E) :
    adjusted V (y + z) = adjusted V y + adjusted V z

Uses 2 · Used by 1

Statement usesResidualized vector after adjustment for a subspace

Proof usesResidual as projection onto the orthogonal complement

Used byStratification within the axis span does not change the residual

TheoremHomogeneity of residualization#✓fully proved

Residualization is homogeneous.

theorem adjusted_smul (V : Submodule ℝ E) (c : ℝ) (y : E) :
    adjusted V (c • y) = c • adjusted V y

Uses 2

Statement usesResidualized vector after adjustment for a subspace

Proof usesResidual as projection onto the orthogonal complement

TheoremResidual vanishes exactly on the subspace#✓fully proved

The residual vanishes exactly on the subspace.

theorem adjusted_eq_zero_iff (V : Submodule ℝ E) (y : E) : adjusted V y = 0 ↔ y ∈ V

Uses 1 · Used by 2

Statement usesResidualized vector after adjustment for a subspace

Used byStratification within the axis span does not change the residual · Genotypes in the axis span carry no signal after adjustment

TheoremStratification within the axis span does not change the residual#✓fully proved

Adding a vector of the subspace (stratification lying in the axis span) does not change the residual.

theorem adjusted_add_of_mem (V : Submodule ℝ E) {s : E} (hs : s ∈ V) (z : E) :
    adjusted V (s + z) = adjusted V z

Uses 3 · Used by 1

Statement usesResidualized vector after adjustment for a subspace

Proof usesAdditivity of residualization · Residual vanishes exactly on the subspace

Used byStratification in the axis span is removed

TheoremVectors orthogonal to the subspace are their own residuals#✓fully proved

Vectors orthogonal to the subspace are their own residuals: stratification outside the axis span is not removed.

theorem adjusted_of_mem_orthogonal (V : Submodule ℝ E) {y : E} (hy : y ∈ Vᗮ) :
    adjusted V y = y

Uses 2

Statement usesResidualized vector after adjustment for a subspace

Proof usesResidual as projection onto the orthogonal complement

TheoremResidual with respect to an orthonormal family of axes#✓fully proved

Regressing on an orthonormal family of axes one axis at a time gives the joint residual: y - ∑ₖ ⟪aₖ, y⟫ aₖ.

theorem adjusted_span_orthonormal {K : ℕ} (a : Fin K → E) (ha : Orthonormal ℝ a) (y : E) :
    adjusted (Submodule.span ℝ (Set.range a)) y = y - ∑ k, ⟪a k, y⟫_ℝ • a k

Uses 1

Statement usesResidualized vector after adjustment for a subspace

TheoremFrisch–Waugh–Lovell theorem, uniqueness#✓fully proved

Frisch–Waugh–Lovell, uniqueness: in any least-squares decomposition y = c + β g + e with c ∈ V and e ⊥ V ⊔ span {g}, the coefficient β is the coefficient of the regression of the residualized y on the residualized g, and the residual e is the residual of that regression.

theorem frischWaughLovell (V : Submodule ℝ E) (y g : E) (hg : adjusted V g ≠ 0) {c : E}
    (hc : c ∈ V) (β : ℝ) (he : y - c - β • g ∈ (V ⊔ Submodule.span ℝ {g})ᗮ) :
    β = ⟪adjusted V g, adjusted V y⟫_ℝ / ‖adjusted V g‖ ^ 2 ∧
      y - c - β • g = adjusted V y - β • adjusted V g

Uses 1

Statement usesResidualized vector after adjustment for a subspace

TheoremFrisch–Waugh–Lovell theorem, existence#✓fully proved

Frisch–Waugh–Lovell, existence: the coefficient of the residual-on-residual regression gives a least-squares decomposition of y on V ⊔ span {g}.

theorem exists_frischWaughLovell (V : Submodule ℝ E) (y g : E) :
    ∃ c ∈ V, y - c - (⟪adjusted V g, adjusted V y⟫_ℝ / ‖adjusted V g‖ ^ 2) • g ∈
      (V ⊔ Submodule.span ℝ {g})ᗮ

Uses 1

Statement usesResidualized vector after adjustment for a subspace

DefinitionEIGENSTRAT association statistic#✓fully proved

The EIGENSTRAT association statistic (N - K - 1) ⟪r_g, r_y⟫² / (‖r_g‖² ‖r_y‖²) of the adjusted genotype r_g and adjusted phenotype r_y: (N - K - 1) times their squared cosine, which is their squared sample correlation when both are centered (Price et al. 2006). When either adjusted vector is zero the ratio is the junk value 0.

noncomputable def chiSq (V : Submodule ℝ E) (K : ℕ) (y g : E) : ℝ :=
  ((N : ℝ) - K - 1) * (⟪adjusted V g, adjusted V y⟫_ℝ ^ 2 /
    (‖adjusted V g‖ ^ 2 * ‖adjusted V y‖ ^ 2))

Uses 1 · Used by 3

Statement usesResidualized vector after adjustment for a subspace

Used byStratification in the axis span is removed · Nonnegativity of the EIGENSTRAT statistic · Genotypes in the axis span carry no signal after adjustment

TheoremStratification in the axis span is removed#✓fully proved

Adding vectors of V to the phenotype and the genotype does not change the EIGENSTRAT statistic.

theorem chiSq_add_of_mem (V : Submodule ℝ E) (K : ℕ) {s t : E} (hs : s ∈ V) (ht : t ∈ V)
    (y g : E) : chiSq V K (s + y) (t + g) = chiSq V K y g

Uses 3

Statement usesEIGENSTRAT association statistic

Proof usesResidualized vector after adjustment for a subspace · Stratification within the axis span does not change the residual

TheoremNonnegativity of the EIGENSTRAT statistic#✓fully proved

The EIGENSTRAT statistic is nonnegative when K + 1 ≤ N.

theorem chiSq_nonneg (V : Submodule ℝ E) {K : ℕ} (hK : K + 1 ≤ N) (y g : E) :
    0 ≤ chiSq V K y g

Uses 2

Statement usesEIGENSTRAT association statistic

Proof usesResidualized vector after adjustment for a subspace

TheoremGenotypes in the axis span carry no signal after adjustment#✓fully proved

A genotype lying in the axis span carries no signal after adjustment (its residual is zero, and the statistic is the junk value 0 of the zero denominator).

theorem chiSq_of_mem (V : Submodule ℝ E) (K : ℕ) (y : E) {g : E} (hg : g ∈ V) :
    chiSq V K y g = 0

Uses 3

Statement usesEIGENSTRAT association statistic

Proof usesResidualized vector after adjustment for a subspace · Residual vanishes exactly on the subspace

Patterson normalization and the axes of variation

DefinitionAllele-frequency estimate of a marker#✓fully proved

The allele-frequency estimate p̂ⱼ = μⱼ / 2 of marker j, where μⱼ is the mean variant-allele count of column j (autosomal diploid data, counts in {0, 1, 2}).

noncomputable def alleleFreq (C : Matrix (Fin N) (Fin M) ℝ) (j : Fin M) : ℝ :=
  colMean C j / 2

Uses 1 · Used by 2

Statement usesSample mean of a data matrix column

Used byPatterson's normalized genotype matrix · All-ones vector lies in the kernel of the relatedness matrix

DefinitionPatterson's normalized genotype matrix#✓fully proved

Patterson's normalized genotype matrix (C i j - μⱼ) / √(p̂ⱼ (1 - p̂ⱼ)). For a monomorphic marker (p̂ⱼ ∈ {0, 1}) the denominator is 0 and the column is the junk value 0; Patterson et al. use polymorphic markers only.

noncomputable def normalizedGenotype (C : Matrix (Fin N) (Fin M) ℝ) : Matrix (Fin N) (Fin M) ℝ :=
  Matrix.of fun i j => center C i j / √(alleleFreq C j * (1 - alleleFreq C j))

Uses 2 · Used by 3

Statement usesAllele-frequency estimate of a marker · Column-centered data matrix

Used byPatterson's relatedness matrix · All-ones vector lies in the kernel of the relatedness matrix · Patterson's relatedness matrix is positive semidefinite

DefinitionPatterson's relatedness matrix#✓fully proved

Patterson's N × N matrix Ψ = M Mᵀ / (number of markers) of the normalized genotypes, whose top eigenvectors are the axes of variation.

noncomputable def relatednessMatrix (C : Matrix (Fin N) (Fin M) ℝ) : Matrix (Fin N) (Fin N) ℝ :=
  (M : ℝ)⁻¹ • (normalizedGenotype C * (normalizedGenotype C)ᵀ)

Uses 1 · Used by 4

Statement usesPatterson's normalized genotype matrix

Used byAxes of variation · Eigenvalues of the axes of variation · All-ones vector lies in the kernel of the relatedness matrix · Patterson's relatedness matrix is positive semidefinite

TheoremPatterson's relatedness matrix is positive semidefinite#✓fully proved

Patterson's matrix Ψ is positive semidefinite.

theorem relatednessMatrix_posSemidef (C : Matrix (Fin N) (Fin M) ℝ) :
    (relatednessMatrix C).PosSemidef

Uses 2 · Used by 2

Statement usesPatterson's relatedness matrix

Proof usesPatterson's normalized genotype matrix

Used byAxes of variation · Eigenvalues of the axes of variation

TheoremAll-ones vector lies in the kernel of the relatedness matrix#✓fully proved

The all-ones vector is in the kernel of Ψ (columns of the normalized matrix are centered), so at most N - 1 eigenvalues are nonzero.

theorem relatednessMatrix_mulVec_one (C : Matrix (Fin N) (Fin M) ℝ) (hN : 0 < N) :
    relatednessMatrix C *ᵥ 1 = 0

Uses 5

Statement usesPatterson's relatedness matrix

Proof usesAllele-frequency estimate of a marker · Patterson's normalized genotype matrix · Column-centered data matrix · Centered columns sum to zero

DefinitionAxes of variation#✓fully proved

The axes of variation: an orthonormal eigenbasis of Ψ, in decreasing eigenvalue order.

noncomputable def axes (C : Matrix (Fin N) (Fin M) ℝ) :
    OrthonormalBasis (Fin N) ℝ (EuclideanSpace ℝ (Fin N)) :=
  orderedEigenbasis (relatednessMatrix_posSemidef C).isHermitian

Uses 3 · Used by 3

Statement usesPatterson's relatedness matrix · Patterson's relatedness matrix is positive semidefinite · Ordered orthonormal eigenbasis of a symmetric matrix

Used byEach top axis lies in the span of the top axes · Dimension of the span of the top axes · Span of the top axes of variation

DefinitionEigenvalues of the axes of variation#✓fully proved

The eigenvalues of Ψ in decreasing order, matching axes.

noncomputable def axisEigenvalues (C : Matrix (Fin N) (Fin M) ℝ) : Fin N → ℝ :=
  orderedEigenvalues (relatednessMatrix_posSemidef C).isHermitian

Uses 3

Statement usesPatterson's relatedness matrix · Patterson's relatedness matrix is positive semidefinite · Eigenvalues of a symmetric matrix in decreasing order

DefinitionSpan of the top axes of variation#✓fully proved

The span of the top K axes of variation, the subspace EIGENSTRAT adjusts for.

noncomputable def topAxesSpan (C : Matrix (Fin N) (Fin M) ℝ) (K : ℕ) :
    Submodule ℝ (EuclideanSpace ℝ (Fin N)) :=
  Submodule.span ℝ (axes C '' {i | i.val < K})

Uses 1 · Used by 2

Statement usesAxes of variation

Used byEach top axis lies in the span of the top axes · Dimension of the span of the top axes

TheoremEach top axis lies in the span of the top axes#✓fully proved

Each of the top K axes lies in their span.

theorem axes_mem_topAxesSpan (C : Matrix (Fin N) (Fin M) ℝ) {K : ℕ} {i : Fin N} (hi : i.val < K) :
    axes C i ∈ topAxesSpan C K

Uses 2

Statement usesAxes of variation · Span of the top axes of variation

TheoremDimension of the span of the top axes#✓fully proved

The top K axes span a K-dimensional subspace.

theorem finrank_topAxesSpan (C : Matrix (Fin N) (Fin M) ℝ) {K : ℕ} (hK : K ≤ N) :
    Module.finrank ℝ (topAxesSpan C K) = K

Uses 2

Statement usesSpan of the top axes of variation

Proof usesAxes of variation

Number of significant axes

DefinitionSequential count of significant axes#✓fully proved

Patterson's sequential count of significant axes: among the first K statistics, the length of the leading run of statistics exceeding the threshold t (testing stops at the first non-significant one).

noncomputable def numSignificant (stat : ℕ → ℝ) (t : ℝ) : ℕ → ℕ
  | 0 => 0
  | K + 1 => open Classical in
      if numSignificant stat t K = K ∧ t < stat K then K + 1 else numSignificant stat t K

Used by 7

Used byCharacterization of the axes counted as significant · Significant axes have statistics above the threshold · Conditional error bound · Count of significant axes decreases with the threshold · Significant-axis count for decreasing statistics · At most K axes are declared significant · Criterion for at least one significant axis

TheoremAt most K axes are declared significant#✓fully proved

At most K axes are declared significant.

theorem numSignificant_le (stat : ℕ → ℝ) (t : ℝ) (K : ℕ) : numSignificant stat t K ≤ K

Uses 1 · Used by 1

Statement usesSequential count of significant axes

Used byCharacterization of the axes counted as significant

TheoremCharacterization of the axes counted as significant#✓fully proved

The first numSignificant stat t K indices are exactly those k < K whose statistics and all earlier ones exceed the threshold.

theorem lt_numSignificant_iff {stat : ℕ → ℝ} {t : ℝ} {K k : ℕ} :
    k < numSignificant stat t K ↔ k < K ∧ ∀ i ≤ k, t < stat i

Uses 2 · Used by 4

Statement usesSequential count of significant axes

Proof usesAt most K axes are declared significant

Used bySignificant axes have statistics above the threshold · Count of significant axes decreases with the threshold · Significant-axis count for decreasing statistics · Criterion for at least one significant axis

TheoremSignificant axes have statistics above the threshold#✓fully proved

Every axis counted as significant has a statistic above the threshold.

theorem lt_stat_of_lt_numSignificant {stat : ℕ → ℝ} {t : ℝ} {K k : ℕ}
    (h : k < numSignificant stat t K) : t < stat k

Uses 2 · Used by 1

Statement usesSequential count of significant axes

Proof usesCharacterization of the axes counted as significant

Used byConditional error bound

TheoremCriterion for at least one significant axis#✓fully proved

At least one axis is significant iff the leading statistic exceeds the threshold.

theorem numSignificant_pos_iff {stat : ℕ → ℝ} {t : ℝ} {K : ℕ} :
    0 < numSignificant stat t K ↔ 0 < K ∧ t < stat 0

Uses 2

Statement usesSequential count of significant axes

Proof usesCharacterization of the axes counted as significant

TheoremCount of significant axes decreases with the threshold#✓fully proved

A higher threshold declares no more axes significant.

theorem numSignificant_antitone {stat : ℕ → ℝ} {t t' : ℝ} (htt : t ≤ t') (K : ℕ) :
    numSignificant stat t' K ≤ numSignificant stat t K

Uses 2

Statement usesSequential count of significant axes

Proof usesCharacterization of the axes counted as significant

TheoremSignificant-axis count for decreasing statistics#✓fully proved

For decreasing statistics (such as ordered eigenvalues compared with a fixed threshold) the sequential count is the number of statistics above the threshold.

theorem numSignificant_eq_card_of_antitone {stat : ℕ → ℝ} (h : Antitone stat) (t : ℝ) (K : ℕ) :
    numSignificant stat t K = ((Finset.range K).filter fun k => t < stat k).card

Uses 2

Statement usesSequential count of significant axes

Proof usesCharacterization of the axes counted as significant

TheoremConditional error bound#✓fully proved

If, under the null hypothesis, the k-th statistic exceeds t with probability at most 1 - F t (the Tracy–Widom approximation with F the TW₁ distribution function, taken here as a hypothesis), then the rule declares more than k significant axes with probability at most 1 - F t.

theorem measure_lt_numSignificant_le {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (stat : Ω → ℕ → ℝ) (F : ℝ → ℝ) (t : ℝ) (K k : ℕ)
    (hnull : P {ω | t < stat ω k} ≤ ENNReal.ofReal (1 - F t)) :
    P {ω | k < numSignificant (stat ω) t K} ≤ ENNReal.ofReal (1 - F t)

Uses 2

Statement usesSequential count of significant axes

Proof usesSignificant axes have statistics above the threshold

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.