Documentation

Papers.OrendayLaresRockel2026XiBeta.SIRegion

← Mathematical handbook

Theorem 1.2: the exact ξ–β region of stochastically increasing copulas #

R^{SI}_{ξ,β} = R^{SI,RS}_{ξ,β} = {(x,y) ∈ [0,1]² : y³ ≤ 2x, 3(1-y)² ≤ 4(1-x)}, and R^{SD} = R^{SD,RS} is its mirror image. Every SI copula satisfies ξ(C) ≤ 1 - (3/4)(1-β(C))², with equality iff C = R_{β(C)}.

source
def Papers.OrendayLaresRockel2026XiBeta.siRegion :
Set (ℝ × ℝ)

The region of Theorem 1.2: {(x,y) ∈ [0,1]² : y³ ≤ 2x, 3(1-y)² ≤ 4(1-x)}.

Equations
Instances For
    source
    theorem Papers.OrendayLaresRockel2026XiBeta.xiBetaRegion_classSI_subset :
    xiBetaRegion classSI ⊆ siRegion
    source
    theorem Papers.OrendayLaresRockel2026XiBeta.siRegion_subset_xiBetaRegion_classSI_rs :
    siRegion ⊆ xiBetaRegion (classSI ∩ classRS)

    L_b ∈ C_SI ∩ C_RS and R_b ∈ C_SI ∩ C_RS, so both attain the two boundary curves.

    source
    theorem Papers.OrendayLaresRockel2026XiBeta.theorem_1_2_region :
    xiBetaRegion classSI = siRegion ∧ xiBetaRegion (classSI ∩ classRS) = siRegion

    Theorem 1.2: R^{SI}_{ξ,β} = R^{SI,RS}_{ξ,β} = {(x,y) ∈ [0,1]² : y³ ≤ 2x, 3(1-y)² ≤ 4(1-x)}.

    source
    theorem Papers.OrendayLaresRockel2026XiBeta.theorem_1_2_sd :
    xiBetaRegion classSD = xiBetaRegion (classSD ∩ classRS) ∧ xiBetaRegion classSD = (fun (p : ℝ × ℝ) => (p.1, -p.2)) '' siRegion ∧ xiBetaRegion (classSD ∩ classRS) = (fun (p : ℝ × ℝ) => (p.1, -p.2)) '' siRegion

    Theorem 1.2: R^{SD} = R^{SD,RS} is the mirror image {(x, -y) : (x,y) ∈ R^{SI}}.

    source
    theorem Papers.OrendayLaresRockel2026XiBeta.theorem_1_2_inequality (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) :
    C.chatterjeeXi ≤ 1 - 3 / 4 * (1 - C.blomqvistBeta) ^ 2 ∧ (C.chatterjeeXi = 1 - 3 / 4 * (1 - C.blomqvistBeta) ^ 2 ↔ C = Rb C.blomqvistBeta ⋯)

    Theorem 1.2, inequality (1.5): every SI copula satisfies ξ(C) ≤ 1 - (3/4)(1 - β(C))², with equality if and only if C = R_{β(C)}.

    source
    theorem Papers.OrendayLaresRockel2026XiBeta.theorem_1_2_inequality_alt (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) :
    3 * (1 - C.blomqvistBeta) ^ 2 ≤ 4 * (1 - C.chatterjeeXi)

    Inequality (1.5) in the equivalent form 3(1 - β)² ≤ 4(1 - ξ).

    source
    theorem Papers.OrendayLaresRockel2026XiBeta.theorem_1_2_beta_lower (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) :
    1 - 2 * √((1 - C.chatterjeeXi) / 3) ≤ C.blomqvistBeta

    Inequality (1.5) as a lower bound on β: β(C) ≥ 1 - 2√((1 - ξ(C))/3).