← Mathematical handbook

The distribution-function rank map used in the rho/Blest rearrangement proof.

def Papers.Rockel2026ExactBlest.quadraticScore (c : ℝ) (x : ↑unitInterval) : ℝ

Equations

• Papers.Rockel2026ExactBlest.quadraticScore c x = (↑x - c) ^ 2

noncomputable def Papers.Rockel2026ExactBlest.quadraticLaw (c : ℝ) : MeasureTheory.Measure ℝ

Equations

• Papers.Rockel2026ExactBlest.quadraticLaw c = MeasureTheory.Measure.map (Papers.Rockel2026ExactBlest.quadraticScore c) MeasureTheory.volume

theorem Papers.Rockel2026ExactBlest.uniform_real_level_null (r : ℝ) : MeasureTheory.volume {x : ↑unitInterval | ↑x = r} = 0

instance Papers.Rockel2026ExactBlest.quadraticLaw_probability (c : ℝ) : MeasureTheory.IsProbabilityMeasure (quadraticLaw c)

instance Papers.Rockel2026ExactBlest.quadraticLaw_atomless (c : ℝ) : MeasureTheory.NullSingletonClass (quadraticLaw c)

theorem Papers.Rockel2026ExactBlest.continuous_quadratic_cdf (c : ℝ) : Continuous ↑(ProbabilityTheory.cdf (quadraticLaw c))

noncomputable def Papers.Rockel2026ExactBlest.quadraticRank (c : ℝ) (x : ↑unitInterval) : ↑unitInterval

Equations

• Papers.Rockel2026ExactBlest.quadraticRank c x = ProbabilityTheory.cdfUnit (Papers.Rockel2026ExactBlest.quadraticLaw c) (Papers.Rockel2026ExactBlest.quadraticScore c x)

theorem Papers.Rockel2026ExactBlest.quadraticRank_uniform (c : ℝ) : MeasureTheory.MeasurePreserving (quadraticRank c) MeasureTheory.volume MeasureTheory.volume

theorem Papers.Rockel2026ExactBlest.quadratic_cdf_at_score (c x : ↑unitInterval) : ↑(ProbabilityTheory.cdf (quadraticLaw ↑c)) (quadraticScore (↑c) x) = min 1 (↑c + |↑x - ↑c|) - max 0 (↑c - |↑x - ↑c|)

theorem Papers.Rockel2026ExactBlest.quadraticRank_paper (c x : ↑unitInterval) : ↑(quadraticRank (↑c) x) = if |↑x - ↑c| ≤ min (↑c) (1 - ↑c) then 2 * |↑x - ↑c| else if 2 * ↑c ≤ ↑x then ↑x else 1 - ↑x

theorem Papers.Rockel2026ExactBlest.quadraticRank_positive (c : ↑unitInterval) (hc : ↑c ≤ 1 / 2) (x : ↑unitInterval) : quadraticRank (↑c) x = rhoRank ⟨2 * ↑c, ⋯⟩ x

theorem Papers.Rockel2026ExactBlest.quadraticRank_symm (c x : ↑unitInterval) : quadraticRank (↑c) (unitInterval.symm x) = quadraticRank (↑(unitInterval.symm c)) x

theorem Papers.Rockel2026ExactBlest.survival_reflect_first (C : ProbabilityTheory.Copula 2) : (C.reflect {0}).survivalCopula = C.survivalCopula.reflect {0}

noncomputable def Papers.Rockel2026ExactBlest.rhoFullFamily (c : ↑unitInterval) : ProbabilityTheory.Copula 2

Equations

• Papers.Rockel2026ExactBlest.rhoFullFamily c = if hc : ↑c ≤ 1 / 2 then Papers.Rockel2026ExactBlest.rhoFamily ⟨2 * ↑c, ⋯⟩ else (Papers.Rockel2026ExactBlest.rhoFamily ⟨2 * (1 - ↑c), ⋯⟩).reflect {0}

theorem Papers.Rockel2026ExactBlest.rhoFullFamily_values (c : ↑unitInterval) : ((rhoFullFamily c).spearmanRho = if ↑c ≤ 1 / 2 then 1 - 8 * ↑c ^ 3 else 8 * (1 - ↑c) ^ 3 - 1) ∧ Rockel2026XiBlest.blestNu (rhoFullFamily c) = if ↑c ≤ 1 / 2 then 1 - 12 * ↑c ^ 4 else 16 * (1 - ↑c) ^ 3 - 12 * (1 - ↑c) ^ 4 - 1

theorem Papers.Rockel2026ExactBlest.rhoFullFamily_graph (c : ↑unitInterval) : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂(rhoFullFamily c).survivalCopula.toMeasure, x 1 = quadraticRank (↑c) (x 0)

theorem Papers.Rockel2026ExactBlest.rhoFullFamily_graph_law (c : ↑unitInterval) : (rhoFullFamily c).survivalCopula.toMeasure = MeasureTheory.Measure.map (fun (x : ↑unitInterval) => ![x, quadraticRank (↑c) x]) MeasureTheory.volume

theorem Papers.Rockel2026ExactBlest.quadraticRank_endpoints (x : ↑unitInterval) : quadraticRank 0 x = x ∧ quadraticRank 1 x = unitInterval.symm x

theorem Papers.Rockel2026ExactBlest.quadraticRank_half (x : ↑unitInterval) : ↑(quadraticRank (↑ProbabilityTheory.Copula.unitHalf) x) = |2 * ↑x - 1|

theorem Papers.Rockel2026ExactBlest.rho_midpoint_reflected_graph : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂(rhoFullFamily ProbabilityTheory.Copula.unitHalf).survivalCopula.toMeasure, ↑(x 1) = |2 * ↑(x 0) - 1|

theorem Papers.Rockel2026ExactBlest.rho_midpoint_original_graph : ∀ᵐ (x : Fin 2 → ↑unitInterval) ∂(rhoFullFamily ProbabilityTheory.Copula.unitHalf).toMeasure, ↑(x 1) = min (2 * ↑(x 0)) (2 - 2 * ↑(x 0))