Principal component analysis

35 fully proved

Sample covariance

DefinitionSample mean of a data matrix column#✓fully proved

The sample mean of column j of an n × p data matrix (rows are observations). For n = 0 it is the junk value 0.

noncomputable def colMean (X : Matrix (Fin n) (Fin p) ℝ) (j : Fin p) : ℝ :=
  (∑ i, X i j) / n

Used by 4

Used byAllele-frequency estimate of a marker · Column-centered data matrix · Entries of the sample covariance matrix · Trace of the sample covariance is the total sample variance

DefinitionColumn-centered data matrix#✓fully proved

The column-centered data matrix X i j - x̄ⱼ.

noncomputable def center (X : Matrix (Fin n) (Fin p) ℝ) : Matrix (Fin n) (Fin p) ℝ :=
  Matrix.of fun i j => X i j - colMean X j

Uses 1 · Used by 9

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 · Unbiased sample covariance matrix · Sample covariance matrix is symmetric · Sample covariance matrix is positive semidefinite · Sample variance of scores is a quadratic form · Principal component scores · Centered columns sum to zero · Principal component scores have sample mean zero

DefinitionUnbiased sample covariance matrix#✓fully proved

The unbiased sample covariance matrix (n - 1)⁻¹ (X - x̄)ᵀ (X - x̄) of an n × p data matrix. The divisor needs 2 ≤ n; for n = 1 the factor is the junk value (0 : ℝ)⁻¹ = 0 (and for n = 0 the product is the zero matrix).

noncomputable def sampleCov (X : Matrix (Fin n) (Fin p) ℝ) : Matrix (Fin p) (Fin p) ℝ :=
  ((n : ℝ) - 1)⁻¹ • ((center X)ᵀ * center X)

Uses 1 · Used by 10

Statement usesColumn-centered data matrix

Used byEntries of the sample covariance matrix · Sample covariance matrix is symmetric · Sample covariance matrix is positive semidefinite · Sample variance of scores is a quadratic form · Trace of the sample covariance is the total sample variance · Proportion of variance explained by principal components · Proportion of variance explained is at most one · More components explain more variance · Proportion of variance explained is nonnegative · All components explain all of the variance

DefinitionPrincipal component scores#✓fully proved

The principal-component scores (X - x̄) w of the observations along a direction w.

noncomputable def scores (X : Matrix (Fin n) (Fin p) ℝ) (w : Fin p → ℝ) : Fin n → ℝ :=
  center X *ᵥ w

Uses 1 · Used by 2

Statement usesColumn-centered data matrix

Used bySample variance of scores is a quadratic form · Principal component scores have sample mean zero

TheoremCentered columns sum to zero#✓fully proved

The centered columns sum to zero (for at least one observation).

theorem sum_center (X : Matrix (Fin n) (Fin p) ℝ) (hn : 0 < n) (j : Fin p) :
    ∑ i, center X i j = 0

Uses 1 · Used by 2

Statement usesColumn-centered data matrix

Used byAll-ones vector lies in the kernel of the relatedness matrix · Principal component scores have sample mean zero

TheoremEntries of the sample covariance matrix#✓fully proved

Entries of the sample covariance matrix: Sⱼₖ = (n - 1)⁻¹ ∑ᵢ (Xᵢⱼ - x̄ⱼ)(Xᵢₖ - x̄ₖ).

theorem sampleCov_apply (X : Matrix (Fin n) (Fin p) ℝ) (j k : Fin p) :
    sampleCov X j k =
      ((n : ℝ) - 1)⁻¹ * ∑ i, (X i j - colMean X j) * (X i k - colMean X k)

Uses 2 · Used by 1

Statement usesSample mean of a data matrix column · Unbiased sample covariance matrix

Used byTrace of the sample covariance is the total sample variance

TheoremSample covariance matrix is symmetric#✓fully proved

The sample covariance matrix is symmetric.

theorem sampleCov_isHermitian (X : Matrix (Fin n) (Fin p) ℝ) : (sampleCov X).IsHermitian

