Documentation

Copula.Rank.Region.XiBeta.RightBoundary

← Copula mathematical handbook

Attaining xi=1 at every beta #

We use a two-block decreasing shuffle, W ⊕ W, as an alternative witness to the increasing shuffle in Proposition 6. No subclass properties of the source's particular witness are inferred from this construction.

source
noncomputable def ProbabilityTheory.Copula.RankRegion.XiBeta.twoBlockFlip (a u : ↑unitInterval) :
↑unitInterval
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ProbabilityTheory.Copula.RankRegion.XiBeta.measurable_twoBlockFlip (a : ↑unitInterval) :
    Measurable (twoBlockFlip a)
    source
    theorem ProbabilityTheory.Copula.RankRegion.XiBeta.xi_twoBlockFlip (a : ↑unitInterval) :
    (countermonotonic.ordinalSum countermonotonic a).chatterjeeXi = 1
    source
    noncomputable def ProbabilityTheory.Copula.RankRegion.XiBeta.rightSplit (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :
    ↑unitInterval
    Equations
    Instances For
      source
      noncomputable def ProbabilityTheory.Copula.RankRegion.XiBeta.rightBoundary (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :
      Copula 2
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem ProbabilityTheory.Copula.RankRegion.XiBeta.rightBoundary_beta (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :
        (rightBoundary b hb).blomqvistBeta = b
        source
        theorem ProbabilityTheory.Copula.RankRegion.XiBeta.rightBoundary_xi (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :
        (rightBoundary b hb).chatterjeeXi = 1
        source
        theorem ProbabilityTheory.Copula.RankRegion.XiBeta.right_boundary_attained (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :
        ∃ (C : Copula 2), C.blomqvistBeta = b ∧ C.chatterjeeXi = 1