← Copula mathematical handbook

Shuffles of M are dense in the bivariate copulas

This file formalizes Nelsen, An Introduction to Copulas, 2nd ed., Theorem 3.2.2 (Mikusiński, Sherwood and Taylor, 1992): for every copula C and every ε > 0 there is a straight shuffle of M whose CDF is uniformly within ε of C.

The construction follows the classical proof. Fix a partition P of [0,1] into n cells and let m i j be the C-mass of the cell P_i × P_j (a CellMass P P). Split the vertical strip P_i into consecutive pieces of lengths m i 0, m i 1, … and the horizontal strip P_j into consecutive pieces of lengths m 0 j, m 1 j, …; the piece (i, j) of the first strip is sent by a translation onto the piece (i, j) of the second one. In the terminology of Copula.Shuffle.Weights the source order of the pieces is lexicographic in (i, j) and the target order is lexicographic in (j, i); zero-mass pieces are discarded automatically.

The resulting straight shuffle A.shuffle puts mass m i j into every cell, so it agrees with C at all grid vertices (cdf_gridShuffle_point); both CDFs are monotone and Lipschitz, which gives |S(u,v) - C(u,v)| ≤ 2/n on the uniform grid (abs_cdf_gridShuffle_uniform_sub_le).

Main results

• CellMass.shuffle, cdf_cellMass_shuffle_point: exact grid interpolation by a shuffle.
• abs_cdf_sub_le_of_eq_on_grid: two copulas that agree on a grid are close.
• uniformCDFDistance_gridShuffle_le: d∞(S_n, C) ≤ 2/n.
• tendstoUniformly_gridShuffle: uniform convergence along refining uniform grids.
• exists_isStraightShuffleOfMin_uniformCDFDistance_lt: Nelsen, Theorem 3.2.2.
• dense_isStraightShuffleOfMin, dense_isShuffleOfMin: density in the uniform metric uniformMetricSpace 2.

Copulas agreeing on a grid

theorem ProbabilityTheory.Copula.abs_cdf_sub_le_of_eq_on_grid {m n : ℕ} (S C : Copula 2) (P : IntervalPartition m) (Q : IntervalPartition n) (h : ∀ (k : Fin (m + 1)) (l : Fin (n + 1)), S.cdf ![P.point k, Q.point l] = C.cdf ![P.point k, Q.point l]) (dx dy : ℝ) (hx : ∀ (i : Fin m), P.width i ≤ dx) (hy : ∀ (j : Fin n), Q.width j ≤ dy) (u v : ↑unitInterval) : |S.cdf ![u, v] - C.cdf ![u, v]| ≤ dx + dy

Two copulas whose CDFs agree at all vertices of a grid differ by at most the mesh sizes.

Lexicographic offsets of the pieces

def ProbabilityTheory.Copula.lexRank {n : ℕ} (q : Fin n × Fin n) : ℕ

The lexicographic rank of the cell (i, j) among the n × n cells (i is the major key).

Equations

• ProbabilityTheory.Copula.lexRank q = ↑(finProdFinEquiv q)

theorem ProbabilityTheory.Copula.lexRank_eq {n : ℕ} (q : Fin n × Fin n) : lexRank q = ↑q.2 + n * ↑q.1

def ProbabilityTheory.Copula.lexOffset {n : ℕ} (m : Fin n → Fin n → ℝ) (i j : Fin n) : ℝ

The total mass of the cells lexicographically before (i, j).

Equations

• ProbabilityTheory.Copula.lexOffset m i j = ∑ q : Fin n × Fin n, if ProbabilityTheory.Copula.lexRank q < ProbabilityTheory.Copula.lexRank (i, j) then m q.1 q.2 else 0

theorem ProbabilityTheory.Copula.lt_lexRank_of_fst_lt {n : ℕ} {q p : Fin n × Fin n} (h : q.1 < p.1) : lexRank q < lexRank p

theorem ProbabilityTheory.Copula.fst_le_of_lexRank_le {n : ℕ} {q p : Fin n × Fin n} (h : lexRank q ≤ lexRank p) : q.1 ≤ p.1

theorem ProbabilityTheory.Copula.sum_rows_lt {n : ℕ} {P : IntervalPartition n} (m : Fin n → Fin n → ℝ) (hrow : ∀ (i : Fin n), ∑ j : Fin n, m i j = P.width i) (k : Fin (n + 1)) : (∑ q : Fin n × Fin n, if ↑q.1 < ↑k then m q.1 q.2 else 0) = ↑(P.point k)

Summing the rows before a threshold gives the partition point.