Uses 2 · Used by 5

Statement usesUnbiased sample covariance matrix

Proof usesColumn-centered data matrix

Used byProportion of variance explained by principal components · Proportion of variance explained is at most one · More components explain more variance · Proportion of variance explained is nonnegative · All components explain all of the variance

TheoremSample covariance matrix is positive semidefinite#✓fully proved

The sample covariance matrix is positive semidefinite (for every n).

theorem sampleCov_posSemidef (X : Matrix (Fin n) (Fin p) ℝ) : (sampleCov X).PosSemidef

Uses 2 · Used by 3

Statement usesUnbiased sample covariance matrix

Proof usesColumn-centered data matrix

Used byProportion of variance explained is at most one · More components explain more variance · Proportion of variance explained is nonnegative

TheoremTrace of the sample covariance is the total sample variance#✓fully proved

The trace of the sample covariance matrix is the total sample variance, the sum of the column sample variances.

theorem trace_sampleCov (X : Matrix (Fin n) (Fin p) ℝ) :
    (sampleCov X).trace = ∑ j, ((n : ℝ) - 1)⁻¹ * ∑ i, (X i j - colMean X j) ^ 2

Uses 3

Statement usesSample mean of a data matrix column · Unbiased sample covariance matrix

Proof usesEntries of the sample covariance matrix

TheoremPrincipal component scores have sample mean zero#✓fully proved

The scores along any direction have sample mean zero.

theorem sum_scores (X : Matrix (Fin n) (Fin p) ℝ) (hn : 0 < n) (w : Fin p → ℝ) :
    ∑ i, scores X w i = 0

Uses 3

Statement usesPrincipal component scores

Proof usesColumn-centered data matrix · Centered columns sum to zero

TheoremSample variance of scores is a quadratic form#✓fully proved

The sample variance of the scores along w is the quadratic form wᵀ S w.

theorem sampleVar_scores (X : Matrix (Fin n) (Fin p) ℝ) (w : Fin p → ℝ) :
    ((n : ℝ) - 1)⁻¹ * ∑ i, scores X w i ^ 2 = w ⬝ᵥ sampleCov X *ᵥ w

Uses 3

Statement usesUnbiased sample covariance matrix · Principal component scores

Proof usesColumn-centered data matrix

Ordered spectral decomposition and the Rayleigh quotient

DefinitionEigenvalues of a symmetric matrix in decreasing order#✓fully proved

