← Mathematical handbook

Gaussian copula identities

Identity correlation gives independence. Selecting, permuting, or repeating coordinates selects the corresponding rows and columns of the correlation matrix.

@[simp]

theorem ProbabilityTheory.Copula.gaussian_one (d : ℕ) : gaussian 1 ⋯ ⋯ = independence d

Independent standard normal coordinates give the independence copula.

theorem ProbabilityTheory.Copula.gaussian_reindex {d e : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) (ρ : Fin e → Fin d) : (gaussian R hR hdiag).reindex ρ = gaussian (R.submatrix ρ ρ) ⋯ ⋯

Gaussian copulas commute with coordinate selection, including repeated coordinates.

theorem ProbabilityTheory.Copula.posSemidef_allOnes (d : ℕ) : (Matrix.of fun (x x_1 : Fin d) => 1).PosSemidef

Repeating a single coordinate produces the all-ones correlation matrix.

@[simp]

theorem ProbabilityTheory.Copula.gaussian_allOnes (d : ℕ) : gaussian (Matrix.of fun (x x_1 : Fin d) => 1) ⋯ ⋯ = comonotonic d

Perfect positive correlation gives the comonotonic copula, including dimension zero.