← Mathematical handbook

Uniform copula limits of the full real-parameter family

theorem Papers.Rockel2026XiBlest.signed_extremal_independence_error (b : ℝ) (u v : ↑unitInterval) : |(signedExtremalCopula b).cdf ![u, v] - ↑u * ↑v| ≤ 2 * |b|

Uniform error at independence from either side of the signed parameter.

theorem Papers.Rockel2026XiBlest.signed_extremal_uniform_zero : TendstoUniformly (fun (b : ℝ) (p : ↑unitInterval × ↑unitInterval) => (signedExtremalCopula b).cdf ![p.1, p.2]) (fun (p : ↑unitInterval × ↑unitInterval) => (ProbabilityTheory.Copula.independence 2).cdf ![p.1, p.2]) (nhds 0)

The family converges uniformly to independence as the real parameter tends to zero.

theorem Papers.Rockel2026XiBlest.signed_extremal_uniform_top : TendstoUniformly (fun (b : ℝ) (p : ↑unitInterval × ↑unitInterval) => (signedExtremalCopula b).cdf ![p.1, p.2]) (fun (p : ↑unitInterval × ↑unitInterval) => (ProbabilityTheory.Copula.comonotonic 2).cdf ![p.1, p.2]) Filter.atTop

Uniform convergence for the entire real parameter at positive infinity.

theorem Papers.Rockel2026XiBlest.signed_extremal_uniform_bot : TendstoUniformly (fun (b : ℝ) (p : ↑unitInterval × ↑unitInterval) => (signedExtremalCopula b).cdf ![p.1, p.2]) (fun (p : ↑unitInterval × ↑unitInterval) => ProbabilityTheory.Copula.countermonotonic.cdf ![p.1, p.2]) Filter.atBot

Uniform convergence for the entire real parameter at negative infinity.