Documentation

Papers.Rockel2026ExactBlest.ExactBlestParameters

← Mathematical handbook

Direct proofs of the full rho parameter bijection and the randomized-gap calculus used in exact-blest-regions.tex.

source
theorem Papers.Rockel2026ExactBlest.continuous_rhoFullFamily_parameter :
Continuous fun (c : ↑unitInterval) => (rhoFullFamily c).spearmanRho
source
theorem Papers.Rockel2026ExactBlest.rhoFullFamily_parameter_endpoints :
(rhoFullFamily 0).spearmanRho = 1 ∧ (rhoFullFamily 1).spearmanRho = -1
source
theorem Papers.Rockel2026ExactBlest.rhoFullFamily_parameter_strictAnti :
StrictAnti fun (c : ↑unitInterval) => (rhoFullFamily c).spearmanRho
source
theorem Papers.Rockel2026ExactBlest.rhoFullFamily_parameter_exists_unique (r : ℝ) (hr : r ∈ Set.Icc (-1) 1) :
∃! c : ↑unitInterval, (rhoFullFamily c).spearmanRho = r
source
theorem Papers.Rockel2026ExactBlest.rhoFullFamily_parameter_range :
(Set.range fun (c : ↑unitInterval) => (rhoFullFamily c).spearmanRho) = Set.Icc (-1) 1
source
theorem Papers.Rockel2026ExactBlest.rhoFullFamily_on_boundary (c : ↑unitInterval) :
Rockel2026XiBlest.blestNu (rhoFullFamily c) = rhoBoundary (rhoFullFamily c).spearmanRho
source
noncomputable def Papers.Rockel2026ExactBlest.randomGap (a : ℝ) :
ℝ

The manuscript's Upsilon(e_a), extended algebraically to real a.

Equations
Instances For
    source
    theorem Papers.Rockel2026ExactBlest.hasDerivAt_nuB (a : ℝ) (ha : a ≠ 0) :
    HasDerivAt nuB (-((1 - a) ^ 2 * (3 * a ^ 2 + 2 * a + 1)) / a ^ 2) a
    source
    theorem Papers.Rockel2026ExactBlest.hasDerivAt_randomGap (a : ℝ) (ha : a ≠ 0) :
    HasDerivAt randomGap (-((1 - a) ^ 2 * (3 * a - 1) * (3 * a ^ 2 + 2 * a + 1)) / (4 * a ^ 3)) a
    source
    theorem Papers.Rockel2026ExactBlest.deriv_randomGap_neg (a : ℝ) (ha : 1 / 2 ≤ a) (ha1 : a < 1) :
    deriv randomGap a < 0
    source
    theorem Papers.Rockel2026ExactBlest.randomGap_strictAnti :
    StrictAntiOn randomGap (Set.Icc (1 / 2) 1)
    source
    theorem Papers.Rockel2026ExactBlest.randomGap_endpoints :
    randomGap (1 / 2) = 1 / 8 ∧ randomGap 1 = 0
    source
    theorem Papers.Rockel2026ExactBlest.randomGap_bounds (a : ℝ) (ha : a ∈ Set.Ioo (1 / 2) 1) :
    0 < randomGap a ∧ randomGap a < 1 / 8
    source
    theorem Papers.Rockel2026ExactBlest.etaGap_randomized_bounds (a : ↑unitInterval) (ha : 1 / 2 < ↑a) (ha1 : ↑a < 1) :
    0 < etaGap (etaB ↑a) ∧ etaGap (etaB ↑a) < 1 / 8
    source
    theorem Papers.Rockel2026ExactBlest.hasDerivAt_etaGap_randomized (a : ℝ) (ha : 1 / 2 < a) (ha1 : a < 1) :
    HasDerivAt (fun (b : ℝ) => etaGap (etaB b)) (-((1 - a) ^ 2 * (3 * a - 1) * (3 * a ^ 2 + 2 * a + 1)) / (4 * a ^ 3)) a
    source
    theorem Papers.Rockel2026ExactBlest.etaGap_join :
    etaGap (-3 / 4) = 1 / 8