← Mathematical handbook

The graph-regime fibres of the (eta,nu) region in exact-blest-regions.tex.

theorem Papers.Rockel2026ExactBlest.integral_potentialsA (w : ↑unitInterval) (hw : ↑w ≤ 1 / 2) : (∫ (u : ↑unitInterval), phiA ↑w ↑u) + ∫ (u : ↑unitInterval), psiA ↑w ↑u = ((1 + kA ↑w) * Rockel2026XiBlest.blestNu (familyA w) - 2 * kA ↑w * eta (familyA w) + 2 * (1 - kA ↑w)) / 12

theorem Papers.Rockel2026ExactBlest.graph_support (C : ProbabilityTheory.Copula 2) (w : ↑unitInterval) (hw : ↑w ≤ 1 / 2) : (1 + kA ↑w) * Rockel2026XiBlest.blestNu C - 2 * kA ↑w * eta C ≤ (1 + kA ↑w) * Rockel2026XiBlest.blestNu (familyA w) - 2 * kA ↑w * eta (familyA w)

theorem Papers.Rockel2026ExactBlest.nu_le_familyA (C : ProbabilityTheory.Copula 2) (w : ↑unitInterval) (hw : ↑w ≤ 1 / 2) (he : eta C = eta (familyA w)) : Rockel2026XiBlest.blestNu C ≤ Rockel2026XiBlest.blestNu (familyA w)

theorem Papers.Rockel2026ExactBlest.graph_fibre (w : ↑unitInterval) (hw : ↑w ≤ 1 / 2) (n : ℝ) : (∃ (C : ProbabilityTheory.Copula 2), eta C = eta (familyA w) ∧ Rockel2026XiBlest.blestNu C = n) ↔ n ∈ Set.Icc (2 * eta (familyA w) - Rockel2026XiBlest.blestNu (familyA w)) (Rockel2026XiBlest.blestNu (familyA w))

Exact fibres for the graph regime, in the paper's parameter w; uniqueness is not asserted.

theorem Papers.Rockel2026ExactBlest.graph_parameter_strictAnti : StrictAntiOn (fun (w : ℝ) => 2 * (1 - w) ^ 3 - 1) (Set.Icc 0 (1 / 2))

theorem Papers.Rockel2026ExactBlest.graph_parameter_exists_unique (e : ℝ) (he : e ∈ Set.Icc (-3 / 4) 1) : ∃! w : ↑unitInterval, ↑w ≤ 1 / 2 ∧ eta (familyA w) = e

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