← Mathematical handbook

Gaussian scale mixture copulas

A centered Gaussian vector, multiplied by an independent, almost surely positive scalar, has atomless marginals even when its correlation matrix is singular. Its unique Sklar copula is therefore available without a density or moments. This is a useful subclass of elliptical distributions, not a characterization of every elliptical distribution.

noncomputable def ProbabilityTheory.Copula.gaussianScaleMixtureLaw {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) : MeasureTheory.ProbabilityMeasure (Fin d → ℝ)

The law of s(T) • Z, with independent T ~ μ and Z ~ N(0,R).

Equations

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

theorem ProbabilityTheory.Copula.atomless_gaussianScaleMixtureLaw_marginal {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hpos : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) (i : Fin d) : MeasureTheory.NullSingletonClass (marginal (gaussianScaleMixtureLaw R μ s) i)

theorem ProbabilityTheory.Copula.continuous_gaussianScaleMixtureLaw_marginal {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hpos : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) (i : Fin d) : Continuous ↑(ProbabilityTheory.cdf (marginal (gaussianScaleMixtureLaw R μ s) i))

noncomputable def ProbabilityTheory.Copula.gaussianScaleMixture {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hpos : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : Copula d

A copula from an independent positive Gaussian scale mixture.

Equations

• ProbabilityTheory.Copula.gaussianScaleMixture R hR hdiag μ s hs hpos = ProbabilityTheory.Copula.ofContinuousMarginals (ProbabilityTheory.Copula.gaussianScaleMixtureLaw R μ s) ⋯

theorem ProbabilityTheory.Copula.isSklarCopula_gaussianScaleMixture {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hpos : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : IsSklarCopula (gaussianScaleMixtureLaw R μ s) (gaussianScaleMixture R hR hdiag μ s hs hpos)