← Mathematical handbook

Elementary properties of the two-branch copulas R_b (Proposition 5.3 (i))

Explicit distribution function of R_b, the identification R_1 = M, radial symmetry, failure of exchangeability for b < 1, and failure of stochastic increasingness of R_bᵀ for b < 1 (via the concavity criterion).

noncomputable def Papers.OrendayLaresRockel2026XiBeta.rbA (b u : ℝ) : ℝ

The median section A_b(u) = min {u, (2u + b)/4, 1/2} of equation (5.5).

Equations

• Papers.OrendayLaresRockel2026XiBeta.rbA b u = min (min u ((2 * u + b) / 4)) (1 / 2)

theorem Papers.OrendayLaresRockel2026XiBeta.Rb_cdf_of_le_half {b : ℝ} (hb : b ∈ Set.Icc 0 1) (u v : ↑unitInterval) (hv : ↑v ≤ 1 / 2) : (Rb b hb).cdf ![u, v] = min (rbA b ↑u) ↑v

Distribution function of R_b, lower half v ≤ 1/2.

theorem Papers.OrendayLaresRockel2026XiBeta.Rb_cdf_of_half_le {b : ℝ} (hb : b ∈ Set.Icc 0 1) (u v : ↑unitInterval) (hv : 1 / 2 ≤ ↑v) : (Rb b hb).cdf ![u, v] = min (↑u) (rbA b ↑u + ↑v - 1 / 2)

Distribution function of R_b, upper half v ≥ 1/2.

theorem Papers.OrendayLaresRockel2026XiBeta.rbA_symm {b : ℝ} (hb : b ∈ Set.Icc 0 1) {u : ℝ} (hu : u ∈ Set.Icc 0 1) : rbA b (1 - u) = rbA b u - u + 1 / 2

theorem Papers.OrendayLaresRockel2026XiBeta.Rb_isRadiallySymmetric {b : ℝ} (hb : b ∈ Set.Icc 0 1) : (Rb b hb).IsRadiallySymmetric

Proposition 5.3 (i): R_b is radially symmetric.

theorem Papers.OrendayLaresRockel2026XiBeta.Rb_one_eq_comonotonic (hb : 1 ∈ Set.Icc 0 1) : Rb 1 hb = ProbabilityTheory.Copula.comonotonic 2

Proposition 5.3 (i): R_1 = M.

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

The point v₀ = (1 + b)/4 = A_b(1/2) of the unit interval.

Equations

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

theorem Papers.OrendayLaresRockel2026XiBeta.rbV0_le_half (b : ℝ) (hb : b ∈ Set.Icc 0 1) : ↑(rbV0 b hb) ≤ 1 / 2

theorem Papers.OrendayLaresRockel2026XiBeta.rbA_half {b : ℝ} (hb : b ∈ Set.Icc 0 1) : rbA b (1 / 2) = (1 + b) / 4

theorem Papers.OrendayLaresRockel2026XiBeta.Rb_not_exchangeable {b : ℝ} (hb : b ∈ Set.Icc 0 1) (hb1 : b < 1) : ¬(Rb b hb).IsExchangeable

Proposition 5.3 (i): for b < 1, R_b is not exchangeable: R_b(1/2, v₀) = v₀ > (1 + 3b)/8 = R_b(v₀, 1/2) where v₀ = (1 + b)/4.

theorem Papers.OrendayLaresRockel2026XiBeta.Rb_transpose_not_isSI {b : ℝ} (hb : b ∈ Set.Icc 0 1) (hb1 : b < 1) : ¬(Rb b hb).transpose.IsSI

Proposition 5.3 (i): for b < 1, R_bᵀ is not SI, because v ↦ R_b(1/2, v) is not concave (concavity criterion transpose_isSI_iff_concave).