Documentation

Papers.Rockel2026ExactBlest.ExactBlestTransposeRegion

← Mathematical handbook

The exact region of `(ν(C), ν(Cᵀ))` #

The corollary on Blest's coefficient and its transpose in exact-blest-regions.tex: both displayed descriptions of the region (through Υ and through Λ), the two boundary curves, unique maximizers and minimizers in every fibre, their identification with the extremal families, the closed-form bound stated in the introduction, and continuity of Υ.

Elementary properties of `Υ` #

theorem Papers.Rockel2026ExactBlest.etaGap_nonneg (e : ℝ) (he : e ∈ Set.Icc (-1) 1) :

theorem Papers.Rockel2026ExactBlest.upper_curve_mem (e : ℝ) (he : e ∈ Set.Icc (-1) 1) :

e + etaGap e ∈ Set.Icc (-1) 1

theorem Papers.Rockel2026ExactBlest.lower_curve_mem (e : ℝ) (he : e ∈ Set.Icc (-1) 1) :

e - etaGap e ∈ Set.Icc (-1) 1

theorem Papers.Rockel2026ExactBlest.etaGap_top :

theorem Papers.Rockel2026ExactBlest.etaGap_mem (e : ℝ) (he : e ∈ Set.Icc (-1) 1) :

etaGap e ∈ Set.Icc 0 (27 / 128)

Υ maps [-1,1] into [0,27/128], as stated where Υ is defined.

The boundary function `Λ` along the boundary of the `(η,ν)`-region #

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

Lambda (transposeParam ↑a) = nuB ↑a

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

Lambda (Rockel2026XiBlest.blestNu (familyA w).transpose) = Rockel2026XiBlest.blestNu (familyA w)

theorem Papers.Rockel2026ExactBlest.Lambda_curve (e : ℝ) (he : e ∈ Set.Icc (-1) 1) :

Lambda (e - etaGap e) = e + etaGap e

L maps the lower boundary curve of the (η,ν)-region onto the graph of Λ.

theorem Papers.Rockel2026ExactBlest.lowerCurve_strictMonoOn :

StrictMonoOn (fun (e : ℝ) => e - etaGap e) (Set.Icc (-1) 1)

Both coordinates of the boundary curves are strictly increasing in e.

theorem Papers.Rockel2026ExactBlest.upperCurve_strictMonoOn :

StrictMonoOn (fun (e : ℝ) => e + etaGap e) (Set.Icc (-1) 1)

The inverse `Λ⁻¹` #

noncomputable def Papers.Rockel2026ExactBlest.LambdaInv :

The inverse of Λ on [-1,1].

Equations

Papers.Rockel2026ExactBlest.LambdaInv = Function.invFunOn Papers.Rockel2026ExactBlest.Lambda (Set.Icc (-1) 1)

Instances For

theorem Papers.Rockel2026ExactBlest.LambdaInv_mem (n : ℝ) (hn : n ∈ Set.Icc (-1) 1) :

LambdaInv n ∈ Set.Icc (-1) 1

theorem Papers.Rockel2026ExactBlest.Lambda_LambdaInv (n : ℝ) (hn : n ∈ Set.Icc (-1) 1) :

Lambda (LambdaInv n) = n

theorem Papers.Rockel2026ExactBlest.LambdaInv_Lambda (m : ℝ) (hm : m ∈ Set.Icc (-1) 1) :

LambdaInv (Lambda m) = m

theorem Papers.Rockel2026ExactBlest.LambdaInv_le_iff (n m : ℝ) (hn : n ∈ Set.Icc (-1) 1) (hm : m ∈ Set.Icc (-1) 1) :

LambdaInv n ≤ m ↔ n ≤ Lambda m

theorem Papers.Rockel2026ExactBlest.LambdaInv_bijOn :

Set.BijOn LambdaInv (Set.Icc (-1) 1) (Set.Icc (-1) 1)

theorem Papers.Rockel2026ExactBlest.LambdaInv_strictMonoOn :

StrictMonoOn LambdaInv (Set.Icc (-1) 1)

theorem Papers.Rockel2026ExactBlest.LambdaInv_le_self (n : ℝ) (hn : n ∈ Set.Icc (-1) 1) :

LambdaInv n ≤ n

theorem Papers.Rockel2026ExactBlest.LambdaInv_neg_one :

