← Mathematical handbook

Reflection, radial symmetry, and dependence of the tent family

theorem Papers.OrendayLaresRockel2026XiBeta.tentDisplacement_symm (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (v : ↑unitInterval) : (tentDisplacement b hb).toFun (unitInterval.symm v) = (tentDisplacement b hb).toFun v

theorem Papers.OrendayLaresRockel2026XiBeta.tentDisplacement_neg (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (hnb : -b ∈ Set.Icc (-1) 1) (v : ↑unitInterval) : (tentDisplacement (-b) hnb).toFun v = -(tentDisplacement b hb).toFun v

theorem Papers.OrendayLaresRockel2026XiBeta.medianWedge_symm (u : ↑unitInterval) : Verification.medianWedge (unitInterval.symm u) = Verification.medianWedge u

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_reflect_second (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).reflect {1} = leftBoundary (-b) ⋯

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_reflect_first (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).reflect {0} = leftBoundary (-b) ⋯

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_radiallySymmetric (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).IsRadiallySymmetric

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_zero (h0 : 0 ∈ Set.Icc (-1) 1) : leftBoundary 0 h0 = ProbabilityTheory.Copula.independence 2

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_isSI (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (hpos : 0 ≤ b) : (leftBoundary b hb).IsSI

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_isSD (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (hneg : b ≤ 0) : (leftBoundary b hb).IsSD

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_pqd_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).IsPQD ↔ 0 ≤ b

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_nqd_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).IsNQD ↔ b ≤ 0

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_si_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).IsSI ↔ 0 ≤ b

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_sd_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).IsSD ↔ b ≤ 0

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_conditionalCDF (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (leftBoundary b hb).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => if u ≤ ProbabilityTheory.Copula.unitHalf then ↑v + (tentDisplacement b hb).toFun v else ↑v - (tentDisplacement b hb).toFun v

Proposition 2, equation (8), as an almost-everywhere conditional-CDF identity.

def Papers.OrendayLaresRockel2026XiBeta.medianQuadrant (p q : Bool) : Set (Fin 2 → ↑unitInterval)

A median quadrant, with true selecting the upper half in that coordinate. The half-open convention has no effect on mass because the marginals are uniform.

Equations

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

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_quadrant_masses (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (p q : Bool) : (leftBoundary b hb).toMeasure.real (medianQuadrant p q) = if p = q then (1 + b) / 4 else (1 - b) / 4

Proposition 3(ii): all four median quadrant masses.