Papers.Rockel2026ExactBlest.ExactBlestRho

← Mathematical handbook

The complete rho/Blest region of exact-blest-regions.tex in natural parameters. Supporting inequalities use explicit potentials, independently of the general rearrangement lemma. Boundary-copula uniqueness is not asserted.

source

noncomputable def Papers.Rockel2026ExactBlest.rhoParamPhi (t x : ℝ) :

ℝ

Equations

Papers.Rockel2026ExactBlest.rhoParamPhi t x = if x ≤ t then 4 / 3 * |x - t / 2| ^ 3 else 2 * x ^ 3 / 3 - t * x ^ 2 / 2

Instances For

source

noncomputable def Papers.Rockel2026ExactBlest.rhoParamPsi (t z : ℝ) :

ℝ

Equations

Papers.Rockel2026ExactBlest.rhoParamPsi t z = if z ≤ t then z ^ 3 / 12 - t ^ 2 * z / 4 else z ^ 3 / 3 - t * z ^ 2 / 2

Instances For

source

theorem Papers.Rockel2026ExactBlest.rho_param_cell00 (t x z : ℝ) (hz : 0 ≤ z) :

0 ≤ 4 / 3 * |x - t / 2| ^ 3 + (z ^ 3 / 12 - t ^ 2 * z / 4) - (x ^ 2 - t * x) * z

source

theorem Papers.Rockel2026ExactBlest.rho_param_cell01 (t x z : ℝ) (ht : 0 ≤ t) (hx : x ∈ Set.Icc 0 t) (hz : t ≤ z) :

0 ≤ 4 / 3 * |x - t / 2| ^ 3 + (z ^ 3 / 3 - t * z ^ 2 / 2) - (x ^ 2 - t * x) * z

source

theorem Papers.Rockel2026ExactBlest.rho_param_cell10 (t x z : ℝ) (ht : 0 ≤ t) (hx : t ≤ x) (hz : z ∈ Set.Icc 0 t) :

0 ≤ 2 * x ^ 3 / 3 - t * x ^ 2 / 2 + (z ^ 3 / 12 - t ^ 2 * z / 4) - (x ^ 2 - t * x) * z

source

theorem Papers.Rockel2026ExactBlest.rho_param_cell11 (t x z : ℝ) (ht : 0 ≤ t) (hx : t ≤ x) (hz : t ≤ z) :

0 ≤ 2 * x ^ 3 / 3 - t * x ^ 2 / 2 + (z ^ 3 / 3 - t * z ^ 2 / 2) - (x ^ 2 - t * x) * z

source

theorem Papers.Rockel2026ExactBlest.rho_param_dual (t x z : ℝ) (ht : 0 ≤ t) (hx : 0 ≤ x) (hz : 0 ≤ z) :

(x ^ 2 - t * x) * z ≤ rhoParamPhi t x + rhoParamPsi t z

source

noncomputable def Papers.Rockel2026ExactBlest.rhoPhiLo (t x : ℝ) :

ℝ

Equations

Papers.Rockel2026ExactBlest.rhoPhiLo t x = 4 / 3 * (t / 2 - x) ^ 3

Instances For

source

noncomputable def Papers.Rockel2026ExactBlest.rhoPhiMid (t x : ℝ) :

ℝ

Equations

Papers.Rockel2026ExactBlest.rhoPhiMid t x = 4 / 3 * (x - t / 2) ^ 3

Instances For

source

noncomputable def Papers.Rockel2026ExactBlest.rhoPhiHi (t x : ℝ) :

ℝ

Equations

Papers.Rockel2026ExactBlest.rhoPhiHi t x = 2 * x ^ 3 / 3 - t * x ^ 2 / 2

Instances For

source

theorem Papers.Rockel2026ExactBlest.rhoPhi_threePieces (t : ↑unitInterval) :

rhoParamPhi ↑t = threePieces (↑t / 2) (↑t) (rhoPhiLo ↑t) (rhoPhiMid ↑t) (rhoPhiHi ↑t)

source

theorem Papers.Rockel2026ExactBlest.integral_rhoParamPhi (t : ↑unitInterval) :

∫ (u : ↑unitInterval), rhoParamPhi ↑t ↑u = ↑t ^ 4 / 24 - ↑t / 6 + 1 / 6

source

theorem Papers.Rockel2026ExactBlest.integral_rhoParamPsi (t : ↑unitInterval) :

∫ (u : ↑unitInterval), rhoParamPsi ↑t ↑u = -↑t ^ 4 / 48 - ↑t / 6 + 1 / 12

source

theorem Papers.Rockel2026ExactBlest.integrable_rhoParamPhi (C : ProbabilityTheory.Copula 2) (t : ℝ) (i : Fin 2) :

MeasureTheory.Integrable (fun (x : Fin 2 → ↑unitInterval) => rhoParamPhi t ↑(x i)) C.toMeasure

source

theorem Papers.Rockel2026ExactBlest.integrable_rhoParamPsi (C : ProbabilityTheory.Copula 2) (t : ℝ) (i : Fin 2) :

MeasureTheory.Integrable (fun (x : Fin 2 → ↑unitInterval) => rhoParamPsi t ↑(x i)) C.toMeasure

source

theorem Papers.Rockel2026ExactBlest.measurable_rhoParamPhi (t : ℝ) :

Measurable fun (u : ↑unitInterval) => rhoParamPhi t ↑u

source

theorem Papers.Rockel2026ExactBlest.measurable_rhoParamPsi (t : ℝ) :

Measurable fun (u : ↑unitInterval) => rhoParamPsi t ↑u

source

