← Mathematical handbook

Blest's coefficient and its transpose

Checks for the corollary on the exact region of (ν(C), ν(Cᵀ)) in exact-blest-regions.tex, for the boundary function Λ displayed before it, and for the further claims of the revised manuscript that are not covered by the earlier modules: the derivative bounds on Υ used in the proof of the corollary, the failure of central symmetry of the (η,ν)-region, the trivial bound 1/2 obtained from the (ρ,ν)-region alone, and the numerical fibre stated in the discussion.

The randomized branch in transposed coordinates

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

The paper's n_a = ν(B_aᵀ).

Equations

• Papers.Rockel2026ExactBlest.transposeParam a = -1 + (1 - a) ^ 4 * (2 * a + 1) / (4 * a ^ 2)

theorem Papers.Rockel2026ExactBlest.transposeParam_eq (a : ℝ) (ha : a ≠ 0) : transposeParam a = 2 * etaB a - nuB a

theorem Papers.Rockel2026ExactBlest.nu_transpose_familyB_param (a : ↑unitInterval) (ha : 1 / 2 ≤ ↑a) : Rockel2026XiBlest.blestNu (familyB a ha).transpose = transposeParam ↑a

theorem Papers.Rockel2026ExactBlest.transposeParam_factor (a : ℝ) (ha : a ≠ 0) : transposeParam a = -1 + (1 - a) ^ 4 * (2 * (1 / a) + (1 / a) ^ 2) / 4

theorem Papers.Rockel2026ExactBlest.nuB_factor (a : ℝ) (ha : a ≠ 0) : nuB a = -1 + (1 - a) ^ 3 * (1 / a + 1)

theorem Papers.Rockel2026ExactBlest.transposeParam_strictAnti : StrictAntiOn transposeParam (Set.Icc (1 / 2) 1)

theorem Papers.Rockel2026ExactBlest.nuB_strictAnti : StrictAntiOn nuB (Set.Icc (1 / 2) 1)

theorem Papers.Rockel2026ExactBlest.transposeParam_endpoints : transposeParam (1 / 2) = -7 / 8 ∧ transposeParam 1 = -1

theorem Papers.Rockel2026ExactBlest.nuB_endpoints : nuB (1 / 2) = -5 / 8 ∧ nuB 1 = -1

theorem Papers.Rockel2026ExactBlest.transposeParam_open (a : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) : transposeParam a ∈ Set.Ioo (-1) (-7 / 8)

theorem Papers.Rockel2026ExactBlest.nuB_open (a : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) : nuB a ∈ Set.Ioo (-1) (-5 / 8)

theorem Papers.Rockel2026ExactBlest.transposeParam_range (a : ↑unitInterval) (ha : 1 / 2 ≤ ↑a) : transposeParam ↑a ∈ Set.Icc (-1) (-7 / 8)

theorem Papers.Rockel2026ExactBlest.transposeParam_exists_unique (n : ℝ) (hn : n ∈ Set.Icc (-1) (-7 / 8)) : ∃! a : ↑unitInterval, 1 / 2 ≤ ↑a ∧ transposeParam ↑a = n

theorem Papers.Rockel2026ExactBlest.transposeParam_bijOn : StrictAntiOn transposeParam (Set.Ioo (1 / 2) 1) ∧ Set.BijOn transposeParam (Set.Ioo (1 / 2) 1) (Set.Ioo (-1) (-7 / 8))

The paper's statement that a ↦ n_a decreases bijectively from (1/2,1) onto (-1,-7/8).

noncomputable def Papers.Rockel2026ExactBlest.lambdaParameter (n : ℝ) : ↑unitInterval

The randomized parameter belonging to a value of ν in the transposed coordinates.

Equations

• Papers.Rockel2026ExactBlest.lambdaParameter n = if hn : n ∈ Set.Icc (-1) (-7 / 8) then Exists.choose ⋯ else 0

theorem Papers.Rockel2026ExactBlest.lambdaParameter_spec (n : ℝ) (hn : n ∈ Set.Icc (-1) (-7 / 8)) : 1 / 2 ≤ ↑(lambdaParameter n) ∧ transposeParam ↑(lambdaParameter n) = n

theorem Papers.Rockel2026ExactBlest.lambdaParameter_value (a : ↑unitInterval) (ha : 1 / 2 ≤ ↑a) : lambdaParameter (transposeParam ↑a) = a

theorem Papers.Rockel2026ExactBlest.lambdaParameter_open (n : ℝ) (hn : n ∈ Set.Ioo (-1) (-7 / 8)) : 1 / 2 < ↑(lambdaParameter n) ∧ ↑(lambdaParameter n) < 1

The boundary function Λ