theorem ProbabilityTheory.Copula.point_castSucc_le_lexOffset {n : ℕ} {P : IntervalPartition n} (m : Fin n → Fin n → ℝ) (hm0 : ∀ (i j : Fin n), 0 ≤ m i j) (hrow : ∀ (i : Fin n), ∑ j : Fin n, m i j = P.width i) (i j : Fin n) : ↑(P.point i.castSucc) ≤ lexOffset m i j

theorem ProbabilityTheory.Copula.lexOffset_add_le_point_succ {n : ℕ} {P : IntervalPartition n} (m : Fin n → Fin n → ℝ) (hm0 : ∀ (i j : Fin n), 0 ≤ m i j) (hrow : ∀ (i : Fin n), ∑ j : Fin n, m i j = P.width i) (i j : Fin n) : lexOffset m i j + m i j ≤ ↑(P.point i.succ)

theorem ProbabilityTheory.Copula.clipLength_point_sub_lexOffset {n : ℕ} {P : IntervalPartition n} (m : Fin n → Fin n → ℝ) (hm0 : ∀ (i j : Fin n), 0 ≤ m i j) (hrow : ∀ (i : Fin n), ∑ j : Fin n, m i j = P.width i) (k : Fin (n + 1)) (i j : Fin n) : clipLength (↑(P.point k) - lexOffset m i j) (m i j) = if ↑i < ↑k then m i j else 0

At a grid point the clipped length of a piece is all or nothing.

The shuffle of a matrix of cell masses

def ProbabilityTheory.Copula.CellMass.lexWeights {n : ℕ} {P : IntervalPartition n} (A : CellMass P P) (k : Fin (n * n)) : ℝ

The masses listed in lexicographic order of the cells.

Equations

• A.lexWeights k = A.mass (finProdFinEquiv.symm k).1 (finProdFinEquiv.symm k).2

theorem ProbabilityTheory.Copula.CellMass.lexWeights_nonneg {n : ℕ} {P : IntervalPartition n} (A : CellMass P P) (k : Fin (n * n)) : 0 ≤ A.lexWeights k

theorem ProbabilityTheory.Copula.CellMass.sum_lexWeights {n : ℕ} {P : IntervalPartition n} (A : CellMass P P) : ∑ k : Fin (n * n), A.lexWeights k = 1

def ProbabilityTheory.Copula.CellMass.transposeRank (n : ℕ) : Equiv.Perm (Fin (n * n))

The permutation of the cells from lexicographic (i, j) order to lexicographic (j, i) order.

Equations

• ProbabilityTheory.Copula.CellMass.transposeRank n = finProdFinEquiv.symm.trans ((Equiv.prodComm (Fin n) (Fin n)).trans finProdFinEquiv)

theorem ProbabilityTheory.Copula.CellMass.transposeRank_apply {n : ℕ} (q : Fin n × Fin n) : (transposeRank n) (finProdFinEquiv q) = finProdFinEquiv (q.2, q.1)

noncomputable def ProbabilityTheory.Copula.CellMass.shuffle {n : ℕ} {P : IntervalPartition n} (A : CellMass P P) : Copula 2

The straight shuffle of M that puts the mass A.mass i j into the cell P_i × P_j (Nelsen, proof of Theorem 3.2.2).

Equations

• A.shuffle = ProbabilityTheory.Copula.weightShuffle A.lexWeights ⋯ ⋯ (ProbabilityTheory.Copula.CellMass.transposeRank n)

theorem ProbabilityTheory.Copula.CellMass.isStraightShuffleOfMin_shuffle {n : ℕ} {P : IntervalPartition n} (A : CellMass P P) : A.shuffle.IsStraightShuffleOfMin

theorem ProbabilityTheory.Copula.CellMass.prefixSum_lexWeights {n : ℕ} {P : IntervalPartition n} (A : CellMass P P) (q : Fin n × Fin n) : prefixSum A.lexWeights ↑(finProdFinEquiv q) = lexOffset A.mass q.1 q.2

theorem ProbabilityTheory.Copula.CellMass.targetOffset_lexWeights {n : ℕ} {P : IntervalPartition n} (A : CellMass P P) (q : Fin n × Fin n) : targetOffset A.lexWeights (transposeRank n) (finProdFinEquiv q) = lexOffset (fun (j i : Fin n) => A.mass i j) q.2 q.1

theorem ProbabilityTheory.Copula.CellMass.cdf_shuffle_point {n : ℕ} {P : IntervalPartition n} (A : CellMass P P) (k l : Fin (n + 1)) : A.shuffle.cdf ![P.point k, P.point l] = ∑ i : Fin n, if ↑i < ↑k then ∑ j : Fin n, if ↑j < ↑l then A.mass i j else 0 else 0

The shuffle of a matrix of cell masses has the prescribed cumulative masses at every grid vertex.

Grid shuffles of a copula

