Documentation

Papers.OrendayLaresRockel2026XiBeta.Subclasses

← Mathematical handbook

Symmetric and quadrant-dependent attainable regions #

The right endpoint uses a centered countermonotonic block with identity outside. This alternative witness has every existential property required by Proposition 6, including exchangeability and radial symmetry.

source
noncomputable def Papers.OrendayLaresRockel2026XiBeta.symmetricRightBoundary (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :
ProbabilityTheory.Copula 2
Equations
Instances For
    source
    theorem Papers.OrendayLaresRockel2026XiBeta.symmetricRightBoundary_xi (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :
    (symmetricRightBoundary b hb).chatterjeeXi = 1
    source
    theorem Papers.OrendayLaresRockel2026XiBeta.symmetricRightBoundary_beta (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :
    (symmetricRightBoundary b hb).blomqvistBeta = b
    source
    theorem Papers.OrendayLaresRockel2026XiBeta.symmetricRightBoundary_radiallySymmetric (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :
    (symmetricRightBoundary b hb).IsRadiallySymmetric
    source
    theorem Papers.OrendayLaresRockel2026XiBeta.symmetricRightBoundary_exchangeable (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :
    (symmetricRightBoundary b hb).IsExchangeable
    source
    theorem Papers.OrendayLaresRockel2026XiBeta.symmetricRightBoundary_pqd (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (hpos : 0 ≤ b) :
    (symmetricRightBoundary b hb).IsPQD
    source
    theorem Papers.OrendayLaresRockel2026XiBeta.symmetric_right_boundary_attained (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) :
    ∃ (C : ProbabilityTheory.Copula 2), C.chatterjeeXi = 1 ∧ C.blomqvistBeta = b ∧ C.IsRadiallySymmetric ∧ C.IsExchangeable ∧ (0 ≤ b → C.IsPQD)

    All the existential conclusions of Proposition 6, with an alternative shuffle.

    source
    theorem Papers.OrendayLaresRockel2026XiBeta.fixed_beta_intermediate_in_class (P : ProbabilityTheory.Copula 2 → Prop) (hMix : ∀ (C D : ProbabilityTheory.Copula 2), P C → P D → ∀ (a : ↑unitInterval), P (C.mix D a)) (C D : ProbabilityTheory.Copula 2) (hPC : P C) (hPD : P D) {b x : ℝ} (hC : C.blomqvistBeta = b) (hD : D.blomqvistBeta = b) (hxC : C.chatterjeeXi ≤ x) (hxD : x ≤ D.chatterjeeXi) :
    ∃ (E : ProbabilityTheory.Copula 2), P E ∧ E.chatterjeeXi = x ∧ E.blomqvistBeta = b

    The intermediate-value construction stays in any class closed under mixtures.

    source
    theorem Papers.OrendayLaresRockel2026XiBeta.exact_radiallySymmetric_xi_beta_region (x b : ℝ) :
    (∃ (C : ProbabilityTheory.Copula 2), C.IsRadiallySymmetric ∧ C.chatterjeeXi = x ∧ C.blomqvistBeta = b) ↔ x ∈ Set.Icc 0 1 ∧ b ∈ Set.Icc (-1) 1 ∧ |b| ^ 3 ≤ 2 * x

    Corollary 7, including all boundary cases.

    source
    theorem Papers.OrendayLaresRockel2026XiBeta.exact_pqd_radiallySymmetric_xi_beta_region (x b : ℝ) :
    (∃ (C : ProbabilityTheory.Copula 2), (C.IsPQD ∧ C.IsRadiallySymmetric) ∧ C.chatterjeeXi = x ∧ C.blomqvistBeta = b) ↔ x ∈ Set.Icc 0 1 ∧ b ∈ Set.Icc 0 1 ∧ b ^ 3 ≤ 2 * x

    Corollary 8: the same region is attained even with radial symmetry imposed.

    source
    theorem Papers.OrendayLaresRockel2026XiBeta.exact_pqd_xi_beta_region (x b : ℝ) :
    (∃ (C : ProbabilityTheory.Copula 2), C.IsPQD ∧ C.chatterjeeXi = x ∧ C.blomqvistBeta = b) ↔ x ∈ Set.Icc 0 1 ∧ b ∈ Set.Icc 0 1 ∧ b ^ 3 ≤ 2 * x
    source
    theorem Papers.OrendayLaresRockel2026XiBeta.pqd_reflect_second_isNQD (C : ProbabilityTheory.Copula 2) (hC : C.IsPQD) :
    (C.reflect {1}).IsNQD
    source
    theorem Papers.OrendayLaresRockel2026XiBeta.exact_nqd_xi_beta_region (x b : ℝ) :
    (∃ (C : ProbabilityTheory.Copula 2), C.IsNQD ∧ C.chatterjeeXi = x ∧ C.blomqvistBeta = b) ↔ x ∈ Set.Icc 0 1 ∧ b ∈ Set.Icc (-1) 0 ∧ |b| ^ 3 ≤ 2 * x

    Remark 9, obtained by reflecting the positive quadrant-dependent region.

    source
    noncomputable def Papers.OrendayLaresRockel2026XiBeta.stochasticUpper (b : ↑unitInterval) :
    ProbabilityTheory.Copula 2

    The comparison family in Remark 10.

    Equations
    Instances For
      source
      theorem Papers.OrendayLaresRockel2026XiBeta.stochasticUpper_isSI (b : ↑unitInterval) :
      (stochasticUpper b).IsSI
      source
      theorem Papers.OrendayLaresRockel2026XiBeta.stochasticUpper_beta (b : ↑unitInterval) :
      (stochasticUpper b).blomqvistBeta = ↑b
      source
      theorem Papers.OrendayLaresRockel2026XiBeta.stochasticUpper_xi (b : ↑unitInterval) :
      (stochasticUpper b).chatterjeeXi = ↑b ^ 2
      source
      theorem Papers.OrendayLaresRockel2026XiBeta.si_inner_region_attained (x b : ℝ) (hb : b ∈ Set.Icc 0 1) (hx : b ^ 3 / 2 ≤ x ∧ x ≤ b ^ 2) :
      ∃ (C : ProbabilityTheory.Copula 2), C.IsSI ∧ C.chatterjeeXi = x ∧ C.blomqvistBeta = b

      The whole inner strip from Remark 10 is attained by SI copulas.

      source
      theorem Papers.OrendayLaresRockel2026XiBeta.sd_inner_region_attained (x b : ℝ) (hb : b ∈ Set.Icc (-1) 0) (hx : |b| ^ 3 / 2 ≤ x ∧ x ≤ b ^ 2) :
      ∃ (C : ProbabilityTheory.Copula 2), C.IsSD ∧ C.chatterjeeXi = x ∧ C.blomqvistBeta = b

      Reflection gives the corresponding attained strip for SD copulas.

      source
      theorem Papers.OrendayLaresRockel2026XiBeta.si_region_outer_bound (C : ProbabilityTheory.Copula 2) (hC : C.IsSI) :
      C.chatterjeeXi ∈ Set.Icc 0 1 ∧ C.blomqvistBeta ∈ Set.Icc 0 1 ∧ C.blomqvistBeta ^ 3 ≤ 2 * C.chatterjeeXi
      source
      theorem Papers.OrendayLaresRockel2026XiBeta.sd_region_outer_bound (C : ProbabilityTheory.Copula 2) (hC : C.IsSD) :
      C.chatterjeeXi ∈ Set.Icc 0 1 ∧ C.blomqvistBeta ∈ Set.Icc (-1) 0 ∧ |C.blomqvistBeta| ^ 3 ≤ 2 * C.chatterjeeXi