← Mathematical handbook

Almost-sure characterizations of the bivariate Fréchet bounds

Uniform coordinates agree almost surely exactly for the comonotonic copula. They sum to one almost surely exactly for the countermonotonic copula. These statements apply to arbitrary copula measures, including singular ones.

theorem ProbabilityTheory.Copula.ae_eval_eq_comonotonic : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂(comonotonic 2).toMeasure, x 0 = x 1

theorem ProbabilityTheory.Copula.eq_comonotonic_iff_ae_eval_eq (C : Copula 2) : C = comonotonic 2 ↔ ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, x 0 = x 1

theorem ProbabilityTheory.Copula.ae_eval_eq_symm_countermonotonic : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂countermonotonic.toMeasure, x 1 = unitInterval.symm (x 0)

theorem ProbabilityTheory.Copula.eq_countermonotonic_iff_ae_eval_eq_symm (C : Copula 2) : C = countermonotonic ↔ ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, x 1 = unitInterval.symm (x 0)

theorem ProbabilityTheory.Copula.eq_countermonotonic_iff_ae_add_eq_one (C : Copula 2) : C = countermonotonic ↔ ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, ↑(x 0) + ↑(x 1) = 1