Probabilistic principal component analysis

TheoremThe transpose of a real matrix is its adjoint#✓fully proved

For every real \(d \times q\) matrix \(W\) and all \(z \in \mathbb{R}^q\) and \(t \in \mathbb{R}^d\), the Euclidean inner products satisfy \(\langle Wz, t\rangle = \langle z, W^\top t\rangle\).

theorem inner_toEuclideanLin (W : Matrix (Fin d) (Fin q) ℝ) (t : EuclideanSpace ℝ (Fin d))
    (z : EuclideanSpace ℝ (Fin q)) :
    ⟪toEuclideanLin W z, t⟫ = ⟪z, toEuclideanLin Wᵀ t⟫

Used by 1

Used byCharacteristic function of a linear image

TheoremCharacteristic function of a linear image#✓fully proved

Let \(\mu\) be a measure on \(\mathbb{R}^q\) and \(W\) a real \(d \times q\) matrix, and write \(\varphi_\nu(t) = \int e^{i\langle x, t\rangle}\,d\nu(x)\) for the characteristic function of a measure \(\nu\). Then the pushforward \(W_*\mu\) of \(\mu\) under \(z \mapsto Wz\) satisfies \(\varphi_{W_*\mu}(t) = \varphi_\mu(W^\top t)\) for every \(t \in \mathbb{R}^d\).

theorem charFun_map_toEuclideanLin (μ : Measure (EuclideanSpace ℝ (Fin q)))
    (W : Matrix (Fin d) (Fin q) ℝ) (t : EuclideanSpace ℝ (Fin d)) :
    charFun (μ.map (toEuclideanLin W)) t = charFun μ (toEuclideanLin Wᵀ t)

Uses 1 · Used by 1

Proof usesThe transpose of a real matrix is its adjoint

Used byThe marginal of probabilistic PCA and factor analysis is Gaussian

TheoremThe marginal of probabilistic PCA and factor analysis is Gaussian#✓fully proved

Let \(Z\) and \(E\) be independent random vectors on a probability space, with values in \(\mathbb{R}^q\) and \(\mathbb{R}^d\), such that \(Z\) has the standard Gaussian law \(N(0, I_q)\) and \(E\) has law \(N(0, \Psi)\) for a positive semidefinite real \(d \times d\) matrix \(\Psi\). Then for every real \(d \times q\) matrix \(W\) and every \(\mu \in \mathbb{R}^d\), the random vector \(WZ + \mu + E\) has law \(N(\mu, WW^\top + \Psi)\).

This is the marginal of Tipping and Bishop's model: probabilistic PCA is the case \(\Psi = \sigma^2 I\), factor analysis the case of a diagonal \(\Psi\).

