← Mathematical handbook

Complete normalization-map properties from Lemma 2.1

noncomputable def Papers.Rockel2026XiBlest.normalizationMean (b q : ℝ) : ℝ

Equations

• Papers.Rockel2026XiBlest.normalizationMean b q = ∫ (t : ↑unitInterval), Verification.unitClamp (b * ((1 - ↑t) ^ 2 - q))

theorem Papers.Rockel2026XiBlest.normalizationMean_eq (b q : ℝ) : normalizationMean b q = Verification.quadraticMean b (-b * q)

theorem Papers.Rockel2026XiBlest.normalizationMean_properties (b : ℝ) (hb : 0 < b) : Continuous (normalizationMean b) ∧ StrictAntiOn (normalizationMean b) (Set.Icc (-1 / b) 1) ∧ normalizationMean b (-1 / b) = 1 ∧ normalizationMean b 1 = 0 ∧ ∀ (q : ℝ), normalizationMean b q ∈ Set.Icc 0 1

theorem Papers.Rockel2026XiBlest.quadraticIntercept_continuous (b : ℝ) (hb : 0 ≤ b) : Continuous (Verification.quadraticIntercept b hb)

theorem Papers.Rockel2026XiBlest.extremalQ_continuous (b : ℝ) (hb : 0 < b) : Continuous (extremalQ b hb)

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

theorem Papers.Rockel2026XiBlest.xi_mixture_continuous (C D : ProbabilityTheory.Copula 2) : Continuous fun (a : ↑unitInterval) => (C.mix D a).chatterjeeXi

Lemma 4.4, including both endpoints and singular copulas.