← Mathematical handbook

Proposition 3: all three uniform limiting cases

theorem Papers.AnsariRockel2026XiRho.sourceBand_independence_error (b : ℝ) (hb : 0 < b) (u v : ↑unitInterval) : |(sourceBand b hb).cdf ![u, v] - ↑u * ↑v| ≤ b

theorem Papers.AnsariRockel2026XiRho.sourceBand_comonotonic_error (b : ℝ) (hb : 0 < b) (u v : ↑unitInterval) : |(sourceBand b hb).cdf ![u, v] - min ↑u ↑v| ≤ 1 / b

theorem Papers.AnsariRockel2026XiRho.negativeSourceBand_independence_error (b : ℝ) (hb : 0 < b) (u v : ↑unitInterval) : |(negativeSourceBand b hb).cdf ![u, v] - ↑u * ↑v| ≤ b

theorem Papers.AnsariRockel2026XiRho.negativeSourceBand_countermonotonic_error (b : ℝ) (hb : 0 < b) (u v : ↑unitInterval) : |(negativeSourceBand b hb).cdf ![u, v] - max (↑u + ↑v - 1) 0| ≤ 1 / b

theorem Papers.AnsariRockel2026XiRho.sourceBand_tendstoUniformly_zero {α : Type u_1} {l : Filter α} (b : α → ℝ) (hb : ∀ (a : α), 0 < b a) (hlim : Filter.Tendsto b l (nhds 0)) : TendstoUniformly (fun (a : α) => (sourceBand (b a) ⋯).cdf) (ProbabilityTheory.Copula.independence 2).cdf l

Any positive parameter net approaching zero converges uniformly to independence.

theorem Papers.AnsariRockel2026XiRho.negativeSourceBand_tendstoUniformly_zero {α : Type u_1} {l : Filter α} (b : α → ℝ) (hb : ∀ (a : α), 0 < b a) (hlim : Filter.Tendsto b l (nhds 0)) : TendstoUniformly (fun (a : α) => (negativeSourceBand (b a) ⋯).cdf) (ProbabilityTheory.Copula.independence 2).cdf l

The negative branch also converges uniformly to independence as its magnitude vanishes.

theorem Papers.AnsariRockel2026XiRho.sourceBand_tendstoUniformly_atTop {α : Type u_1} {l : Filter α} (b : α → ℝ) (hb : ∀ (a : α), 0 < b a) (hlim : Filter.Tendsto b l Filter.atTop) : TendstoUniformly (fun (a : α) => (sourceBand (b a) ⋯).cdf) (ProbabilityTheory.Copula.comonotonic 2).cdf l

Parameters tending to positive infinity converge uniformly to M.

theorem Papers.AnsariRockel2026XiRho.negativeSourceBand_tendstoUniformly_atTop {α : Type u_1} {l : Filter α} (b : α → ℝ) (hb : ∀ (a : α), 0 < b a) (hlim : Filter.Tendsto b l Filter.atTop) : TendstoUniformly (fun (a : α) => (negativeSourceBand (b a) ⋯).cdf) ProbabilityTheory.Copula.countermonotonic.cdf l

Negative parameters with magnitude tending to infinity converge uniformly to W.