← Copula mathematical handbook

Upper orthants and survival probabilities

noncomputable def ProbabilityTheory.Copula.survival {d : ℕ} (C : Copula d) (u : Fin d → ↑unitInterval) : ℝ

Upper orthant probability, using closed coordinate orthants. Uniform marginals make the choice of open or closed faces immaterial.

Equations

• C.survival u = C.toMeasure.real (Set.Ici u)

theorem ProbabilityTheory.Copula.ae_eval_ne {d : ℕ} (C : Copula d) (i : Fin d) (t : ↑unitInterval) : ∀ᵐ (x : Fin d → ↑unitInterval) ∂C.toMeasure, x i ≠ t

theorem ProbabilityTheory.Copula.survival_eq_strict {d : ℕ} (C : Copula d) (u : Fin d → ↑unitInterval) : C.survival u = C.toMeasure.real {x : Fin d → ↑unitInterval | ∀ (i : Fin d), u i < x i}

theorem ProbabilityTheory.Copula.survival_eq_cdf_reflect {d : ℕ} (C : Copula d) (u : Fin d → ↑unitInterval) : C.survival u = (C.reflect Finset.univ).cdf (reflectPoint Finset.univ u)

theorem ProbabilityTheory.Copula.survival_two (C : Copula 2) (u : Fin 2 → ↑unitInterval) : C.survival u = 1 - ↑(u 0) - ↑(u 1) + C.cdf u