← Copula mathematical handbook

The bivariate Gaussian copula

For a correlation r ∈ [-1, 1] let bivariateNormal r be the law of (Z₁, r Z₁ + √(1 − r²) Z₂) for independent standard normal Z₁, Z₂: the centered bivariate normal law with unit variances and correlation r. It is characterized by its linear forms (eq_bivariateNormal_of_linear_laws, a Cramér–Wold argument).

The bivariate Gaussian copula bivariateGaussian r hr is the library's gaussian copula for the correlation matrix !![1, r; r, 1]. We show:

• toMeasure_bivariateGaussian: it is the law of (Φ(X), Φ(Y)) for (X, Y) ~ bivariateNormal r;
• cdf_bivariateGaussian: C_r(Φ(x), Φ(y)) = P(X ≤ x, Y ≤ y), the classical formula C_r(u, v) = Φ_r(Φ⁻¹(u), Φ⁻¹(v)) given by Sklar's theorem (Joe 2014, §4.3);
• endpoint cases r = 0, 1, −1 give Π, M, W;
• C_r is exchangeable and radially symmetric, and reflecting one coordinate turns r into −r.

Standard normal CDF facts (strictMono_standardNormalCDF, standardNormalCDF_neg) are proved on the way.

References

• R. B. Nelsen, An Introduction to Copulas, 2nd ed., Springer 2006.
• H. Joe, Dependence Modeling with Copulas, CRC Press 2014, §4.3.

The standard normal CDF

theorem ProbabilityTheory.Copula.strictMono_standardNormalCDF : StrictMono ↑(ProbabilityTheory.cdf (gaussianReal 0 1))

The standard normal CDF Φ is strictly increasing.

theorem ProbabilityTheory.Copula.standardNormalCDF_neg (x : ℝ) : ↑(ProbabilityTheory.cdf (gaussianReal 0 1)) (-x) = 1 - ↑(ProbabilityTheory.cdf (gaussianReal 0 1)) x

Symmetry of the standard normal CDF: Φ(−x) = 1 − Φ(x).

theorem ProbabilityTheory.Copula.standardNormalCDF_zero : ↑(ProbabilityTheory.cdf (gaussianReal 0 1)) 0 = 1 / 2

Φ(0) = 1/2.

theorem ProbabilityTheory.Copula.standardNormalCDFUnit_neg (x : ℝ) : cdfUnit (gaussianReal 0 1) (-x) = unitInterval.symm (cdfUnit (gaussianReal 0 1) x)

Φ(−x) = 1 − Φ(x) as points of the unit interval.

theorem ProbabilityTheory.Copula.standardNormalCDFUnit_zero : cdfUnit (gaussianReal 0 1) 0 = unitHalf

Φ(0) = 1/2 as a point of the unit interval.

theorem ProbabilityTheory.Copula.standardNormalCDFUnit_le_iff {x y : ℝ} : cdfUnit (gaussianReal 0 1) x ≤ cdfUnit (gaussianReal 0 1) y ↔ x ≤ y

The standard bivariate normal law

noncomputable def ProbabilityTheory.Copula.bivariateNormal (r : ℝ) : MeasureTheory.Measure (ℝ × ℝ)

The centered bivariate normal law with unit variances and correlation r, realized as the law of (Z₁, r Z₁ + √(1 − r²) Z₂) for independent standard normal Z₁, Z₂.

Equations

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

instance ProbabilityTheory.Copula.instIsProbabilityMeasureProdRealBivariateNormal (r : ℝ) : MeasureTheory.IsProbabilityMeasure (bivariateNormal r)

theorem ProbabilityTheory.Copula.map_linear_bivariateNormal {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (a b : ℝ) : MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => a * p.1 + b * p.2) (bivariateNormal r) = gaussianReal 0 (a ^ 2 + 2 * a * b * r + b ^ 2).toNNReal

Linear forms of the bivariate normal law: aX + bY ~ N(0, a² + 2abr + b²).

