← Mathematical handbook

Checks for exact-blest-regions.tex

The population coefficient below is the CDF-based Blest coefficient from the pinned supplement, not a new moment-only surrogate. See COVERAGE.md for the mapping from manuscript claims to their checked formal statements.

noncomputable def Papers.Rockel2026ExactBlest.eta (C : ProbabilityTheory.Copula 2) : ℝ

Equations

• Papers.Rockel2026ExactBlest.eta C = (Papers.Rockel2026XiBlest.blestNu C + Papers.Rockel2026XiBlest.blestNu C.transpose) / 2

theorem Papers.Rockel2026ExactBlest.eta_transpose (C : ProbabilityTheory.Copula 2) : eta C.transpose = eta C

theorem Papers.Rockel2026ExactBlest.nu_transpose (C : ProbabilityTheory.Copula 2) : Rockel2026XiBlest.blestNu C.transpose = 2 * eta C - Rockel2026XiBlest.blestNu C

theorem Papers.Rockel2026ExactBlest.eta_mix (C D : ProbabilityTheory.Copula 2) (t : ↑unitInterval) : eta (C.mix D t) = ↑t * eta C + (1 - ↑t) * eta D

theorem Papers.Rockel2026ExactBlest.eta_mem_Icc (C : ProbabilityTheory.Copula 2) : eta C ∈ Set.Icc (-1) 1

theorem Papers.Rockel2026ExactBlest.nu_survival (C : ProbabilityTheory.Copula 2) : Rockel2026XiBlest.blestNu C.survivalCopula = 2 * C.spearmanRho - Rockel2026XiBlest.blestNu C

theorem Papers.Rockel2026ExactBlest.eta_survival (C : ProbabilityTheory.Copula 2) : eta C.survivalCopula = 2 * C.spearmanRho - eta C

theorem Papers.Rockel2026ExactBlest.nu_reflect_first (C : ProbabilityTheory.Copula 2) : Rockel2026XiBlest.blestNu (C.reflect {0}) = Rockel2026XiBlest.blestNu C - 2 * C.spearmanRho

theorem Papers.Rockel2026ExactBlest.eta_reflect_second (C : ProbabilityTheory.Copula 2) : eta (C.reflect {1}) = -C.spearmanRho + (Rockel2026XiBlest.blestNu C.transpose - Rockel2026XiBlest.blestNu C) / 2

theorem Papers.Rockel2026ExactBlest.reflection_byproduct (C : ProbabilityTheory.Copula 2) : Rockel2026XiBlest.blestNu (C.reflect {1}) - eta (C.reflect {1}) = C.spearmanRho - eta C

theorem Papers.Rockel2026ExactBlest.asymmetry_identity (C : ProbabilityTheory.Copula 2) : |Rockel2026XiBlest.blestNu C - Rockel2026XiBlest.blestNu C.transpose| = 2 * |Rockel2026XiBlest.blestNu C - eta C|

theorem Papers.Rockel2026ExactBlest.support_identity (C : ProbabilityTheory.Copula 2) (k : ℝ) : (1 + k) * Rockel2026XiBlest.blestNu C - 2 * k * eta C = Rockel2026XiBlest.blestNu C - k * Rockel2026XiBlest.blestNu C.transpose

theorem Papers.Rockel2026ExactBlest.integral_weighted_upper_indicator (u : ↑unitInterval) : (∫ (t : ↑unitInterval), if u ≤ t then 1 - ↑t else 0) = (1 - ↑u) ^ 2 / 2

theorem Papers.Rockel2026ExactBlest.nu_moment (C : ProbabilityTheory.Copula 2) : Rockel2026XiBlest.blestNu C = 12 * ∫ (y : Fin 2 → ↑unitInterval), (1 - ↑(y 0)) ^ 2 * (1 - ↑(y 1)) ∂C.toMeasure - 2

theorem Papers.Rockel2026ExactBlest.nu_transpose_moment (C : ProbabilityTheory.Copula 2) : Rockel2026XiBlest.blestNu C.transpose = 12 * ∫ (y : Fin 2 → ↑unitInterval), (1 - ↑(y 0)) * (1 - ↑(y 1)) ^ 2 ∂C.toMeasure - 2

