← Mathematical handbook

theorem Papers.Rockel2026XiFootrule.footrule_tendsto_of_cdf (C : ℕ → ProbabilityTheory.Copula 2) (D : ProbabilityTheory.Copula 2) (hC : ∀ (u v : ↑unitInterval), Filter.Tendsto (fun (n : ℕ) => (C n).cdf ![u, v]) Filter.atTop (nhds (D.cdf ![u, v]))) : Filter.Tendsto (fun (n : ℕ) => (C n).spearmanFootrule) Filter.atTop (nhds D.spearmanFootrule)

theorem Papers.Rockel2026XiFootrule.attainable_region_closed : IsClosed attainableRegion

Theorem 3.3: closedness of the full attained region, including its negative part.

theorem Papers.Rockel2026XiFootrule.attainable_region_compact : IsCompact attainableRegion

Compactness concerns actual coefficient pairs, not the relaxed lower-bound profile.

theorem Papers.Rockel2026XiFootrule.minimal_footrule_attained (x : ℝ) (hx : x ∈ Set.Icc 0 1) : ∃ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = x ∧ ∀ (D : ProbabilityTheory.Copula 2), D.chatterjeeXi = x → C.spearmanFootrule ≤ D.spearmanFootrule

The lower footrule boundary is attained at every prescribed xi.

theorem Papers.Rockel2026XiFootrule.minimal_xi_attained (y : ℝ) (hy : y ∈ Set.Icc (-1 / 2) 1) : ∃ (C : ProbabilityTheory.Copula 2), C.spearmanFootrule = y ∧ ∀ (D : ProbabilityTheory.Copula 2), D.spearmanFootrule = y → C.chatterjeeXi ≤ D.chatterjeeXi

Every horizontal slice, including negative footrule, attains its least xi.