← Mathematical handbook

Copula construction and exact fibres for the two-branch eta regime. Only claims from exact-blest-regions.tex are formalized here.

def Papers.Rockel2026ExactBlest.stripLower (a : ↑unitInterval) (x : Fin 2 → ↑unitInterval) : Fin 2 → ↑unitInterval

Put the second coordinate in one of two adjacent horizontal strips.

Equations

• Papers.Rockel2026ExactBlest.stripLower a x = ![x 0, ProbabilityTheory.Copula.OrdinalSum.lowerEmbed a (x 1)]

def Papers.Rockel2026ExactBlest.stripUpper (a : ↑unitInterval) (x : Fin 2 → ↑unitInterval) : Fin 2 → ↑unitInterval

Equations

• Papers.Rockel2026ExactBlest.stripUpper a x = ![x 0, ProbabilityTheory.Copula.OrdinalSum.upperEmbed a (x 1)]

theorem Papers.Rockel2026ExactBlest.continuous_stripLower (a : ↑unitInterval) : Continuous (stripLower a)

theorem Papers.Rockel2026ExactBlest.continuous_stripUpper (a : ↑unitInterval) : Continuous (stripUpper a)

theorem Papers.Rockel2026ExactBlest.map_embed_eval (C : ProbabilityTheory.Copula 2) (i : Fin 2) (f : ↑unitInterval → ↑unitInterval) (hf : Measurable f) : MeasureTheory.Measure.map (fun (x : Fin 2 → ↑unitInterval) => f (x i)) C.toMeasure = MeasureTheory.Measure.map f MeasureTheory.volume

theorem Papers.Rockel2026ExactBlest.uniform_split (a : ↑unitInterval) : ENNReal.ofReal ↑a • MeasureTheory.Measure.map (ProbabilityTheory.Copula.OrdinalSum.lowerEmbed a) MeasureTheory.volume + ENNReal.ofReal (1 - ↑a) • MeasureTheory.Measure.map (ProbabilityTheory.Copula.OrdinalSum.upperEmbed a) MeasureTheory.volume = MeasureTheory.volume

noncomputable def Papers.Rockel2026ExactBlest.stripMeasure (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) : MeasureTheory.Measure (Fin 2 → ↑unitInterval)

Equations

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

theorem Papers.Rockel2026ExactBlest.stripMeasure_probability (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) : MeasureTheory.IsProbabilityMeasure (stripMeasure C D a)

theorem Papers.Rockel2026ExactBlest.stripMeasure_marginal (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) (i : Fin 2) : MeasureTheory.Measure.map (fun (x : Fin 2 → ↑unitInterval) => x i) (stripMeasure C D a) = MeasureTheory.volume

noncomputable def Papers.Rockel2026ExactBlest.stripCopula (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) : ProbabilityTheory.Copula 2

Horizontal gluing, with both marginals proved uniform.

Equations

• Papers.Rockel2026ExactBlest.stripCopula C D a = { measure := ⟨Papers.Rockel2026ExactBlest.stripMeasure C D a, ⋯⟩, marginal_eq := ⋯ }

