Documentation

Copula.Rank.Region.Basic

← Copula mathematical handbook

A uniform API for the ten pairwise rank regions #

An attainable region is the image of actual copulas. Defining one is distinct from proving a formula for its boundary; see the coverage table in docs/rank-regions.md for the exact-region theorems currently available.

source
inductive ProbabilityTheory.Copula.RankRegion.Coefficient :
Type

The five coefficients considered in the classical pairwise region problem.

Instances For
    source
    @[instance_reducible]
    instance ProbabilityTheory.Copula.RankRegion.instDecidableEqCoefficient :
    DecidableEq Coefficient
    Equations
    source
    @[instance_reducible]
    instance ProbabilityTheory.Copula.RankRegion.instReprCoefficient :
    Repr Coefficient
    Equations
    source
    def ProbabilityTheory.Copula.RankRegion.instReprCoefficient.repr :
    Coefficient → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def ProbabilityTheory.Copula.RankRegion.Coefficient.eval :
      Coefficient → Copula 2 → ℝ

      Evaluate a coefficient using the package's population normalization.

      Equations
      Instances For
        source
        def ProbabilityTheory.Copula.RankRegion.attainable (a b : Coefficient) :
        Set (ℝ × ℝ)

        All jointly attainable values, in the stated coordinate order.

        Equations
        Instances For
          source
          theorem ProbabilityTheory.Copula.RankRegion.mem_attainable_iff (a b : Coefficient) (x y : ℝ) :
          (x, y) ∈ attainable a b ↔ ∃ (C : Copula 2), a.eval C = x ∧ b.eval C = y
          source
          theorem ProbabilityTheory.Copula.RankRegion.mem_attainable_swap (a b : Coefficient) (x y : ℝ) :
          (x, y) ∈ attainable a b ↔ (y, x) ∈ attainable b a
          source
          theorem ProbabilityTheory.Copula.RankRegion.Coefficient.eval_mix (k : Coefficient) (hk : k ≠ tau) (C D : Copula 2) (a : ↑unitInterval) :
          k.eval (C.mix D a) = ↑a * k.eval C + (1 - ↑a) * k.eval D
          source
          theorem ProbabilityTheory.Copula.RankRegion.Coefficient.continuous_eval_mix (k : Coefficient) (C D : Copula 2) :
          Continuous fun (a : ↑unitInterval) => k.eval (C.mix D a)
          source
          theorem ProbabilityTheory.Copula.RankRegion.attainable_convex (a b : Coefficient) (ha : a ≠ Coefficient.tau) (hb : b ≠ Coefficient.tau) :
          Convex ℝ (attainable a b)

          The six pairs among the four affine coefficients have convex attainable regions.

          source
          theorem ProbabilityTheory.Copula.RankRegion.fixed_coefficient_intermediate (a b : Coefficient) (ha : a ≠ Coefficient.tau) (C D : Copula 2) {x y : ℝ} (hC : a.eval C = x) (hD : a.eval D = x) (hyC : b.eval C ≤ y) (hyD : y ≤ b.eval D) :
          (x, y) ∈ attainable a b

          At fixed affine coefficient, the other coefficient attains intermediate values. This also applies to Kendall's tau, whose dependence on mixture weights is quadratic.

          source
          theorem ProbabilityTheory.Copula.RankRegion.Coefficient.eval_reflect (k : Coefficient) (hk : k ≠ footrule) (C : Copula 2) :
          k.eval (C.reflect {1}) = -k.eval C
          source
          theorem ProbabilityTheory.Copula.RankRegion.mem_attainable_neg (a b : Coefficient) (ha : a ≠ Coefficient.footrule) (hb : b ≠ Coefficient.footrule) (x y : ℝ) :
          (x, y) ∈ attainable a b ↔ (-x, -y) ∈ attainable a b