← Copula mathematical handbook

Algebraic laws of the Markov product

Further properties of the Darsow–Nguyen–Olsen Markov product A * B = A.markovProduct B (Darsow, Nguyen and Olsen, Copulas and Markov processes, Illinois J. Math. 36 (1992); Durante and Sempi, Principles of Copula Theory, §5.2), complementing Copula.MarkovProduct (associativity, M is the identity, Π is absorbing) and Copula.Rearrangement (W * W = M, products of graph copulas):

• the classical CDF formula (A * B)(u,v) = ∫₀¹ ∂₂A(u,s) ∂₁B(s,v) ds, with the partial derivatives realized by the conditional distribution functions of Aᵀ and B (cdf_markovProduct_eq_integral);
• the transposition law (A * B)ᵀ = Bᵀ * Aᵀ (transpose_markovProduct);
• multiplication by a graph copula on the right transforms the second coordinate (markovProduct_graphCopula_right), so C * W and W * C are the reflections of C in the second and first coordinate;
• ξ(C) = 6 ∫₀¹ (Cᵀ * C)(t,t) dt - 2, and Cᵀ * C = M if and only if ξ(C) = 1 (in particular for completely dependent copulas, which are left invertible);
• the data-processing inequality ξ(A * B) ≤ ξ(B) for Chatterjee's xi.

Disintegration along the first coordinate

theorem ProbabilityTheory.Copula.map_pair_eq_compProd_conditionalKernel (C : Copula 2) : MeasureTheory.Measure.map (fun (x : Fin 2 → ↑unitInterval) => (x 0, x 1)) C.toMeasure = MeasureTheory.volume.compProd C.conditionalKernel

theorem ProbabilityTheory.Copula.integral_mul_eq_integral_conditionalKernel (C : Copula 2) {f g : ↑unitInterval → ℝ} (hf : Measurable f) (hg : Measurable g) (hf1 : ∀ (t : ↑unitInterval), |f t| ≤ 1) (hg1 : ∀ (s : ↑unitInterval), |g s| ≤ 1) : ∫ (x : Fin 2 → ↑unitInterval), f (x 0) * g (x 1) ∂C.toMeasure = ∫ (t : ↑unitInterval), f t * ∫ (s : ↑unitInterval), g s ∂C.conditionalKernel t

Integrals of products of bounded functions of the two coordinates, disintegrated along the first coordinate.

theorem ProbabilityTheory.Copula.measureReal_comp_eq_integral (κ η : Kernel ↑unitInterval ↑unitInterval) [IsMarkovKernel κ] [IsMarkovKernel η] (t : ↑unitInterval) {S : Set ↑unitInterval} (hS : MeasurableSet S) : ((η.comp κ) t).real S = ∫ (s : ↑unitInterval), (η s).real S ∂κ t

theorem ProbabilityTheory.Copula.abs_conditionalCDF_le_one (C : Copula 2) (u t : ↑unitInterval) : |C.conditionalCDF u t| ≤ 1

theorem ProbabilityTheory.Copula.abs_indicator_one_le_one (S : Set ↑unitInterval) (t : ↑unitInterval) : |S.indicator 1 t| ≤ 1

The CDF of the Markov product

theorem ProbabilityTheory.Copula.cdf_markovProduct_eq_integral (A B : Copula 2) (u v : ↑unitInterval) : (A.markovProduct B).cdf ![u, v] = ∫ (s : ↑unitInterval), A.transpose.conditionalCDF s u * B.conditionalCDF s v

The classical formula (A * B)(u,v) = ∫₀¹ ∂₂A(u,s) ∂₁B(s,v) ds: the partial derivative ∂₂A(u,s) = P(U ≤ u | V = s) is the conditional CDF of the transpose.

theorem ProbabilityTheory.Copula.transpose_markovProduct (A B : Copula 2) : (A.markovProduct B).transpose = B.transpose.markovProduct A.transpose

The transposition law of the Markov product, (A * B)ᵀ = Bᵀ * Aᵀ.