LambdaInv (-1) = -1

The two descriptions of the region #

theorem Papers.Rockel2026ExactBlest.nu_transpose_fibre_gap (n m : ℝ) :

(∃ (C : ProbabilityTheory.Copula 2), Rockel2026XiBlest.blestNu C = n ∧ Rockel2026XiBlest.blestNu C.transpose = m) ↔ n ∈ Set.Icc (-1) 1 ∧ m ∈ Set.Icc (-1) 1 ∧ |n - m| ≤ 2 * etaGap ((n + m) / 2)

The first displayed description: |n - m| ≤ 2 Υ((n+m)/2).

theorem Papers.Rockel2026ExactBlest.nu_transpose_region_gap :

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

theorem Papers.Rockel2026ExactBlest.gap_band_iff (n m : ℝ) (hn : n ∈ Set.Icc (-1) 1) (hm : m ∈ Set.Icc (-1) 1) :

|n - m| ≤ 2 * etaGap ((n + m) / 2) ↔ LambdaInv n ≤ m ∧ m ≤ Lambda n

The band between the graphs of Λ⁻¹ and Λ is the band |n - m| ≤ 2 Υ((n+m)/2).

theorem Papers.Rockel2026ExactBlest.nu_transpose_fibre (n m : ℝ) :

(∃ (C : ProbabilityTheory.Copula 2), Rockel2026XiBlest.blestNu C = n ∧ Rockel2026XiBlest.blestNu C.transpose = m) ↔ n ∈ Set.Icc (-1) 1 ∧ m ∈ Set.Icc (-1) 1 ∧ LambdaInv n ≤ m ∧ m ≤ Lambda n

The second displayed description: Λ⁻¹(n) ≤ m ≤ Λ(n).

theorem Papers.Rockel2026ExactBlest.nu_transpose_region :

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

theorem Papers.Rockel2026ExactBlest.nu_transpose_fibre_eq (n : ℝ) (hn : n ∈ Set.Icc (-1) 1) :

{m : ℝ | ∃ (C : ProbabilityTheory.Copula 2), Rockel2026XiBlest.blestNu C = n ∧ Rockel2026XiBlest.blestNu C.transpose = m} = Set.Icc (LambdaInv n) (Lambda n)

The fibre above n is the interval [Λ⁻¹(n), Λ(n)].

theorem Papers.Rockel2026ExactBlest.eta_nu_region_linear_image :

(Set.range fun (C : ProbabilityTheory.Copula 2) => (eta C, Rockel2026XiBlest.blestNu C)) = (fun (p : ℝ × ℝ) => ((p.1 + p.2) / 2, p.1)) '' Set.range fun (C : ProbabilityTheory.Copula 2) => (Rockel2026XiBlest.blestNu C, Rockel2026XiBlest.blestNu C.transpose)

The (η,ν)-region is the image of the (ν,νᵀ)-region under (n,m) ↦ ((n+m)/2, n).

Boundary curves #

theorem Papers.Rockel2026ExactBlest.nu_transpose_max_lower (C : ProbabilityTheory.Copula 2) (hC : Rockel2026XiBlest.blestNu C.transpose = Lambda (Rockel2026XiBlest.blestNu C)) :

Rockel2026XiBlest.blestNu C = eta C - etaGap (eta C)

theorem Papers.Rockel2026ExactBlest.nu_transpose_min_upper (C : ProbabilityTheory.Copula 2) (hC : Rockel2026XiBlest.blestNu C.transpose = LambdaInv (Rockel2026XiBlest.blestNu C)) :

Rockel2026XiBlest.blestNu C = eta C + etaGap (eta C)

theorem Papers.Rockel2026ExactBlest.upper_boundary_curve :

(fun (e : ℝ) => (e - etaGap e, e + etaGap e)) '' Set.Icc (-1) 1 = {p : ℝ × ℝ | p.1 ∈ Set.Icc (-1) 1 ∧ p.2 = Lambda p.1}

The image of the lower boundary curve under L is the graph of Λ.

theorem Papers.Rockel2026ExactBlest.lower_boundary_curve :

(fun (e : ℝ) => (e + etaGap e, e - etaGap e)) '' Set.Icc (-1) 1 = {p : ℝ × ℝ | p.1 ∈ Set.Icc (-1) 1 ∧ p.2 = LambdaInv p.1}

