← Mathematical handbook

Proposition 3.1 (tent copulas), in the notation of the article

L_b = leftBoundary b hb, L_b(u,v) = u v + ℓ(u) g_b(v) (equation (3.2)):

• the CDF formula and its two strip forms,
• the copula density c_b = 1 + σ(u) g_b'(v) ∈ {0,1,2} a.e. (3.3), and L_b(u,v) = ∫∫ c_b,
• the Markov kernel ∂₁ L_b(u,v) = v + σ(u) g_b(v) (3.4) (a.e. and classical derivative),
• v ↦ v ± g_b(v) are distribution functions,
• β(L_b) = b, L_b(1/2,1/2) = (1+b)/4, ξ(L_b) = |b|³/2 and the integral computation ∫∫ (∂₁ L_b)² = 1/3 + |b|³/12.

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

Equation (3.2): L_b(u,v) = u v + ℓ(u) g_b(v).

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_cdf_left_strip (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) {u : ↑unitInterval} (v : ↑unitInterval) (hu : ↑u ≤ 1 / 2) : (leftBoundary b hb).cdf ![u, v] = ↑u * (↑v + tentG b ↑v)

L_b(u,v) = u (v + g_b(v)) on the strip u ≤ 1/2.

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_cdf_right_strip (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) {u : ↑unitInterval} (v : ↑unitInterval) (hu : 1 / 2 ≤ ↑u) : (leftBoundary b hb).cdf ![u, v] = ↑u * ↑v + (1 - ↑u) * tentG b ↑v

L_b(u,v) = u v + (1 - u) g_b(v) on the strip u ≥ 1/2.

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_cdf_half (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).cdf ![ProbabilityTheory.Copula.unitHalf, ProbabilityTheory.Copula.unitHalf] = (1 + b) / 4

theorem Papers.OrendayLaresRockel2026XiBeta.tent_distribution_functions (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (Monotone fun (v : ℝ) => v + tentG b v) ∧ (Monotone fun (v : ℝ) => v - tentG b v) ∧ tentG b 0 = 0 ∧ tentG b 1 = 0

The two conditional distribution functions v ↦ v + g_b(v) and v ↦ v - g_b(v) are nondecreasing, vanish at 0 and equal 1 at 1.

theorem Papers.OrendayLaresRockel2026XiBeta.hasDerivAt_tent_formula (b v : ℝ) {u : ℝ} (hu : u ≠ 1 / 2) : HasDerivAt (fun (w : ℝ) => w * v + ellFun w * tentG b v) (v + sigmaFun u * tentG b v) u

Equation (3.4), classical form: for u ≠ 1/2 the map u ↦ L_b(u,v) (extended by its formula to ℝ) has derivative v + σ(u) g_b(v).

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_kernel_paper (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (leftBoundary b hb).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => ↑v + sigmaFun ↑u * tentG b ↑v

Equation (3.4): the Markov kernel ∂₁ L_b(u,v) = v + σ(u) g_b(v) for a.e. u.

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_deriv_paper (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (v : ↑unitInterval) : ∀ᵐ (u : ↑unitInterval), deriv ((leftBoundary b hb).cdfSection v) ↑u = ↑v + sigmaFun ↑u * tentG b ↑v

Equation (3.4) with the classical partial derivative: for a.e. u, ∂₁L_b(u,v) = v + σ(u) g_b(v).

The density (3.3)

theorem Papers.OrendayLaresRockel2026XiBeta.tentSlope_eq (r v : ↑unitInterval) (h1 : ↑v ≠ (1 - ↑r) / 2) (h2 : ↑v ≠ 1 / 2) (h3 : ↑v ≠ (1 + ↑r) / 2) : tentSlope r v = (if (1 - ↑r) / 2 < ↑v ∧ ↑v < 1 / 2 then 1 else 0) - if 1 / 2 < ↑v ∧ ↑v < (1 + ↑r) / 2 then 1 else 0

theorem Papers.OrendayLaresRockel2026XiBeta.signedTentSlope_eq_tentGDeriv (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (v : ↑unitInterval) (h1 : ↑v ≠ (1 - |b|) / 2) (h2 : ↑v ≠ 1 / 2) (h3 : ↑v ≠ (1 + |b|) / 2) : signedTentSlope b hb v = tentGDeriv b ↑v

theorem Papers.OrendayLaresRockel2026XiBeta.ae_coord_ne (i : Fin 2) (c : ℝ) : ∀ᵐ (x : Fin 2 → ↑unitInterval), ↑(x i) ≠ c

noncomputable def Papers.OrendayLaresRockel2026XiBeta.tentDensityPaper (b : ℝ) (x : Fin 2 → ↑unitInterval) : ℝ

The density of the article, c_b(u,v) = 1 + σ(u) g_b'(v).

Equations

• Papers.OrendayLaresRockel2026XiBeta.tentDensityPaper b x = 1 + Papers.OrendayLaresRockel2026XiBeta.sigmaFun ↑(x 0) * Papers.OrendayLaresRockel2026XiBeta.tentGDeriv b ↑(x 1)

theorem Papers.OrendayLaresRockel2026XiBeta.tentDensity_ae_eq_paper (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∀ᵐ (x : Fin 2 → ↑unitInterval), tentDensity b hb x = tentDensityPaper b x

The version-1 density agrees a.e. with 1 + σ(u) g_b'(v).

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_density_paper (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (tentDensityPaper b x)

Equation (3.3): the actual law of L_b has density 1 + σ(u) g_b'(v).

theorem Papers.OrendayLaresRockel2026XiBeta.tentDensityPaper_values_ae (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∀ᵐ (x : Fin 2 → ↑unitInterval), tentDensityPaper b x = 0 ∨ tentDensityPaper b x = 1 ∨ tentDensityPaper b x = 2

The density takes the values 0, 1, 2 almost everywhere.

theorem Papers.OrendayLaresRockel2026XiBeta.measurable_tentGDeriv (b : ℝ) : Measurable (tentGDeriv b)

theorem Papers.OrendayLaresRockel2026XiBeta.measurable_sigmaFun : Measurable sigmaFun

theorem Papers.OrendayLaresRockel2026XiBeta.measurable_tentDensityPaper (b : ℝ) : Measurable (tentDensityPaper b)

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_cdf_eq_integral_density (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) (u v : ↑unitInterval) : (leftBoundary b hb).cdf ![u, v] = ∫ (x : Fin (Nat.succ 1) → ↑unitInterval) in Set.Iic ![u, v], tentDensityPaper b x

L_b(u,v) = ∫_{[0,u]×[0,v]} c_b.

theorem Papers.OrendayLaresRockel2026XiBeta.integral_sigmaFun_sq_kernel (g w : ℝ) : ∫ (u : ↑unitInterval), (w + sigmaFun ↑u * g) ^ 2 = w ^ 2 + g ^ 2

theorem Papers.OrendayLaresRockel2026XiBeta.tent_kernel_sq_integral (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∫ (v : ↑unitInterval) (u : ↑unitInterval), (↑v + sigmaFun ↑u * tentG b ↑v) ^ 2 = 1 / 3 + |b| ^ 3 / 12

The computation in the proof of Proposition 3.1: ∫∫ (∂₁L_b)² = ∫ (v² + g_b(v)²) dv = 1/3 + |b|³/12.

theorem Papers.OrendayLaresRockel2026XiBeta.xi_leftBoundary_from_kernel (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).chatterjeeXi = 6 * (1 / 3 + |b| ^ 3 / 12) - 2

Proposition 3.1, ξ(L_b) = |b|³/2 computed from the kernel exactly as in the article.