← Mathematical handbook

R_0 and the ordinal-sum structure of R_b (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]} (Copula.finiteOrdinalSum).

theorem Papers.OrendayLaresRockel2026XiBeta.zero_mem_Icc01 : 0 ∈ Set.Icc 0 1

theorem Papers.OrendayLaresRockel2026XiBeta.Rb_zero_cdf_of_le_half (u v : ↑unitInterval) (hv : ↑v ≤ 1 / 2) : (Rb 0 zero_mem_Icc01).cdf ![u, v] = min (↑u / 2) ↑v

R_0: R_0(u, v) = min (u/2, v) for v ≤ 1/2 and min (u, u/2 + v - 1/2) for v ≥ 1/2.

theorem Papers.OrendayLaresRockel2026XiBeta.Rb_zero_cdf_of_half_le (u v : ↑unitInterval) (hv : 1 / 2 ≤ ↑v) : (Rb 0 zero_mem_Icc01).cdf ![u, v] = min (↑u) (↑u / 2 + ↑v - 1 / 2)

noncomputable def Papers.OrendayLaresRockel2026XiBeta.rbPartition (b : ℝ) (h0 : 0 < b) (h1 : b < 1) : ProbabilityTheory.Copula.IntervalPartition 3

The partition {[0, b/2], [b/2, 1 - b/2], [1 - b/2, 1]}.

Equations

• Papers.OrendayLaresRockel2026XiBeta.rbPartition b h0 h1 = { point := ![0, ⟨b / 2, ⋯⟩, ⟨1 - b / 2, ⋯⟩, 1], strictMono := ⋯, zero := ⋯, one := ⋯ }

theorem Papers.OrendayLaresRockel2026XiBeta.rbPartition_point_one (b : ℝ) (h0 : 0 < b) (h1 : b < 1) : ↑((rbPartition b h0 h1).point 1) = b / 2

theorem Papers.OrendayLaresRockel2026XiBeta.rbPartition_point_two (b : ℝ) (h0 : 0 < b) (h1 : b < 1) : ↑((rbPartition b h0 h1).point 2) = 1 - b / 2

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

noncomputable def Papers.OrendayLaresRockel2026XiBeta.ordLhs (b u v : ℝ) : ℝ

The real-variable identity behind the ordinal-sum decomposition (one zone).

Equations

• Papers.OrendayLaresRockel2026XiBeta.ordLhs b u v = if v ≤ 1 / 2 then min (Papers.OrendayLaresRockel2026XiBeta.rbA b u) v else min u (Papers.OrendayLaresRockel2026XiBeta.rbA b u + v - 1 / 2)

noncomputable def Papers.OrendayLaresRockel2026XiBeta.ordRhs (b u v : ℝ) : ℝ

Equations

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

theorem Papers.OrendayLaresRockel2026XiBeta.ordinal_real_00 {b u v : ℝ} (_hb0 : 0 ≤ b) (_hb1 : b ≤ 1) (_h0 : 0 < b) (_h1 : b < 1) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) (h0 : u ≤ b / 2) (h1 : v ≤ b / 2) : ordLhs b u v = ordRhs b u v

theorem Papers.OrendayLaresRockel2026XiBeta.ordinal_real_01 {b u v : ℝ} (_hb0 : 0 ≤ b) (_hb1 : b ≤ 1) (_h0 : 0 < b) (_h1 : b < 1) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) (h0 : u ≤ b / 2) (h1 : b / 2 ≤ v) (h2 : v ≤ 1 - b / 2) : ordLhs b u v = ordRhs b u v

theorem Papers.OrendayLaresRockel2026XiBeta.ordinal_real_02 {b u v : ℝ} (_hb0 : 0 ≤ b) (_hb1 : b ≤ 1) (_h0 : 0 < b) (_h1 : b < 1) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) (h0 : u ≤ b / 2) (h1 : 1 - b / 2 ≤ v) : ordLhs b u v = ordRhs b u v

theorem Papers.OrendayLaresRockel2026XiBeta.ordinal_real_10 {b u v : ℝ} (_hb0 : 0 ≤ b) (_hb1 : b ≤ 1) (_h0 : 0 < b) (_h1 : b < 1) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) (h0 : b / 2 ≤ u) (h1 : u ≤ 1 - b / 2) (h2 : v ≤ b / 2) : ordLhs b u v = ordRhs b u v

theorem Papers.OrendayLaresRockel2026XiBeta.ordinal_real_11 {b u v : ℝ} (_hb0 : 0 ≤ b) (_hb1 : b ≤ 1) (_h0 : 0 < b) (_h1 : b < 1) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) (h0 : b / 2 ≤ u) (h1 : u ≤ 1 - b / 2) (h2 : b / 2 ≤ v) (h3 : v ≤ 1 - b / 2) : ordLhs b u v = ordRhs b u v

theorem Papers.OrendayLaresRockel2026XiBeta.ordinal_real_12 {b u v : ℝ} (_hb0 : 0 ≤ b) (_hb1 : b ≤ 1) (_h0 : 0 < b) (_h1 : b < 1) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) (h0 : b / 2 ≤ u) (h1 : u ≤ 1 - b / 2) (h2 : 1 - b / 2 ≤ v) : ordLhs b u v = ordRhs b u v

theorem Papers.OrendayLaresRockel2026XiBeta.ordinal_real_20 {b u v : ℝ} (_hb0 : 0 ≤ b) (_hb1 : b ≤ 1) (_h0 : 0 < b) (_h1 : b < 1) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) (h0 : 1 - b / 2 ≤ u) (h1 : v ≤ b / 2) : ordLhs b u v = ordRhs b u v

theorem Papers.OrendayLaresRockel2026XiBeta.ordinal_real_21 {b u v : ℝ} (_hb0 : 0 ≤ b) (_hb1 : b ≤ 1) (_h0 : 0 < b) (_h1 : b < 1) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) (h0 : 1 - b / 2 ≤ u) (h1 : b / 2 ≤ v) (h2 : v ≤ 1 - b / 2) : ordLhs b u v = ordRhs b u v

theorem Papers.OrendayLaresRockel2026XiBeta.ordinal_real_22 {b u v : ℝ} (_hb0 : 0 ≤ b) (_hb1 : b ≤ 1) (_h0 : 0 < b) (_h1 : b < 1) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) (hv0 : 0 ≤ v) (hv1 : v ≤ 1) (h0 : 1 - b / 2 ≤ u) (h1 : 1 - b / 2 ≤ v) : ordLhs b u v = ordRhs b u v

theorem Papers.OrendayLaresRockel2026XiBeta.ordinal_real {b : ℝ} (hb0 : 0 ≤ b) (hb1 : b ≤ 1) (h0 : 0 < b) (h1 : b < 1) {u v : ℝ} (hu : u ∈ Set.Icc 0 1) (hv : v ∈ Set.Icc 0 1) : ordLhs b u v = ordRhs b u v

theorem Papers.OrendayLaresRockel2026XiBeta.Rb_eq_finiteOrdinalSum {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]}.