← Mathematical handbook

Constructed clamped extremizers and their unique optimality

noncomputable def Papers.Rockel2026XiBlest.extremalCopula (b : ℝ) (hb : 0 ≤ b) : ProbabilityTheory.Copula 2

Equations

• Papers.Rockel2026XiBlest.extremalCopula b hb = Verification.quadraticBand b hb

noncomputable def Papers.Rockel2026XiBlest.extremalQ (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : ℝ

The source's normalization parameter, including response thresholds 0 and 1.

Equations

• Papers.Rockel2026XiBlest.extremalQ b hb v = -Verification.quadraticIntercept b ⋯ v / b

theorem Papers.Rockel2026XiBlest.extremal_normalization (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : ∃! q : ℝ, q ∈ Set.Icc (-1 / b) 1 ∧ ∫ (t : ↑unitInterval), Verification.unitClamp (b * ((1 - ↑t) ^ 2 - q)) = ↑v

theorem Papers.Rockel2026XiBlest.extremalQ_antitone (b : ℝ) (hb : 0 < b) : Antitone (extremalQ b hb)

theorem Papers.Rockel2026XiBlest.extremal_kernel_measurable (b : ℝ) (hb : 0 ≤ b) : Measurable fun (p : ↑unitInterval × ↑unitInterval) => Verification.quadraticKernel b hb p.2 p.1

theorem Papers.Rockel2026XiBlest.extremal_cdf (b : ℝ) (hb : 0 < b) (u v : ↑unitInterval) : (extremalCopula b ⋯).cdf ![u, v] = ∫ (t : ↑unitInterval) in Set.Iic u, Verification.unitClamp (b * ((1 - ↑t) ^ 2 - extremalQ b hb v))

theorem Papers.Rockel2026XiBlest.extremal_conditionalCDF (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (extremalCopula b ⋯).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Verification.unitClamp (b * ((1 - ↑u) ^ 2 - extremalQ b hb v))

theorem Papers.Rockel2026XiBlest.extremal_isSI (b : ℝ) (hb : 0 ≤ b) : (extremalCopula b hb).IsSI

theorem Papers.Rockel2026XiBlest.extremal_support (C : ProbabilityTheory.Copula 2) (b : ℝ) (hb : 0 ≤ b) : b * blestNu C - C.chatterjeeXi ≤ b * blestNu (extremalCopula b hb) - (extremalCopula b hb).chatterjeeXi

theorem Papers.Rockel2026XiBlest.extremal_support_eq_iff (C : ProbabilityTheory.Copula 2) (b : ℝ) (hb : 0 ≤ b) : b * blestNu C - C.chatterjeeXi = b * blestNu (extremalCopula b hb) - (extremalCopula b hb).chatterjeeXi ↔ C = extremalCopula b hb

theorem Papers.Rockel2026XiBlest.extremal_maximal_blest (C : ProbabilityTheory.Copula 2) (b : ℝ) (hb : 0 < b) (hx : C.chatterjeeXi ≤ (extremalCopula b ⋯).chatterjeeXi) : blestNu C ≤ blestNu (extremalCopula b ⋯)

theorem Papers.Rockel2026XiBlest.extremal_maximal_blest_eq_iff (C : ProbabilityTheory.Copula 2) (b : ℝ) (hb : 0 < b) (hx : C.chatterjeeXi = (extremalCopula b ⋯).chatterjeeXi) : blestNu C = blestNu (extremalCopula b ⋯) ↔ C = extremalCopula b ⋯

theorem Papers.Rockel2026XiBlest.extremal_zero : extremalCopula 0 ⋯ = ProbabilityTheory.Copula.independence 2