Documentation

Copula.Rank.Region.TauFootruleBeta.Paper.FootruleBetaLower

← Copula mathematical handbook

The lower footrule-beta boundary and the complete pairwise region #

The lower seed of Proposition 3.2 is constructed by reflection of a centered ordinal sum. No shuffle formula or assumed coefficient values are required.

source
theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.diagonal_beta_lower (C : Copula 2) (t : ↑unitInterval) :
countermonotonic.cdf ![t, t] + 2 * Common.medianTent ((C.blomqvistBeta + 1) / 4) ↑t ≤ C.cdf ![t, t]
source
theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.beta_lower_le_footrule (C : Copula 2) :
3 / 16 * (1 + C.blomqvistBeta) ^ 2 - 1 / 2 ≤ C.spearmanFootrule
source
noncomputable def ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.medianWBlocks :
Copula 2
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.lowerSeed (α : ↑unitInterval) :
    Copula 2
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.lowerSeed_coefficients (α : ↑unitInterval) :
      (lowerSeed α).kendallTau = ↑α ^ 2 - 1 ∧ (lowerSeed α).spearmanFootrule = 3 / 4 * ↑α ^ 2 - 1 / 2 ∧ (lowerSeed α).blomqvistBeta = 2 * ↑α - 1
      source
      noncomputable def ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.footruleBetaLower (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :
      Copula 2
      Equations
      Instances For
        source
        theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.footruleBetaLower_coefficients (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :
        (footruleBetaLower b hb).kendallTau = (1 + b) ^ 2 / 4 - 1 ∧ (footruleBetaLower b hb).spearmanFootrule = 3 / 16 * (1 + b) ^ 2 - 1 / 2 ∧ (footruleBetaLower b hb).blomqvistBeta = b
        source
        theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.minimal_footrule_at_beta (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :
        ∃ (D : Copula 2), D.blomqvistBeta = b ∧ D.spearmanFootrule = 3 / 16 * (1 + b) ^ 2 - 1 / 2 ∧ ∀ (C : Copula 2), C.blomqvistBeta = b → D.spearmanFootrule ≤ C.spearmanFootrule
        source
        theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.exact_footrule_beta_region (p b : ℝ) :
        (∃ (C : Copula 2), C.spearmanFootrule = p ∧ C.blomqvistBeta = b) ↔ b ∈ Set.Icc (-1) 1 ∧ 3 / 16 * (1 + b) ^ 2 - 1 / 2 ≤ p ∧ p ≤ 1 - 3 / 8 * (1 - b) ^ 2