← Mathematical handbook

Proposition 3.2 (further properties of L_b) and Remark 3.3

• (i) Ľ_b = L_{-b}, L̂_b = L_b, exchangeability iff b ∈ {-1,0,1}, L_0 = Π, L_1 = Π ⊕_{1/2} Π (ordinal sum), L_{-1} = Ľ_1, the explicit asymmetry L_b(u,1/2) ≠ L_b(1/2,u) and the density c_1;
• (ii) stochastic monotonicity and quadrant dependence;
• (iii) reverse direction;
• (iv) total positivity (with the article's density 1 + σ g_b');
• (v) ρ(L_b) = 3b|b|/4, τ(L_b) = b|b|/2.

theorem Papers.OrendayLaresRockel2026XiBeta.tentG_one (v : ℝ) (hv : v ∈ Set.Icc 0 1) : tentG 1 v = min v (1 - v)

theorem Papers.OrendayLaresRockel2026XiBeta.tentG_neg_one (v : ℝ) (hv : v ∈ Set.Icc 0 1) : tentG (-1) v = -min v (1 - v)

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_one_cdf (hb : 1 ∈ Set.Icc (-1) 1) (u v : ↑unitInterval) : (leftBoundary 1 hb).cdf ![u, v] = ↑u * ↑v + ellFun ↑u * ellFun ↑v

L_{±1}(u,v) = u v ± ℓ(u) ℓ(v).

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_neg_one_cdf (hb : -1 ∈ Set.Icc (-1) 1) (u v : ↑unitInterval) : (leftBoundary (-1) hb).cdf ![u, v] = ↑u * ↑v - ellFun ↑u * ellFun ↑v

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_one_eq_ordinalSum (hb : 1 ∈ Set.Icc (-1) 1) : leftBoundary 1 hb = (ProbabilityTheory.Copula.independence 2).ordinalSum (ProbabilityTheory.Copula.independence 2) ProbabilityTheory.Copula.unitHalf

