← Mathematical handbook

Proposition 5.3 (two-branch copulas R_b), assembled

• the law: R_b is the copula of (U, V_b) (Rb_eq_ofMap, Rb_toMeasure_eq_lawVb);
• (i) singular, SI, radially symmetric; for b < 1 neither R_b exchangeable nor R_bᵀ SI; R_1 = M;
• (ii) ordinal sum of M, R_0, M for 0 < b < 1;
• (iii) β(R_b) = b, ξ(R_b) = 1 - (3/4)(1-b)²;
• (iv) τ(R_b) = 1 - (1/2)(1-b)², ρ(R_b) = 1 - (1/2)(1-b)³.

theorem Papers.OrendayLaresRockel2026XiBeta.proposition_5_3_i (b : ℝ) (hb : b ∈ Set.Icc 0 1) : (Rb b hb).toMeasure.MutuallySingular MeasureTheory.volume ∧ (Rb b hb).IsSI ∧ (Rb b hb).IsRadiallySymmetric ∧ (b < 1 → ¬(Rb b hb).IsExchangeable ∧ ¬(Rb b hb).transpose.IsSI) ∧ (b = 1 → Rb b hb = ProbabilityTheory.Copula.comonotonic 2)

Proposition 5.3 (i): singular, SI and radially symmetric, for all b ∈ [0,1]; not exchangeable and with non-SI transpose for b < 1; and R_1 = M.

theorem Papers.OrendayLaresRockel2026XiBeta.proposition_5_3_ii (b : ℝ) (hb : b ∈ Set.Icc 0 1) (h0 : 0 < b) (h1 : b < 1) : Rb b hb = ProbabilityTheory.Copula.finiteOrdinalSum (rbPartition b h0 h1) ![ProbabilityTheory.Copula.comonotonic 2, Rb 0 zero_mem_Icc01, ProbabilityTheory.Copula.comonotonic 2]

Proposition 5.3 (ii): for 0 < b < 1, R_b is the ordinal sum of M, R_0, M with respect to the partition {[0, b/2], [b/2, 1 - b/2], [1 - b/2, 1]}.

theorem Papers.OrendayLaresRockel2026XiBeta.proposition_5_3_iii_iv (b : ℝ) (hb : b ∈ Set.Icc 0 1) : (Rb b hb).blomqvistBeta = b ∧ (Rb b hb).chatterjeeXi = 1 - 3 / 4 * (1 - b) ^ 2 ∧ (Rb b hb).kendallTau = 1 - 1 / 2 * (1 - b) ^ 2 ∧ (Rb b hb).spearmanRho = 1 - 1 / 2 * (1 - b) ^ 3

Proposition 5.3 (iii) and (iv): β, ξ, τ, ρ of R_b.

theorem Papers.OrendayLaresRockel2026XiBeta.proposition_5_3_law (b : ℝ) (hb : b ∈ Set.Icc 0 1) : Rb b hb = ProbabilityTheory.Copula.ofMap probVb (Xb b) ⋯ ⋯ ∧ (Rb b hb).toMeasure = lawVb b

Proposition 5.3, first statement: R_b is the copula of (U, V_b) for independent U ~ U(0,1) and fair coin ε, and V_b is uniform.