The eigenvalues λ₀ ≥ λ₁ ≥ ⋯ ≥ λ_{p-1} of a real symmetric p × p matrix, in decreasing order (Mathlib's LinearMap.IsSymmetric.eigenvalues of Matrix.toEuclideanLin S).

noncomputable def orderedEigenvalues (hS : S.IsHermitian) : Fin p → ℝ :=
  (isSymmetric_toEuclideanLin_iff.mpr hS).eigenvalues finrank_euclideanSpace_fin

Used by 16

Used byEigenvalues of the axes of variation · Quadratic form expanded in the ordered eigenbasis · Courant–Fischer min–max, matrix form · Courant–Fischer max–min, matrix form · Lower bound on the Rayleigh quotient for orthogonal directions · Ordered eigenbasis vectors are eigenvectors · Ordered eigenvalues are decreasing · Eigenvalues of a positive semidefinite matrix are nonnegative · Hotelling's characterization of the principal axes · Rayleigh quotient of an eigenvector is its eigenvalue · Ordered eigenvalues sum to the trace · Proportion of variance explained by principal components · Proportion of variance explained is at most one · More components explain more variance · Proportion of variance explained is nonnegative · All components explain all of the variance

DefinitionOrdered orthonormal eigenbasis of a symmetric matrix#✓fully proved

An orthonormal eigenbasis of a real symmetric matrix, ordered to match orderedEigenvalues; for a covariance matrix these are the principal axes.

noncomputable def orderedEigenbasis (hS : S.IsHermitian) :
    OrthonormalBasis (Fin p) ℝ (EuclideanSpace ℝ (Fin p)) :=
  (isSymmetric_toEuclideanLin_iff.mpr hS).eigenvectorBasis finrank_euclideanSpace_fin

Used by 7

Used byAxes of variation · Quadratic form expanded in the ordered eigenbasis · Lower bound on the Rayleigh quotient for orthogonal directions · Ordered eigenbasis vectors are eigenvectors · Eigenvalues of a positive semidefinite matrix are nonnegative · Hotelling's characterization of the principal axes · Rayleigh quotient of an eigenvector is its eigenvalue

DefinitionRayleigh quotient of a matrix#✓fully proved

The Rayleigh quotient wᵀ S w / wᵀ w of a real matrix (junk value 0 at w = 0).

noncomputable def rayleigh (S : Matrix (Fin p) (Fin p) ℝ) (w : Fin p → ℝ) : ℝ :=
  (w ⬝ᵥ S *ᵥ w) / (w ⬝ᵥ w)

Used by 5

Used byCourant–Fischer min–max, matrix form · Courant–Fischer max–min, matrix form · Lower bound on the Rayleigh quotient for orthogonal directions · Hotelling's characterization of the principal axes · Rayleigh quotient of an eigenvector is its eigenvalue

TheoremOrdered eigenvalues are decreasing#✓fully proved

The ordered eigenvalues are decreasing.

theorem orderedEigenvalues_antitone (hS : S.IsHermitian) : Antitone (orderedEigenvalues hS)

Uses 1 · Used by 2

Statement usesEigenvalues of a symmetric matrix in decreasing order

Used byLower bound on the Rayleigh quotient for orthogonal directions · Hotelling's characterization of the principal axes

TheoremOrdered eigenbasis vectors are eigenvectors#✓fully proved

The k-th basis vector is an eigenvector for the k-th eigenvalue.

theorem mulVec_orderedEigenbasis (hS : S.IsHermitian) (k : Fin p) :
    S *ᵥ ⇑(orderedEigenbasis hS k) = orderedEigenvalues hS k • ⇑(orderedEigenbasis hS k)

Uses 2 · Used by 1

Statement usesOrdered orthonormal eigenbasis of a symmetric matrix · Eigenvalues of a symmetric matrix in decreasing order

Used byEigenvalues of a positive semidefinite matrix are nonnegative

TheoremQuadratic form expanded in the ordered eigenbasis#✓fully proved

The quadratic form expanded in the ordered eigenbasis: xᵀ S x = ∑ λᵢ ⟪vᵢ, x⟫².

theorem dotProduct_mulVec_eq_sum (hS : S.IsHermitian) (x : EuclideanSpace ℝ (Fin p)) :
    (⇑x ⬝ᵥ S *ᵥ ⇑x) = ∑ i, orderedEigenvalues hS i * ⟪orderedEigenbasis hS i, x⟫_ℝ ^ 2

Uses 3 · Used by 3

Statement usesOrdered orthonormal eigenbasis of a symmetric matrix · Eigenvalues of a symmetric matrix in decreasing order

Proof usesEigenbasis expansion of the quadratic form of a self-adjoint operator

Used byLower bound on the Rayleigh quotient for orthogonal directions · Hotelling's characterization of the principal axes · Rayleigh quotient of an eigenvector is its eigenvalue

TheoremOrdered eigenvalues sum to the trace#✓fully proved

The ordered eigenvalues sum to the trace.

theorem sum_orderedEigenvalues (hS : S.IsHermitian) :
    ∑ i, orderedEigenvalues hS i = S.trace

Uses 1 · Used by 4

Statement usesEigenvalues of a symmetric matrix in decreasing order

Used byProportion of variance explained is at most one · More components explain more variance · Proportion of variance explained is nonnegative · All components explain all of the variance

TheoremEigenvalues of a positive semidefinite matrix are nonnegative#✓fully proved

The eigenvalues of a positive semidefinite matrix are nonnegative.

theorem orderedEigenvalues_nonneg (hS : S.PosSemidef) (k : Fin p) :
    0 ≤ orderedEigenvalues hS.isHermitian k

Uses 3 · Used by 3

Statement usesEigenvalues of a symmetric matrix in decreasing order

Proof usesOrdered eigenbasis vectors are eigenvectors · Ordered orthonormal eigenbasis of a symmetric matrix

Used byProportion of variance explained is at most one · More components explain more variance · Proportion of variance explained is nonnegative

TheoremRayleigh quotient of an eigenvector is its eigenvalue#✓fully proved

The Rayleigh quotient of the k-th eigenvector is the k-th eigenvalue.

theorem rayleigh_orderedEigenbasis (hS : S.IsHermitian) (k : Fin p) :
    rayleigh S ⇑(orderedEigenbasis hS k) = orderedEigenvalues hS k

Uses 4

Statement usesOrdered orthonormal eigenbasis of a symmetric matrix · Eigenvalues of a symmetric matrix in decreasing order · Rayleigh quotient of a matrix

Proof usesQuadratic form expanded in the ordered eigenbasis

TheoremHotelling's characterization of the principal axes#✓fully proved

On nonzero directions orthogonal to the first k eigenvectors, the Rayleigh quotient is at most the k-th eigenvalue; the bound is attained at the k-th eigenvector (rayleigh_orderedEigenbasis).

theorem rayleigh_le_of_orthogonal (hS : S.IsHermitian) (k : Fin p) (w : EuclideanSpace ℝ (Fin p))
    (hw : w ≠ 0) (horth : ∀ i : Fin p, i < k → ⟪orderedEigenbasis hS i, w⟫_ℝ = 0) :
    rayleigh S ⇑w ≤ orderedEigenvalues hS k

Uses 5

Statement usesOrdered orthonormal eigenbasis of a symmetric matrix · Eigenvalues of a symmetric matrix in decreasing order · Rayleigh quotient of a matrix

Proof usesQuadratic form expanded in the ordered eigenbasis · Ordered eigenvalues are decreasing

TheoremLower bound on the Rayleigh quotient for orthogonal directions#✓fully proved

Dual of rayleigh_le_of_orthogonal: on nonzero directions orthogonal to the eigenvectors after index k, the Rayleigh quotient is at least the k-th eigenvalue.

theorem le_rayleigh_of_orthogonal (hS : S.IsHermitian) (k : Fin p) (w : EuclideanSpace ℝ (Fin p))
    (hw : w ≠ 0) (horth : ∀ i : Fin p, k < i → ⟪orderedEigenbasis hS i, w⟫_ℝ = 0) :
    orderedEigenvalues hS k ≤ rayleigh S ⇑w

Uses 5

Statement usesOrdered orthonormal eigenbasis of a symmetric matrix · Eigenvalues of a symmetric matrix in decreasing order · Rayleigh quotient of a matrix

Proof usesQuadratic form expanded in the ordered eigenbasis · Ordered eigenvalues are decreasing

TheoremCourant–Fischer min–max, matrix form#✓fully proved

Every subspace of dimension p - k contains a nonzero vector whose Rayleigh quotient is at least λₖ.

theorem exists_le_rayleigh_of_finrank (hS : S.IsHermitian) (k : Fin p)
    (W : Submodule ℝ (EuclideanSpace ℝ (Fin p))) (hW : Module.finrank ℝ W = p - k) :
    ∃ w ∈ W, w ≠ 0 ∧ orderedEigenvalues hS k ≤ rayleigh S ⇑w

Uses 4

Statement usesEigenvalues of a symmetric matrix in decreasing order · Rayleigh quotient of a matrix

Proof usesCourant–Fischer min–max, lower-bound form · Rayleigh form of an operator

TheoremCourant–Fischer max–min, matrix form#✓fully proved

Every subspace of dimension k + 1 contains a nonzero vector whose Rayleigh quotient is at most λₖ.

theorem exists_rayleigh_le_of_finrank (hS : S.IsHermitian) (k : Fin p)
    (U : Submodule ℝ (EuclideanSpace ℝ (Fin p))) (hU : Module.finrank ℝ U = k + 1) :
    ∃ w ∈ U, w ≠ 0 ∧ rayleigh S ⇑w ≤ orderedEigenvalues hS k

Uses 4

Statement usesEigenvalues of a symmetric matrix in decreasing order · Rayleigh quotient of a matrix

Proof usesCourant–Fischer max–min, lower-bound form · Rayleigh form of an operator

Proportion of variance explained

DefinitionProportion of variance explained by principal components#✓fully proved

The proportion of total sample variance explained by the first k principal components: (λ₀ + ⋯ + λ_{k-1}) / tr S for the sample covariance matrix S. The junk value 0 is returned when the total variance tr S is 0 (constant data).

noncomputable def varianceExplained (X : Matrix (Fin n) (Fin p) ℝ) (k : ℕ) : ℝ :=
  (∑ i : Fin p with i.val < k, orderedEigenvalues (sampleCov_isHermitian X) i) /
    (sampleCov X).trace

Uses 3 · Used by 4

Statement usesEigenvalues of a symmetric matrix in decreasing order · Unbiased sample covariance matrix · Sample covariance matrix is symmetric

Used byProportion of variance explained is at most one · More components explain more variance · Proportion of variance explained is nonnegative · All components explain all of the variance

TheoremProportion of variance explained is nonnegative#✓fully proved

The proportion of variance explained is nonnegative.

theorem varianceExplained_nonneg (X : Matrix (Fin n) (Fin p) ℝ) (k : ℕ) :
    0 ≤ varianceExplained X k

Uses 7

Statement usesProportion of variance explained by principal components

Proof usesEigenvalues of a symmetric matrix in decreasing order · Eigenvalues of a positive semidefinite matrix are nonnegative · Unbiased sample covariance matrix · Sample covariance matrix is symmetric · Sample covariance matrix is positive semidefinite · Ordered eigenvalues sum to the trace

TheoremProportion of variance explained is at most one#✓fully proved

The proportion of variance explained is at most one.

theorem varianceExplained_le_one (X : Matrix (Fin n) (Fin p) ℝ) (k : ℕ) :
    varianceExplained X k ≤ 1

Uses 7

Statement usesProportion of variance explained by principal components

Proof usesEigenvalues of a symmetric matrix in decreasing order · Eigenvalues of a positive semidefinite matrix are nonnegative · Unbiased sample covariance matrix · Sample covariance matrix is symmetric · Sample covariance matrix is positive semidefinite · Ordered eigenvalues sum to the trace

TheoremMore components explain more variance#✓fully proved

Keeping more components explains more variance.

theorem varianceExplained_mono (X : Matrix (Fin n) (Fin p) ℝ) :
    Monotone (varianceExplained X)

Uses 7

Statement usesProportion of variance explained by principal components

Proof usesEigenvalues of a symmetric matrix in decreasing order · Eigenvalues of a positive semidefinite matrix are nonnegative · Unbiased sample covariance matrix · Sample covariance matrix is symmetric · Sample covariance matrix is positive semidefinite · Ordered eigenvalues sum to the trace

TheoremAll components explain all of the variance#✓fully proved

All p components explain all of the variance, when the total variance is positive.

theorem varianceExplained_of_le (X : Matrix (Fin n) (Fin p) ℝ) {k : ℕ} (hk : p ≤ k)
    (htr : 0 < (sampleCov X).trace) : varianceExplained X k = 1

Uses 5

Statement usesUnbiased sample covariance matrix · Proportion of variance explained by principal components

Proof usesEigenvalues of a symmetric matrix in decreasing order · Sample covariance matrix is symmetric · Ordered eigenvalues sum to the trace

Eckart–Young in the Frobenius norm

DefinitionRight singular vectors of a matrix#✓fully proved

Right singular vectors of A: an orthonormal eigenbasis of Aᵀ A, ordered so that the i-th vector has eigenvalue σᵢ² with σ₀ ≥ σ₁ ≥ ⋯ the singular values.

noncomputable def rightSingularBasis (A : Matrix (Fin m) (Fin n) ℝ) :
    OrthonormalBasis (Fin n) ℝ (EuclideanSpace ℝ (Fin n)) :=
  (Matrix.toEuclideanLin A).isSymmetric_adjoint_comp_self.eigenvectorBasis
    finrank_euclideanSpace_fin

Used by 4

Used byFrobenius error of the truncated SVD · Rank of the truncated SVD is at most k · Eckart–Young (Frobenius norm) · Truncated singular value decomposition

DefinitionTruncated singular value decomposition#✓fully proved

The rank-k truncated singular value decomposition A Vₖ Vₖᵀ = ∑_{i<k} σᵢ uᵢ vᵢᵀ, where Vₖ collects the first k right singular vectors.

noncomputable def truncSVD (A : Matrix (Fin m) (Fin n) ℝ) (k : ℕ) : Matrix (Fin m) (Fin n) ℝ :=
  A * ∑ i : Fin n with i.val < k,
    vecMulVec ⇑(rightSingularBasis A i) ⇑(rightSingularBasis A i)

Uses 1 · Used by 3

Statement usesRight singular vectors of a matrix

Used byFrobenius error of the truncated SVD · Eckart–Young, best-approximation form · Rank of the truncated SVD is at most k

TheoremRank of the truncated SVD is at most k#✓fully proved

The truncated SVD has rank at most k.

theorem rank_truncSVD_le (A : Matrix (Fin m) (Fin n) ℝ) (k : ℕ) : (truncSVD A k).rank ≤ k

Uses 2 · Used by 1

Statement usesTruncated singular value decomposition

Proof usesRight singular vectors of a matrix

Used byEckart–Young, best-approximation form

TheoremFrobenius error of the truncated SVD#✓fully proved

The squared Frobenius error of the truncated SVD is the sum of the discarded squared singular values.

theorem frobenius_sub_truncSVD_sq (A : Matrix (Fin m) (Fin n) ℝ) (k : ℕ) :
    ‖A - truncSVD A k‖ ^ 2 =
      ∑ i ∈ Finset.Ico k n, (Matrix.toEuclideanLin A).singularValues i ^ 2

Uses 2 · Used by 1

Statement usesTruncated singular value decomposition

Proof usesRight singular vectors of a matrix

Used byEckart–Young, best-approximation form

TheoremEckart–Young (Frobenius norm)#✓fully proved

Every matrix of rank at most k has squared Frobenius distance from A at least the sum of the discarded squared singular values.

theorem sum_sq_singularValues_le_frobenius_sub_sq (A : Matrix (Fin m) (Fin n) ℝ) {k : ℕ}
    (B : Matrix (Fin m) (Fin n) ℝ) (hB : B.rank ≤ k) :
    ∑ i ∈ Finset.Ico k n, (Matrix.toEuclideanLin A).singularValues i ^ 2 ≤ ‖A - B‖ ^ 2

Uses 1 · Used by 1

Proof usesRight singular vectors of a matrix

Used byEckart–Young, best-approximation form

TheoremEckart–Young, best-approximation form#✓fully proved

The truncated SVD is a best rank-k approximation of A in the Frobenius norm: the least squared distance from A to a matrix of rank at most k is ∑_{k ≤ i < n} σᵢ², attained by truncSVD A k.

theorem isLeast_frobenius_sub_sq (A : Matrix (Fin m) (Fin n) ℝ) (k : ℕ) :
    IsLeast {r | ∃ B : Matrix (Fin m) (Fin n) ℝ, B.rank ≤ k ∧ r = ‖A - B‖ ^ 2}
      (∑ i ∈ Finset.Ico k n, (Matrix.toEuclideanLin A).singularValues i ^ 2)

Uses 4

Proof usesFrobenius error of the truncated SVD · Rank of the truncated SVD is at most k · Eckart–Young (Frobenius norm) · Truncated singular value decomposition

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.