The image of the upper boundary curve under L is the graph of Λ⁻¹.

theorem Papers.Rockel2026ExactBlest.lowerCurve_image :

(fun (e : ℝ) => e - etaGap e) '' Set.Icc (-1) 1 = Set.Icc (-1) 1

Maximum and minimum of `ν(Cᵀ)` at fixed `ν(C)` #

theorem Papers.Rockel2026ExactBlest.nu_transpose_isGreatest (n : ℝ) (hn : n ∈ Set.Icc (-1) 1) :

IsGreatest {m : ℝ | ∃ (C : ProbabilityTheory.Copula 2), Rockel2026XiBlest.blestNu C = n ∧ Rockel2026XiBlest.blestNu C.transpose = m} (Lambda n)

theorem Papers.Rockel2026ExactBlest.nu_transpose_isLeast (n : ℝ) (hn : n ∈ Set.Icc (-1) 1) :

IsLeast {m : ℝ | ∃ (C : ProbabilityTheory.Copula 2), Rockel2026XiBlest.blestNu C = n ∧ Rockel2026XiBlest.blestNu C.transpose = m} (LambdaInv n)

theorem Papers.Rockel2026ExactBlest.nu_transpose_max_exists_unique (n : ℝ) (hn : n ∈ Set.Icc (-1) 1) :

∃! C : ProbabilityTheory.Copula 2, Rockel2026XiBlest.blestNu C = n ∧ Rockel2026XiBlest.blestNu C.transpose = Lambda n

theorem Papers.Rockel2026ExactBlest.nu_transpose_min_exists_unique (n : ℝ) (hn : n ∈ Set.Icc (-1) 1) :

∃! C : ProbabilityTheory.Copula 2, Rockel2026XiBlest.blestNu C = n ∧ Rockel2026XiBlest.blestNu C.transpose = LambdaInv n

theorem Papers.Rockel2026ExactBlest.upper_extremizer_cases (C : ProbabilityTheory.Copula 2) (hC : Rockel2026XiBlest.blestNu C = eta C + etaGap (eta C)) :

(∃ (w : ↑unitInterval), ↑w ≤ 1 / 2 ∧ C = familyA w) ∨ (∃ (a : ↑unitInterval) (ha : 1 / 2 < ↑a), ↑a < 1 ∧ C = familyB a ⋯) ∨ C = ProbabilityTheory.Copula.countermonotonic

Every upper extremizer of the (η,ν)-region is A_w, B_a, or W.

theorem Papers.Rockel2026ExactBlest.nu_transpose_max_transpose_upper (C : ProbabilityTheory.Copula 2) (hC : Rockel2026XiBlest.blestNu C.transpose = Lambda (Rockel2026XiBlest.blestNu C)) :

Rockel2026XiBlest.blestNu C.transpose = eta C.transpose + etaGap (eta C.transpose)

The maximizer is the transpose of an upper extremizer of the (η,ν)-region.

theorem Papers.Rockel2026ExactBlest.nu_transpose_extremizer_neg_one (C : ProbabilityTheory.Copula 2) (hC : Rockel2026XiBlest.blestNu C = -1) :

C = ProbabilityTheory.Copula.countermonotonic

For n = -1, the only copula in the fibre is W.

theorem Papers.Rockel2026ExactBlest.nu_transpose_neg_one_values :

Lambda (-1) = -1 ∧ LambdaInv (-1) = -1 ∧ Rockel2026XiBlest.blestNu ProbabilityTheory.Copula.countermonotonic.transpose = -1

theorem Papers.Rockel2026ExactBlest.nu_transpose_max_familyA (n : ℝ) (hn : n ∈ Set.Icc (-7 / 8) 1) :

∃ (w : ↑unitInterval), ↑w = 1 - ((1 + n) / 2) ^ (1 / 4) ∧ ↑w ≤ 1 / 2 ∧ Rockel2026XiBlest.blestNu (familyA w).transpose = n ∧ Rockel2026XiBlest.blestNu (familyA w) = Lambda n ∧ ∀ (C : ProbabilityTheory.Copula 2), Rockel2026XiBlest.blestNu C = n → Rockel2026XiBlest.blestNu C.transpose = Lambda n → C = (familyA w).transpose

For n ∈ [-7/8,1], the maximizer is A_wᵀ with w = 1 - ((1+n)/2)^(1/4).

