← Copula mathematical handbook

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.blest_tendsto_of_cdf (C : ℕ → Copula 2) (D : 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 ProbabilityTheory.Copula.RankRegion.XiBlest.attainable_region_closed : IsClosed attainableRegion

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

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.attainable_region_compact : IsCompact attainableRegion

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.blest_extrema_attained (x : ℝ) (hx : x ∈ Set.Icc 0 1) : ∃ (L : Copula 2) (U : Copula 2), L.chatterjeeXi = x ∧ U.chatterjeeXi = x ∧ ∀ (D : 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 ProbabilityTheory.Copula.RankRegion.XiBlest.minimal_xi_attained (y : ℝ) (hy : y ∈ Set.Icc (-1) 1) : ∃ (C : Copula 2), blestNu C = y ∧ ∀ (D : Copula 2), blestNu D = y → C.chatterjeeXi ≤ D.chatterjeeXi

The least xi is attained at every prescribed Blest coefficient.