← Copula mathematical handbook

Sharp bounds for directional and symmetrized Blest correlation

theorem ProbabilityTheory.Copula.integral_unit_one_sub_pow (n : ℕ) : ∫ (u : ↑unitInterval), (1 - ↑u) ^ n = 1 / (↑n + 1)

theorem ProbabilityTheory.Copula.blestNu_mem_Icc (C : Copula 2) : C.blestNu ∈ Set.Icc (-1) 1

theorem ProbabilityTheory.Copula.symmetrizedBlest_mem_Icc (C : Copula 2) : C.symmetrizedBlest ∈ Set.Icc (-1) 1