Finite mixtures of multivariate Gaussian laws

A multivariate Gaussian mixture with simplex weights p, means m and covariance parameters S is the finite weighted sum ∑ k, pₖ • N(mₖ, Sₖ) on EuclideanSpace ℝ ι. Every parameter value gives a probability measure.

The components with positive-definite covariance have Lebesgue densities, while every other component is singular with respect to Lebesgue measure. The mixture density multivariateGaussianMixturePDFReal is therefore the weighted sum of the densities of the positive-definite components only. It is the Radon–Nikodym derivative of the mixture at every parameter value, and when every positive-weight component is positive definite it is the weighted sum of all component densities and the mixture is absolutely continuous.

The remaining results are the categorical-mixture presentation, parameter measurability, finite-mixture integration, the exponential-integrability domain, and the mean ∑ k, pₖ • mₖ for every parameter value. When every positive-weight component has a positive-semidefinite covariance parameter, they also include the moment-generating function of every linear observable, the characteristic function, and the law of total covariance ∑ k, pₖ • (Sₖ + (mₖ - μ)(mₖ - μ)ᵀ) with μ the mean.

References

• G. McLachlan and D. Peel, Finite Mixture Models, Wiley (2000), Chapter 3.

noncomputable def TauCeti.Probability.multivariateGaussianMixtureMeasure {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) : MeasureTheory.Measure (EuclideanSpace ℝ ι)

The finite mixture of the multivariate Gaussian laws N(m k, S k) with weights p.

theorem TauCeti.Probability.multivariateGaussianMixtureMeasure_def {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) : multivariateGaussianMixtureMeasure p m S = ∑ k : κ, ↑(p.weights k) • ProbabilityTheory.multivariateGaussian (m k) (S k)

The multivariate Gaussian mixture as its defining weighted sum of Gaussian laws.

instance TauCeti.Probability.isProbabilityMeasure_multivariateGaussianMixtureMeasure {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) : MeasureTheory.IsProbabilityMeasure (multivariateGaussianMixtureMeasure p m S)

Every multivariate Gaussian mixture is a probability measure.

theorem TauCeti.Probability.multivariateGaussianMixtureMeasure_eq_bind {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] [MeasurableSpace κ] [MeasurableSingletonClass κ] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) : multivariateGaussianMixtureMeasure p m S = (categoricalMeasure p).bind fun (k : κ) => ProbabilityTheory.multivariateGaussian (m k) (S k)

The multivariate Gaussian mixture is the categorical mixture of its Gaussian components.

@[simp]