noncomputable def ProbabilityTheory.Copula.gridShuffle {n : ℕ} (C : Copula 2) (P : IntervalPartition n) : Copula 2

The straight shuffle of M carrying the C-mass of every cell of the grid P × P.

Equations

• C.gridShuffle P = (C.cellMass P P).shuffle

theorem ProbabilityTheory.Copula.isStraightShuffleOfMin_gridShuffle {n : ℕ} (C : Copula 2) (P : IntervalPartition n) : (C.gridShuffle P).IsStraightShuffleOfMin

theorem ProbabilityTheory.Copula.isShuffleOfMin_gridShuffle {n : ℕ} (C : Copula 2) (P : IntervalPartition n) : (C.gridShuffle P).IsShuffleOfMin

theorem ProbabilityTheory.Copula.cdf_gridShuffle_point {n : ℕ} (C : Copula 2) (P : IntervalPartition n) (k l : Fin (n + 1)) : (C.gridShuffle P).cdf ![P.point k, P.point l] = C.cdf ![P.point k, P.point l]

The grid shuffle agrees with C at every vertex of the grid.

theorem ProbabilityTheory.Copula.abs_cdf_gridShuffle_sub_le {n : ℕ} (C : Copula 2) (P : IntervalPartition n) (δ : ℝ) (hδ : ∀ (i : Fin n), P.width i ≤ δ) (u v : ↑unitInterval) : |(C.gridShuffle P).cdf ![u, v] - C.cdf ![u, v]| ≤ 2 * δ

The CDF error of a grid shuffle is at most twice the mesh.

theorem ProbabilityTheory.Copula.abs_cdf_gridShuffle_uniform_sub_le {n : ℕ} (C : Copula 2) (hn : 0 < n) (u v : ↑unitInterval) : |(C.gridShuffle (IntervalPartition.uniform n hn)).cdf ![u, v] - C.cdf ![u, v]| ≤ 2 / ↑n

On the uniform grid with n cells, the grid shuffle is within 2/n of C.

theorem ProbabilityTheory.Copula.uniformCDFDistance_gridShuffle_le {n : ℕ} (C : Copula 2) (hn : 0 < n) : (C.gridShuffle (IntervalPartition.uniform n hn)).uniformCDFDistance C ≤ 2 / ↑n

theorem ProbabilityTheory.Copula.tendsto_uniformCDFDistance_gridShuffle (C : Copula 2) : Filter.Tendsto (fun (k : ℕ) => (C.gridShuffle (IntervalPartition.uniform (k + 1) ⋯)).uniformCDFDistance C) Filter.atTop (nhds 0)

Grid shuffles along refining uniform grids converge uniformly to C.

theorem ProbabilityTheory.Copula.tendstoUniformly_gridShuffle (C : Copula 2) : TendstoUniformly (fun (k : ℕ) => (C.gridShuffle (IntervalPartition.uniform (k + 1) ⋯)).cdf) C.cdf Filter.atTop

theorem ProbabilityTheory.Copula.exists_isStraightShuffleOfMin_uniformCDFDistance_lt (C : Copula 2) {ε : ℝ} (hε : 0 < ε) : ∃ (S : Copula 2), S.IsStraightShuffleOfMin ∧ S.uniformCDFDistance C < ε

Nelsen, Theorem 3.2.2 (Mikusiński–Sherwood–Taylor): every bivariate copula is uniformly approximated by straight shuffles of M.

theorem ProbabilityTheory.Copula.exists_isStraightShuffleOfMin_abs_cdf_sub_lt (C : Copula 2) {ε : ℝ} (hε : 0 < ε) : ∃ (S : Copula 2), S.IsStraightShuffleOfMin ∧ ∀ (u v : ↑unitInterval), |S.cdf ![u, v] - C.cdf ![u, v]| < ε

Pointwise form of Nelsen, Theorem 3.2.2.

theorem ProbabilityTheory.Copula.dense_isStraightShuffleOfMin : Dense {S : Copula 2 | S.IsStraightShuffleOfMin}

Straight shuffles of M are dense in the bivariate copulas for the uniform metric.

theorem ProbabilityTheory.Copula.dense_isShuffleOfMin : Dense {S : Copula 2 | S.IsShuffleOfMin}

Shuffles of M are dense in the bivariate copulas for the uniform metric.

theorem ProbabilityTheory.Copula.exists_seq_isStraightShuffleOfMin_tendstoUniformly (C : Copula 2) : ∃ (S : ℕ → Copula 2), (∀ (k : ℕ), (S k).IsStraightShuffleOfMin) ∧ TendstoUniformly (fun (k : ℕ) => (S k).cdf) C.cdf Filter.atTop

Every bivariate copula is the uniform limit of a sequence of straight shuffles of M.