Proposition 3.2(i): L_1 is the ordinal sum of Π and Π with respect to the partition {[0,1/2],[1/2,1]}.

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_neg_one_eq_check (hb : 1 ∈ Set.Icc (-1) 1) (hb' : -1 ∈ Set.Icc (-1) 1) : leftBoundary (-1) hb' = (leftBoundary 1 hb).reflect {1}

L_{-1} = Ľ_1.

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

Proposition 3.2(i): Ľ_b = L_{-b}.

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_survival (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).survivalCopula = leftBoundary b hb

Proposition 3.2(i): L̂_b = L_b.

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_asymmetry (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) {u : ↑unitInterval} (hu0 : 0 < ↑u) (hu : ↑u < (1 - |b|) / 2) (hb0 : b ≠ 0) : (leftBoundary b hb).cdf ![u, ProbabilityTheory.Copula.unitHalf] = ↑u / 2 + b / 2 * ellFun ↑u ∧ (leftBoundary b hb).cdf ![ProbabilityTheory.Copula.unitHalf, u] = ↑u / 2 ∧ (leftBoundary b hb).cdf ![u, ProbabilityTheory.Copula.unitHalf] ≠ (leftBoundary b hb).cdf ![ProbabilityTheory.Copula.unitHalf, u]

The explicit asymmetry from the proof of (i): for 0 < |b| < 1 and 0 < u < α_b, L_b(u,1/2) = u/2 + (b/2) ℓ(u) ≠ u/2 = L_b(1/2,u).

theorem Papers.OrendayLaresRockel2026XiBeta.tentDensity_one (hb : 1 ∈ Set.Icc (-1) 1) (x : Fin 2 → ↑unitInterval) : tentDensity 1 hb x = 1 + Verification.medianSign (x 0) * Verification.medianSign (x 1)

The density c_1 = 1 + σ(u) σ(v)-type formula: c_1 = 2 on the two diagonal median quadrants and 0 on the other two (with the half-open convention at 1/2).

theorem Papers.OrendayLaresRockel2026XiBeta.tentDensity_one_diagonal (hb : 1 ∈ Set.Icc (-1) 1) (x : Fin 2 → ↑unitInterval) (h : x 0 ≤ ProbabilityTheory.Copula.unitHalf ∧ x 1 ≤ ProbabilityTheory.Copula.unitHalf ∨ ¬x 0 ≤ ProbabilityTheory.Copula.unitHalf ∧ ¬x 1 ≤ ProbabilityTheory.Copula.unitHalf) : tentDensity 1 hb x = 2

theorem Papers.OrendayLaresRockel2026XiBeta.tentDensity_one_antidiagonal (hb : 1 ∈ Set.Icc (-1) 1) (x : Fin 2 → ↑unitInterval) (h : x 0 ≤ ProbabilityTheory.Copula.unitHalf ∧ ¬x 1 ≤ ProbabilityTheory.Copula.unitHalf ∨ ¬x 0 ≤ ProbabilityTheory.Copula.unitHalf ∧ x 1 ≤ ProbabilityTheory.Copula.unitHalf) : tentDensity 1 hb x = 0

theorem Papers.OrendayLaresRockel2026XiBeta.tentDensityPaper_nonneg (b : ℝ) (x : Fin 2 → ↑unitInterval) : 0 ≤ tentDensityPaper b x

theorem Papers.OrendayLaresRockel2026XiBeta.tentDensityPaper_ae_tp2_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (Verification.HasAEOrderedMinors 1 fun (u v : ↑unitInterval) => tentDensityPaper b ![u, v]) ↔ b = 0 ∨ b = 1

Proposition 3.2(iv) for the article's density c_b = 1 + σ(u) g_b'(v).

theorem Papers.OrendayLaresRockel2026XiBeta.tentDensityPaper_ae_rr2_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (Verification.HasAEOrderedMinors (-1) fun (u v : ↑unitInterval) => tentDensityPaper b ![u, v]) ↔ b = 0 ∨ b = -1

theorem Papers.OrendayLaresRockel2026XiBeta.proposition_3_2 (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).reflect {1} = leftBoundary (-b) ⋯ ∧ (leftBoundary b hb).survivalCopula = leftBoundary b hb ∧ ((leftBoundary b hb).IsExchangeable ↔ b = -1 ∨ b = 0 ∨ b = 1) ∧ (0 ≤ b → (leftBoundary b hb).IsSI) ∧ (b ≤ 0 → (leftBoundary b hb).IsSD) ∧ ((leftBoundary b hb).IsPQD ↔ 0 ≤ b) ∧ ((leftBoundary b hb).IsNQD ↔ b ≤ 0) ∧ ((leftBoundary b hb).transpose.IsSI ↔ b = 0 ∨ b = 1) ∧ ((leftBoundary b hb).transpose.IsSD ↔ b = 0 ∨ b = -1) ∧ ((Verification.HasAEOrderedMinors 1 fun (u v : ↑unitInterval) => tentDensityPaper b ![u, v]) ↔ b = 0 ∨ b = 1) ∧ ((Verification.HasAEOrderedMinors (-1) fun (u v : ↑unitInterval) => tentDensityPaper b ![u, v]) ↔ b = 0 ∨ b = -1) ∧ (leftBoundary b hb).spearmanRho = 3 * b * |b| / 4 ∧ (leftBoundary b hb).kendallTau = b * |b| / 2

Proposition 3.2, all five parts in the article's notation.

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

Proposition 3.2(i): L_0 = Π.

Values of the density (Figure 2) and the second partial derivative

theorem Papers.OrendayLaresRockel2026XiBeta.hasDerivAt_tent_formula_second (b u : ℝ) {v : ℝ} (h1 : v ≠ (1 - |b|) / 2) (h2 : v ≠ 1 / 2) (h3 : v ≠ (1 + |b|) / 2) : HasDerivAt (fun (w : ℝ) => u * w + ellFun u * tentG b w) (u + ellFun u * tentGDeriv b v) v

Proposition 3.2(iii): ∂₂ L_b(u,v) = u + ℓ(u) g_b'(v) away from the break points of g_b.

theorem Papers.OrendayLaresRockel2026XiBeta.tentDensityPaper_left {b : ℝ} {x : Fin 2 → ↑unitInterval} (hu : ↑(x 0) < 1 / 2) : ((1 - |b|) / 2 < ↑(x 1) ∧ ↑(x 1) < 1 / 2 → tentDensityPaper b x = 1 + sgn b) ∧ (1 / 2 < ↑(x 1) ∧ ↑(x 1) < (1 + |b|) / 2 → tentDensityPaper b x = 1 - sgn b) ∧ (¬((1 - |b|) / 2 < ↑(x 1) ∧ ↑(x 1) < 1 / 2) → ¬(1 / 2 < ↑(x 1) ∧ ↑(x 1) < (1 + |b|) / 2) → tentDensityPaper b x = 1)

Figure 2, strip u < 1/2: the density is 1 + sgn b on (α_b, 1/2), 1 - sgn b on (1/2, 1 - α_b) and 1 elsewhere.

theorem Papers.OrendayLaresRockel2026XiBeta.tentDensityPaper_right {b : ℝ} {x : Fin 2 → ↑unitInterval} (hu : 1 / 2 ≤ ↑(x 0)) : ((1 - |b|) / 2 < ↑(x 1) ∧ ↑(x 1) < 1 / 2 → tentDensityPaper b x = 1 - sgn b) ∧ (1 / 2 < ↑(x 1) ∧ ↑(x 1) < (1 + |b|) / 2 → tentDensityPaper b x = 1 + sgn b) ∧ (¬((1 - |b|) / 2 < ↑(x 1) ∧ ↑(x 1) < 1 / 2) → ¬(1 / 2 < ↑(x 1) ∧ ↑(x 1) < (1 + |b|) / 2) → tentDensityPaper b x = 1)

Figure 2, strip u ≥ 1/2: the density is 1 - sgn b on (α_b, 1/2), 1 + sgn b on (1/2, 1 - α_b) and 1 elsewhere.