theorem TauCeti.Probability.multivariateGaussianMixtureMeasure_const {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (μ : EuclideanSpace ℝ ι) (C : Matrix ι ι ℝ) : (multivariateGaussianMixtureMeasure p (fun (x : κ) => μ) fun (x : κ) => C) = ProbabilityTheory.multivariateGaussian μ C

A mixture of identical multivariate Gaussian components is that Gaussian law.

theorem TauCeti.Probability.multivariateGaussianMixtureMeasure_congr {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] {p : Convexity.StdSimplex NNReal κ} {m : κ → EuclideanSpace ℝ ι} {S : κ → Matrix ι ι ℝ} {m' : κ → EuclideanSpace ℝ ι} {S' : κ → Matrix ι ι ℝ} (h : ∀ (k : κ), 0 < p.weights k → m k = m' k ∧ S k = S' k) : multivariateGaussianMixtureMeasure p m S = multivariateGaussianMixtureMeasure p m' S'

Changing the parameters of zero-weight components leaves the mixture unchanged.

theorem TauCeti.Probability.measurable_multivariateGaussianMixtureMeasure {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] : Measurable fun (z : Convexity.StdSimplex NNReal κ × (κ → EuclideanSpace ℝ ι) × (κ → Matrix ι ι ℝ)) => multivariateGaussianMixtureMeasure z.1 z.2.1 z.2.2

Multivariate Gaussian mixtures are measurable in their weights, means, and covariance parameters.

Densities

noncomputable def TauCeti.Probability.multivariateGaussianMixturePDFReal {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) (x : EuclideanSpace ℝ ι) : ℝ

The real density of the absolutely continuous part of a multivariate Gaussian mixture: the weighted sum of the Gaussian densities of the components with positive-definite covariance. The other components are singular with respect to Lebesgue measure and contribute nothing.

theorem TauCeti.Probability.multivariateGaussianMixturePDFReal_def {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) (x : EuclideanSpace ℝ ι) : multivariateGaussianMixturePDFReal p m S x = ∑ k : κ with (S k).PosDef, ↑(p.weights k) * multivariateGaussianPDFReal (m k) (S k) x

The mixture density as its defining weighted sum over the positive-definite components.

noncomputable def TauCeti.Probability.multivariateGaussianMixturePDF {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) (x : EuclideanSpace ℝ ι) : ENNReal

The extended nonnegative density of the absolutely continuous part of a multivariate Gaussian mixture.

theorem TauCeti.Probability.multivariateGaussianMixturePDF_eq_ofReal {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) (x : EuclideanSpace ℝ ι) : multivariateGaussianMixturePDF p m S x = ENNReal.ofReal (multivariateGaussianMixturePDFReal p m S x)

The ℝ≥0∞-valued mixture density is the ENNReal.ofReal lift of the real-valued one.

theorem TauCeti.Probability.multivariateGaussianMixturePDFReal_eq_sum_of_posDef {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] {p : Convexity.StdSimplex NNReal κ} {m : κ → EuclideanSpace ℝ ι} {S : κ → Matrix ι ι ℝ} (hS : ∀ (k : κ), 0 < p.weights k → (S k).PosDef) (x : EuclideanSpace ℝ ι) : multivariateGaussianMixturePDFReal p m S x = ∑ k : κ, ↑(p.weights k) * multivariateGaussianPDFReal (m k) (S k) x

If every positive-weight component has positive-definite covariance, the mixture density is the weighted sum of all component densities.

theorem TauCeti.Probability.multivariateGaussianMixturePDF_eq_sum {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) (x : EuclideanSpace ℝ ι) : multivariateGaussianMixturePDF p m S x = ∑ k : κ with (S k).PosDef, ↑(p.weights k) * multivariateGaussianPDF (m k) (S k) x

The extended mixture density as a weighted sum over the positive-definite components.

theorem TauCeti.Probability.multivariateGaussianMixturePDF_eq_sum_of_posDef {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] {p : Convexity.StdSimplex NNReal κ} {m : κ → EuclideanSpace ℝ ι} {S : κ → Matrix ι ι ℝ} (hS : ∀ (k : κ), 0 < p.weights k → (S k).PosDef) (x : EuclideanSpace ℝ ι) : multivariateGaussianMixturePDF p m S x = ∑ k : κ, ↑(p.weights k) * multivariateGaussianPDF (m k) (S k) x

If every positive-weight component has positive-definite covariance, the extended mixture density is the weighted sum of all component densities.

theorem TauCeti.Probability.multivariateGaussianMixturePDFReal_nonneg {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) (x : EuclideanSpace ℝ ι) : 0 ≤ multivariateGaussianMixturePDFReal p m S x

The real-valued mixture density is nonnegative.

@[simp]

theorem TauCeti.Probability.toReal_multivariateGaussianMixturePDF {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) (x : EuclideanSpace ℝ ι) : (multivariateGaussianMixturePDF p m S x).toReal = multivariateGaussianMixturePDFReal p m S x

The ℝ≥0∞-valued mixture density carries the real-valued one back through ENNReal.toReal.

theorem TauCeti.Probability.multivariateGaussianMixturePDFReal_pos {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] {p : Convexity.StdSimplex NNReal κ} {m : κ → EuclideanSpace ℝ ι} {S : κ → Matrix ι ι ℝ} (h : ∃ (k : κ), 0 < p.weights k ∧ (S k).PosDef) (x : EuclideanSpace ℝ ι) : 0 < multivariateGaussianMixturePDFReal p m S x

The mixture density is positive everywhere as soon as one positive-weight component has positive-definite covariance.

theorem TauCeti.Probability.measurable_multivariateGaussianMixturePDFReal {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) : Measurable (multivariateGaussianMixturePDFReal p m S)

The real-valued mixture density is measurable.

theorem TauCeti.Probability.measurable_multivariateGaussianMixturePDF {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) : Measurable (multivariateGaussianMixturePDF p m S)

The ℝ≥0∞-valued mixture density is measurable.

theorem TauCeti.Probability.multivariateGaussianMixtureMeasure_eq_add_withDensity {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) : multivariateGaussianMixtureMeasure p m S = ∑ k : κ with ¬(S k).PosDef, ↑(p.weights k) • ProbabilityTheory.multivariateGaussian (m k) (S k) + MeasureTheory.volume.withDensity (multivariateGaussianMixturePDF p m S)

Lebesgue decomposition. A multivariate Gaussian mixture is the sum of its weighted components whose covariance is not positive definite, each singular with respect to Lebesgue measure by mutuallySingular_multivariateGaussian_volume, and of Lebesgue measure weighted by the mixture density.

theorem TauCeti.Probability.multivariateGaussianMixtureMeasure_eq_withDensity {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] {p : Convexity.StdSimplex NNReal κ} {m : κ → EuclideanSpace ℝ ι} {S : κ → Matrix ι ι ℝ} (hS : ∀ (k : κ), 0 < p.weights k → (S k).PosDef) : multivariateGaussianMixtureMeasure p m S = MeasureTheory.volume.withDensity (multivariateGaussianMixturePDF p m S)

If every positive-weight component has positive-definite covariance, the mixture is Lebesgue measure weighted by the mixture density.

theorem TauCeti.Probability.rnDeriv_multivariateGaussianMixtureMeasure {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) : (multivariateGaussianMixtureMeasure p m S).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] multivariateGaussianMixturePDF p m S