noncomputable def Papers.Rockel2026ExactBlest.lambdaClosed (n : ℝ) : ℝ

The closed-form branch of the paper's Λ.

Equations

• Papers.Rockel2026ExactBlest.lambdaClosed n = 4 * ((1 + n) / 2) ^ (3 / 4) - n - 2

noncomputable def Papers.Rockel2026ExactBlest.Lambda (n : ℝ) : ℝ

The paper's Λ: equal to -1 at -1, parametric on (-1,-7/8), closed form on [-7/8,1]. Values outside [-1,1] play no role.

Equations

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

theorem Papers.Rockel2026ExactBlest.Lambda_neg_one : Lambda (-1) = -1

theorem Papers.Rockel2026ExactBlest.Lambda_param_branch (n : ℝ) (hn : n ∈ Set.Ioo (-1) (-7 / 8)) : Lambda n = nuB ↑(lambdaParameter n)

theorem Papers.Rockel2026ExactBlest.Lambda_closed_branch (n : ℝ) (hn : -7 / 8 ≤ n) : Lambda n = lambdaClosed n

theorem Papers.Rockel2026ExactBlest.rpow_fourth_three_quarters (s : ℝ) (hs : 0 ≤ s) : (s ^ 4) ^ (3 / 4) = s ^ 3

theorem Papers.Rockel2026ExactBlest.fourthRoot_pow (x : ℝ) (hx : 0 ≤ x) : (x ^ (1 / 4)) ^ 4 = x

theorem Papers.Rockel2026ExactBlest.lambdaClosed_param (s : ℝ) (hs : 0 ≤ s) : lambdaClosed (2 * s ^ 4 - 1) = 4 * s ^ 3 - 2 * s ^ 4 - 1

theorem Papers.Rockel2026ExactBlest.closed_root (n : ℝ) (hn : -1 ≤ n) : 0 ≤ ((1 + n) / 2) ^ (1 / 4) ∧ n = 2 * (((1 + n) / 2) ^ (1 / 4)) ^ 4 - 1

Every n ≥ -1 is 2 s^4 - 1 for the nonnegative fourth root s = ((1+n)/2)^{1/4}.

theorem Papers.Rockel2026ExactBlest.quartic_strictMono (s t : ℝ) (hs : 0 ≤ s) (hst : s < t) (ht : t ≤ 1) : 4 * s ^ 3 - 2 * s ^ 4 < 4 * t ^ 3 - 2 * t ^ 4

The quartic 4 s^3 - 2 s^4 is strictly increasing on [0,1].

theorem Papers.Rockel2026ExactBlest.root_bounds (n : ℝ) (hn : n ∈ Set.Icc (-7 / 8) 1) : 1 / 2 ≤ ((1 + n) / 2) ^ (1 / 4) ∧ ((1 + n) / 2) ^ (1 / 4) ≤ 1

theorem Papers.Rockel2026ExactBlest.lambdaClosed_root (n : ℝ) (hn : -1 ≤ n) : lambdaClosed n = 4 * (((1 + n) / 2) ^ (1 / 4)) ^ 3 - 2 * (((1 + n) / 2) ^ (1 / 4)) ^ 4 - 1

theorem Papers.Rockel2026ExactBlest.lambdaClosed_bounds (n : ℝ) (hn : n ∈ Set.Icc (-7 / 8) 1) : -5 / 8 ≤ lambdaClosed n ∧ lambdaClosed n ≤ 1

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

theorem Papers.Rockel2026ExactBlest.Lambda_strictMonoOn : StrictMonoOn Lambda (Set.Icc (-1) 1)

Λ is strictly increasing on [-1,1].

theorem Papers.Rockel2026ExactBlest.Lambda_ge_self (x : ℝ) (hx : x ∈ Set.Icc (-1) 1) : x ≤ Lambda x

theorem Papers.Rockel2026ExactBlest.Lambda_mapsTo : Set.MapsTo Lambda (Set.Icc (-1) 1) (Set.Icc (-1) 1)

theorem Papers.Rockel2026ExactBlest.Lambda_surjOn : Set.SurjOn Lambda (Set.Icc (-1) 1) (Set.Icc (-1) 1)

theorem Papers.Rockel2026ExactBlest.Lambda_bijOn : Set.BijOn Lambda (Set.Icc (-1) 1) (Set.Icc (-1) 1)

Λ is a strictly increasing bijection of [-1,1].

theorem Papers.Rockel2026ExactBlest.Lambda_junction : Lambda (-7 / 8) = -5 / 8 ∧ transposeParam (1 / 2) = -7 / 8 ∧ nuB (1 / 2) = -5 / 8

Both displayed formulas give Λ(-7/8) = -5/8.