theorem Papers.Rockel2026ExactBlest.integral_stripCopula (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂(stripCopula C D a).toMeasure = ↑a * ∫ (x : Fin 2 → ↑unitInterval), f (stripLower a x) ∂C.toMeasure + (1 - ↑a) * ∫ (x : Fin 2 → ↑unitInterval), f (stripUpper a x) ∂D.toMeasure

noncomputable def Papers.Rockel2026ExactBlest.skewTent (p : ↑unitInterval) : ProbabilityTheory.Copula 2

Equations

• Papers.Rockel2026ExactBlest.skewTent p = Papers.Rockel2026ExactBlest.stripCopula (ProbabilityTheory.Copula.comonotonic 2) ProbabilityTheory.Copula.countermonotonic p

theorem Papers.Rockel2026ExactBlest.nu_skewTent (p : ↑unitInterval) : Rockel2026XiBlest.blestNu (skewTent p) = 2 * ↑p - 1

theorem Papers.Rockel2026ExactBlest.nu_transpose_skewTent (p : ↑unitInterval) : Rockel2026XiBlest.blestNu (skewTent p).transpose = -↑p ^ 2 + 3 * ↑p - 1

theorem Papers.Rockel2026ExactBlest.rho_skewTent (p : ↑unitInterval) : (skewTent p).spearmanRho = 2 * ↑p - 1

noncomputable def Papers.Rockel2026ExactBlest.randomSplit (a : ↑unitInterval) (ha : 1 / 2 ≤ ↑a) : ↑unitInterval

Equations

• Papers.Rockel2026ExactBlest.randomSplit a ha = ⟨(2 * ↑a - 1) / (2 * ↑a), ⋯⟩

noncomputable def Papers.Rockel2026ExactBlest.familyB (a : ↑unitInterval) (ha : 1 / 2 ≤ ↑a) : ProbabilityTheory.Copula 2

The original-coordinate B_a, including the continuous coefficient endpoint a=1.

Equations

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

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

Equations

• Papers.Rockel2026ExactBlest.nuB a = -1 + (1 + a) * (1 - a) ^ 3 / a

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

Equations

• Papers.Rockel2026ExactBlest.etaB a = -1 + (1 - a) ^ 3 * (2 * a ^ 2 + 5 * a + 1) / (8 * a ^ 2)

theorem Papers.Rockel2026ExactBlest.nu_familyB (a : ↑unitInterval) (ha : 1 / 2 ≤ ↑a) : Rockel2026XiBlest.blestNu (familyB a ha) = nuB ↑a

theorem Papers.Rockel2026ExactBlest.transpose_comonotonic_two : (ProbabilityTheory.Copula.comonotonic 2).transpose = ProbabilityTheory.Copula.comonotonic 2

theorem Papers.Rockel2026ExactBlest.nu_transpose_familyB (a : ↑unitInterval) (ha : 1 / 2 ≤ ↑a) : Rockel2026XiBlest.blestNu (familyB a ha).transpose = 2 * etaB ↑a - nuB ↑a

theorem Papers.Rockel2026ExactBlest.eta_familyB (a : ↑unitInterval) (ha : 1 / 2 ≤ ↑a) : eta (familyB a ha) = etaB ↑a

theorem Papers.Rockel2026ExactBlest.nu_rho_upper_attained : ∃ (C : ProbabilityTheory.Copula 2), Rockel2026XiBlest.blestNu C - C.spearmanRho = 1 / 4

theorem Papers.Rockel2026ExactBlest.nu_rho_lower_attained : ∃ (C : ProbabilityTheory.Copula 2), Rockel2026XiBlest.blestNu C - C.spearmanRho = -1 / 4

noncomputable def Papers.Rockel2026ExactBlest.threePieces (c b : ℝ) (f0 f1 f2 : ℝ → ℝ) (x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.threePieces c b f0 f1 f2 x = if x ≤ c then f0 x else if x ≤ b then f1 x else f2 x

theorem Papers.Rockel2026ExactBlest.integral_threePieces (c b : ℝ) (hc : c ∈ Set.Icc 0 1) (hb : b ∈ Set.Icc 0 1) (hcb : c ≤ b) (f0 f1 f2 : ℝ → ℝ) (h0 : Continuous f0) (h1 : Continuous f1) (h2 : Continuous f2) : ∫ (u : ↑unitInterval), threePieces c b f0 f1 f2 ↑u = ((∫ (u : ↑unitInterval), f2 ↑u) + ∫ (x : ℝ) in 0..b, f1 x - f2 x) + ∫ (x : ℝ) in 0..c, f0 x - f1 x

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

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

theorem Papers.Rockel2026ExactBlest.measurable_phiB (a : ℝ) : Measurable fun (u : ↑unitInterval) => phiB a ↑u

theorem Papers.Rockel2026ExactBlest.measurable_psiB (a : ℝ) : Measurable fun (u : ↑unitInterval) => psiB a ↑u

theorem Papers.Rockel2026ExactBlest.integral_phiB (a : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) : ∫ (u : ↑unitInterval), phiB a ↑u = (2 * a ^ 5 - a ^ 4 - 8 * a ^ 3 + 2 * a ^ 2 + 2 * a - 1) / (24 * a * (a - 1))

theorem Papers.Rockel2026ExactBlest.integral_psiB (a : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) : ∫ (u : ↑unitInterval), psiB a ↑u = -a * (a ^ 3 - 6 * a + 1) / (12 * (a - 1))

theorem Papers.Rockel2026ExactBlest.integral_potentialsB (a : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) : (∫ (u : ↑unitInterval), phiB a ↑u) + ∫ (u : ↑unitInterval), psiB a ↑u = ((1 + kB a) * nuB a - 2 * kB a * etaB a + 2 * (1 - kB a)) / 12

theorem Papers.Rockel2026ExactBlest.randomized_support (C : ProbabilityTheory.Copula 2) (a : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) : (1 + kB a) * Rockel2026XiBlest.blestNu C - 2 * kB a * eta C ≤ (1 + kB a) * nuB a - 2 * kB a * etaB a

theorem Papers.Rockel2026ExactBlest.nu_le_familyB (C : ProbabilityTheory.Copula 2) (a : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) (he : eta C = etaB a) : Rockel2026XiBlest.blestNu C ≤ nuB a

theorem Papers.Rockel2026ExactBlest.randomized_fibre (a : ↑unitInterval) (ha : 1 / 2 < ↑a) (ha1 : ↑a < 1) (n : ℝ) : (∃ (C : ProbabilityTheory.Copula 2), eta C = etaB ↑a ∧ Rockel2026XiBlest.blestNu C = n) ↔ n ∈ Set.Icc (2 * etaB ↑a - nuB ↑a) (nuB ↑a)

theorem Papers.Rockel2026ExactBlest.etaB_factor (a : ℝ) (ha : a ≠ 0) : etaB a = -1 + (1 - a) ^ 3 * (2 + 5 * (1 / a) + (1 / a) ^ 2) / 8

theorem Papers.Rockel2026ExactBlest.randomized_parameter_strictAnti : StrictAntiOn etaB (Set.Icc (1 / 2) 1)

theorem Papers.Rockel2026ExactBlest.randomized_parameter_exists_unique (e : ℝ) (he : e ∈ Set.Icc (-1) (-3 / 4)) : ∃! a : ↑unitInterval, 1 / 2 ≤ ↑a ∧ etaB ↑a = e

theorem Papers.Rockel2026ExactBlest.randomized_parameter_exists_open (e : ℝ) (he : e ∈ Set.Ioo (-1) (-3 / 4)) : ∃ (a : ↑unitInterval), 1 / 2 < ↑a ∧ ↑a < 1 ∧ etaB ↑a = e

theorem Papers.Rockel2026ExactBlest.eta_bottom_fibre (n : ℝ) : (∃ (C : ProbabilityTheory.Copula 2), eta C = -1 ∧ Rockel2026XiBlest.blestNu C = n) ↔ n = -1

def Papers.Rockel2026ExactBlest.etaRegion (e n : ℝ) : Prop

An exact parameterization of the complete attainable eta/nu region.

Equations

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

theorem Papers.Rockel2026ExactBlest.eta_fibre_complete (e n : ℝ) : (∃ (C : ProbabilityTheory.Copula 2), eta C = e ∧ Rockel2026XiBlest.blestNu C = n) ↔ etaRegion e n

theorem Papers.Rockel2026ExactBlest.eta_nu_region_parametric : (Set.range fun (C : ProbabilityTheory.Copula 2) => (eta C, Rockel2026XiBlest.blestNu C)) = {p : ℝ × ℝ | etaRegion p.1 p.2}

Full set equality, in the two natural parameters; boundary uniqueness is separate.