theorem Papers.Rockel2026ExactBlest.nu_transpose_max_familyB (n : ℝ) (hn : n ∈ Set.Ioo (-1) (-7 / 8)) :

∃ (a : ↑unitInterval) (ha : 1 / 2 < ↑a), ↑a < 1 ∧ transposeParam ↑a = n ∧ Rockel2026XiBlest.blestNu (familyB a ⋯).transpose = n ∧ Rockel2026XiBlest.blestNu (familyB a ⋯) = Lambda n ∧ ∀ (C : ProbabilityTheory.Copula 2), Rockel2026XiBlest.blestNu C = n → Rockel2026XiBlest.blestNu C.transpose = Lambda n → C = (familyB a ⋯).transpose

For n ∈ (-1,-7/8), the maximizer is B_aᵀ with n_a = n.

theorem Papers.Rockel2026ExactBlest.nu_transpose_min_cases (C : ProbabilityTheory.Copula 2) (hn : -1 < Rockel2026XiBlest.blestNu C) (hC : Rockel2026XiBlest.blestNu C.transpose = LambdaInv (Rockel2026XiBlest.blestNu C)) :

(∃ (w : ↑unitInterval), ↑w ≤ 1 / 2 ∧ C = familyA w) ∨ ∃ (a : ↑unitInterval) (ha : 1 / 2 < ↑a), ↑a < 1 ∧ C = familyB a ⋯

For n ∈ (-1,1], the minimizer is an upper extremizer A_w or B_a itself.

theorem Papers.Rockel2026ExactBlest.nu_transpose_max_cases (C : ProbabilityTheory.Copula 2) (hn : -1 < Rockel2026XiBlest.blestNu C) (hC : Rockel2026XiBlest.blestNu C.transpose = Lambda (Rockel2026XiBlest.blestNu C)) :

(∃ (w : ↑unitInterval), ↑w ≤ 1 / 2 ∧ C = (familyA w).transpose) ∨ ∃ (a : ↑unitInterval) (ha : 1 / 2 < ↑a), ↑a < 1 ∧ C = (familyB a ⋯).transpose

For n ∈ (-1,1], the maximizer is the transpose of A_w or B_a.

The closed-form bound stated in the introduction #

theorem Papers.Rockel2026ExactBlest.nu_transpose_closed_bound (C : ProbabilityTheory.Copula 2) (hn : -7 / 8 ≤ Rockel2026XiBlest.blestNu C) :

Rockel2026XiBlest.blestNu C.transpose ≤ 4 * ((1 + Rockel2026XiBlest.blestNu C) / 2) ^ (3 / 4) - Rockel2026XiBlest.blestNu C - 2

theorem Papers.Rockel2026ExactBlest.nu_transpose_closed_bound_unique (n : ℝ) (hn : n ∈ Set.Icc (-7 / 8) 1) :

∃! C : ProbabilityTheory.Copula 2, Rockel2026XiBlest.blestNu C = n ∧ Rockel2026XiBlest.blestNu C.transpose = 4 * ((1 + n) / 2) ^ (3 / 4) - n - 2

Continuity of `Υ` #

theorem Papers.Rockel2026ExactBlest.etaGap_le_one_add (e : ℝ) (he : e ∈ Set.Icc (-1) 1) :

etaGap e ≤ 1 + e

theorem Papers.Rockel2026ExactBlest.etaGap_le_one_sub (e : ℝ) (he : e ∈ Set.Icc (-1) 1) :

etaGap e ≤ 1 - e

theorem Papers.Rockel2026ExactBlest.lowerCurve_continuousAt (e : ℝ) (he : e ∈ Set.Ioo (-1) 1) :

ContinuousAt (fun (e : ℝ) => e - etaGap e) e

theorem Papers.Rockel2026ExactBlest.etaGap_continuousAt (e : ℝ) (he : e ∈ Set.Ioo (-1) 1) :

ContinuousAt etaGap e

theorem Papers.Rockel2026ExactBlest.etaGap_continuousOn :

ContinuousOn etaGap (Set.Icc (-1) 1)

Υ is continuous on [-1,1], in particular at the regime change -3/4.

theorem Papers.Rockel2026ExactBlest.etaGap_continuousAt_join :

ContinuousAt etaGap (-3 / 4)