← Copula mathematical handbook

Markov products of checkerboard copulas

A checkerboard copula with cell masses A = (aᵢⱼ) on the grid P × Q has the piecewise constant density aᵢⱼ / (|Pᵢ| |Qⱼ|) on the cell Pᵢ × Qⱼ. Its conditional distribution functions are therefore

∂₁C(s, v) = ∑ᵢ 1_{Pᵢ}(s)/|Pᵢ| · ∑ⱼ aᵢⱼ coordⱼ(v) for almost every s

(conditionalCDF_checkerboard), and the Darsow–Nguyen–Olsen product of two checkerboards over a common middle grid Q is again a checkerboard, with the (width-normalized) matrix product of the cell masses (checkerboard_markovProduct_checkerboard):

(A ⋆ B)ᵢₖ = ∑ⱼ aᵢⱼ bⱼₖ / |Qⱼ|.

On uniform n-grids, with the doubly stochastic matrices n aᵢⱼ, this is the ordinary matrix product (Durante and Sempi 2016, §5.2 and §4.1; Darsow, Nguyen and Olsen 1992). We also record the transpose of a checkerboard (transpose_checkerboard).

noncomputable def ProbabilityTheory.Copula.IntervalPartition.cellDensity {n : ℕ} (P : IntervalPartition n) (i : Fin n) : ↑unitInterval → ℝ

The normalized indicator 1_{(pᵢ, pᵢ₊₁]} / |Pᵢ| of a cell: the uniform density on it.

Equations

• P.cellDensity i = (Set.Ioc (P.point i.castSucc) (P.point i.succ)).indicator fun (x : ↑unitInterval) => 1 / P.width i

theorem ProbabilityTheory.Copula.IntervalPartition.cellDensity_nonneg {n : ℕ} (P : IntervalPartition n) (i : Fin n) (s : ↑unitInterval) : 0 ≤ P.cellDensity i s

theorem ProbabilityTheory.Copula.IntervalPartition.measurable_cellDensity {n : ℕ} (P : IntervalPartition n) (i : Fin n) : Measurable (P.cellDensity i)

theorem ProbabilityTheory.Copula.IntervalPartition.integrable_cellDensity {n : ℕ} (P : IntervalPartition n) (i : Fin n) : MeasureTheory.Integrable (P.cellDensity i) MeasureTheory.volume

theorem ProbabilityTheory.Copula.IntervalPartition.setIntegral_cellDensity {n : ℕ} (P : IntervalPartition n) (i : Fin n) (u : ↑unitInterval) : ∫ (t : ↑unitInterval) in Set.Iic u, P.cellDensity i t = ↑(P.coord i u)

The cell density integrates to the clipped local coordinate: ∫_{[0,u]} 1_{Pᵢ}/|Pᵢ| = coordᵢ(u).

theorem ProbabilityTheory.Copula.IntervalPartition.integral_cellDensity {n : ℕ} (P : IntervalPartition n) (i : Fin n) : ∫ (t : ↑unitInterval), P.cellDensity i t = 1

The total mass of a cell density is one.

theorem ProbabilityTheory.Copula.IntervalPartition.cellDensity_mul {n : ℕ} (P : IntervalPartition n) (i j : Fin n) (s : ↑unitInterval) : P.cellDensity i s * P.cellDensity j s = if i = j then P.cellDensity i s / P.width i else 0

Distinct cells are disjoint: 1_{Pᵢ} 1_{Pⱼ} / (|Pᵢ||Pⱼ|) vanishes for i ≠ j.

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

The transposed cell masses on the grid Q × P.

Equations

• A.transpose = { mass := fun (j : Fin n) (i : Fin m) => A.mass i j, nonneg := ⋯, row_sum := ⋯, col_sum := ⋯ }

noncomputable def ProbabilityTheory.Copula.CellMass.mul {m n l : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} {R : IntervalPartition l} (A : CellMass P Q) (B : CellMass Q R) : CellMass P R

The width-normalized matrix product ∑ⱼ aᵢⱼ bⱼₖ / |Qⱼ| of cell masses.

Equations

• A.mul B = { mass := fun (i : Fin m) (k : Fin l) => ∑ j : Fin n, A.mass i j * B.mass j k / Q.width j, nonneg := ⋯, row_sum := ⋯, col_sum := ⋯ }

theorem ProbabilityTheory.Copula.CellMass.transpose_checkerboard {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) : A.checkerboard.transpose = A.transpose.checkerboard

The transpose of a checkerboard copula is the checkerboard of the transposed masses.

theorem ProbabilityTheory.Copula.CellMass.conditionalCDF_checkerboard {m n : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} (A : CellMass P Q) (v : ↑unitInterval) : (fun (s : ↑unitInterval) => A.checkerboard.conditionalCDF s v) =ᵐ[MeasureTheory.volume] fun (s : ↑unitInterval) => ∑ i : Fin m, P.cellDensity i s * ∑ j : Fin n, A.mass i j * ↑(Q.coord j v)

The conditional distribution functions of a checkerboard copula: ∂₁C(s,v) = ∑ᵢ 1_{Pᵢ}(s)/|Pᵢ| ∑ⱼ aᵢⱼ coordⱼ(v) for almost every s.

theorem ProbabilityTheory.Copula.CellMass.checkerboard_markovProduct_checkerboard {m n l : ℕ} {P : IntervalPartition m} {Q : IntervalPartition n} {R : IntervalPartition l} (A : CellMass P Q) (B : CellMass Q R) : A.checkerboard.markovProduct B.checkerboard = (A.mul B).checkerboard

The Markov product of two checkerboard copulas over a common middle grid is the checkerboard copula of the width-normalized matrix product of their cell masses.