← Mathematical handbook

Convexity of xi regions with an affine second coefficient

An ordinary mixture can fall below the desired xi coordinate. If every coefficient value has a witness with xi=1, a second mixture fills that gap while preserving the coefficient. No compactness or closure is assumed.

def Verification.xiCoefficientRegion (φ : ProbabilityTheory.Copula 2 → ℝ) : Set (ℝ × ℝ)

Equations

• Verification.xiCoefficientRegion φ = {p : ℝ × ℝ | ∃ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = p.1 ∧ φ C = p.2}

theorem Verification.xi_intermediate_at_coefficient (φ : ProbabilityTheory.Copula 2 → ℝ) (hφ : ∀ (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval), φ (C.mix D a) = ↑a * φ C + (1 - ↑a) * φ D) (C D : ProbabilityTheory.Copula 2) (he : φ C = φ D) (x : ℝ) (hC : C.chatterjeeXi ≤ x) (hD : x ≤ D.chatterjeeXi) : ∃ (E : ProbabilityTheory.Copula 2), E.chatterjeeXi = x ∧ φ E = φ C

Every intermediate xi value is attained at the same coefficient value.

theorem Verification.xi_upward_at_coefficient (φ : ProbabilityTheory.Copula 2 → ℝ) (hφ : ∀ (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval), φ (C.mix D a) = ↑a * φ C + (1 - ↑a) * φ D) (htop : ∀ (C : ProbabilityTheory.Copula 2), ∃ (D : ProbabilityTheory.Copula 2), D.chatterjeeXi = 1 ∧ φ D = φ C) (C : ProbabilityTheory.Copula 2) (x : ℝ) (hx : C.chatterjeeXi ≤ x) (hx1 : x ≤ 1) : ∃ (D : ProbabilityTheory.Copula 2), D.chatterjeeXi = x ∧ φ D = φ C

At any attained coefficient value, all xi values up to one are attained.

theorem Verification.convex_xiCoefficientRegion (φ : ProbabilityTheory.Copula 2 → ℝ) (hφ : ∀ (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval), φ (C.mix D a) = ↑a * φ C + (1 - ↑a) * φ D) (htop : ∀ (C : ProbabilityTheory.Copula 2), ∃ (D : ProbabilityTheory.Copula 2), D.chatterjeeXi = 1 ∧ φ D = φ C) : Convex ℝ (xiCoefficientRegion φ)

Convexity follows from actual copula witnesses, not from assuming xi is affine.