Skip to content

Gaussian graphical models

12 fully proved

Matrix

TheoremThe conditional covariance is the inverse of a precision block#✓fully proved

For positive definite S on ι ⊕ κ, S₁₁ - S₁₂ S₂₂⁻¹ S₂₁ = ((S⁻¹)₁₁)⁻¹.

theorem inv_toBlocks₁₁_inv {S : Matrix (ι ⊕ κ) (ι ⊕ κ) ℝ} (hS : S.PosDef) :
    (S⁻¹.toBlocks₁₁)⁻¹ = S.toBlocks₁₁ - S.toBlocks₁₂ * S.toBlocks₂₂⁻¹ * S.toBlocks₂₁
Used by 2
Used byPairwise Markov property of Gaussian vectors · Partial correlation from the precision matrix

DefinitionPartial correlation from the conditional covariance#✓fully proved

The partial correlation of coordinates 0 and 1 given the κ-block, computed from the conditional covariance C = S₁₁ - S₁₂ S₂₂⁻¹ S₂₁: C₀₁ / √(C₀₀ C₁₁).

noncomputable def partialCorrelation (S : Matrix (Fin 2 ⊕ κ) (Fin 2 ⊕ κ) ℝ) : ℝ :=
  let C := S.toBlocks₁₁ - S.toBlocks₁₂ * S.toBlocks₂₂⁻¹ * S.toBlocks₂₁
  C 0 1 / √(C 0 0 * C 1 1)
Used by 1
Used byPartial correlation from the precision matrix

TheoremPartial correlation from the precision matrix#✓fully proved

The partial correlation from the precision matrix: ρ₁₂·rest = -Ω₀₁ / √(Ω₀₀ Ω₁₁).

theorem partialCorrelation_eq {S : Matrix (Fin 2 ⊕ κ) (Fin 2 ⊕ κ) ℝ} (hS : S.PosDef) :
    partialCorrelation S =
      -S⁻¹ (.inl 0) (.inl 1) / √(S⁻¹ (.inl 0) (.inl 0) * S⁻¹ (.inl 1) (.inl 1))
Uses 2
Statement usesPartial correlation from the conditional covariance
Proof usesThe conditional covariance is the inverse of a precision block

Cond Indep

DefinitionConditioning block of a vector#✓fully proved

The κ-block (the conditioning coordinates) of a vector on Fin 2 ⊕ κ.

noncomputable def rest (v : EuclideanSpace ℝ (Fin 2 ⊕ κ)) : EuclideanSpace ℝ κ :=
  toLp 2 fun j => v (.inr j)
Used by 2
Used byPairwise Markov property of Gaussian vectors · Measurability of the conditioning block

TheoremMeasurability of the conditioning block#✓fully proved

The κ-block is a measurable function of the vector.

theorem measurable_rest [Finite κ] : Measurable (rest (κ := κ))
Uses 1 · Used by 1
Statement usesConditioning block of a vector
Used byPairwise Markov property of Gaussian vectors

TheoremPairwise Markov property of Gaussian vectors#✓fully proved