The Radon–Nikodym derivative of a multivariate Gaussian mixture with respect to Lebesgue measure is the mixture density, also when some components are degenerate.

theorem TauCeti.Probability.hasPDF_of_hasLaw_multivariateGaussianMixtureMeasure {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] {p : Convexity.StdSimplex NNReal κ} {m : κ → EuclideanSpace ℝ ι} {S : κ → Matrix ι ι ℝ} {Ω : Type u_3} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → EuclideanSpace ℝ ι} (hS : ∀ (k : κ), 0 < p.weights k → (S k).PosDef) (hX : ProbabilityTheory.HasLaw X (multivariateGaussianMixtureMeasure p m S) P) : MeasureTheory.HasPDF X P MeasureTheory.volume

A random vector whose law is a multivariate Gaussian mixture with positive-definite positive-weight components has a Lebesgue density.

theorem TauCeti.Probability.pdf_eq_multivariateGaussianMixturePDF_of_hasLaw_multivariateGaussianMixtureMeasure {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] {p : Convexity.StdSimplex NNReal κ} {m : κ → EuclideanSpace ℝ ι} {S : κ → Matrix ι ι ℝ} {Ω : Type u_3} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → EuclideanSpace ℝ ι} (hS : ∀ (k : κ), 0 < p.weights k → (S k).PosDef) (hX : ProbabilityTheory.HasLaw X (multivariateGaussianMixtureMeasure p m S) P) : MeasureTheory.pdf X P MeasureTheory.volume =ᵐ[MeasureTheory.volume] multivariateGaussianMixturePDF p m S

The canonical pdf of such a random vector agrees almost everywhere with the mixture density.

Integration and transforms

theorem TauCeti.Probability.integrable_multivariateGaussianMixtureMeasure_iff {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] {p : Convexity.StdSimplex NNReal κ} {m : κ → EuclideanSpace ℝ ι} {S : κ → Matrix ι ι ℝ} {E : Type u_4} [NormedAddCommGroup E] {f : EuclideanSpace ℝ ι → E} : MeasureTheory.Integrable f (multivariateGaussianMixtureMeasure p m S) ↔ ∀ (k : κ), 0 < p.weights k → MeasureTheory.Integrable f (ProbabilityTheory.multivariateGaussian (m k) (S k))

Integrability under a multivariate Gaussian mixture is integrability under every positive-weight component.

theorem TauCeti.Probability.integral_multivariateGaussianMixtureMeasure {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] {p : Convexity.StdSimplex NNReal κ} {m : κ → EuclideanSpace ℝ ι} {S : κ → Matrix ι ι ℝ} {E : Type u_4} [NormedAddCommGroup E] {f : EuclideanSpace ℝ ι → E} [NormedSpace ℝ E] (hf : MeasureTheory.Integrable f (multivariateGaussianMixtureMeasure p m S)) : ∫ (x : EuclideanSpace ℝ ι), f x ∂multivariateGaussianMixtureMeasure p m S = ∑ k : κ, ↑(p.weights k) • ∫ (x : EuclideanSpace ℝ ι), f x ∂ProbabilityTheory.multivariateGaussian (m k) (S k)

The expectation of an integrable observable is the weighted sum of its component expectations.

@[simp]

theorem TauCeti.Probability.integrableExpSet_inner_multivariateGaussianMixtureMeasure {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) (θ : EuclideanSpace ℝ ι) : ProbabilityTheory.integrableExpSet (fun (x : EuclideanSpace ℝ ι) => inner ℝ θ x) (multivariateGaussianMixtureMeasure p m S) = Set.univ

Every linear observable of a multivariate Gaussian mixture has finite exponential moments of all real orders.

