Verification.CheckerboardConvergence

theorem Verification.checkerboard_energy_tendsto (C : ProbabilityTheory.Copula 2) (v : ↑unitInterval) :

Filter.Tendsto (fun (k : ℕ) => conditionalEnergy (C.cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (k + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (k + 1) ⋯)).checkerboard v) Filter.atTop (nhds (conditionalEnergy C v))

Population checkerboard conditional energies converge at every response threshold.

source

theorem Verification.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)

Every copula, including singular laws, is approximated in xi by its population checkerboards. This is distinct from consistency of empirical checkerboards.

source

theorem Verification.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)

CDF approximation at a rate faster than the reciprocal grid order implies xi consistency after rebinning. The input rate remains an explicit hypothesis.

source

theorem Verification.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 : ℕ) => checkerboardEstimator ((D k).cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (N k + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (N k + 1) ⋯))) Filter.atTop (nhds C.chatterjeeXi)