← Mathematical handbook

theorem Papers.Rockel2026XiBlest.blest_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 : ℕ) => blestNu (C n)) Filter.atTop (nhds (blestNu D))

theorem Papers.Rockel2026XiBlest.attainable_region_closed : IsClosed attainableRegion

Theorem 1.1: the entire attained xi-Blest region is closed.

theorem Papers.Rockel2026XiBlest.attainable_region_compact : IsCompact attainableRegion

theorem Papers.Rockel2026XiBlest.blest_extrema_attained (x : ℝ) (hx : x ∈ Set.Icc 0 1) : ∃ (L : ProbabilityTheory.Copula 2) (U : ProbabilityTheory.Copula 2), L.chatterjeeXi = x ∧ U.chatterjeeXi = x ∧ ∀ (D : ProbabilityTheory.Copula 2), D.chatterjeeXi = x → blestNu L ≤ blestNu D ∧ blestNu D ≤ blestNu U

Both extremal Blest values exist at every prescribed xi. Their formulas are a separate result.

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

The least xi is attained at every prescribed Blest coefficient.