theorem TauCeti.Probability.mgf_inner_multivariateGaussianMixtureMeasure {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] {p : Convexity.StdSimplex NNReal κ} {m : κ → EuclideanSpace ℝ ι} {S : κ → Matrix ι ι ℝ} (hS : ∀ (k : κ), 0 < p.weights k → (S k).PosSemidef) (θ : EuclideanSpace ℝ ι) (t : ℝ) : ProbabilityTheory.mgf (fun (x : EuclideanSpace ℝ ι) => inner ℝ θ x) (multivariateGaussianMixtureMeasure p m S) t = ∑ k : κ, ↑(p.weights k) * Real.exp (t * inner ℝ θ (m k) + t ^ 2 / 2 * inner ℝ θ ((Matrix.toEuclideanLin (S k)) θ))

The moment-generating function of a linear observable of a multivariate Gaussian mixture with positive-semidefinite positive-weight components is the weighted sum of the Gaussian ones.

theorem TauCeti.Probability.cgf_inner_multivariateGaussianMixtureMeasure {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] {p : Convexity.StdSimplex NNReal κ} {m : κ → EuclideanSpace ℝ ι} {S : κ → Matrix ι ι ℝ} (hS : ∀ (k : κ), 0 < p.weights k → (S k).PosSemidef) (θ : EuclideanSpace ℝ ι) (t : ℝ) : ProbabilityTheory.cgf (fun (x : EuclideanSpace ℝ ι) => inner ℝ θ x) (multivariateGaussianMixtureMeasure p m S) t = Real.log (∑ k : κ, ↑(p.weights k) * Real.exp (t * inner ℝ θ (m k) + t ^ 2 / 2 * inner ℝ θ ((Matrix.toEuclideanLin (S k)) θ)))

The cumulant-generating function of a linear observable of a multivariate Gaussian mixture is the logarithm of the weighted sum of the Gaussian moment-generating functions.

theorem TauCeti.Probability.charFun_multivariateGaussianMixtureMeasure {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] {p : Convexity.StdSimplex NNReal κ} {m : κ → EuclideanSpace ℝ ι} {S : κ → Matrix ι ι ℝ} (hS : ∀ (k : κ), 0 < p.weights k → (S k).PosSemidef) (t : EuclideanSpace ℝ ι) : MeasureTheory.charFun (multivariateGaussianMixtureMeasure p m S) t = ∑ k : κ, ↑↑(p.weights k) * Complex.exp (↑(inner ℝ t (m k)) * Complex.I - ↑(t.ofLp ⬝ᵥ (S k).mulVec t.ofLp) / 2)

The characteristic function of a multivariate Gaussian mixture with positive-semidefinite positive-weight components is the weighted sum of the Gaussian characteristic functions.

Mean and covariance

theorem TauCeti.Probability.memLp_id_multivariateGaussianMixtureMeasure {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) {q : ENNReal} (hq : q ≠ ⊤) : MeasureTheory.MemLp id q (multivariateGaussianMixtureMeasure p m S)

A multivariate Gaussian mixture has finite moments of every finite order.

@[simp]

theorem TauCeti.Probability.integral_id_multivariateGaussianMixtureMeasure {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] (p : Convexity.StdSimplex NNReal κ) (m : κ → EuclideanSpace ℝ ι) (S : κ → Matrix ι ι ℝ) : ∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussianMixtureMeasure p m S = ∑ k : κ, ↑(p.weights k) • m k

The mean of a multivariate Gaussian mixture is the weighted mean of the component means.

theorem TauCeti.Probability.covMatrix_multivariateGaussianMixtureMeasure {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] {p : Convexity.StdSimplex NNReal κ} {m : κ → EuclideanSpace ℝ ι} {S : κ → Matrix ι ι ℝ} (hS : ∀ (k : κ), 0 < p.weights k → (S k).PosSemidef) : covMatrix (multivariateGaussianMixtureMeasure p m S) = ∑ k : κ, ↑(p.weights k) • (S k + Matrix.vecMulVec (m k - ∑ j : κ, ↑(p.weights j) • m j).ofLp (m k - ∑ j : κ, ↑(p.weights j) • m j).ofLp)

Law of total covariance for a multivariate Gaussian mixture with positive-semidefinite positive-weight components: the weighted component covariance plus the weighted spread of the component means about the overall mean.

theorem TauCeti.Probability.integral_of_hasLaw_multivariateGaussianMixtureMeasure {κ : Type u_1} {ι : Type u_2} [Fintype κ] [Fintype ι] [DecidableEq ι] {p : Convexity.StdSimplex NNReal κ} {m : κ → EuclideanSpace ℝ ι} {S : κ → Matrix ι ι ℝ} {Ω : Type u_3} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → EuclideanSpace ℝ ι} (hX : ProbabilityTheory.HasLaw X (multivariateGaussianMixtureMeasure p m S) P) : ∫ (ω : Ω), X ω ∂P = ∑ k : κ, ↑(p.weights k) • m k

The mean of a random vector whose law is a multivariate Gaussian mixture.