← Mathematical handbook

Convexity of the directional xi--eta attainable region

def Papers.AnsariRockel2026RhoFootrule.directionalRegion : Set (ℝ × ℝ)

Actual copula coefficient pairs, with the predictor in the first coordinate.

Equations

• One or more equations did not get rendered due to their size.

theorem Papers.AnsariRockel2026RhoFootrule.tagged_coefficients (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (ha0 : 0 < a) (ha1 : a < 1) : (Verification.conditionalJoin C D a ha0 ha1).chatterjeeXi = ↑a * C.chatterjeeXi + (1 - ↑a) * D.chatterjeeXi ∧ copulaCorrelationRatio (Verification.conditionalJoin C D a ha0 ha1) = ↑a * copulaCorrelationRatio C + (1 - ↑a) * copulaCorrelationRatio D

Equations (117)--(118): the tagged construction realizes both affine coordinates.

theorem Papers.AnsariRockel2026RhoFootrule.directional_region_convex : Convex ℝ directionalRegion

Proposition 2.10: every convex combination of attained pairs is attained.

theorem Papers.AnsariRockel2026RhoFootrule.convex_hull_attained (S : Set (ℝ × ℝ)) (hS : S ⊆ directionalRegion) : (convexHull ℝ) S ⊆ directionalRegion

Convexification of any collection of actual witnesses preserves attainability.

theorem Papers.AnsariRockel2026RhoFootrule.directional_vertical_interval (x l u y : ℝ) (hl : (x, l) ∈ directionalRegion) (hu : (x, u) ∈ directionalRegion) (hy : y ∈ Set.Icc l u) : (x, y) ∈ directionalRegion

An attained lower and upper ordinate fill the entire vertical interval.