← Mathematical handbook

Corollary 4.1 and Remark 4.3: geometry of the attained region

def Papers.OrendayLaresRockel2026TauFootruleBeta.jointRegion : Set (ℝ × ℝ × ℝ)

Equations

• Papers.OrendayLaresRockel2026TauFootruleBeta.jointRegion = {z : ℝ × ℝ × ℝ | ∃ (C : ProbabilityTheory.Copula 2), C.kendallTau = z.1 ∧ C.spearmanFootrule = z.2.1 ∧ C.blomqvistBeta = z.2.2}

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.mem_jointRegion (t p b : ℝ) : (t, p, b) ∈ jointRegion ↔ b ∈ Set.Icc (-1) 1 ∧ 3 / 16 * (1 + b) ^ 2 - 1 / 2 ≤ p ∧ p ≤ 1 - 3 / 8 * (1 - b) ^ 2 ∧ 4 / 3 * p - 1 / 3 ≤ t ∧ t ≤ 2 / 3 * p + 1 / 3

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.jointRegion_closed : IsClosed jointRegion

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.jointRegion_compact : IsCompact jointRegion

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.jointRegion_convex : Convex ℝ jointRegion

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.fibre_reflection (t p b : ℝ) : (2 * p - t, p, b) ∈ jointRegion ↔ (t, p, b) ∈ jointRegion

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.fibre_midpoint_attained (p b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (hpL : 3 / 16 * (1 + b) ^ 2 - 1 / 2 ≤ p) (hpU : p ≤ 1 - 3 / 8 * (1 - b) ^ 2) : ∃ (C : ProbabilityTheory.Copula 2), C.kendallTau = p ∧ C.spearmanFootrule = p ∧ C.blomqvistBeta = b

noncomputable def Papers.OrendayLaresRockel2026TauFootruleBeta.betaSectionLower (p : ℝ) : ℝ

Equations

• Papers.OrendayLaresRockel2026TauFootruleBeta.betaSectionLower p = 1 - √(8 / 3 * (1 - p))

noncomputable def Papers.OrendayLaresRockel2026TauFootruleBeta.betaSectionUpper (p : ℝ) : ℝ

Equations

• Papers.OrendayLaresRockel2026TauFootruleBeta.betaSectionUpper p = min 1 (-1 + 4 / √3 * √(p + 1 / 2))

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.footrule_beta_section (p b : ℝ) (hp : p ∈ Set.Icc (-1 / 2) 1) : b ∈ Set.Icc (-1) 1 ∧ 3 / 16 * (1 + b) ^ 2 - 1 / 2 ≤ p ∧ p ≤ 1 - 3 / 8 * (1 - b) ^ 2 ↔ b ∈ Set.Icc (betaSectionLower p) (betaSectionUpper p)

theorem Papers.OrendayLaresRockel2026TauFootruleBeta.fixed_footrule_rectangle (p : ℝ) (hp : p ∈ Set.Icc (-1 / 2) 1) : {z : ℝ × ℝ | (z.1, p, z.2) ∈ jointRegion} = Set.Icc (4 / 3 * p - 1 / 3) (2 / 3 * p + 1 / 3) ×ˢ Set.Icc (betaSectionLower p) (betaSectionUpper p)