Documentation

Copula.Rank.Region.Beta

← Copula mathematical handbook

The four exact regions involving Blomqvist beta #

The fixed-median bounds recalled by Kokol Bukovšek et al. are attained by centered half-turn shuffles and their reflections. Mixture paths preserve beta and fill every fibre, including when the other coefficient is tau.

source
noncomputable def ProbabilityTheory.Copula.RankRegion.Beta.upperCopula (r : ↑unitInterval) :
Copula 2

A centered half-turn is simultaneously extremal for all four other coefficients.

Equations
Instances For
    source
    theorem ProbabilityTheory.Copula.RankRegion.Beta.upperCopula_coefficients (r : ↑unitInterval) :
    (upperCopula r).blomqvistBeta = 1 - 2 * ↑r ∧ (upperCopula r).spearmanRho = 1 - 3 / 2 * ↑r ^ 3 ∧ (upperCopula r).kendallTau = 1 - ↑r ^ 2 ∧ (upperCopula r).spearmanFootrule = 1 - 3 / 2 * ↑r ^ 2 ∧ (upperCopula r).giniGamma = 1 - 3 / 2 * ↑r ^ 2
    source
    theorem ProbabilityTheory.Copula.RankRegion.Beta.exists_upper {b : ℝ} (hb : b ∈ Set.Icc (-1) 1) :
    ∃ (C : Copula 2), C.blomqvistBeta = b ∧ C.spearmanRho = 1 - 3 / 16 * (1 - b) ^ 3 ∧ C.kendallTau = 1 - 1 / 4 * (1 - b) ^ 2 ∧ C.spearmanFootrule = 1 - 3 / 8 * (1 - b) ^ 2 ∧ C.giniGamma = 1 - 3 / 8 * (1 - b) ^ 2

    All four upper boundaries have a common witness at every prescribed beta.

    source
    theorem ProbabilityTheory.Copula.RankRegion.Beta.exists_lower {b : ℝ} (hb : b ∈ Set.Icc (-1) 1) :
    ∃ (C : Copula 2), C.blomqvistBeta = b ∧ C.spearmanRho = 3 / 16 * (1 + b) ^ 3 - 1 ∧ C.kendallTau = 1 / 4 * (1 + b) ^ 2 - 1 ∧ C.spearmanFootrule = 3 / 16 * (1 + b) ^ 2 - 1 / 2 ∧ C.giniGamma = 3 / 8 * (1 + b) ^ 2 - 1

    Reflections supply all four lower boundaries, including the footrule normalization.

    source
    theorem ProbabilityTheory.Copula.RankRegion.Beta.rho_iff (b r : ℝ) :
    (∃ (C : Copula 2), C.blomqvistBeta = b ∧ C.spearmanRho = r) ↔ b ∈ Set.Icc (-1) 1 ∧ 3 / 16 * (1 + b) ^ 3 - 1 ≤ r ∧ r ≤ 1 - 3 / 16 * (1 - b) ^ 3
    source
    theorem ProbabilityTheory.Copula.RankRegion.Beta.tau_iff (b t : ℝ) :
    (∃ (C : Copula 2), C.blomqvistBeta = b ∧ C.kendallTau = t) ↔ b ∈ Set.Icc (-1) 1 ∧ 1 / 4 * (1 + b) ^ 2 - 1 ≤ t ∧ t ≤ 1 - 1 / 4 * (1 - b) ^ 2
    source
    theorem ProbabilityTheory.Copula.RankRegion.Beta.footrule_iff (b p : ℝ) :
    (∃ (C : Copula 2), C.blomqvistBeta = b ∧ C.spearmanFootrule = p) ↔ b ∈ Set.Icc (-1) 1 ∧ 3 / 16 * (1 + b) ^ 2 - 1 / 2 ≤ p ∧ p ≤ 1 - 3 / 8 * (1 - b) ^ 2
    source
    theorem ProbabilityTheory.Copula.RankRegion.Beta.gamma_iff (b g : ℝ) :
    (∃ (C : Copula 2), C.blomqvistBeta = b ∧ C.giniGamma = g) ↔ b ∈ Set.Icc (-1) 1 ∧ 3 / 8 * (1 + b) ^ 2 - 1 ≤ g ∧ g ≤ 1 - 3 / 8 * (1 - b) ^ 2