← Copula mathematical handbook

Slepian's inequality and quadrant dependence of the Gaussian copula

The bivariate Gaussian copulas are increasing in the concordance (pointwise) order: r ≤ r' implies C_r ≤ C_{r'} (Slepian's inequality in dimension two, Slepian 1962). In particular C_r is positively quadrant dependent iff r ≥ 0 and negatively quadrant dependent iff r ≤ 0.

Proof

For r ∈ [0, 1] the bivariate normal vector has the common factor representation (√r W + √(1−r) Z₁, √r W + √(1−r) Z₂) with W, Z₁, Z₂ i.i.d. standard normal, hence P(X ≤ x, Y ≤ y) = E[K(x − √r W) K(y − √r W)] with K the N(0, 1 − r) CDF (bivariateNormal_real_Iic_eq_integral). For 0 ≤ r ≤ r' split √r' W = √r W + √(r'−r) V; conditionally on W both factors are antitone in V, and Chebyshev's integral inequality (integral_mul_integral_le_integral_mul_of_antitone) removes the common V, which turns r' into r. Negative correlations follow by reflection (reflect_second_bivariateGaussian).

Main results

• bivariateGaussian_lowerOrthantLE, bivariateGaussian_concordanceLE: r ≤ r' → C_r ≤ C_{r'}.
• isPQD_bivariateGaussian_iff, isNQD_bivariateGaussian_iff.

References

• D. Slepian, The one-sided barrier problem for Gaussian noise, Bell System Tech. J. 41 (1962).
• H. Joe, Dependence Modeling with Copulas, CRC Press 2014, §4.3 (concordance ordering of the Gaussian family); R. B. Nelsen, An Introduction to Copulas, 2nd ed., 2006, §5.2 (PQD).

Chebyshev's integral inequality

theorem ProbabilityTheory.Copula.integral_mul_integral_le_integral_mul_of_antitone (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] {f g : ℝ → ℝ} (hf : Antitone f) (hg : Antitone g) (hf01 : ∀ (x : ℝ), f x ∈ Set.Icc 0 1) (hg01 : ∀ (x : ℝ), g x ∈ Set.Icc 0 1) : (∫ (x : ℝ), f x ∂μ) * ∫ (x : ℝ), g x ∂μ ≤ ∫ (x : ℝ), f x * g x ∂μ

Chebyshev's integral inequality: for two antitone functions with values in [0, 1], ∫ f · ∫ g ≤ ∫ f g under a probability measure.

Scaled normal CDFs

noncomputable def ProbabilityTheory.Copula.scaledNormalCDF (e t : ℝ) : ℝ

P(e Z ≤ t) for a standard normal Z; for e ≥ 0 this is the N(0, e²) CDF at t.

Equations

• ProbabilityTheory.Copula.scaledNormalCDF e t = (ProbabilityTheory.gaussianReal 0 1).real {z : ℝ | e * z ≤ t}

theorem ProbabilityTheory.Copula.scaledNormalCDF_mono (e : ℝ) : Monotone (scaledNormalCDF e)

theorem ProbabilityTheory.Copula.scaledNormalCDF_mem_Icc (e t : ℝ) : scaledNormalCDF e t ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.measurable_scaledNormalCDF (e : ℝ) : Measurable (scaledNormalCDF e)

theorem ProbabilityTheory.Copula.scaledNormalCDF_eq (e t : ℝ) : scaledNormalCDF e t = (gaussianReal 0 (e ^ 2).toNNReal).real (Set.Iic t)

P(e Z ≤ t) = P(N(0, e²) ≤ t), written through gaussianReal.

theorem ProbabilityTheory.Copula.integral_scaledNormalCDF_sub (d e t : ℝ) : ∫ (v : ℝ), scaledNormalCDF e (t - d * v) ∂gaussianReal 0 1 = scaledNormalCDF (√(d ^ 2 + e ^ 2)) t

Convolution of scaled normal CDFs: E[K_e(t − d V)] = K_{√(d² + e²)}(t).

theorem ProbabilityTheory.Copula.integral_comp_sqrt_add_sq (F : ℝ → ℝ) (hF : Measurable F) (hF01 : ∀ (s : ℝ), F s ∈ Set.Icc 0 1) (c d : ℝ) : ∫ (w : ℝ), F (√(c ^ 2 + d ^ 2) * w) ∂gaussianReal 0 1 = ∫ (w : ℝ), ∫ (v : ℝ), F (c * w + d * v) ∂gaussianReal 0 1 ∂gaussianReal 0 1

A Gaussian scale can be split into two independent pieces inside an integral: E[F(√(c² + d²) W)] = E[F(c W + d V)] for independent standard normal W, V.

theorem ProbabilityTheory.Copula.scaledNormalCDF_of_pos {e : ℝ} (he : 0 < e) (t : ℝ) : scaledNormalCDF e t = ↑(ProbabilityTheory.cdf (gaussianReal 0 1)) (t / e)

For e > 0, P(e Z ≤ t) = Φ(t / e).

theorem ProbabilityTheory.Copula.bivariateNormal_real_Iic_eq_setIntegral (r x y : ℝ) : (bivariateNormal r).real {p : ℝ × ℝ | p.1 ≤ x ∧ p.2 ≤ y} = ∫ (z : ℝ) in Set.Iic x, scaledNormalCDF (√(1 - r ^ 2)) (y - r * z) ∂gaussianReal 0 1

Conditional representation of the bivariate normal CDF: P(X ≤ x, Y ≤ y) = ∫_{z ≤ x} P(√(1 − r²) Z ≤ y − r z) dΦ(z); for |r| < 1 the integrand is Φ((y − r z)/√(1 − r²)) (scaledNormalCDF_of_pos).

Slepian's inequality for the bivariate normal law

theorem ProbabilityTheory.Copula.bivariateNormal_real_Iic_eq_integral {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r ≤ 1) (x y : ℝ) : (bivariateNormal r).real {p : ℝ × ℝ | p.1 ≤ x ∧ p.2 ≤ y} = ∫ (w : ℝ), scaledNormalCDF (√(1 - r)) (x - √r * w) * scaledNormalCDF (√(1 - r)) (y - √r * w) ∂gaussianReal 0 1

Common factor representation of the bivariate normal law with correlation r ∈ [0, 1]: P(X ≤ x, Y ≤ y) = E[K(x − √r W) K(y − √r W)] with K = P(√(1 − r) Z ≤ ·).

theorem ProbabilityTheory.Copula.bivariateNormal_real_Iic_mono {r r' : ℝ} (hr0 : 0 ≤ r) (hrr : r ≤ r') (hr1 : r' ≤ 1) (x y : ℝ) : (bivariateNormal r).real {p : ℝ × ℝ | p.1 ≤ x ∧ p.2 ≤ y} ≤ (bivariateNormal r').real {p : ℝ × ℝ | p.1 ≤ x ∧ p.2 ≤ y}

Slepian's inequality (bivariate, nonnegative correlations): for 0 ≤ r ≤ r' ≤ 1, the orthant probabilities of the bivariate normal law increase with the correlation.

Concordance ordering of the Gaussian copulas

theorem ProbabilityTheory.Copula.lowerOrthantLE_of_normalCDFPair {C D : Copula 2} (h : ∀ (q : ℝ × ℝ), C.cdf (normalCDFPair q) ≤ D.cdf (normalCDFPair q)) : C.LowerOrthantLE D

To compare two bivariate copulas pointwise it suffices to compare them at the points (Φ(x), Φ(y)), which exhaust the open unit square.

theorem ProbabilityTheory.Copula.bivariateGaussian_lowerOrthantLE_of_nonneg {r r' : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hr' : r' ∈ Set.Icc (-1) 1) (hr0 : 0 ≤ r) (hrr : r ≤ r') : (bivariateGaussian r hr).LowerOrthantLE (bivariateGaussian r' hr')

theorem ProbabilityTheory.Copula.bivariateGaussian_lowerOrthantLE_of_nonpos {r r' : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hr' : r' ∈ Set.Icc (-1) 1) (hr0 : r' ≤ 0) (hrr : r ≤ r') : (bivariateGaussian r hr).LowerOrthantLE (bivariateGaussian r' hr')

theorem ProbabilityTheory.Copula.bivariateGaussian_lowerOrthantLE {r r' : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hr' : r' ∈ Set.Icc (-1) 1) (hrr : r ≤ r') : (bivariateGaussian r hr).LowerOrthantLE (bivariateGaussian r' hr')

Slepian's inequality / concordance ordering: the bivariate Gaussian copulas increase pointwise with the correlation, r ≤ r' → C_r ≤ C_{r'}.

theorem ProbabilityTheory.Copula.bivariateGaussian_concordanceLE {r r' : ℝ} (hr : r ∈ Set.Icc (-1) 1) (hr' : r' ∈ Set.Icc (-1) 1) (hrr : r ≤ r') : (bivariateGaussian r hr).ConcordanceLE (bivariateGaussian r' hr')

The Gaussian copulas are increasing in r for the concordance order (lower and upper orthants).

theorem ProbabilityTheory.Copula.isPQD_bivariateGaussian_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (bivariateGaussian r hr).IsPQD ↔ 0 ≤ r

The bivariate Gaussian copula is positively quadrant dependent iff r ≥ 0.

theorem ProbabilityTheory.Copula.isNQD_bivariateGaussian_iff {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (bivariateGaussian r hr).IsNQD ↔ r ≤ 0

The bivariate Gaussian copula is negatively quadrant dependent iff r ≤ 0.