← Mathematical handbook

The diagonal evaluated at a coordinate maximum

The integral identity in Kokol Bukovšek–Stopar (2023), Proposition 1, holds directly for every copula measure: the maximum has no atoms and two independent copies are equally likely to occur in either order.

theorem ProbabilityTheory.Copula.ae_max_ne (C : Copula 2) (t : ↑unitInterval) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, max (x 0) (x 1) ≠ t

theorem ProbabilityTheory.Copula.integral_diagonal_max (C : Copula 2) : ∫ (x : Fin 2 → ↑unitInterval), C.diagonal (max (x 0) (x 1)) ∂C.toMeasure = 1 / 2

The expected CDF of the atomless coordinate maximum is one half.