← Mathematical handbook

The attaining left boundary in Proposition 3(i)

noncomputable def Papers.OrendayLaresRockel2026XiBeta.tentDisplacement (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : Verification.StripDisplacement

The signed median tent from equations (4)-(6). The sign at zero is immaterial.

Equations

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

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

Equations

• Papers.OrendayLaresRockel2026XiBeta.leftBoundary b hb = Verification.twoStrip (Papers.OrendayLaresRockel2026XiBeta.tentDisplacement b hb)

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_cdf (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (u v : ↑unitInterval) : (leftBoundary b hb).cdf ![u, v] = ↑u * ↑v + min (↑u) (1 - ↑u) * if 0 ≤ b then Verification.medianTent b ↑v else -Verification.medianTent (-b) ↑v

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

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_xi (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).chatterjeeXi = |b| ^ 3 / 2

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

The cubic lower boundary is attained for every allowed beta.

theorem Papers.OrendayLaresRockel2026XiBeta.xi_eq_lower_iff (C : ProbabilityTheory.Copula 2) (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (hbeta : C.blomqvistBeta = b) : C.chatterjeeXi = |b| ^ 3 / 2 ↔ C = leftBoundary b hb

Proposition 5, equality case. Strict convexity rules out a second minimizer.