← Mathematical handbook

Measurable functional dependence survives ordinal sums

def Verification.HasFunctionalWitness (C : ProbabilityTheory.Copula 2) : Prop

Equations

• Verification.HasFunctionalWitness C = ∃ (f : ↑unitInterval → ↑unitInterval), Measurable f ∧ ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂C.toMeasure, x 1 = f (x 0)

theorem Verification.HasFunctionalWitness.xi_eq_one {C : ProbabilityTheory.Copula 2} (h : HasFunctionalWitness C) : C.chatterjeeXi = 1

theorem Verification.functional_comonotonic : HasFunctionalWitness (ProbabilityTheory.Copula.comonotonic 2)

theorem Verification.functional_countermonotonic : HasFunctionalWitness ProbabilityTheory.Copula.countermonotonic

theorem Verification.HasFunctionalWitness.ordinalSum {C D : ProbabilityTheory.Copula 2} (hC : HasFunctionalWitness C) (hD : HasFunctionalWitness D) (a : ↑unitInterval) : HasFunctionalWitness (C.ordinalSum D a)