theorem ProbabilityTheory.Copula.eq_bivariateNormal_of_linear_laws {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) {μ : MeasureTheory.Measure (ℝ × ℝ)} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (a b : ℝ), MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => a * p.1 + b * p.2) μ = gaussianReal 0 (a ^ 2 + 2 * a * b * r + b ^ 2).toNNReal) : μ = bivariateNormal r

Cramér–Wold characterization of the bivariate normal law.

theorem ProbabilityTheory.Copula.bivariateNormal_orthant {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (bivariateNormal r).real {p : ℝ × ℝ | p.1 ≤ 0 ∧ p.2 ≤ 0} = 1 / 4 + Real.arcsin r / (2 * Real.pi)

Sheppard's orthant formula for the bivariate normal law.

theorem ProbabilityTheory.Copula.bivariateNormal_map_swap {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : MeasureTheory.Measure.map Prod.swap (bivariateNormal r) = bivariateNormal r

The bivariate normal law is exchangeable.

theorem ProbabilityTheory.Copula.bivariateNormal_map_neg_snd {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => (p.1, -p.2)) (bivariateNormal r) = bivariateNormal (-r)

Changing the sign of the second coordinate changes the correlation r into −r.

theorem ProbabilityTheory.Copula.bivariateNormal_map_neg {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : MeasureTheory.Measure.map (fun (p : ℝ × ℝ) => (-p.1, -p.2)) (bivariateNormal r) = bivariateNormal r

Changing the sign of both coordinates preserves the bivariate normal law.

The correlation matrix and the Gaussian copula

def ProbabilityTheory.Copula.corrMatrix (r : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

The 2 × 2 correlation matrix with off-diagonal entry r.

Equations

• ProbabilityTheory.Copula.corrMatrix r = !![1, r; r, 1]

theorem ProbabilityTheory.Copula.corrMatrix_diag (r : ℝ) (i : Fin 2) : corrMatrix r i i = 1

theorem ProbabilityTheory.Copula.posSemidef_corrMatrix {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (corrMatrix r).PosSemidef

theorem ProbabilityTheory.Copula.map_linear_multivariateGaussian_corrMatrix {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (a b : ℝ) : MeasureTheory.Measure.map (fun (x : EuclideanSpace ℝ (Fin 2)) => a * x.ofLp 0 + b * x.ofLp 1) (multivariateGaussian 0 (corrMatrix r)) = gaussianReal 0 (a ^ 2 + 2 * a * b * r + b ^ 2).toNNReal

Linear forms of the multivariate normal law with correlation matrix corrMatrix r.

noncomputable def ProbabilityTheory.Copula.normalCDFPair (p : ℝ × ℝ) : Fin 2 → ↑unitInterval

The coordinate map (x, y) ↦ (Φ(x), Φ(y)) into the unit square.

Equations

• ProbabilityTheory.Copula.normalCDFPair p = ![ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) p.1, ProbabilityTheory.cdfUnit (ProbabilityTheory.gaussianReal 0 1) p.2]

theorem ProbabilityTheory.Copula.measurable_normalCDFPair : Measurable normalCDFPair

theorem ProbabilityTheory.Copula.normalCDFPair_le_iff (p q : ℝ × ℝ) : normalCDFPair p ≤ normalCDFPair q ↔ p.1 ≤ q.1 ∧ p.2 ≤ q.2

noncomputable def ProbabilityTheory.Copula.bivariateGaussian (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) : Copula 2

The bivariate Gaussian copula with correlation r ∈ [-1, 1].

Equations

• ProbabilityTheory.Copula.bivariateGaussian r hr = ProbabilityTheory.Copula.gaussian (ProbabilityTheory.Copula.corrMatrix r) ⋯ ⋯

theorem ProbabilityTheory.Copula.toMeasure_bivariateGaussian {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (bivariateGaussian r hr).toMeasure = MeasureTheory.Measure.map normalCDFPair (bivariateNormal r)

The bivariate Gaussian copula is the law of (Φ(X), Φ(Y)) for (X, Y) ~ bivariateNormal r.

theorem ProbabilityTheory.Copula.cdf_bivariateGaussian {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (q : ℝ × ℝ) : (bivariateGaussian r hr).cdf (normalCDFPair q) = (bivariateNormal r).real {p : ℝ × ℝ | p.1 ≤ q.1 ∧ p.2 ≤ q.2}

CDF of the bivariate Gaussian copula: C_r(Φ(x), Φ(y)) = P(X ≤ x, Y ≤ y) for (X, Y) ~ bivariateNormal r, i.e. C_r(u, v) = Φ_r(Φ⁻¹(u), Φ⁻¹(v)).

theorem ProbabilityTheory.Copula.exists_standardNormalCDFUnit_eq {u : ↑unitInterval} (hu0 : 0 < ↑u) (hu1 : ↑u < 1) : ∃ (x : ℝ), cdfUnit (gaussianReal 0 1) x = u

Every point of the open unit interval is a value of Φ.

Endpoints and symmetries

theorem ProbabilityTheory.Copula.gaussian_congr {d : ℕ} {R R' : Matrix (Fin d) (Fin d) ℝ} (h : R = R') (hR : R.PosSemidef) (hd : ∀ (i : Fin d), R i i = 1) (hR' : R'.PosSemidef) (hd' : ∀ (i : Fin d), R' i i = 1) : gaussian R hR hd = gaussian R' hR' hd'

theorem ProbabilityTheory.Copula.bivariateGaussian_congr {r r' : ℝ} (h : r = r') (hr : r ∈ Set.Icc (-1) 1) (hr' : r' ∈ Set.Icc (-1) 1) : bivariateGaussian r hr = bivariateGaussian r' hr'

theorem ProbabilityTheory.Copula.neg_mem_corrInterval {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : -r ∈ Set.Icc (-1) 1

@[simp]

theorem ProbabilityTheory.Copula.bivariateGaussian_zero (h : 0 ∈ Set.Icc (-1) 1) : bivariateGaussian 0 h = independence 2

Zero correlation gives the independence copula.

@[simp]

theorem ProbabilityTheory.Copula.bivariateGaussian_one (h : 1 ∈ Set.Icc (-1) 1) : bivariateGaussian 1 h = comonotonic 2

Correlation one gives the comonotonic copula M.

@[simp]

theorem ProbabilityTheory.Copula.transpose_bivariateGaussian {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (bivariateGaussian r hr).transpose = bivariateGaussian r hr

The bivariate Gaussian copula is exchangeable.

theorem ProbabilityTheory.Copula.isExchangeable_bivariateGaussian {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (bivariateGaussian r hr).IsExchangeable

theorem ProbabilityTheory.Copula.reflect_second_bivariateGaussian {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (bivariateGaussian r hr).reflect {1} = bivariateGaussian (-r) ⋯

Reflecting the second coordinate changes the correlation r into −r.

theorem ProbabilityTheory.Copula.reflect_first_bivariateGaussian {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (bivariateGaussian r hr).reflect {0} = bivariateGaussian (-r) ⋯

Reflecting the first coordinate changes the correlation r into −r.

@[simp]

theorem ProbabilityTheory.Copula.bivariateGaussian_neg_one (h : -1 ∈ Set.Icc (-1) 1) : bivariateGaussian (-1) h = countermonotonic

Correlation −1 gives the countermonotonic copula W.

@[simp]

theorem ProbabilityTheory.Copula.survivalCopula_bivariateGaussian {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (bivariateGaussian r hr).survivalCopula = bivariateGaussian r hr

The bivariate Gaussian copula is radially symmetric: Ĉ_r = C_r.

theorem ProbabilityTheory.Copula.isRadiallySymmetric_bivariateGaussian {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) : (bivariateGaussian r hr).IsRadiallySymmetric