← Copula mathematical handbook

The CDF integral formula and concordance monotonicity of Spearman's rho

theorem ProbabilityTheory.Copula.integral_unit_upper_indicator (u : ↑unitInterval) : (∫ (t : ↑unitInterval), if u ≤ t then 1 else 0) = 1 - ↑u

theorem ProbabilityTheory.Copula.integral_cdf_independence (C : Copula 2) : ∫ (x : Fin 2 → ↑unitInterval), C.cdf x ∂(independence 2).toMeasure = ∫ (x : Fin 2 → ↑unitInterval), ↑(x 0) * ↑(x 1) ∂C.toMeasure

The uniform CDF integral equals the mixed first moment.

theorem ProbabilityTheory.Copula.spearmanRho_eq_integral_cdf (C : Copula 2) : C.spearmanRho = 12 * ∫ (x : Fin 2 → ↑unitInterval), C.cdf x ∂(independence 2).toMeasure - 3

theorem ProbabilityTheory.Copula.spearmanRho_mono {C D : Copula 2} (h : ∀ (u : Fin 2 → ↑unitInterval), C.cdf u ≤ D.cdf u) : C.spearmanRho ≤ D.spearmanRho