← Mathematical handbook

The right-boundary median sections A_b and the copulas R_b (equation (5.5))

For b ∈ [0,1] the slope p_b equals 1 on [0, b/2], 1/2 on (b/2, 1 - b/2] and 0 afterwards, so that A_b(u) = min {u, (2u + b)/4, 1/2}. The two-branch copula of the source is R_b := Q_{A_b}, the maximal completion of A_b. Its gap function is w_b(u) = max {|u - 1/2|, (1 - b)/2}.

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

The slope of A_b: 1 on [0, b/2], 1/2 on (b/2, 1 - b/2], 0 afterwards.

Equations

• Papers.OrendayLaresRockel2026XiBeta.rightSlope b u = if u ≤ b / 2 then 1 else if u ≤ 1 - b / 2 then 1 / 2 else 0

theorem Papers.OrendayLaresRockel2026XiBeta.antitone_rightSlope (b : ℝ) : Antitone (rightSlope b)

theorem Papers.OrendayLaresRockel2026XiBeta.integral_eq_of_eq_on_Ioc {f : ℝ → ℝ} {c d k : ℝ} (hcd : c ≤ d) (h : ∀ t ∈ Set.Ioc c d, f t = k) : ∫ (t : ℝ) in c..d, f t = (d - c) * k

theorem Papers.OrendayLaresRockel2026XiBeta.integral_rightSlope {b : ℝ} (hb : b ∈ Set.Icc 0 1) {u : ℝ} (hu : 0 ≤ u) : ∫ (t : ℝ) in 0..u, rightSlope b t = min (min u ((2 * u + b) / 4)) (1 / 2)

∫₀ᵘ p_b = min {u, (2u + b)/4, 1/2} for u ≥ 0 and b ∈ [0,1].

noncomputable def Papers.OrendayLaresRockel2026XiBeta.rightSection (b : ℝ) (hb : b ∈ Set.Icc 0 1) : MedianSection

The median section A_b of equation (5.5), as an element of S.

Equations

• Papers.OrendayLaresRockel2026XiBeta.rightSection b hb = { p := Papers.OrendayLaresRockel2026XiBeta.rightSlope b, antitone := ⋯, nonneg := ⋯, le_one := ⋯, integral_eq := ⋯ }

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

The two-branch copula R_b of equation (5.5): the maximal completion of A_b.

Equations

• Papers.OrendayLaresRockel2026XiBeta.Rb b hb = (Papers.OrendayLaresRockel2026XiBeta.rightSection b hb).completion

theorem Papers.OrendayLaresRockel2026XiBeta.rightSection_A {b : ℝ} (hb : b ∈ Set.Icc 0 1) {u : ℝ} (hu : 0 ≤ u) : (rightSection b hb).A u = min (min u ((2 * u + b) / 4)) (1 / 2)

theorem Papers.OrendayLaresRockel2026XiBeta.rightSection_gap {b : ℝ} (hb : b ∈ Set.Icc 0 1) {u : ℝ} (hu : 0 ≤ u) : (rightSection b hb).gap u = max |u - 1 / 2| ((1 - b) / 2)

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

theorem Papers.OrendayLaresRockel2026XiBeta.Rb_cdf_half {b : ℝ} (hb : b ∈ Set.Icc 0 1) (u : ↑unitInterval) : (Rb b hb).cdf ![u, ProbabilityTheory.Copula.unitHalf] = min (min (↑u) ((2 * ↑u + b) / 4)) (1 / 2)

theorem Papers.OrendayLaresRockel2026XiBeta.Rb_beta {b : ℝ} (hb : b ∈ Set.Icc 0 1) : (Rb b hb).blomqvistBeta = b