← Mathematical handbook

Attaining xi=1 at every beta

We use a two-block decreasing shuffle, W ⊕ W, as an alternative witness to the increasing shuffle in Proposition 6. No subclass properties of the source's particular witness are inferred from this construction.

noncomputable def Papers.OrendayLaresRockel2026XiBeta.twoBlockFlip (a u : ↑unitInterval) : ↑unitInterval

Equations

• One or more equations did not get rendered due to their size.

theorem Papers.OrendayLaresRockel2026XiBeta.measurable_twoBlockFlip (a : ↑unitInterval) : Measurable (twoBlockFlip a)

theorem Papers.OrendayLaresRockel2026XiBeta.xi_twoBlockFlip (a : ↑unitInterval) : (ProbabilityTheory.Copula.countermonotonic.ordinalSum ProbabilityTheory.Copula.countermonotonic a).chatterjeeXi = 1

noncomputable def Papers.OrendayLaresRockel2026XiBeta.rightSplit (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ↑unitInterval

Equations

• Papers.OrendayLaresRockel2026XiBeta.rightSplit b hb = ⟨(b + 1) / 4, ⋯⟩

noncomputable def Papers.OrendayLaresRockel2026XiBeta.rightBoundary (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ProbabilityTheory.Copula 2

Equations

• One or more equations did not get rendered due to their size.

theorem Papers.OrendayLaresRockel2026XiBeta.rightBoundary_beta (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (rightBoundary b hb).blomqvistBeta = b

theorem Papers.OrendayLaresRockel2026XiBeta.rightBoundary_xi (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (rightBoundary b hb).chatterjeeXi = 1

theorem Papers.OrendayLaresRockel2026XiBeta.right_boundary_attained (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∃ (C : ProbabilityTheory.Copula 2), C.blomqvistBeta = b ∧ C.chatterjeeXi = 1