← Copula mathematical handbook

Kendall's tau and Blomqvist's beta of bivariate Gaussian scale mixtures

Let (X, Y) = S · (G₁, G₂) where G ~ N(0, R) with R = !![1, r; r, 1] and S > 0 is an independent scale (gaussianScaleMixture). This covers the Student-t, Cauchy, variance-gamma, Laplace, slash and normal–lognormal copulas of the library. Then, whatever the mixing law,

• kendallTau_gaussianScaleMixture: τ = (2/π) arcsin r (Lindskog, McNeil and Schmock 2003);
• blomqvistBeta_gaussianScaleMixture: β = (2/π) arcsin r;
• the same values for the Student-t (any ν > 0), Cauchy, variance-gamma, Laplace, slash and normal–lognormal copulas with correlation matrix !![1, r; r, 1].

Both reduce to Sheppard's formula conditionally on the scales: given S = s, S' = s', the vector (s' G'₁ − s G₁, s' G'₂ − s G₂) is centered bivariate normal with correlation r (multivariateGaussian_corrMatrix_orthant_sub). In contrast to the Gaussian case, Spearman's rho of a scale mixture depends on the mixing law and is not treated here.

References

• F. Lindskog, A. McNeil, U. Schmock, Kendall's tau for elliptical distributions, in Credit Risk (2003), 149–156.
• H. Joe, Dependence Modeling with Copulas, CRC Press 2014, §4.3 and §2.12.

Mixtures

theorem ProbabilityTheory.Copula.measure_prod_eq_const_of_ae {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [MeasurableSpace F] (N : MeasureTheory.Measure E) (μ : MeasureTheory.Measure F) [MeasureTheory.IsProbabilityMeasure N] [MeasureTheory.IsProbabilityMeasure μ] {A : Set (E × F)} (hA : MeasurableSet A) {c : ENNReal} (h : ∀ᵐ (t : F) ∂μ, N {g : E | (g, t) ∈ A} = c) : (N.prod μ) A = c

A set whose sections have constant mass c (for a.e. value of the second factor) has mass c under a product of probability measures.

theorem ProbabilityTheory.Copula.measure_prod_prod_eq_const_of_ae {E : Type u_1} {F : Type u_2} [MeasurableSpace E] [MeasurableSpace F] (N : MeasureTheory.Measure E) (μ : MeasureTheory.Measure F) [MeasureTheory.IsProbabilityMeasure N] [MeasureTheory.IsProbabilityMeasure μ] {A : Set ((E × F) × E × F)} (hA : MeasurableSet A) {c : ENNReal} (h : ∀ᵐ (t : F) (t' : F) ∂μ, (N.prod N) {g : E × E | ((g.1, t), g.2, t') ∈ A} = c) : ((N.prod μ).prod (N.prod μ)) A = c

Two-fold mixture version of measure_prod_eq_const_of_ae: if conditionally on the mixing variables t, t' the set has N ⊗ N-mass c, then it has mass c under (N ⊗ μ) ⊗ (N ⊗ μ).

Orthant probabilities of the normal law with correlation matrix corrMatrix r

