Documentation

Copula.Order.Orthant

← Mathematical handbook

Lower orthant, upper orthant, and concordance orders #

These predicates use the copula convention: smaller lower orthant probabilities mean a smaller copula. No global LE instance selects one of the different orders.

source
def ProbabilityTheory.Copula.LowerOrthantLE {d : ℕ} (C D : Copula d) :
Prop

Pointwise comparison of distribution functions.

Equations
Instances For
    source
    def ProbabilityTheory.Copula.UpperOrthantLE {d : ℕ} (C D : Copula d) :
    Prop

    Pointwise comparison of upper orthant probabilities.

    Equations
    Instances For
      source
      def ProbabilityTheory.Copula.ConcordanceLE {d : ℕ} (C D : Copula d) :
      Prop

      Concordance compares both lower and upper orthants.

      Equations
      Instances For
        source
        theorem ProbabilityTheory.Copula.LowerOrthantLE.refl {d : ℕ} (C : Copula d) :
        C.LowerOrthantLE C
        source
        theorem ProbabilityTheory.Copula.LowerOrthantLE.trans {d : ℕ} {C D E : Copula d} (h : C.LowerOrthantLE D) (k : D.LowerOrthantLE E) :
        C.LowerOrthantLE E
        source
        theorem ProbabilityTheory.Copula.LowerOrthantLE.antisymm {d : ℕ} {C D : Copula d} (h : C.LowerOrthantLE D) (k : D.LowerOrthantLE C) :
        C = D
        source
        theorem ProbabilityTheory.Copula.UpperOrthantLE.refl {d : ℕ} (C : Copula d) :
        C.UpperOrthantLE C
        source
        theorem ProbabilityTheory.Copula.UpperOrthantLE.trans {d : ℕ} {C D E : Copula d} (h : C.UpperOrthantLE D) (k : D.UpperOrthantLE E) :
        C.UpperOrthantLE E
        source
        theorem ProbabilityTheory.Copula.upperOrthantLE_iff_reflect {d : ℕ} (C D : Copula d) :
        C.UpperOrthantLE D ↔ (C.reflect Finset.univ).LowerOrthantLE (D.reflect Finset.univ)
        source
        theorem ProbabilityTheory.Copula.UpperOrthantLE.antisymm {d : ℕ} {C D : Copula d} (h : C.UpperOrthantLE D) (k : D.UpperOrthantLE C) :
        C = D
        source
        theorem ProbabilityTheory.Copula.ConcordanceLE.refl {d : ℕ} (C : Copula d) :
        C.ConcordanceLE C
        source
        theorem ProbabilityTheory.Copula.ConcordanceLE.trans {d : ℕ} {C D E : Copula d} (h : C.ConcordanceLE D) (k : D.ConcordanceLE E) :
        C.ConcordanceLE E
        source
        theorem ProbabilityTheory.Copula.ConcordanceLE.antisymm {d : ℕ} {C D : Copula d} (h : C.ConcordanceLE D) (k : D.ConcordanceLE C) :
        C = D
        source
        theorem ProbabilityTheory.Copula.concordanceLE_reflect_iff {d : ℕ} (C D : Copula d) :
        (C.reflect Finset.univ).ConcordanceLE (D.reflect Finset.univ) ↔ C.ConcordanceLE D
        source
        theorem ProbabilityTheory.Copula.upperOrthantLE_iff_lowerOrthantLE (C D : Copula 2) :
        C.UpperOrthantLE D ↔ C.LowerOrthantLE D

        In dimension two the two orthant comparisons coincide.

        source
        theorem ProbabilityTheory.Copula.concordanceLE_iff_lowerOrthantLE (C D : Copula 2) :
        C.ConcordanceLE D ↔ C.LowerOrthantLE D
        source
        theorem ProbabilityTheory.Copula.LowerOrthantLE.mix {d : ℕ} {C D E F : Copula d} (h : C.LowerOrthantLE D) (k : E.LowerOrthantLE F) (a : ↑unitInterval) :
        (C.mix E a).LowerOrthantLE (D.mix F a)
        source
        theorem ProbabilityTheory.Copula.LowerOrthantLE.mix_weight {d : ℕ} {C D : Copula d} (h : C.LowerOrthantLE D) {a b : ↑unitInterval} (hab : a ≤ b) :
        (D.mix C a).LowerOrthantLE (D.mix C b)

        Increasing the weight of the larger copula increases the mixture.