← Mathematical handbook

The unconditional Blest--beta inequality in exact-blest-regions.tex. The certificate below is checked as an exact polynomial identity in each rectangle. No numeric solver or assumed beta-region theorem enters the proof.

noncomputable def Papers.Rockel2026ExactBlest.betaPhi0 (x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.betaPhi0 x = 2 * x ^ 3 / 3

noncomputable def Papers.Rockel2026ExactBlest.betaPhi1 (x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.betaPhi1 x = 2 * x ^ 3 / 3 + x ^ 2 / 3 - 1 / 108

noncomputable def Papers.Rockel2026ExactBlest.betaPhi2 (x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.betaPhi2 x = 2 * x ^ 3 / 3 - x ^ 2 / 3 + 13 / 324

noncomputable def Papers.Rockel2026ExactBlest.betaPhi3 (x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.betaPhi3 x = 2 * x ^ 3 / 3 - 31 / 162

noncomputable def Papers.Rockel2026ExactBlest.betaPsi0 (z : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.betaPsi0 z = z ^ 3 / 3

noncomputable def Papers.Rockel2026ExactBlest.betaPsi1 (z : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.betaPsi1 z = z ^ 3 / 3 + z ^ 2 / 3 + z / 9 - 1 / 36

noncomputable def Papers.Rockel2026ExactBlest.betaPsi2 (z : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.betaPsi2 z = z ^ 3 / 3 - z ^ 2 / 3 + z / 9 - 1 / 324

noncomputable def Papers.Rockel2026ExactBlest.betaPsi3 (z : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.betaPsi3 z = z ^ 3 / 3 - 23 / 162

def Papers.Rockel2026ExactBlest.bernsteinRow (a b c d t : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.bernsteinRow a b c d t = a * (1 - t) ^ 3 + 3 * b * t * (1 - t) ^ 2 + 3 * c * t ^ 2 * (1 - t) + d * t ^ 3

theorem Papers.Rockel2026ExactBlest.bernsteinRow_nonneg (a b c d t : ℝ) (ht : t ∈ Set.Icc 0 1) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hd : 0 ≤ d) : 0 ≤ bernsteinRow a b c d t

theorem Papers.Rockel2026ExactBlest.beta_cell_00 (x z : ℝ) (hx : x ∈ Set.Icc 0 (1 / 6)) (hz : z ∈ Set.Icc 0 (1 / 6)) : 0 ≤ betaPhi0 x + betaPsi0 z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_cell_01 (x z : ℝ) (hx : x ∈ Set.Icc 0 (1 / 6)) (hz : z ∈ Set.Icc (1 / 6) (1 / 2)) : 0 ≤ betaPhi0 x + betaPsi1 z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_cell_02 (x z : ℝ) (hx : x ∈ Set.Icc 0 (1 / 6)) (hz : z ∈ Set.Icc (1 / 2) (5 / 6)) : 0 ≤ betaPhi0 x + betaPsi2 z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_cell_03 (x z : ℝ) (hx : x ∈ Set.Icc 0 (1 / 6)) (hz : z ∈ Set.Icc (5 / 6) 1) : 0 ≤ betaPhi0 x + betaPsi3 z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_cell_10 (x z : ℝ) (hx : x ∈ Set.Icc (1 / 6) (1 / 2)) (hz : z ∈ Set.Icc 0 (1 / 6)) : 0 ≤ betaPhi1 x + betaPsi0 z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_cell_11 (x z : ℝ) (hx : x ∈ Set.Icc (1 / 6) (1 / 2)) (hz : z ∈ Set.Icc (1 / 6) (1 / 2)) : 0 ≤ betaPhi1 x + betaPsi1 z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_cell_12 (x z : ℝ) (hx : x ∈ Set.Icc (1 / 6) (1 / 2)) (hz : z ∈ Set.Icc (1 / 2) (5 / 6)) : 0 ≤ betaPhi1 x + betaPsi2 z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_cell_13 (x z : ℝ) (hx : x ∈ Set.Icc (1 / 6) (1 / 2)) (hz : z ∈ Set.Icc (5 / 6) 1) : 0 ≤ betaPhi1 x + betaPsi3 z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_cell_20 (x z : ℝ) (hx : x ∈ Set.Icc (1 / 2) (5 / 6)) (hz : z ∈ Set.Icc 0 (1 / 6)) : 0 ≤ betaPhi2 x + betaPsi0 z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_cell_21 (x z : ℝ) (hx : x ∈ Set.Icc (1 / 2) (5 / 6)) (hz : z ∈ Set.Icc (1 / 6) (1 / 2)) : 0 ≤ betaPhi2 x + betaPsi1 z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_cell_22 (x z : ℝ) (hx : x ∈ Set.Icc (1 / 2) (5 / 6)) (hz : z ∈ Set.Icc (1 / 2) (5 / 6)) : 0 ≤ betaPhi2 x + betaPsi2 z - x ^ 2 * z + 1 / 3

theorem Papers.Rockel2026ExactBlest.beta_cell_23 (x z : ℝ) (hx : x ∈ Set.Icc (1 / 2) (5 / 6)) (hz : z ∈ Set.Icc (5 / 6) 1) : 0 ≤ betaPhi2 x + betaPsi3 z - x ^ 2 * z + 1 / 3

theorem Papers.Rockel2026ExactBlest.beta_cell_30 (x z : ℝ) (hx : x ∈ Set.Icc (5 / 6) 1) (hz : z ∈ Set.Icc 0 (1 / 6)) : 0 ≤ betaPhi3 x + betaPsi0 z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_cell_31 (x z : ℝ) (hx : x ∈ Set.Icc (5 / 6) 1) (hz : z ∈ Set.Icc (1 / 6) (1 / 2)) : 0 ≤ betaPhi3 x + betaPsi1 z - x ^ 2 * z

theorem Papers.Rockel2026ExactBlest.beta_cell_32 (x z : ℝ) (hx : x ∈ Set.Icc (5 / 6) 1) (hz : z ∈ Set.Icc (1 / 2) (5 / 6)) : 0 ≤ betaPhi3 x + betaPsi2 z - x ^ 2 * z + 1 / 3

theorem Papers.Rockel2026ExactBlest.beta_cell_33 (x z : ℝ) (hx : x ∈ Set.Icc (5 / 6) 1) (hz : z ∈ Set.Icc (5 / 6) 1) : 0 ≤ betaPhi3 x + betaPsi3 z - x ^ 2 * z + 1 / 3

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

Equations

• Papers.Rockel2026ExactBlest.fourPiece f0 f1 f2 f3 x = if x ≤ 1 / 6 then f0 x else if x ≤ 1 / 2 then f1 x else if x ≤ 5 / 6 then f2 x else f3 x

noncomputable def Papers.Rockel2026ExactBlest.betaPhi : ℝ → ℝ

Equations

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

noncomputable def Papers.Rockel2026ExactBlest.betaPsi : ℝ → ℝ

Equations

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

noncomputable def Papers.Rockel2026ExactBlest.cutValue (f : ℝ → ℝ) (t x : ℝ) : ℝ

Equations

• Papers.Rockel2026ExactBlest.cutValue f t x = if x ≤ t then f x else 0

theorem Papers.Rockel2026ExactBlest.integral_cutValue (f : ℝ → ℝ) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : ∫ (u : ↑unitInterval), cutValue f t ↑u = ∫ (x : ℝ) in 0..t, f x

theorem Papers.Rockel2026ExactBlest.integrable_cutValue (f : ℝ → ℝ) (hf : Continuous f) (t : ℝ) : MeasureTheory.Integrable (fun (u : ↑unitInterval) => cutValue f t ↑u) MeasureTheory.volume

theorem Papers.Rockel2026ExactBlest.fourPiece_decomposition (f0 f1 f2 f3 : ℝ → ℝ) : fourPiece f0 f1 f2 f3 = fun (x : ℝ) => f3 x + cutValue (fun (x : ℝ) => f2 x - f3 x) (5 / 6) x + cutValue (fun (x : ℝ) => f1 x - f2 x) (1 / 2) x + cutValue (fun (x : ℝ) => f0 x - f1 x) (1 / 6) x

theorem Papers.Rockel2026ExactBlest.integral_fourPiece (f0 f1 f2 f3 : ℝ → ℝ) (h0 : Continuous f0) (h1 : Continuous f1) (h2 : Continuous f2) (h3 : Continuous f3) : ∫ (u : ↑unitInterval), fourPiece f0 f1 f2 f3 ↑u = (((∫ (u : ↑unitInterval), f3 ↑u) + ∫ (x : ℝ) in 0..5 / 6, f2 x - f3 x) + ∫ (x : ℝ) in 0..1 / 2, f1 x - f2 x) + ∫ (x : ℝ) in 0..1 / 6, f0 x - f1 x

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

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

theorem Papers.Rockel2026ExactBlest.beta_dual (x z : ℝ) (hx : x ∈ Set.Icc 0 1) (hz : z ∈ Set.Icc 0 1) : x ^ 2 * z - (if 1 / 2 < x ∧ 1 / 2 < z then 1 else 0) / 3 ≤ betaPhi x + betaPsi z

theorem Papers.Rockel2026ExactBlest.integral_betaPhi : ∫ (u : ↑unitInterval), betaPhi ↑u = 35 / 324

theorem Papers.Rockel2026ExactBlest.integral_betaPsi : ∫ (u : ↑unitInterval), betaPsi ↑u = 4 / 81

noncomputable def Papers.Rockel2026ExactBlest.upperQuadrant (x : Fin 2 → ↑unitInterval) : ℝ

Equations

• Papers.Rockel2026ExactBlest.upperQuadrant x = if 1 / 2 < ↑(x 0) ∧ 1 / 2 < ↑(x 1) then 1 else 0

theorem Papers.Rockel2026ExactBlest.integrable_upperQuadrant (C : ProbabilityTheory.Copula 2) : MeasureTheory.Integrable upperQuadrant C.toMeasure

theorem Papers.Rockel2026ExactBlest.integral_upperQuadrant (C : ProbabilityTheory.Copula 2) : ∫ (x : Fin 2 → ↑unitInterval), upperQuadrant x ∂C.toMeasure = C.cdf ![ProbabilityTheory.Copula.unitHalf, ProbabilityTheory.Copula.unitHalf]

theorem Papers.Rockel2026ExactBlest.beta_quadrant_formula (C : ProbabilityTheory.Copula 2) : C.blomqvistBeta = 4 * ∫ (x : Fin 2 → ↑unitInterval), upperQuadrant x ∂C.toMeasure - 1

theorem Papers.Rockel2026ExactBlest.transport_beta_upper (C : ProbabilityTheory.Copula 2) : ∫ (x : Fin 2 → ↑unitInterval), ↑(x 0) ^ 2 * ↑(x 1) - upperQuadrant x / 3 ∂C.toMeasure ≤ 17 / 108

theorem Papers.Rockel2026ExactBlest.nu_beta_upper (C : ProbabilityTheory.Copula 2) : Rockel2026XiBlest.blestNu C - C.blomqvistBeta ≤ 8 / 9

theorem Papers.Rockel2026ExactBlest.nu_beta_bound (C : ProbabilityTheory.Copula 2) : |Rockel2026XiBlest.blestNu C - C.blomqvistBeta| ≤ 8 / 9

The manuscript's unconditional bound; no exact-region hypothesis is assumed.

theorem Papers.Rockel2026ExactBlest.raw_blest_moment (C : ProbabilityTheory.Copula 2) : 12 * ∫ (x : Fin 2 → ↑unitInterval), ↑(x 0) ^ 2 * ↑(x 1) ∂C.toMeasure - 2 = 2 * C.spearmanRho - Rockel2026XiBlest.blestNu C

theorem Papers.Rockel2026ExactBlest.blest_ordinalSum (C D : ProbabilityTheory.Copula 2) (a : ↑unitInterval) : Rockel2026XiBlest.blestNu (C.ordinalSum D a) = ↑a ^ 4 * Rockel2026XiBlest.blestNu C + (1 - ↑a) ^ 4 * Rockel2026XiBlest.blestNu D + 2 * ↑a ^ 3 * (1 - ↑a) * C.spearmanRho + 2 * ↑a * (1 - ↑a) * (2 - ↑a)

noncomputable def Papers.Rockel2026ExactBlest.halfRotation : ProbabilityTheory.Copula 2

Equations

• Papers.Rockel2026ExactBlest.halfRotation = (ProbabilityTheory.Copula.countermonotonic.ordinalSum ProbabilityTheory.Copula.countermonotonic ProbabilityTheory.Copula.unitHalf).reflect {0}

theorem Papers.Rockel2026ExactBlest.halfRotation_values : Rockel2026XiBlest.blestNu halfRotation = -1 / 2 ∧ halfRotation.spearmanRho = -1 / 2 ∧ halfRotation.blomqvistBeta = -1

noncomputable def Papers.Rockel2026ExactBlest.betaWitness : ProbabilityTheory.Copula 2

Equations

• Papers.Rockel2026ExactBlest.betaWitness = Verification.centeredOrdinal Papers.Rockel2026ExactBlest.halfRotation ⟨2 / 3, Papers.Rockel2026ExactBlest.betaWitness._proof_1⟩

theorem Papers.Rockel2026ExactBlest.betaWitness_values : Rockel2026XiBlest.blestNu betaWitness = 5 / 9 ∧ betaWitness.blomqvistBeta = -1 / 3

The upper extremizer P_(1/6), assembled from its three ordinal blocks.

theorem Papers.Rockel2026ExactBlest.nu_beta_upper_attained : ∃ (C : ProbabilityTheory.Copula 2), Rockel2026XiBlest.blestNu C - C.blomqvistBeta = 8 / 9

theorem Papers.Rockel2026ExactBlest.nu_beta_lower_attained : ∃ (C : ProbabilityTheory.Copula 2), Rockel2026XiBlest.blestNu C - C.blomqvistBeta = -8 / 9