theorem ProbabilityTheory.Copula.multivariateGaussian_corrMatrix_orthant {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (multivariateGaussian 0 (corrMatrix r)).real {g : EuclideanSpace ℝ (Fin 2) | g.ofLp 0 ≤ 0 ∧ g.ofLp 1 ≤ 0} = 1 / 4 + Real.arcsin r / (2 * Real.pi)

Sheppard's formula for N(0, corrMatrix r).

theorem ProbabilityTheory.Copula.multivariateGaussian_corrMatrix_orthant_sub {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : ((multivariateGaussian 0 (corrMatrix r)).prod (multivariateGaussian 0 (corrMatrix r))).real {z : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2) | b * z.2.ofLp 0 - a * z.1.ofLp 0 ≤ 0 ∧ b * z.2.ofLp 1 - a * z.1.ofLp 1 ≤ 0} = 1 / 4 + Real.arcsin r / (2 * Real.pi)

Sheppard's formula for scaled differences of two independent N(0, corrMatrix r) vectors.

Medians of symmetric marginals

theorem ProbabilityTheory.Copula.cdf_zero_of_map_neg_eq {ν : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure ν] [MeasureTheory.NullSingletonClass ν] (h : MeasureTheory.Measure.map (fun (x : ℝ) => -x) ν = ν) : ↑(ProbabilityTheory.cdf ν) 0 = 1 / 2

A symmetric atomless law has median 0: F(0) = 1/2.

theorem ProbabilityTheory.Copula.marginal_gaussianScaleMixtureLaw_map_neg {d : ℕ} (R : Matrix (Fin d) (Fin d) ℝ) (hR : R.PosSemidef) (hdiag : ∀ (i : Fin d), R i i = 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (i : Fin d) : MeasureTheory.Measure.map (fun (x : ℝ) => -x) (marginal (gaussianScaleMixtureLaw R μ s) i) = marginal (gaussianScaleMixtureLaw R μ s) i

The marginals of a Gaussian scale mixture are symmetric.

Blomqvist's beta and Kendall's tau

theorem ProbabilityTheory.Copula.sheppard_nonneg (r : ℝ) : 0 ≤ 1 / 4 + Real.arcsin r / (2 * Real.pi)

theorem ProbabilityTheory.Copula.marginalTransform_zero_gaussianScaleMixtureLaw {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hpos : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : marginalTransform (gaussianScaleMixtureLaw (corrMatrix r) μ s) 0 = ![unitHalf, unitHalf]

The marginal medians of a bivariate Gaussian scale mixture are 0, so the marginal transform maps 0 to (1/2, 1/2).

theorem ProbabilityTheory.Copula.blomqvistBeta_gaussianScaleMixture {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hpos : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : (gaussianScaleMixture (corrMatrix r) ⋯ ⋯ μ s hs hpos).blomqvistBeta = 2 / Real.pi * Real.arcsin r

Blomqvist's beta of an elliptical (Gaussian scale mixture) copula: β = (2/π) arcsin r, independently of the mixing law.

theorem ProbabilityTheory.Copula.kendallTau_gaussianScaleMixture {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hpos : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : (gaussianScaleMixture (corrMatrix r) ⋯ ⋯ μ s hs hpos).kendallTau = 2 / Real.pi * Real.arcsin r

Kendall's tau of an elliptical (Gaussian scale mixture) copula (Lindskog–McNeil–Schmock): τ = (2/π) arcsin r, independently of the mixing law.

Named elliptical families

theorem ProbabilityTheory.Copula.kendallTau_studentT {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (studentT (corrMatrix r) ⋯ ⋯ ν hν).kendallTau = 2 / Real.pi * Real.arcsin r

Kendall's tau of the Student-t copula: τ = (2/π) arcsin r for every ν > 0.

theorem ProbabilityTheory.Copula.blomqvistBeta_studentT {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (ν : ℝ) (hν : 0 < ν) : (studentT (corrMatrix r) ⋯ ⋯ ν hν).blomqvistBeta = 2 / Real.pi * Real.arcsin r

Blomqvist's beta of the Student-t copula: β = (2/π) arcsin r for every ν > 0.

theorem ProbabilityTheory.Copula.kendallTau_cauchy {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (cauchy (corrMatrix r) ⋯ ⋯).kendallTau = 2 / Real.pi * Real.arcsin r

theorem ProbabilityTheory.Copula.kendallTau_varianceGamma {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (κ : ℝ) (hκ : 0 < κ) : (varianceGamma (corrMatrix r) ⋯ ⋯ κ hκ).kendallTau = 2 / Real.pi * Real.arcsin r

theorem ProbabilityTheory.Copula.kendallTau_laplace {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (laplace (corrMatrix r) ⋯ ⋯).kendallTau = 2 / Real.pi * Real.arcsin r

theorem ProbabilityTheory.Copula.kendallTau_slash {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (q : ℝ) (hq : 0 < q) : (slash (corrMatrix r) ⋯ ⋯ q hq).kendallTau = 2 / Real.pi * Real.arcsin r

theorem ProbabilityTheory.Copula.kendallTau_normalLognormal {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (τ : NNReal) : (normalLognormal (corrMatrix r) ⋯ ⋯ τ).kendallTau = 2 / Real.pi * Real.arcsin r