← Mathematical handbook

Exact beta--Blest region in exact-blest-regions.tex, without uniqueness. All certificate identities and nonnegative Bernstein coefficients are kernel checked.

noncomputable def Papers.Rockel2026ExactBlest.paramPhi0 (_q x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.paramPhi0 _q x = 2 * x ^ 3 / 3

noncomputable def Papers.Rockel2026ExactBlest.paramPhi1 (q x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.paramPhi1 q x = 2 * x ^ 3 / 3 + (1 / 2 - q) * x ^ 2 + q ^ 3 - q ^ 2 / 2

noncomputable def Papers.Rockel2026ExactBlest.paramPhi2 (q x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.paramPhi2 q x = 2 * x ^ 3 / 3 + (q - 1 / 2) * x ^ 2 + 1 / 24 - q ^ 3 / 3

noncomputable def Papers.Rockel2026ExactBlest.paramPhi3 (q x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.paramPhi3 q x = 2 * x ^ 3 / 3 + 2 * q ^ 3 / 3 - 5 * q ^ 2 / 2 + 2 * q - 11 / 24

noncomputable def Papers.Rockel2026ExactBlest.paramPsi0 (_q z : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.paramPsi0 _q z = z ^ 3 / 3

noncomputable def Papers.Rockel2026ExactBlest.paramPsi1 (q z : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.paramPsi1 q z = z ^ 3 / 3 + (1 / 2 - q) * z ^ 2 + (q ^ 2 - q + 1 / 4) * z + q ^ 2 / 2 - q / 4

noncomputable def Papers.Rockel2026ExactBlest.paramPsi2 (q z : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.paramPsi2 q z = z ^ 3 / 3 + (q - 1 / 2) * z ^ 2 + (q ^ 2 - q + 1 / 4) * z - 2 * q ^ 3 / 3 + q / 4 - 1 / 24

noncomputable def Papers.Rockel2026ExactBlest.paramPsi3 (q z : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.paramPsi3 q z = z ^ 3 / 3 - 2 * q ^ 3 / 3 - q ^ 2 / 2 + q - 7 / 24

theorem Papers.Rockel2026ExactBlest.interval_parameter (lo hi x : ℝ) (hx : x ∈ Set.Icc lo hi) : ∃ (t : ↑unitInterval), lo + (hi - lo) * ↑t = x

theorem Papers.Rockel2026ExactBlest.beta_param_cell_00 (q x z : ℝ) (_hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc 0 q) (hz : z ∈ Set.Icc 0 q) : 0 ≤ paramPhi0 q x + paramPsi0 q z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_param_cell_01 (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc 0 q) (hz : z ∈ Set.Icc q (1 / 2)) : 0 ≤ paramPhi0 q x + paramPsi1 q z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_param_cell_02 (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc 0 q) (hz : z ∈ Set.Icc (1 / 2) (1 - q)) : 0 ≤ paramPhi0 q x + paramPsi2 q z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_param_cell_03 (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc 0 q) (hz : z ∈ Set.Icc (1 - q) 1) : 0 ≤ paramPhi0 q x + paramPsi3 q z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_param_cell_10 (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc q (1 / 2)) (hz : z ∈ Set.Icc 0 q) : 0 ≤ paramPhi1 q x + paramPsi0 q z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_param_cell_11 (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc q (1 / 2)) (hz : z ∈ Set.Icc q (1 / 2)) : 0 ≤ paramPhi1 q x + paramPsi1 q z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_param_cell_12 (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc q (1 / 2)) (hz : z ∈ Set.Icc (1 / 2) (1 - q)) : 0 ≤ paramPhi1 q x + paramPsi2 q z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_param_cell_13 (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc q (1 / 2)) (hz : z ∈ Set.Icc (1 - q) 1) : 0 ≤ paramPhi1 q x + paramPsi3 q z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_param_cell_20 (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc (1 / 2) (1 - q)) (hz : z ∈ Set.Icc 0 q) : 0 ≤ paramPhi2 q x + paramPsi0 q z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_param_cell_21 (q x z : ℝ) (_hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc (1 / 2) (1 - q)) (hz : z ∈ Set.Icc q (1 / 2)) : 0 ≤ paramPhi2 q x + paramPsi1 q z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_param_cell_22 (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc (1 / 2) (1 - q)) (hz : z ∈ Set.Icc (1 / 2) (1 - q)) : 0 ≤ paramPhi2 q x + paramPsi2 q z - x ^ 2 * z + 3 * (1 / 2 - q) ^ 2

theorem Papers.Rockel2026ExactBlest.beta_param_cell_23 (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc (1 / 2) (1 - q)) (hz : z ∈ Set.Icc (1 - q) 1) : 0 ≤ paramPhi2 q x + paramPsi3 q z - x ^ 2 * z + 3 * (1 / 2 - q) ^ 2

theorem Papers.Rockel2026ExactBlest.beta_param_cell_30 (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc (1 - q) 1) (hz : z ∈ Set.Icc 0 q) : 0 ≤ paramPhi3 q x + paramPsi0 q z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_param_cell_31 (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc (1 - q) 1) (hz : z ∈ Set.Icc q (1 / 2)) : 0 ≤ paramPhi3 q x + paramPsi1 q z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_param_cell_32 (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc (1 - q) 1) (hz : z ∈ Set.Icc (1 / 2) (1 - q)) : 0 ≤ paramPhi3 q x + paramPsi2 q z - x ^ 2 * z + 3 * (1 / 2 - q) ^ 2

theorem Papers.Rockel2026ExactBlest.beta_param_cell_33 (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc (1 - q) 1) (hz : z ∈ Set.Icc (1 - q) 1) : 0 ≤ paramPhi3 q x + paramPsi3 q z - x ^ 2 * z + 3 * (1 / 2 - q) ^ 2

noncomputable def Papers.Rockel2026ExactBlest.paramPieces (q : ℝ) (f0 f1 f2 f3 : ℝ → ℝ) (x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.paramPieces q f0 f1 f2 f3 x = if x ≤ q then f0 x else if x ≤ 1 / 2 then f1 x else if x ≤ 1 - q then f2 x else f3 x

noncomputable def Papers.Rockel2026ExactBlest.paramPhi (q : ℝ) : ℝ → ℝ

Equations

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

noncomputable def Papers.Rockel2026ExactBlest.paramPsi (q : ℝ) : ℝ → ℝ

Equations

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

theorem Papers.Rockel2026ExactBlest.paramPieces_decomposition (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (f0 f1 f2 f3 : ℝ → ℝ) : paramPieces q f0 f1 f2 f3 = fun (x : ℝ) => f3 x + cutValue (fun (x : ℝ) => f2 x - f3 x) (1 - q) x + cutValue (fun (x : ℝ) => f1 x - f2 x) (1 / 2) x + cutValue (fun (x : ℝ) => f0 x - f1 x) q x

theorem Papers.Rockel2026ExactBlest.integral_paramPieces (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (f0 f1 f2 f3 : ℝ → ℝ) (h0 : Continuous f0) (h1 : Continuous f1) (h2 : Continuous f2) (h3 : Continuous f3) : ∫ (u : ↑unitInterval), paramPieces q f0 f1 f2 f3 ↑u = (((∫ (u : ↑unitInterval), f3 ↑u) + ∫ (x : ℝ) in 0..1 - q, f2 x - f3 x) + ∫ (x : ℝ) in 0..1 / 2, f1 x - f2 x) + ∫ (x : ℝ) in 0..q, f0 x - f1 x

theorem Papers.Rockel2026ExactBlest.integrable_paramPieces (C : ProbabilityTheory.Copula 2) (i : Fin 2) (q : ℝ) (f0 f1 f2 f3 : ℝ → ℝ) (h0 : Continuous f0) (h1 : Continuous f1) (h2 : Continuous f2) (h3 : Continuous f3) : MeasureTheory.Integrable (fun (x : Fin 2 → ↑unitInterval) => paramPieces q f0 f1 f2 f3 ↑(x i)) C.toMeasure

theorem Papers.Rockel2026ExactBlest.measurable_paramPieces (q : ℝ) (f0 f1 f2 f3 : ℝ → ℝ) (h0 : Continuous f0) (h1 : Continuous f1) (h2 : Continuous f2) (h3 : Continuous f3) : Measurable fun (u : ↑unitInterval) => paramPieces q f0 f1 f2 f3 ↑u

theorem Papers.Rockel2026ExactBlest.beta_param_dual (q x z : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) (hx : x ∈ Set.Icc 0 1) (hz : z ∈ Set.Icc 0 1) : (x ^ 2 * z - 3 * (1 / 2 - q) ^ 2 * if 1 / 2 < x ∧ 1 / 2 < z then 1 else 0) ≤ paramPhi q x + paramPsi q z

theorem Papers.Rockel2026ExactBlest.integral_paramPhi (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) : ∫ (u : ↑unitInterval), paramPhi q ↑u = -2 * q ^ 3 / 3 + q ^ 2 / 4 + q / 4 + 1 / 16

theorem Papers.Rockel2026ExactBlest.integral_paramPsi (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) : ∫ (u : ↑unitInterval), paramPsi q ↑u = -4 * q ^ 3 / 3 + 5 * q ^ 2 / 4 - q / 4 + 1 / 16

theorem Papers.Rockel2026ExactBlest.transport_beta_param_upper (C : ProbabilityTheory.Copula 2) (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 2)) : ∫ (x : Fin 2 → ↑unitInterval), ↑(x 0) ^ 2 * ↑(x 1) - 3 * (1 / 2 - q) ^ 2 * upperQuadrant x ∂C.toMeasure ≤ -2 * q ^ 3 + 3 * q ^ 2 / 2 + 1 / 8

theorem Papers.Rockel2026ExactBlest.beta_region_upper (C : ProbabilityTheory.Copula 2) : Rockel2026XiBlest.blestNu C ≤ betaUpper C.blomqvistBeta

theorem Papers.Rockel2026ExactBlest.beta_region_lower (C : ProbabilityTheory.Copula 2) : betaLower C.blomqvistBeta ≤ Rockel2026XiBlest.blestNu C

theorem Papers.Rockel2026ExactBlest.blest_centered_of_equal (C : ProbabilityTheory.Copula 2) (h : Rockel2026XiBlest.blestNu C = C.spearmanRho) (a : ↑unitInterval) : Rockel2026XiBlest.blestNu (Verification.centeredOrdinal C a) = 1 - ↑a ^ 3 + ↑a ^ 3 * C.spearmanRho

theorem Papers.Rockel2026ExactBlest.beta_upper_attained (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∃ (C : ProbabilityTheory.Copula 2), C.blomqvistBeta = b ∧ Rockel2026XiBlest.blestNu C = betaUpper b

theorem Papers.Rockel2026ExactBlest.beta_lower_attained (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∃ (C : ProbabilityTheory.Copula 2), C.blomqvistBeta = b ∧ Rockel2026XiBlest.blestNu C = betaLower b

theorem Papers.Rockel2026ExactBlest.beta_fibre (b n : ℝ) : (∃ (C : ProbabilityTheory.Copula 2), C.blomqvistBeta = b ∧ Rockel2026XiBlest.blestNu C = n) ↔ b ∈ Set.Icc (-1) 1 ∧ n ∈ Set.Icc (betaLower b) (betaUpper b)

theorem Papers.Rockel2026ExactBlest.beta_nu_region : (Set.range fun (C : ProbabilityTheory.Copula 2) => (C.blomqvistBeta, Rockel2026XiBlest.blestNu C)) = {p : ℝ × ℝ | p.1 ∈ Set.Icc (-1) 1 ∧ p.2 ∈ Set.Icc (betaLower p.1) (betaUpper p.1)}

The full set equality in thm:beta-nu; no boundary-uniqueness claim.

theorem Papers.Rockel2026ExactBlest.beta_rho_bounds (C : ProbabilityTheory.Copula 2) : C.spearmanRho ∈ Set.Icc (betaLower C.blomqvistBeta) (betaUpper C.blomqvistBeta)

The beta/rho bounds follow by averaging a copula and its survival copula.

theorem Papers.Rockel2026ExactBlest.beta_upper_attained_joint (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∃ (C : ProbabilityTheory.Copula 2), C.blomqvistBeta = b ∧ Rockel2026XiBlest.blestNu C = betaUpper b ∧ C.spearmanRho = betaUpper b

theorem Papers.Rockel2026ExactBlest.beta_lower_attained_joint (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ∃ (C : ProbabilityTheory.Copula 2), C.blomqvistBeta = b ∧ Rockel2026XiBlest.blestNu C = betaLower b ∧ C.spearmanRho = betaLower b

theorem Papers.Rockel2026ExactBlest.beta_rho_fibre (b r : ℝ) : (∃ (C : ProbabilityTheory.Copula 2), C.blomqvistBeta = b ∧ C.spearmanRho = r) ↔ b ∈ Set.Icc (-1) 1 ∧ r ∈ Set.Icc (betaLower b) (betaUpper b)

theorem Papers.Rockel2026ExactBlest.beta_rho_region : (Set.range fun (C : ProbabilityTheory.Copula 2) => (C.blomqvistBeta, C.spearmanRho)) = {p : ℝ × ℝ | p.1 ∈ Set.Icc (-1) 1 ∧ p.2 ∈ Set.Icc (betaLower p.1) (betaUpper p.1)}