← Mathematical handbook

theorem Verification.patchwork_survival {m n : ℕ} {P : ProbabilityTheory.Copula.IntervalPartition m} {Q : ProbabilityTheory.Copula.IntervalPartition n} (A : ProbabilityTheory.Copula.CellMass P Q) (C : Fin m → Fin n → ProbabilityTheory.Copula 2) (u v : ↑unitInterval) : (A.patchwork C).survival ![u, v] = ∑ i : Fin m, ∑ j : Fin n, A.mass i j * (C i j).survival ![P.coord i u, Q.coord j v]

theorem Verification.survival_independence_two (u v : ↑unitInterval) : (ProbabilityTheory.Copula.independence 2).survival ![u, v] = (1 - ↑u) * (1 - ↑v)

theorem Verification.survival_comonotonic_two (u v : ↑unitInterval) : (ProbabilityTheory.Copula.comonotonic 2).survival ![u, v] = min (1 - ↑u) (1 - ↑v)

theorem Verification.survival_countermonotonic_two (u v : ↑unitInterval) : ProbabilityTheory.Copula.countermonotonic.survival ![u, v] = max (1 - ↑u + (1 - ↑v) - 1) 0