Documentation

Copula.Rank.Region.TauFootrule

← Copula mathematical handbook

The exact Kendall tau–Spearman footrule region #

Kokol Bukovšek–Stopar, On the exact regions determined by Kendall's tau and other concordance measures (2023), Theorem 4. The lower-bound argument is applied directly to a copula measure.

source
theorem ProbabilityTheory.Copula.kendallTau_le_footrule (C : Copula 2) :
C.kendallTau ≤ 2 / 3 * C.spearmanFootrule + 1 / 3
source
theorem ProbabilityTheory.Copula.footrule_le_kendallTau (C : Copula 2) :
4 / 3 * C.spearmanFootrule - 1 / 3 ≤ C.kendallTau
source
noncomputable def ProbabilityTheory.Copula.RankRegion.TauFootrule.lowerCopula (a : ↑unitInterval) :
Copula 2

Lower boundary family (Example 2 of the source).

Equations
Instances For
    source
    noncomputable def ProbabilityTheory.Copula.RankRegion.TauFootrule.upperCopula (a : ↑unitInterval) :
    Copula 2

    A rescaled half-turn supplies the upper boundary.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem ProbabilityTheory.Copula.RankRegion.TauFootrule.lowerCopula_coefficients (a : ↑unitInterval) :
      (lowerCopula a).spearmanFootrule = 1 - 3 / 2 * (1 - ↑a) ^ 2 ∧ (lowerCopula a).kendallTau = 1 - 2 * (1 - ↑a) ^ 2
      source
      theorem ProbabilityTheory.Copula.RankRegion.TauFootrule.upperCopula_coefficients (a : ↑unitInterval) :
      (upperCopula a).spearmanFootrule = 1 - 3 / 2 * (1 - ↑a) ^ 2 ∧ (upperCopula a).kendallTau = 1 - (1 - ↑a) ^ 2
      source
      theorem ProbabilityTheory.Copula.RankRegion.TauFootrule.exists_copula {p t : ℝ} (hp : p ∈ Set.Icc (-1 / 2) 1) (hl : 4 / 3 * p - 1 / 3 ≤ t) (hu : t ≤ 2 / 3 * p + 1 / 3) :
      ∃ (C : Copula 2), C.spearmanFootrule = p ∧ C.kendallTau = t

      Every value between the two sharp bounds is attained.

      source
      theorem ProbabilityTheory.Copula.RankRegion.TauFootrule.exists_copula_iff (p t : ℝ) :
      (∃ (C : Copula 2), C.spearmanFootrule = p ∧ C.kendallTau = t) ↔ p ∈ Set.Icc (-1 / 2) 1 ∧ 4 / 3 * p - 1 / 3 ≤ t ∧ t ≤ 2 / 3 * p + 1 / 3

      Exact membership, including the three vertices and every boundary point.