theorem map_eq_multivariateGaussian {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
    [IsProbabilityMeasure P] {Z : Ω → EuclideanSpace ℝ (Fin q)} {E : Ω → EuclideanSpace ℝ (Fin d)}
    {Ψ : Matrix (Fin d) (Fin d) ℝ} (hZ : HasLaw Z (stdGaussian _) P)
    (hE : HasLaw E (multivariateGaussian 0 Ψ) P) (hΨ : Ψ.PosSemidef) (hind : IndepFun Z E P)
    (W : Matrix (Fin d) (Fin q) ℝ) (μ : EuclideanSpace ℝ (Fin d)) :
    P.map (fun ω => toEuclideanLin W (Z ω) + μ + E ω) = multivariateGaussian μ (W * Wᵀ + Ψ)

Uses 1 · Used by 2

Proof usesCharacteristic function of a linear image

Used byThe factor-analysis marginal · The probabilistic PCA marginal

TheoremThe probabilistic PCA marginal#✓fully proved

Let \(Z\) and \(E\) be independent random vectors on a probability space, with values in \(\mathbb{R}^q\) and \(\mathbb{R}^d\), such that \(Z\) has the standard Gaussian law \(N(0, I_q)\) and \(E\) has the isotropic law \(N(0, \sigma^2 I_d)\) for a real \(\sigma^2 \ge 0\). Then for every real \(d \times q\) matrix \(W\) and every \(\mu \in \mathbb{R}^d\), the random vector \(WZ + \mu + E\) has law \(N(\mu, WW^\top + \sigma^2 I_d)\).

theorem ppca_map_eq {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
    {Z : Ω → EuclideanSpace ℝ (Fin q)} {E : Ω → EuclideanSpace ℝ (Fin d)} {σ2 : ℝ} (hσ : 0 ≤ σ2)
    (hZ : HasLaw Z (stdGaussian _) P) (hE : HasLaw E (multivariateGaussian 0 (σ2 • 1)) P)
    (hind : IndepFun Z E P) (W : Matrix (Fin d) (Fin q) ℝ) (μ : EuclideanSpace ℝ (Fin d)) :
    P.map (fun ω => toEuclideanLin W (Z ω) + μ + E ω) = multivariateGaussian μ (W * Wᵀ + σ2 • 1)

Uses 1 · Used by 1

Proof usesThe marginal of probabilistic PCA and factor analysis is Gaussian

Used byThe density of the probabilistic PCA observation

TheoremThe factor-analysis marginal#✓fully proved

Let \(Z\) and \(E\) be independent random vectors on a probability space, with values in \(\mathbb{R}^q\) and \(\mathbb{R}^d\), such that \(Z\) has the standard Gaussian law \(N(0, I_q)\) and \(E\) has law \(N(0, \operatorname{diag}\psi)\) for a vector \(\psi \in \mathbb{R}^d\) with \(\psi_i \ge 0\) for all \(i\). Then for every real \(d \times q\) matrix \(W\) and every \(\mu \in \mathbb{R}^d\), the random vector \(WZ + \mu + E\) has law \(N(\mu, WW^\top + \operatorname{diag}\psi)\).

theorem factorAnalysis_map_eq {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
    [IsProbabilityMeasure P] {Z : Ω → EuclideanSpace ℝ (Fin q)} {E : Ω → EuclideanSpace ℝ (Fin d)}
    {ψ : Fin d → ℝ} (hψ : ∀ i, 0 ≤ ψ i) (hZ : HasLaw Z (stdGaussian _) P)
    (hE : HasLaw E (multivariateGaussian 0 (diagonal ψ)) P) (hind : IndepFun Z E P)
    (W : Matrix (Fin d) (Fin q) ℝ) (μ : EuclideanSpace ℝ (Fin d)) :
    P.map (fun ω => toEuclideanLin W (Z ω) + μ + E ω) =
      multivariateGaussian μ (W * Wᵀ + diagonal ψ)

Uses 1

Proof usesThe marginal of probabilistic PCA and factor analysis is Gaussian

DefinitionProbabilistic PCA covariance#✓fully proved

For a real \(d \times q\) matrix \(W\) and a real number \(\sigma^2\), the probabilistic PCA covariance is the \(d \times d\) matrix \(W W^\top + \sigma^2 I\).

def ppcaCov (W : Matrix (Fin d) (Fin q) ℝ) (σ2 : ℝ) : Matrix (Fin d) (Fin d) ℝ :=
  W * Wᵀ + σ2 • 1

Used by 7

Used byProbabilistic PCA MLE when the sample covariance has the model form · Probabilistic PCA log-likelihood · The probabilistic PCA likelihood is at most the unconstrained Gaussian maximum · The mean MLE is the sample mean · The log-likelihood of no data is zero · No latent factors: the noise-variance MLE is the average sample variance · The density of the probabilistic PCA observation

TheoremThe density of the probabilistic PCA observation#✓fully proved

Let \(z\) and \(\varepsilon\) be independent random vectors on a probability space, with \(z\) standard Gaussian in \(\mathbb{R}^q\) and \(\varepsilon\) Gaussian in \(\mathbb{R}^d\) with mean \(0\) and covariance \(\sigma^2 I\), where \(\sigma^2 > 0\). Then for every real \(d \times q\) matrix \(W\) and every \(\mu \in \mathbb{R}^d\), the law of \(x = W z + \mu + \varepsilon\) has density \(\mathcal{N}(x \mid \mu, W W^\top + \sigma^2 I)\) with respect to Lebesgue measure on \(\mathbb{R}^d\), where \(\mathcal{N}(x \mid \mu, \Sigma)\) is the multivariate Gaussian density with mean \(\mu\) and covariance \(\Sigma\).

theorem ppca_map_eq_withDensity {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω}
    [IsProbabilityMeasure P] {Z : Ω → EuclideanSpace ℝ (Fin q)} {E : Ω → EuclideanSpace ℝ (Fin d)}
    {σ2 : ℝ} (hσ : 0 < σ2) (hZ : HasLaw Z (stdGaussian _) P)
    (hE : HasLaw E (multivariateGaussian 0 (σ2 • 1)) P) (hind : IndepFun Z E P)
    (W : Matrix (Fin d) (Fin q) ℝ) (μ : EuclideanSpace ℝ (Fin d)) :
    P.map (fun ω => toEuclideanLin W (Z ω) + μ + E ω) =
      volume.withDensity fun x =>
        ENNReal.ofReal (multivariateGaussianPDFReal μ (ppcaCov W σ2) x)

Uses 4

Statement usesProbabilistic PCA covariance · Multivariate Gaussian density function

Proof usesThe probabilistic PCA marginal · The multivariate Gaussian density

DefinitionProbabilistic PCA log-likelihood#✓fully proved

For data \(x_1, \dots, x_N \in \mathbb{R}^d\), a mean \(\mu \in \mathbb{R}^d\), a real \(d \times q\) loading matrix \(W\) and a real number \(\sigma^2\), the probabilistic PCA log-likelihood of the data is

\[ \sum_{n=1}^N \log \mathcal{N}(x_n \mid \mu, W W^\top + \sigma^2 I), \]

where, for a real \(d \times d\) matrix \(\Sigma\) and \(x \in \mathbb{R}^d\),

\[ \mathcal{N}(x \mid \mu, \Sigma) = (2\pi)^{-d/2} \bigl(\sqrt{\det \Sigma}\bigr)^{-1} \exp\bigl(-\tfrac{1}{2} (x - \mu)^\top \Sigma^{-1} (x - \mu)\bigr) \]

is the multivariate Gaussian density formula, read with the conventions \(\sqrt{t} = 0\) for \(t < 0\), \(0^{-1} = 0\), \(\Sigma^{-1} = 0\) for singular \(\Sigma\) and \(\log 0 = 0\). These conventions matter only when \(W W^\top + \sigma^2 I\) is not positive definite. When \(\sigma^2 > 0\) the matrix \(W W^\top + \sigma^2 I\) is positive definite, and this is the density of the Gaussian with mean \(\mu\) and covariance \(W W^\top + \sigma^2 I\).

noncomputable def logLik (xs : Fin N → EuclideanSpace ℝ (Fin d)) (μ : EuclideanSpace ℝ (Fin d))
    (W : Matrix (Fin d) (Fin q) ℝ) (σ2 : ℝ) : ℝ :=
  ∑ n, log (multivariateGaussianPDFReal μ (ppcaCov W σ2) (xs n))

Uses 2 · Used by 6

Statement usesProbabilistic PCA covariance · Multivariate Gaussian density function

Used byProbabilistic PCA maximum-likelihood estimate · Probabilistic PCA MLE when the sample covariance has the model form · The probabilistic PCA likelihood is at most the unconstrained Gaussian maximum · The mean MLE is the sample mean · The log-likelihood of no data is zero · No latent factors: the noise-variance MLE is the average sample variance

AbbreviationSample mean#✓fully proved

For data points \(x_1, \dots, x_N \in \mathbb{R}^d\), the sample mean is \(\bar x = \frac{1}{N} \sum_{n=1}^{N} x_n \in \mathbb{R}^d\).

When \(N = 0\) the sample mean is \(0\).

noncomputable abbrev sampleMean (xs : Fin N → EuclideanSpace ℝ (Fin d)) :
    EuclideanSpace ℝ (Fin d) :=
  weightedMean 1 xs

Uses 1 · Used by 5

Statement usesWeighted mean

Used byProbabilistic PCA MLE when the sample covariance has the model form · The probabilistic PCA likelihood is at most the unconstrained Gaussian maximum · The mean MLE is the sample mean · No latent factors: the noise-variance MLE is the average sample variance · Sample covariance

AbbreviationSample covariance#✓fully proved

For data \(x_1, \dots, x_N \in \mathbb{R}^d\) with sample mean \(\bar{x}\), the sample covariance is the \(d \times d\) matrix \(S = \frac{1}{N} \sum_{n=1}^N (x_n - \bar{x})(x_n - \bar{x})^\top\), taken to be \(0\) when \(N = 0\).

noncomputable abbrev sampleCov (xs : Fin N → EuclideanSpace ℝ (Fin d)) :
    Matrix (Fin d) (Fin d) ℝ :=
  weightedScatter 1 xs (sampleMean xs)

Uses 2 · Used by 3

Statement usesSample mean · Weighted scatter matrix

Used byProbabilistic PCA MLE when the sample covariance has the model form · The probabilistic PCA likelihood is at most the unconstrained Gaussian maximum · No latent factors: the noise-variance MLE is the average sample variance

TheoremThe log-likelihood of no data is zero#✓fully proved

For the empty data set (\(N = 0\)), the probabilistic PCA log-likelihood at every \(\mu \in \mathbb{R}^d\), every real \(d \times q\) matrix \(W\) and every real number \(\sigma^2\) is \(0\).

theorem logLik_of_N_eq_zero (hN : N = 0) (xs : Fin N → EuclideanSpace ℝ (Fin d))
    (μ : EuclideanSpace ℝ (Fin d)) (W : Matrix (Fin d) (Fin q) ℝ) (σ2 : ℝ) :
    logLik xs μ W σ2 = 0

Uses 3 · Used by 1

Statement usesProbabilistic PCA log-likelihood

Proof usesProbabilistic PCA covariance · Multivariate Gaussian density function

Used byThe mean MLE is the sample mean

TheoremThe mean MLE is the sample mean#✓fully proved

Let \(x_1, \dots, x_N \in \mathbb{R}^d\) be data with sample mean \(\bar{x}\). For every \(\mu \in \mathbb{R}^d\), every real \(d \times q\) loading matrix \(W\) and every real \(\sigma^2 > 0\), the probabilistic PCA log-likelihood of the data at \((\mu, W, \sigma^2)\) is at most its value at \((\bar{x}, W, \sigma^2)\).

theorem logLik_le_sampleMean (xs : Fin N → EuclideanSpace ℝ (Fin d))
    (μ : EuclideanSpace ℝ (Fin d)) (W : Matrix (Fin d) (Fin q) ℝ) {σ2 : ℝ} (hσ : 0 < σ2) :
    logLik xs μ W σ2 ≤ logLik xs (sampleMean xs) W σ2

Uses 7 · Used by 1

Statement usesProbabilistic PCA log-likelihood · Sample mean

Proof usesThe log-likelihood of no data is zero · Probabilistic PCA covariance · Multivariate Gaussian density function · The weighted mean is the Gaussian MLE of the mean · Weighted mean

Used byNo latent factors: the noise-variance MLE is the average sample variance

TheoremThe probabilistic PCA likelihood is at most the unconstrained Gaussian maximum#✓fully proved

Let \(x_1, \dots, x_N \in \mathbb{R}^d\) be data whose sample covariance \(S\) is positive definite, and let \(\bar{x}\) be their sample mean. Then for every \(\mu \in \mathbb{R}^d\), every real \(d \times q\) matrix \(W\) and every real \(\sigma^2 > 0\), the probabilistic PCA log-likelihood of the data at \((\mu, W, \sigma^2)\) is at most \(\sum_{n=1}^N \log \mathcal{N}(x_n \mid \bar{x}, S)\), where \(\mathcal{N}(x \mid \bar{x}, S)\) is the multivariate Gaussian density with mean \(\bar{x}\) and covariance \(S\).

The sample covariance is positive definite, for example, when the data do not all lie in an affine hyperplane.

theorem logLik_le_gaussianMLE {xs : Fin N → EuclideanSpace ℝ (Fin d)}
    (hS : (sampleCov xs).PosDef) (μ : EuclideanSpace ℝ (Fin d)) (W : Matrix (Fin d) (Fin q) ℝ)
    {σ2 : ℝ} (hσ : 0 < σ2) :
    logLik xs μ W σ2 ≤
      ∑ n, log (multivariateGaussianPDFReal (sampleMean xs) (sampleCov xs) (xs n))

Uses 8 · Used by 1

Statement usesProbabilistic PCA log-likelihood · Sample covariance · Sample mean · Multivariate Gaussian density function

Proof usesProbabilistic PCA covariance · The weighted Gaussian MLE when the sample covariance is positive definite · Weighted mean · Weighted scatter matrix

Used byProbabilistic PCA MLE when the sample covariance has the model form

DefinitionProbabilistic PCA maximum-likelihood estimate#✓fully proved

Given data \(x_1, \dots, x_N \in \mathbb{R}^d\), a triple \((\mu_0, W_0, \sigma_0^2)\) of a mean \(\mu_0 \in \mathbb{R}^d\), a real \(d \times q\) loading matrix \(W_0\) and a real number \(\sigma_0^2\) is a probabilistic PCA maximum-likelihood estimate when \(\sigma_0^2 > 0\) and, for every \(\mu \in \mathbb{R}^d\), every real \(d \times q\) matrix \(W\) and every real \(\sigma^2 > 0\), the probabilistic PCA log-likelihood of the data at \((\mu, W, \sigma^2)\) is at most its value at \((\mu_0, W_0, \sigma_0^2)\).

def IsMLE (xs : Fin N → EuclideanSpace ℝ (Fin d)) (μ₀ : EuclideanSpace ℝ (Fin d))
    (W₀ : Matrix (Fin d) (Fin q) ℝ) (σ₀2 : ℝ) : Prop :=
  0 < σ₀2 ∧ ∀ (μ : EuclideanSpace ℝ (Fin d)) (W : Matrix (Fin d) (Fin q) ℝ) (σ2 : ℝ), 0 < σ2 →
    logLik xs μ W σ2 ≤ logLik xs μ₀ W₀ σ₀2

Uses 1 · Used by 1

Statement usesProbabilistic PCA log-likelihood

Used byProbabilistic PCA MLE when the sample covariance has the model form

TheoremProbabilistic PCA MLE when the sample covariance has the model form#✓fully proved

Let \(x_1, \dots, x_N \in \mathbb{R}^d\) be data with sample mean \(\bar{x}\) and sample covariance \(S\). If \(W_0\) is a real \(d \times q\) matrix and \(\sigma_0^2 > 0\) is a real number with \(S = W_0 W_0^\top + \sigma_0^2 I\), then \((\bar{x}, W_0, \sigma_0^2)\) is a probabilistic PCA maximum-likelihood estimate for the data.

theorem isMLE_of_sampleCov_eq {xs : Fin N → EuclideanSpace ℝ (Fin d)}
    {W₀ : Matrix (Fin d) (Fin q) ℝ} {σ₀2 : ℝ} (hσ₀ : 0 < σ₀2)
    (h : sampleCov xs = ppcaCov W₀ σ₀2) : IsMLE xs (sampleMean xs) W₀ σ₀2

Uses 7

Statement usesProbabilistic PCA maximum-likelihood estimate · Probabilistic PCA covariance · Sample covariance · Sample mean

Proof usesProbabilistic PCA log-likelihood · The probabilistic PCA likelihood is at most the unconstrained Gaussian maximum · Multivariate Gaussian density function

TheoremNo latent factors: the noise-variance MLE is the average sample variance#✓fully proved

Let \(x_1, \dots, x_N \in \mathbb{R}^d\) be data with sample mean \(\bar{x}\) and sample covariance \(S\), and suppose \(\operatorname{tr} S > 0\). Then for every \(\mu \in \mathbb{R}^d\) and every real \(\sigma^2 > 0\), the probabilistic PCA log-likelihood of the data with the zero \(d \times q\) loading matrix at \((\mu, 0, \sigma^2)\) is at most its value at \((\bar{x}, 0, \operatorname{tr} S / d)\).

Here \(\operatorname{tr} S / d\) is the average sample variance (Tipping and Bishop's \(\sigma^2\) estimate with no retained components).

theorem logLik_zero_le {xs : Fin N → EuclideanSpace ℝ (Fin d)}
    (hT : 0 < (sampleCov xs).trace) (μ : EuclideanSpace ℝ (Fin d)) {σ2 : ℝ} (hσ : 0 < σ2) :
    logLik xs μ (0 : Matrix (Fin d) (Fin q) ℝ) σ2 ≤
      logLik xs (sampleMean xs) (0 : Matrix (Fin d) (Fin q) ℝ) ((sampleCov xs).trace / d)

Uses 8

Statement usesProbabilistic PCA log-likelihood · Sample covariance · Sample mean

Proof usesThe mean MLE is the sample mean · Probabilistic PCA covariance · Multivariate Gaussian density function · The weighted Gaussian log-likelihood via the scatter matrix · Weighted scatter matrix

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.