Papers.Rockel2026ExactBlest.ExactBlestRegions

← Mathematical handbook

Displayed exact-region formulas from exact-blest-regions.tex. Copula uniqueness and the standalone rearrangement equality case remain separate.

source

noncomputable def Papers.Rockel2026ExactBlest.graphGap (e : ℝ) :

ℝ

Equations

Papers.Rockel2026ExactBlest.graphGap e = 1 + e - 2 ^ (-1 / 3) * (1 + e) ^ (4 / 3)

Instances For

source

theorem Papers.Rockel2026ExactBlest.graphGap_value (w : ↑unitInterval) :

graphGap (eta (familyA w)) = Rockel2026XiBlest.blestNu (familyA w) - eta (familyA w)

source

theorem Papers.Rockel2026ExactBlest.graph_eta_range (w : ↑unitInterval) (hw : ↑w ≤ 1 / 2) :

eta (familyA w) ∈ Set.Icc (-3 / 4) 1

source

theorem Papers.Rockel2026ExactBlest.etaB_range (a : ↑unitInterval) (ha : 1 / 2 ≤ ↑a) :

etaB ↑a ∈ Set.Icc (-1) (-3 / 4)

source

noncomputable def Papers.Rockel2026ExactBlest.randomEtaParameter (e : ℝ) :

↑unitInterval

Equations

Papers.Rockel2026ExactBlest.randomEtaParameter e = if he : e ∈ Set.Icc (-1) (-3 / 4) then Exists.choose ⋯ else 0

Instances For

source

theorem Papers.Rockel2026ExactBlest.randomEtaParameter_value (a : ↑unitInterval) (ha : 1 / 2 ≤ ↑a) :

randomEtaParameter (etaB ↑a) = a

source

noncomputable def Papers.Rockel2026ExactBlest.etaGap (e : ℝ) :

ℝ

The paper's Upsilon: graph formula above -3/4, inverse-parameter formula below it.

Equations

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

Instances For

source

theorem Papers.Rockel2026ExactBlest.etaGap_graph (w : ↑unitInterval) (hw : ↑w ≤ 1 / 2) :

etaGap (eta (familyA w)) = Rockel2026XiBlest.blestNu (familyA w) - eta (familyA w)

source

theorem Papers.Rockel2026ExactBlest.etaGap_randomized (a : ↑unitInterval) (ha : 1 / 2 < ↑a) :

etaGap (etaB ↑a) = nuB ↑a - etaB ↑a

source

theorem Papers.Rockel2026ExactBlest.etaGap_randomized_formula (a : ↑unitInterval) (ha : 1 / 2 < ↑a) :

etaGap (etaB ↑a) = (1 - ↑a) ^ 3 * (6 * ↑a ^ 2 + 3 * ↑a - 1) / (8 * ↑a ^ 2)

source

theorem Papers.Rockel2026ExactBlest.etaGap_bottom :

etaGap (-1) = 0

source

theorem Papers.Rockel2026ExactBlest.eta_fibre_displayed (e n : ℝ) :

(∃ (C : ProbabilityTheory.Copula 2), eta C = e ∧ Rockel2026XiBlest.blestNu C = n) ↔ e ∈ Set.Icc (-1) 1 ∧ |n - e| ≤ etaGap e

The full fibre statement with the paper's displayed Upsilon formulas.

source

theorem Papers.Rockel2026ExactBlest.eta_nu_region :

(Set.range fun (C : ProbabilityTheory.Copula 2) => (eta C, Rockel2026XiBlest.blestNu C)) = {p : ℝ × ℝ | p.1 ∈ Set.Icc (-1) 1 ∧ |p.2 - p.1| ≤ etaGap p.1}