← Mathematical handbook

Further elliptical Gaussian scale mixture families

These are stochastic constructions with proved uniform marginals. They do not claim elementary copula CDF or density formulas. All use an independent common scale, so an identity dispersion matrix does not generally imply independence.

noncomputable def ProbabilityTheory.Copula.varianceGamma {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) (κ : ℝ) (hκ : 0 < κ) : Copula d

Symmetric variance-gamma copula: gamma variance with shape and rate κ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.Copula.laplace {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) : Copula d

Symmetric multivariate Laplace copula, with an exponential common variance.

Equations

• ProbabilityTheory.Copula.laplace R hR hdiag = ProbabilityTheory.Copula.varianceGamma R hR hdiag 1 ProbabilityTheory.Copula.laplace._proof_1

@[simp]

theorem ProbabilityTheory.Copula.varianceGamma_one {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) : varianceGamma R hR hdiag 1 ⋯ = laplace R hR hdiag

noncomputable def ProbabilityTheory.Copula.slash {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) (q : ℝ) (_hq : 0 < q) : Copula d

Generalized slash copula: the common scale is exp(E/q) for E ~ Exp(1). Equivalently the scale is U^(-1/q) for a uniform U; q = 1 is the usual slash law.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.Copula.normalLognormal {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) (τ : NNReal) : Copula d

Lognormal-scale Gaussian copulas. τ is the standard deviation of the log scale.

Equations

• One or more equations did not get rendered due to their size.