If V = (X₀, X₁, Y) ~ N(μ, S) with S positive definite, then X₀ and X₁ are conditionally independent given Y iff (S⁻¹)₀₁ = 0. (The standard Borel sample space is the setting of Mathlib's conditional independence.)

theorem condIndepFun_iff_inv_apply_eq_zero {V : Ω → EuclideanSpace ℝ (Fin 2 ⊕ κ)}
    (hV : Measurable V) {μ : EuclideanSpace ℝ (Fin 2 ⊕ κ)} {S : Matrix (Fin 2 ⊕ κ) (Fin 2 ⊕ κ) ℝ}
    (hS : S.PosDef) (hlaw : P.map V = multivariateGaussian μ S) :
    ((fun ω => V ω (.inl 0)) ⟂ᵢ[fun ω => rest (V ω), measurable_rest.comp hV; P]
      (fun ω => V ω (.inl 1))) ↔ S⁻¹ (.inl 0) (.inl 1) = 0
Uses 6
Statement usesMeasurability of the conditioning block · Conditioning block of a vector
Proof usesThe conditional covariance is the inverse of a precision block · Horizontal block matrix · Gaussian conditioning (Schur complement) · Covariances of linear functionals of a Gaussian vector

Dempster

DefinitionSample second-moment matrix#✓fully proved

The sample second-moment matrix m⁻¹ ∑ₛ xₛ xₛᵀ of m observations in ℝ^ι.

noncomputable def sampleCov {m : ℕ} (x : Fin m → ι → ℝ) : Matrix ι ι ℝ :=
  (m : ℝ)⁻¹ • ∑ s, vecMulVec (x s) (x s)
Used by 1
Used bySum of sample quadratic forms as a trace

TheoremSum of sample quadratic forms as a trace#✓fully proved

The quadratic forms of a sample add up to m · tr (S K).

theorem sum_dotProduct_mulVec_eq {m : ℕ} (hm : 0 < m) (x : Fin m → ι → ℝ) (K : Matrix ι ι ℝ) :
    ∑ s, x s ⬝ᵥ K *ᵥ x s = m * (sampleCov x * K).trace
Uses 1
Statement usesSample second-moment matrix

DefinitionGaussian log-likelihood of a precision matrix#✓fully proved

The Gaussian log-likelihood objective log det K - tr (S K) of a precision matrix K.

noncomputable def gaussLogLik (S K : Matrix ι ι ℝ) : ℝ := log K.det - (S * K).trace
Used by 2
Used byUniqueness of Dempster's MLE · Dempster's covariance-selection MLE

DefinitionMatrix supported on the edges of a graph#✓fully proved

A matrix vanishes off the edges of G: K i j = 0 for distinct non-adjacent i, j.

def IsSupportedOn (G : SimpleGraph ι) (K : Matrix ι ι ℝ) : Prop :=
  ∀ i j, i ≠ j → ¬ G.Adj i j → K i j = 0
Used by 2
Used byUniqueness of Dempster's MLE · Dempster's covariance-selection MLE

TheoremDempster's covariance-selection MLE#✓fully proved

Dempster's covariance-selection MLE (sufficiency): a positive definite K̂ supported on G whose inverse agrees with S on the diagonal and the edges maximizes log det K - tr (S K) over positive definite K supported on G.

theorem gaussLogLik_le_of_inv_eq_on_graph {G : SimpleGraph ι} {S K₀ : Matrix ι ι ℝ}
    (hK₀ : K₀.PosDef) (hsupp₀ : IsSupportedOn G K₀)
    (hmatch : ∀ i j, (i = j ∨ G.Adj i j) → K₀⁻¹ i j = S i j)
    {K : Matrix ι ι ℝ} (hK : K.PosDef) (hsupp : IsSupportedOn G K) :
    gaussLogLik S K ≤ gaussLogLik S K₀
Uses 3
Statement usesMatrix supported on the edges of a graph · Gaussian log-likelihood of a precision matrix
Proof usesLog-determinant trace inequality

TheoremUniqueness of Dempster's MLE#✓fully proved

Under the hypotheses of gaussLogLik_le_of_inv_eq_on_graph, a positive definite K supported on G with the same objective value is K̂.

theorem eq_of_gaussLogLik_eq {G : SimpleGraph ι} {S K₀ : Matrix ι ι ℝ}
    (hK₀ : K₀.PosDef) (hsupp₀ : IsSupportedOn G K₀)
    (hmatch : ∀ i j, (i = j ∨ G.Adj i j) → K₀⁻¹ i j = S i j)
    {K : Matrix ι ι ℝ} (hK : K.PosDef) (hsupp : IsSupportedOn G K)
    (heq : gaussLogLik S K = gaussLogLik S K₀) : K = K₀
Uses 2
Statement usesMatrix supported on the edges of a graph · Gaussian log-likelihood of a precision matrix

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.