← Copula mathematical handbook

Checkerboard, check-min and local-copula grid constructions

Entries are cell probabilities: row sums are row widths and column sums are column widths. The grid can be rectangular and nonuniform. In particular, no implicit matrix normalization or equal-marginal assumption is hidden in a constructor.

structure ProbabilityTheory.Copula.CellMass {m n : ℕ} (P : IntervalPartition m) (Q : IntervalPartition n) : Type

A nonnegative matrix of cell probabilities with prescribed uniform marginals.

• mass : Fin m → Fin n → ℝ
• nonneg (i : Fin m) (j : Fin n) : 0 ≤ self.mass i j
• row_sum (i : Fin m) : ∑ j : Fin n, self.mass i j = P.width i
• col_sum (j : Fin n) : ∑ i : Fin m, self.mass i j = Q.width j

noncomputable def ProbabilityTheory.Copula.CellMass.patchworkData {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) : PatchworkData (Fin m × Fin n)

The coordinate and weight data attached to a matrix of cell masses.

Equations

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

noncomputable def ProbabilityTheory.Copula.CellMass.patchwork {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) : Copula 2

Fill every cell with an independently specified local copula.

Equations

• A.patchwork C = A.patchworkData.copula fun (ij : Fin m × Fin n) => C ij.1 ij.2

@[simp]

theorem ProbabilityTheory.Copula.CellMass.cdf_patchwork {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (C : Fin m → Fin n → Copula 2) (u : Fin 2 → ↑unitInterval) : (A.patchwork C).cdf u = ∑ i : Fin m, ∑ j : Fin n, A.mass i j * (C i j).cdf ![P.coord i (u 0), Q.coord j (u 1)]

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

Checkerboard copula: independent local coordinates in every cell.

Equations

• A.checkerboard = A.patchwork fun (x : Fin m) (x_1 : Fin n) => ProbabilityTheory.Copula.independence 2

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

Check-min copula: comonotonic local coordinates in every cell.

Equations

• A.checkMin = A.patchwork fun (x : Fin m) (x_1 : Fin n) => ProbabilityTheory.Copula.comonotonic 2

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

Check-W copula: countermonotonic local coordinates in every cell.

Equations

• A.checkW = A.patchwork fun (x : Fin m) (x_1 : Fin n) => ProbabilityTheory.Copula.countermonotonic

theorem ProbabilityTheory.Copula.CellMass.cdf_checkerboard {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (u v : ↑unitInterval) : A.checkerboard.cdf ![u, v] = ∑ i : Fin m, ∑ j : Fin n, A.mass i j * (↑(P.coord i u) * ↑(Q.coord j v))

theorem ProbabilityTheory.Copula.CellMass.cdf_checkMin {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (u v : ↑unitInterval) : A.checkMin.cdf ![u, v] = ∑ i : Fin m, ∑ j : Fin n, A.mass i j * min ↑(P.coord i u) ↑(Q.coord j v)

theorem ProbabilityTheory.Copula.CellMass.cdf_checkW {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (u v : ↑unitInterval) : A.checkW.cdf ![u, v] = ∑ i : Fin m, ∑ j : Fin n, A.mass i j * max (↑(P.coord i u) + ↑(Q.coord j v) - 1) 0

theorem ProbabilityTheory.Copula.CellMass.checkerboard_le_checkMin {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (u : Fin 2 → ↑unitInterval) : A.checkerboard.cdf u ≤ A.checkMin.cdf u

def ProbabilityTheory.Copula.CellMass.product {m n : ℕ} (P : IntervalPartition m) (Q : IntervalPartition n) : CellMass P Q

The product matrix produces global independence under checkerboard filling.

Equations

• ProbabilityTheory.Copula.CellMass.product P Q = { mass := fun (i : Fin m) (j : Fin n) => P.width i * Q.width j, nonneg := ⋯, row_sum := ⋯, col_sum := ⋯ }

@[simp]

theorem ProbabilityTheory.Copula.CellMass.checkerboard_product {m n : ℕ} (P : IntervalPartition m) (Q : IntervalPartition n) : (product P Q).checkerboard = independence 2

noncomputable def ProbabilityTheory.Copula.cellMass {m n : ℕ} (C : Copula 2) (P : IntervalPartition m) (Q : IntervalPartition n) : CellMass P Q

Sample the actual rectangle probabilities of a copula on a finite grid.

Equations

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

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

Checkerboard approximation on the chosen grid.

Equations

• C.checkerboard P Q = (C.cellMass P Q).checkerboard

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

Check-min approximation on the chosen grid.

Equations

• C.checkMin P Q = (C.cellMass P Q).checkMin