← Mathematical handbook

theorem Verification.isClosed_xiCoefficientRegion (r : ProbabilityTheory.Copula 2 → ℝ) (hcont : ∀ (C : ℕ → ProbabilityTheory.Copula 2) (D : ProbabilityTheory.Copula 2), (∀ (u v : ↑unitInterval), Filter.Tendsto (fun (n : ℕ) => (C n).cdf ![u, v]) Filter.atTop (nhds (D.cdf ![u, v]))) → Filter.Tendsto (fun (n : ℕ) => r (C n)) Filter.atTop (nhds (r D))) (hup : ∀ (C : ProbabilityTheory.Copula 2) (x : ℝ), C.chatterjeeXi ≤ x → x ≤ 1 → ∃ (D : ProbabilityTheory.Copula 2), D.chatterjeeXi = x ∧ r D = r C) : IsClosed (xiCoefficientRegion r)

Lower semicontinuity of xi plus filling toward xi=1 makes the actual region closed.

theorem Verification.isCompact_xiCoefficientRegion (r : ProbabilityTheory.Copula 2 → ℝ) (hc : IsClosed (xiCoefficientRegion r)) (a b : ℝ) (hr : ∀ (C : ProbabilityTheory.Copula 2), r C ∈ Set.Icc a b) : IsCompact (xiCoefficientRegion r)

A closed xi region with a bounded second coefficient is compact.

theorem Verification.xi_slice_extrema (r : ProbabilityTheory.Copula 2 → ℝ) (hc : IsCompact (xiCoefficientRegion r)) (C : ProbabilityTheory.Copula 2) : ∃ (L : ProbabilityTheory.Copula 2) (U : ProbabilityTheory.Copula 2), L.chatterjeeXi = C.chatterjeeXi ∧ U.chatterjeeXi = C.chatterjeeXi ∧ ∀ (D : ProbabilityTheory.Copula 2), D.chatterjeeXi = C.chatterjeeXi → r L ≤ r D ∧ r D ≤ r U

Every nonempty vertical slice attains both coefficient extrema.

theorem Verification.coefficient_slice_minimum (r : ProbabilityTheory.Copula 2 → ℝ) (hc : IsCompact (xiCoefficientRegion r)) (C : ProbabilityTheory.Copula 2) : ∃ (L : ProbabilityTheory.Copula 2), r L = r C ∧ ∀ (D : ProbabilityTheory.Copula 2), r D = r C → L.chatterjeeXi ≤ D.chatterjeeXi

Every nonempty horizontal slice attains its least xi.