← Mathematical handbook

Population convergence and an explicit empirical consistency criterion

theorem Papers.Rockel2025Approximation.checkerboard_xi_stability {m n : ℕ} (C D : ProbabilityTheory.Copula 2) (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition n) (ε : ℝ) (h : ∀ (u v : ↑unitInterval), |C.cdf ![u, v] - D.cdf ![u, v]| ≤ ε) : |(C.cellMass P Q).checkerboard.chatterjeeXi - (D.cellMass P Q).checkerboard.chatterjeeXi| ≤ 24 * ↑m * ε

Quantitative stability under CDF perturbations, for arbitrary partitions.

theorem Papers.Rockel2025Approximation.checkerboard_xi_tendsto (C : ProbabilityTheory.Copula 2) : Filter.Tendsto (fun (k : ℕ) => (C.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (k + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (k + 1) ⋯)).checkerboard.chatterjeeXi) Filter.atTop (nhds C.chatterjeeXi)

Population checkerboards converge in xi for every copula, including singular laws.

theorem Papers.Rockel2025Approximation.checkerboard_xi_tendsto_of_cdf_error (C : ProbabilityTheory.Copula 2) (D : ℕ → ProbabilityTheory.Copula 2) (N : ℕ → ℕ) (hN : Filter.Tendsto N Filter.atTop Filter.atTop) (ε : ℕ → ℝ) (hCDF : ∀ᶠ (k : ℕ) in Filter.atTop, ∀ (u v : ↑unitInterval), |(D k).cdf ![u, v] - C.cdf ![u, v]| ≤ ε k) (hε : Filter.Tendsto (fun (k : ℕ) => (↑(N k) + 1) * ε k) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => ((D k).cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (N k + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (N k + 1) ⋯)).checkerboard.chatterjeeXi) Filter.atTop (nhds C.chatterjeeXi)

The statistical CDF error rate is an explicit hypothesis, not an assumed conclusion.

theorem Papers.Rockel2025Approximation.checkerboardEstimator_tendsto_of_cdf_error (C : ProbabilityTheory.Copula 2) (D : ℕ → ProbabilityTheory.Copula 2) (N : ℕ → ℕ) (hN : Filter.Tendsto N Filter.atTop Filter.atTop) (ε : ℕ → ℝ) (hCDF : ∀ᶠ (k : ℕ) in Filter.atTop, ∀ (u v : ↑unitInterval), |(D k).cdf ![u, v] - C.cdf ![u, v]| ≤ ε k) (hε : Filter.Tendsto (fun (k : ℕ) => (↑(N k) + 1) * ε k) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (k : ℕ) => Verification.checkerboardEstimator ((D k).cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (N k + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (N k + 1) ⋯))) Filter.atTop (nhds C.chatterjeeXi)