← Copula mathematical handbook

Quantitative continuity of the normalized quadratic family

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticIntercept_abs_sub_le (b d : ℝ) (hb : 0 ≤ b) (hd : 0 ≤ d) (v : ↑unitInterval) : |quadraticIntercept b hb v - quadraticIntercept d hd v| ≤ |b - d|

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticKernel_abs_sub_le (b d : ℝ) (hb : 0 ≤ b) (hd : 0 ≤ d) (v u : ↑unitInterval) : |quadraticKernel b hb v u - quadraticKernel d hd v u| ≤ 2 * |b - d|

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.quadraticBand_xi_abs_sub_le (b d : ℝ) (hb : 0 ≤ b) (hd : 0 ≤ d) : |(quadraticBand b hb).chatterjeeXi - (quadraticBand d hd).chatterjeeXi| ≤ 24 * |b - d|

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.continuous_quadraticBand_xi : Continuous fun (b : ↑(Set.Ici 0)) => (quadraticBand ↑b ⋯).chatterjeeXi