← Mathematical handbook

Kendall's τ and Spearman's ρ of R_b (Proposition 5.3 (iv))

τ(R_b) = 1 - (1/2)(1-b)² and ρ(R_b) = 1 - (1/2)(1-b)³, computed from the representation of R_b as the law of (U, V_b).

theorem Papers.OrendayLaresRockel2026XiBeta.integral_Rb {b : ℝ} (hb : b ∈ Set.Icc 0 1) {g : (Fin 2 → ↑unitInterval) → ℝ} (hg : Continuous g) : ∫ (x : Fin 2 → ↑unitInterval), g x ∂(Rb b hb).toMeasure = ∫ (t : ↑unitInterval), (g (Xb b (t, false)) + g (Xb b (t, true))) / 2

Integrals against R_b reduce to a one-dimensional integral over U of the average over the two coin outcomes.

theorem Papers.OrendayLaresRockel2026XiBeta.integral_unit_add_Ioo (f1 h : ℝ → ℝ) (hf1 : Continuous f1) (hh : Continuous h) {s e : ℝ} (hs0 : 0 ≤ s) (hse : s ≤ e) (he1 : e ≤ 1) : ∫ (t : ↑unitInterval), f1 ↑t + (Set.Ioo s e).indicator h ↑t = (∫ (x : ℝ) in 0..1, f1 x) + ∫ (x : ℝ) in s..e, h x

theorem Papers.OrendayLaresRockel2026XiBeta.integral_quad (A B D l r : ℝ) : ∫ (x : ℝ) in l..r, A * x ^ 2 + B * x + D = A * (r ^ 3 - l ^ 3) / 3 + B * (r ^ 2 - l ^ 2) / 2 + D * (r - l)

theorem Papers.OrendayLaresRockel2026XiBeta.Rb_cdf_Xb_outside {b : ℝ} (hb : b ∈ Set.Icc 0 1) (t : ↑unitInterval) (e : Bool) (hc : ¬(b / 2 < ↑t ∧ ↑t < 1 - b / 2)) : (Rb b hb).cdf (Xb b (t, e)) = ↑t

On the support, R_b(t, V_b) = t outside (b/2, 1 - b/2).

theorem Papers.OrendayLaresRockel2026XiBeta.Rb_cdf_Xb_mid {b : ℝ} (hb : b ∈ Set.Icc 0 1) (t : ↑unitInterval) (hc : b / 2 < ↑t ∧ ↑t < 1 - b / 2) : (Rb b hb).cdf (Xb b (t, false)) = (2 * ↑t + b) / 4 ∧ (Rb b hb).cdf (Xb b (t, true)) = ↑t

On the support, in the middle block: R_b(t, A_b(t)) = A_b(t) and R_b(t, B_b(t)) = t.

theorem Papers.OrendayLaresRockel2026XiBeta.kendallTau_Rb {b : ℝ} (hb : b ∈ Set.Icc 0 1) : (Rb b hb).kendallTau = 1 - 1 / 2 * (1 - b) ^ 2

Proposition 5.3 (iv): τ(R_b) = 1 - (1/2)(1 - b)².

theorem Papers.OrendayLaresRockel2026XiBeta.spearmanRho_Rb {b : ℝ} (hb : b ∈ Set.Icc 0 1) : (Rb b hb).spearmanRho = 1 - 1 / 2 * (1 - b) ^ 3

Proposition 5.3 (iv): ρ(R_b) = 1 - (1/2)(1 - b)³.