theorem Papers.Rockel2026ExactBlest.transport_rho_param_upper (C : ProbabilityTheory.Copula 2) (t : ↑unitInterval) :

∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) ^ 2 - ↑t * ↑(x 0)) * ↑(x 1) ∂C.toMeasure ≤ ↑t ^ 4 / 48 - ↑t / 3 + 1 / 4

source

theorem Papers.Rockel2026ExactBlest.rho_support_moment (C : ProbabilityTheory.Copula 2) (t : ℝ) :

Rockel2026XiBlest.blestNu C - t * C.spearmanRho = 12 * ∫ (x : Fin 2 → ↑unitInterval), (↑(x 0) ^ 2 - t * ↑(x 0)) * ↑(x 1) ∂C.survivalCopula.toMeasure - 2 + 3 * t

source

theorem Papers.Rockel2026ExactBlest.rho_support (C : ProbabilityTheory.Copula 2) (t : ↑unitInterval) :

Rockel2026XiBlest.blestNu C - ↑t * C.spearmanRho ≤ 1 - ↑t + ↑t ^ 4 / 4

source

def Papers.Rockel2026ExactBlest.rhoPosR (t : ℝ) :

ℝ

Equations

Papers.Rockel2026ExactBlest.rhoPosR t = 1 - t ^ 3

Instances For

source

noncomputable def Papers.Rockel2026ExactBlest.rhoPosN (t : ℝ) :

ℝ

Equations

Papers.Rockel2026ExactBlest.rhoPosN t = 1 - 3 / 4 * t ^ 4

Instances For

source

noncomputable def Papers.Rockel2026ExactBlest.rhoFamily (t : ↑unitInterval) :

ProbabilityTheory.Copula 2

Equations

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

Instances For

source

theorem Papers.Rockel2026ExactBlest.rho_family_values (t : ↑unitInterval) :

(rhoFamily t).spearmanRho = rhoPosR ↑t ∧ Rockel2026XiBlest.blestNu (rhoFamily t) = rhoPosN ↑t

source

theorem Papers.Rockel2026ExactBlest.rho_positive_upper (C : ProbabilityTheory.Copula 2) (t : ↑unitInterval) (hr : C.spearmanRho = rhoPosR ↑t) :

Rockel2026XiBlest.blestNu C ≤ rhoPosN ↑t

source

theorem Papers.Rockel2026ExactBlest.rho_positive_fibre (t : ↑unitInterval) (n : ℝ) :

(∃ (C : ProbabilityTheory.Copula 2), C.spearmanRho = rhoPosR ↑t ∧ Rockel2026XiBlest.blestNu C = n) ↔ n ∈ Set.Icc (2 * rhoPosR ↑t - rhoPosN ↑t) (rhoPosN ↑t)

source

theorem Papers.Rockel2026ExactBlest.rho_negative_fibre (t : ↑unitInterval) (n : ℝ) :

(∃ (C : ProbabilityTheory.Copula 2), C.spearmanRho = -rhoPosR ↑t ∧ Rockel2026XiBlest.blestNu C = n) ↔ n ∈ Set.Icc (-rhoPosN ↑t) (rhoPosN ↑t - 2 * rhoPosR ↑t)

source

theorem Papers.Rockel2026ExactBlest.rhoPosR_mem_Icc (t : ↑unitInterval) :

rhoPosR ↑t ∈ Set.Icc 0 1

source

theorem Papers.Rockel2026ExactBlest.rho_parameter_strictAnti :

StrictAntiOn rhoPosR (Set.Icc 0 1)

source

theorem Papers.Rockel2026ExactBlest.rho_parameter_exists_unique (r : ℝ) (hr : r ∈ Set.Icc 0 1) :

∃! t : ↑unitInterval, rhoPosR ↑t = r

source

theorem Papers.Rockel2026ExactBlest.rpow_cube_four_thirds (x : ℝ) (hx : 0 ≤ x) :

(x ^ 3) ^ (4 / 3) = x ^ 4

source

noncomputable def Papers.Rockel2026ExactBlest.rhoBoundary (r : ℝ) :

ℝ

The manuscript's Phi, with the agreeing branches joined at rho=0.

Equations

Papers.Rockel2026ExactBlest.rhoBoundary r = if 0 ≤ r then 1 - 3 / 4 * (1 - r) ^ (4 / 3) else 2 * r + 1 - 3 / 4 * (1 + r) ^ (4 / 3)

Instances For

source

theorem Papers.Rockel2026ExactBlest.rhoBoundary_positive (t : ↑unitInterval) :

rhoBoundary (rhoPosR ↑t) = rhoPosN ↑t

source

theorem Papers.Rockel2026ExactBlest.rhoBoundary_neg (r : ℝ) (hr : 0 ≤ r) :

rhoBoundary (-r) = rhoBoundary r - 2 * r

source

theorem Papers.Rockel2026ExactBlest.rhoBoundary_negative (t : ↑unitInterval) :

rhoBoundary (-rhoPosR ↑t) = rhoPosN ↑t - 2 * rhoPosR ↑t

source

theorem Papers.Rockel2026ExactBlest.rho_fibre_complete (r n : ℝ) :

(∃ (C : ProbabilityTheory.Copula 2), C.spearmanRho = r ∧ Rockel2026XiBlest.blestNu C = n) ↔ r ∈ Set.Icc (-1) 1 ∧ n ∈ Set.Icc (2 * r - rhoBoundary r) (rhoBoundary r)

source

theorem Papers.Rockel2026ExactBlest.rho_nu_region :

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

The exact rho/nu set equality with the displayed 4/3-power boundary.