Graph copulas on the right

theorem ProbabilityTheory.Copula.markovProduct_graphCopula_right (C : Copula 2) (f : ↑unitInterval → ↑unitInterval) (hf : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) : C.markovProduct (graphCopula f hf) = C.rearrange ![id, f] ⋯

Multiplying by the graph copula of a measure-preserving map f on the right applies f to the second coordinate.

@[simp]

theorem ProbabilityTheory.Copula.markovProduct_countermonotonic (C : Copula 2) : C.markovProduct countermonotonic = C.reflect {1}

Right multiplication by W reflects the second coordinate: C * W = C.reflect {1}.

@[simp]

theorem ProbabilityTheory.Copula.countermonotonic_markovProduct (C : Copula 2) : countermonotonic.markovProduct C = C.reflect {0}

Left multiplication by W reflects the first coordinate: W * C = C.reflect {0}.

Left invertibility and Chatterjee's xi

theorem ProbabilityTheory.Copula.cdf_transpose_markovProduct_self (C : Copula 2) (u v : ↑unitInterval) : (C.transpose.markovProduct C).cdf ![u, v] = ∫ (s : ↑unitInterval), C.conditionalCDF s u * C.conditionalCDF s v

(Cᵀ * C)(u,v) = ∫₀¹ ∂₁C(s,u) ∂₁C(s,v) ds.

theorem ProbabilityTheory.Copula.chatterjeeXi_eq_integral_diagonal_transpose_markovProduct (C : Copula 2) : C.chatterjeeXi = (6 * ∫ (t : ↑unitInterval), (C.transpose.markovProduct C).cdf ![t, t]) - 2

Chatterjee's xi through the diagonal of Cᵀ * C: ξ(C) = 6 ∫₀¹ (Cᵀ * C)(t,t) dt - 2.

theorem ProbabilityTheory.Copula.transpose_markovProduct_self_eq_comonotonic_iff (C : Copula 2) : C.transpose.markovProduct C = comonotonic 2 ↔ C.chatterjeeXi = 1

Cᵀ * C = M (i.e. C is left invertible) if and only if ξ(C) = 1.

theorem ProbabilityTheory.Copula.IsCompletelyDependent.transpose_markovProduct_self {C : Copula 2} (h : C.IsCompletelyDependent) : C.transpose.markovProduct C = comonotonic 2

Completely dependent copulas are left invertible: Cᵀ * C = M.

Data processing for Chatterjee's xi

theorem ProbabilityTheory.Copula.sq_integral_le_integral_sq_of_unit {ν : MeasureTheory.Measure ↑unitInterval} [MeasureTheory.IsProbabilityMeasure ν] {g : ↑unitInterval → ℝ} (hg : Measurable g) (hg0 : ∀ (s : ↑unitInterval), 0 ≤ g s) (hg1 : ∀ (s : ↑unitInterval), g s ≤ 1) : (∫ (s : ↑unitInterval), g s ∂ν) ^ 2 ≤ ∫ (s : ↑unitInterval), g s ^ 2 ∂ν

Jensen's inequality (∫ g)² ≤ ∫ g² for a [0,1]-valued function and a probability measure.

theorem ProbabilityTheory.Copula.integral_integral_conditionalKernel (C : Copula 2) {g : ↑unitInterval → ℝ} (hg : Measurable g) (hg1 : ∀ (s : ↑unitInterval), |g s| ≤ 1) : ∫ (u : ↑unitInterval), ∫ (s : ↑unitInterval), g s ∂C.conditionalKernel u = ∫ (s : ↑unitInterval), g s

Averaging a bounded measurable function against the conditional laws recovers the uniform second marginal.

theorem ProbabilityTheory.Copula.chatterjeeXi_markovProduct_le (A B : Copula 2) : (A.markovProduct B).chatterjeeXi ≤ B.chatterjeeXi

The data-processing inequality for Chatterjee's xi: ξ(A * B) ≤ ξ(B). Following the transition of A before that of B cannot increase the dependence of the endpoint on the starting point.