← Mathematical handbook

Compactness and attained maxima of the full directional region

theorem Papers.AnsariRockel2026RhoFootrule.directional_region_compact : IsCompact directionalRegion

Example 2.9: compactness concerns the full attainable region.

noncomputable def Papers.AnsariRockel2026RhoFootrule.upperRatio (x : ℝ) : ℝ

Equations

• Papers.AnsariRockel2026RhoFootrule.upperRatio x = sSup {y : ℝ | (x, y) ∈ Papers.AnsariRockel2026RhoFootrule.directionalRegion}

theorem Papers.AnsariRockel2026RhoFootrule.upperRatio_isGreatest (x : ℝ) (hx : x ∈ Set.Icc 0 1) : IsGreatest {y : ℝ | (x, y) ∈ directionalRegion} (upperRatio x)

Every vertical slice of the full region has an attained upper endpoint.

theorem Papers.AnsariRockel2026RhoFootrule.upper_ratio_attained (x : ℝ) (hx : x ∈ Set.Icc 0 1) : ∃ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = x ∧ copulaCorrelationRatio C = upperRatio x

A genuine copula attains the upper boundary for every xi.

theorem Papers.AnsariRockel2026RhoFootrule.quarter_xi_maximum : ∃ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = 1 / 4 ∧ copulaCorrelationRatio C ≤ 256 / 525 ∧ ∀ (D : ProbabilityTheory.Copula 2), D.chatterjeeXi = 1 / 4 → copulaCorrelationRatio D ≤ copulaCorrelationRatio C

Example 2.9: the attained quarter-xi maximum is uniformly below one half.