Documentation

Copula.Rank.Region.Common.Functional

← Copula mathematical handbook

Measurable functional dependence survives ordinal sums #

def ProbabilityTheory.Copula.RankRegion.Common.HasFunctionalWitness (C : Copula 2) :

Equations

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

Instances For

theorem ProbabilityTheory.Copula.RankRegion.Common.HasFunctionalWitness.xi_eq_one {C : Copula 2} (h : HasFunctionalWitness C) :

C.chatterjeeXi = 1

theorem ProbabilityTheory.Copula.RankRegion.Common.functional_comonotonic :

HasFunctionalWitness (comonotonic 2)

theorem ProbabilityTheory.Copula.RankRegion.Common.functional_countermonotonic :

HasFunctionalWitness countermonotonic

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

HasFunctionalWitness (C.ordinalSum D a)