theorem Papers.Rockel2026ExactBlest.eta_moment (C : ProbabilityTheory.Copula 2) : eta C = 6 * ∫ (y : Fin 2 → ↑unitInterval), (1 - ↑(y 0)) * (1 - ↑(y 1)) * (1 - ↑(y 0) + (1 - ↑(y 1))) ∂C.toMeasure - 2

theorem Papers.Rockel2026ExactBlest.support_moment (C : ProbabilityTheory.Copula 2) (k : ℝ) : (1 + k) * Rockel2026XiBlest.blestNu C - 2 * k * eta C = 12 * ∫ (y : Fin 2 → ↑unitInterval), (1 - ↑(y 0)) ^ 2 * (1 - ↑(y 1)) - k * (1 - ↑(y 0)) * (1 - ↑(y 1)) ^ 2 ∂C.toMeasure - 2 * (1 - k)

Explicit antiderivatives for the two transport certificates.

def Papers.Rockel2026ExactBlest.cost (k x z : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.cost k x z = x ^ 2 * z - k * x * z ^ 2

noncomputable def Papers.Rockel2026ExactBlest.antiPhi (k x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.antiPhi k x = -k * x + (1 + k) * x ^ 2 - (2 + k) * x ^ 3 / 3

noncomputable def Papers.Rockel2026ExactBlest.linearPsi (k m b z : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.linearPsi k m b z = (m ^ 2 - 2 * k * m) * z ^ 3 / 3 + b * (m - k) * z ^ 2 + b ^ 2 * z

noncomputable def Papers.Rockel2026ExactBlest.kA (w : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.kA w = (1 + 2 * w) / (2 * (1 - w))

noncomputable def Papers.Rockel2026ExactBlest.phiA0 (w x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.phiA0 w x = Papers.Rockel2026ExactBlest.antiPhi (Papers.Rockel2026ExactBlest.kA w) x - Papers.Rockel2026ExactBlest.antiPhi (Papers.Rockel2026ExactBlest.kA w) w

noncomputable def Papers.Rockel2026ExactBlest.graphPhi (w x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.graphPhi w x = (2 - Papers.Rockel2026ExactBlest.kA w) * x ^ 3 / 3 + w * (Papers.Rockel2026ExactBlest.kA w - 1) * x ^ 2 - Papers.Rockel2026ExactBlest.kA w * w ^ 2 * x

noncomputable def Papers.Rockel2026ExactBlest.phiA1 (w x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.phiA1 w x = Papers.Rockel2026ExactBlest.graphPhi w x - Papers.Rockel2026ExactBlest.graphPhi w w

noncomputable def Papers.Rockel2026ExactBlest.psiA0 (w z : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.psiA0 w z = Papers.Rockel2026ExactBlest.linearPsi (Papers.Rockel2026ExactBlest.kA w) 1 w z

noncomputable def Papers.Rockel2026ExactBlest.psiA1 (w z : ℝ) : ℝ

Equations

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

noncomputable def Papers.Rockel2026ExactBlest.phiA (w x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.phiA w x = if x ≤ w then Papers.Rockel2026ExactBlest.phiA0 w x else Papers.Rockel2026ExactBlest.phiA1 w x

noncomputable def Papers.Rockel2026ExactBlest.psiA (w z : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.psiA w z = if z ≤ 1 - w then Papers.Rockel2026ExactBlest.psiA0 w z else Papers.Rockel2026ExactBlest.psiA1 w z

theorem Papers.Rockel2026ExactBlest.slackA00 (w x z : ℝ) (hw : w ≠ 1) : phiA0 w x + psiA0 w z - cost (kA w) x z = w * z ^ 2 * (1 - w - z) / (1 - w) + ((1 - w - z) * ((1 - 2 * w) * (1 - w) + z * (2 * w + 1)) * (w - x) + ((1 - 2 * w) * (1 - w) + z * (2 * w + 1) + (1 - w - z) * (5 - 2 * w)) * (w - x) ^ 2 / 2 + (5 - 2 * w) * (w - x) ^ 3 / 3) / (2 * (1 - w))

theorem Papers.Rockel2026ExactBlest.slackA01 (w x z : ℝ) (hw : w ≠ 1) : phiA0 w x + psiA1 w z - cost (kA w) x z = (x + z - 1) ^ 2 * (3 * (1 - w) + (5 - 2 * w) * (w - x) + (2 * w + 4) * (z - (1 - w))) / (6 * (1 - w))

theorem Papers.Rockel2026ExactBlest.slackA10 (w x z : ℝ) (hw : w ≠ 1) : phiA1 w x + psiA0 w z - cost (kA w) x z = (x - w - z) ^ 2 * (2 * w * (1 - w - z) + (x - w) * (1 - 2 * w)) / (2 * (1 - w))

theorem Papers.Rockel2026ExactBlest.slackA11 (w x z : ℝ) (hw : w ≠ 1) : phiA1 w x + psiA1 w z - cost (kA w) x z = (x - w) * (1 - 2 * w) * (1 - x) ^ 2 / (2 * (1 - w)) + ((x - w) * ((1 - w) * (1 + w - x)) * (z - (1 - w)) + ((1 - w) * (1 + w - x) + (x - w) * (w + 2)) * (z - (1 - w)) ^ 2 / 2 + (w + 2) * (z - (1 - w)) ^ 3 / 3) / (1 - w)

theorem Papers.Rockel2026ExactBlest.dualA (w x z : ℝ) (hw0 : 0 ≤ w) (hw1 : w ≤ 1 / 2) (hx : x ∈ Set.Icc 0 1) (hz : z ∈ Set.Icc 0 1) : cost (kA w) x z ≤ phiA w x + psiA w z

noncomputable def Papers.Rockel2026ExactBlest.kB (a : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.kB a = 2 * a / (1 - a)

noncomputable def Papers.Rockel2026ExactBlest.cutB (a : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.cutB a = (1 - a) / (2 * a)

noncomputable def Papers.Rockel2026ExactBlest.phiB0 (a x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.phiB0 a x = Papers.Rockel2026ExactBlest.antiPhi (Papers.Rockel2026ExactBlest.kB a) x - Papers.Rockel2026ExactBlest.antiPhi (Papers.Rockel2026ExactBlest.kB a) a

noncomputable def Papers.Rockel2026ExactBlest.splitPhi (a x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.splitPhi a x = x ^ 3 / (3 * a) - x ^ 2 / 2 - Papers.Rockel2026ExactBlest.kB a * (x - a) ^ 3 / (12 * a ^ 2)

noncomputable def Papers.Rockel2026ExactBlest.phiB1 (a x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.phiB1 a x = Papers.Rockel2026ExactBlest.splitPhi a x - Papers.Rockel2026ExactBlest.splitPhi a a

noncomputable def Papers.Rockel2026ExactBlest.psiB0 (a z : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.psiB0 a z = Papers.Rockel2026ExactBlest.linearPsi (Papers.Rockel2026ExactBlest.kB a) (2 * a) a z

noncomputable def Papers.Rockel2026ExactBlest.psiB1 (a z : ℝ) : ℝ

Equations

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

noncomputable def Papers.Rockel2026ExactBlest.psiB2 (a z : ℝ) : ℝ

Equations

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

noncomputable def Papers.Rockel2026ExactBlest.phiB (a x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.phiB a x = if x ≤ a then Papers.Rockel2026ExactBlest.phiB0 a x else Papers.Rockel2026ExactBlest.phiB1 a x

noncomputable def Papers.Rockel2026ExactBlest.psiB (a z : ℝ) : ℝ

Equations

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

theorem Papers.Rockel2026ExactBlest.slackB00 (a x z : ℝ) (ha : a ≠ 1) : phiB0 a x + psiB0 a z - cost (kB a) x z = 2 * a * z ^ 2 * ((1 - a) * (2 * a - 1) + (1 + a) * (1 - a - 2 * a * z)) / (3 * (1 - a)) + 2 * ((1 - a - z) * a * z * (a - x) + (1 - a - z + a * z) * (a - x) ^ 2 / 2 + (a - x) ^ 3 / 3) / (1 - a)

theorem Papers.Rockel2026ExactBlest.slackB01 (a x z : ℝ) (ha0 : a ≠ 0) (ha1 : a ≠ 1) (ha2 : 2 * a - 1 ≠ 0) : phiB0 a x + psiB1 a z - cost (kB a) x z = 2 * a * (1 - a - z) ^ 2 * ((1 - a) * (2 * a - 1) + (3 * a - 1) * (2 * a * z - (1 - a))) / (3 * (1 - a) * (2 * a - 1) ^ 2) + 2 * ((1 - a - z) * a * z * (a - x) + (1 - a - z + a * z) * (a - x) ^ 2 / 2 + (a - x) ^ 3 / 3) / (1 - a)

theorem Papers.Rockel2026ExactBlest.slackB02 (a x z : ℝ) (ha0 : a ≠ 0) (ha1 : a ≠ 1) (ha2 : 2 * a - 1 ≠ 0) : phiB0 a x + psiB2 a z - cost (kB a) x z = (x + z - 1) ^ 2 * (3 * a * (1 - a) + 2 * (a - x) + (3 * a + 1) * (z - (1 - a))) / (3 * (1 - a))

theorem Papers.Rockel2026ExactBlest.slackB10 (a x z : ℝ) (ha0 : a ≠ 0) (ha1 : a ≠ 1) : phiB1 a x + psiB0 a z - cost (kB a) x z = (x - 2 * a * z - a) ^ 2 * ((2 * a - 1) * (1 - x) + (1 + a) * (1 - a - 2 * a * z)) / (6 * a * (1 - a))

theorem Papers.Rockel2026ExactBlest.slackB11 (a x z : ℝ) (ha0 : a ≠ 0) (ha1 : a ≠ 1) (ha2 : 2 * a - 1 ≠ 0) : phiB1 a x + psiB1 a z - cost (kB a) x z = (x * (2 * a - 1) + 2 * a * z - a) ^ 2 * ((2 * a - 1) * (1 - x) + (3 * a - 1) * (2 * a * z - (1 - a))) / (6 * a * (1 - a) * (2 * a - 1) ^ 2)

theorem Papers.Rockel2026ExactBlest.slackB12 (a x z : ℝ) (ha0 : a ≠ 0) (ha1 : a ≠ 1) (ha2 : 2 * a - 1 ≠ 0) : phiB1 a x + psiB2 a z - cost (kB a) x z = (z - (1 - a)) ^ 2 * (3 * a * (1 - a) + (3 * a + 1) * (z - (1 - a))) / (3 * (1 - a)) + ((2 * a * z - (x - a)) * (2 * a * (z - (1 - a))) * (x - a) + (2 * a * (z - (1 - a)) + (2 * a * z - (x - a)) * (2 * a - 1)) * (x - a) ^ 2 / 2 + (2 * a - 1) * (x - a) ^ 3 / 6) / (2 * a * (1 - a))

theorem Papers.Rockel2026ExactBlest.dualB (a x z : ℝ) (ha0 : 1 / 2 < a) (ha1 : a < 1) (hx : x ∈ Set.Icc 0 1) (hz : z ∈ Set.Icc 0 1) : cost (kB a) x z ≤ phiB a x + psiB a z

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

theorem Papers.Rockel2026ExactBlest.integral_unit_piecewise (f g : ℝ → ℝ) (hf : Continuous f) (hg : Continuous g) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : (∫ (u : ↑unitInterval), if ↑u ≤ t then f ↑u else g ↑u) = (∫ (x : ℝ) in 0..t, f x) + ∫ (x : ℝ) in t..1, g x

theorem Papers.Rockel2026ExactBlest.integral_phiA_quarter : ∫ (u : ↑unitInterval), phiA (1 / 4) ↑u = 115 / 1536

theorem Papers.Rockel2026ExactBlest.integral_psiA_quarter : ∫ (u : ↑unitInterval), psiA (1 / 4) ↑u = -61 / 1536

theorem Papers.Rockel2026ExactBlest.integrable_phiA (C : ProbabilityTheory.Copula 2) (w : ℝ) (i : Fin 2) : MeasureTheory.Integrable (fun (x : Fin 2 → ↑unitInterval) => phiA w ↑(x i)) C.toMeasure

theorem Papers.Rockel2026ExactBlest.integrable_psiA (C : ProbabilityTheory.Copula 2) (w : ℝ) (i : Fin 2) : MeasureTheory.Integrable (fun (x : Fin 2 → ↑unitInterval) => psiA w ↑(x i)) C.toMeasure

theorem Papers.Rockel2026ExactBlest.measurable_phiA (w : ℝ) : Measurable fun (u : ↑unitInterval) => phiA w ↑u

theorem Papers.Rockel2026ExactBlest.measurable_psiA (w : ℝ) : Measurable fun (u : ↑unitInterval) => psiA w ↑u

theorem Papers.Rockel2026ExactBlest.transport_asymmetry_upper (C : ProbabilityTheory.Copula 2) : ∫ (x : Fin 2 → ↑unitInterval), cost 1 ↑(x 0) ↑(x 1) ∂C.toMeasure ≤ 9 / 256

theorem Papers.Rockel2026ExactBlest.support_moment_survival (C : ProbabilityTheory.Copula 2) (k : ℝ) : (1 + k) * Rockel2026XiBlest.blestNu C - 2 * k * eta C = 12 * ∫ (y : Fin 2 → ↑unitInterval), cost k ↑(y 0) ↑(y 1) ∂C.survivalCopula.toMeasure - 2 * (1 - k)

theorem Papers.Rockel2026ExactBlest.nu_eta_upper (C : ProbabilityTheory.Copula 2) : Rockel2026XiBlest.blestNu C - eta C ≤ 27 / 128

The universal inequality, for the original CDF coefficient, not just its boundary formula. Attainment and uniqueness are separate obligations; see COVERAGE.md.

theorem Papers.Rockel2026ExactBlest.nu_eta_bound (C : ProbabilityTheory.Copula 2) : |Rockel2026XiBlest.blestNu C - eta C| ≤ 27 / 128

theorem Papers.Rockel2026ExactBlest.nu_transpose_bound (C : ProbabilityTheory.Copula 2) : |Rockel2026XiBlest.blestNu C - Rockel2026XiBlest.blestNu C.transpose| ≤ 27 / 64

theorem Papers.Rockel2026ExactBlest.rho_eta_bound (C : ProbabilityTheory.Copula 2) : |C.spearmanRho - eta C| ≤ 27 / 128

noncomputable def Papers.Rockel2026ExactBlest.rhoPhi (x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.rhoPhi x = 4 / 3 * |x - 1 / 2| ^ 3

noncomputable def Papers.Rockel2026ExactBlest.rhoPsi (z : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.rhoPsi z = z ^ 3 / 12 - z / 4

theorem Papers.Rockel2026ExactBlest.rho_slack (x z : ℝ) : rhoPhi x + rhoPsi z - (x ^ 2 - x) * z = (z - 2 * |x - 1 / 2|) ^ 2 * (z + 4 * |x - 1 / 2|) / 12

theorem Papers.Rockel2026ExactBlest.rho_dual (x z : ℝ) (hz : 0 ≤ z) : (x ^ 2 - x) * z ≤ rhoPhi x + rhoPsi z

theorem Papers.Rockel2026ExactBlest.integral_rhoPhi : ∫ (u : ↑unitInterval), rhoPhi ↑u = 1 / 24

theorem Papers.Rockel2026ExactBlest.integral_rhoPsi : ∫ (u : ↑unitInterval), rhoPsi ↑u = -5 / 48

theorem Papers.Rockel2026ExactBlest.transport_rho_upper (C : ProbabilityTheory.Copula 2) : ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) ^ 2 - ↑(x 0)) * ↑(x 1) ∂C.toMeasure ≤ -1 / 16

theorem Papers.Rockel2026ExactBlest.nu_rho_moment (C : ProbabilityTheory.Copula 2) : Rockel2026XiBlest.blestNu C - C.spearmanRho = 12 * ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) ^ 2 - ↑(x 0)) * ↑(x 1) ∂C.survivalCopula.toMeasure + 1

theorem Papers.Rockel2026ExactBlest.nu_rho_upper (C : ProbabilityTheory.Copula 2) : Rockel2026XiBlest.blestNu C - C.spearmanRho ≤ 1 / 4

theorem Papers.Rockel2026ExactBlest.nu_rho_bound (C : ProbabilityTheory.Copula 2) : |Rockel2026XiBlest.blestNu C - C.spearmanRho| ≤ 1 / 4

noncomputable def Papers.Rockel2026ExactBlest.betaUpper (b : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.betaUpper b = 1 - 3 / 16 * (1 - b) ^ 3

noncomputable def Papers.Rockel2026ExactBlest.betaLower (b : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.betaLower b = -1 + 3 / 16 * (1 + b) ^ 3

theorem Papers.Rockel2026ExactBlest.beta_width (b : ℝ) : betaUpper b - betaLower b = (13 - 9 * b ^ 2) / 8

theorem Papers.Rockel2026ExactBlest.beta_scalar_bound (b n : ℝ) (hb : b ∈ Set.Icc (-1) 1) (hn : n ∈ Set.Icc (betaLower b) (betaUpper b)) : |n - b| ≤ 8 / 9

Scalar consequence of the cubic boundaries; this is not the copula region theorem.

theorem Papers.Rockel2026ExactBlest.graph_gap_max (w : ℝ) (hw : w ∈ Set.Icc 0 1) : 2 * w * (1 - w) ^ 3 ≤ 27 / 128

theorem Papers.Rockel2026ExactBlest.graph_gap_max_iff (w : ℝ) (hw : w ∈ Set.Icc 0 1) : 2 * w * (1 - w) ^ 3 = 27 / 128 ↔ w = 1 / 4

theorem Papers.Rockel2026ExactBlest.integral_unit_poly3 (A B D E : ℝ) : ∫ (u : ↑unitInterval), A * ↑u ^ 3 + B * ↑u ^ 2 + D * ↑u + E = A / 4 + B / 3 + D / 2 + E

noncomputable def Papers.Rockel2026ExactBlest.familyA (w : ↑unitInterval) : ProbabilityTheory.Copula 2

The paper's A_w in original coordinates, constructed as an actual library copula. Its reflected-coordinate coupling is supported on z=1-x below w and z=x-w above w.

Equations

• Papers.Rockel2026ExactBlest.familyA w = ((ProbabilityTheory.Copula.comonotonic 2).ordinalSum ProbabilityTheory.Copula.countermonotonic w).reflect {0}

theorem Papers.Rockel2026ExactBlest.nu_familyA (w : ↑unitInterval) : Rockel2026XiBlest.blestNu (familyA w) = 2 * (1 + ↑w) * (1 - ↑w) ^ 3 - 1

theorem Papers.Rockel2026ExactBlest.nu_transpose_familyA (w : ↑unitInterval) : Rockel2026XiBlest.blestNu (familyA w).transpose = 2 * (1 - ↑w) ^ 4 - 1

theorem Papers.Rockel2026ExactBlest.eta_familyA (w : ↑unitInterval) : eta (familyA w) = 2 * (1 - ↑w) ^ 3 - 1

noncomputable def Papers.Rockel2026ExactBlest.quarter : ↑unitInterval

Equations

• Papers.Rockel2026ExactBlest.quarter = ⟨1 / 4, Papers.Rockel2026ExactBlest.quarter._proof_1⟩

theorem Papers.Rockel2026ExactBlest.quarter_values : eta (familyA quarter) = -5 / 32 ∧ Rockel2026XiBlest.blestNu (familyA quarter) = 7 / 128

theorem Papers.Rockel2026ExactBlest.asymmetry_attained : ∃ (C : ProbabilityTheory.Copula 2), Rockel2026XiBlest.blestNu C - eta C = 27 / 128

theorem Papers.Rockel2026ExactBlest.asymmetry_lower_attained : ∃ (C : ProbabilityTheory.Copula 2), Rockel2026XiBlest.blestNu C - eta C = -27 / 128

theorem Papers.Rockel2026ExactBlest.transposition_attained : ∃ (C : ProbabilityTheory.Copula 2), |Rockel2026XiBlest.blestNu C - Rockel2026XiBlest.blestNu C.transpose| = 27 / 64

theorem Papers.Rockel2026ExactBlest.rho_eta_attained : ∃ (C : ProbabilityTheory.Copula 2), C.spearmanRho - eta C = 27 / 128