← Mathematical handbook

noncomputable def Verification.checkerboardEstimator {n : ℕ} (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯)) : ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Verification.checkerboardEstimator_eq_average {n : ℕ} (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯)) : checkerboardEstimator A = (A.checkerboard.chatterjeeXi + A.checkMin.chatterjeeXi) / 2

theorem Verification.checkerboardEstimator_mem {n : ℕ} (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯)) : checkerboardEstimator A ∈ Set.Icc 0 1

theorem Verification.checkerboardEstimator_correction {n : ℕ} (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯)) : checkerboardEstimator A - A.checkerboard.chatterjeeXi = ((Matrix.of A.mass).transpose * Matrix.of A.mass).trace / 2

theorem Verification.checkerboardEstimator_correction_bounds {n : ℕ} (A : ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯)) : 0 ≤ checkerboardEstimator A - A.checkerboard.chatterjeeXi ∧ checkerboardEstimator A - A.checkerboard.chatterjeeXi ≤ 1 / (↑n + 1) / 2

theorem Verification.checkerboardEstimator_correction_tendsto (N : ℕ → ℕ) (hN : Filter.Tendsto N Filter.atTop Filter.atTop) (A : (k : ℕ) → ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (N k + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (N k + 1) ⋯)) : Filter.Tendsto (fun (k : ℕ) => checkerboardEstimator (A k) - (A k).checkerboard.chatterjeeXi) Filter.atTop (nhds 0)

The finite-sample correction vanishes for every refining sequence of square matrices.

theorem Verification.checkerboardEstimator_tendsto_iff (N : ℕ → ℕ) (hN : Filter.Tendsto N Filter.atTop Filter.atTop) (A : (k : ℕ) → ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (N k + 1) ⋯) (ProbabilityTheory.Copula.IntervalPartition.uniform (N k + 1) ⋯)) (l : ℝ) : Filter.Tendsto (fun (k : ℕ) => checkerboardEstimator (A k)) Filter.atTop (nhds l) ↔ Filter.Tendsto (fun (k : ℕ) => (A k).checkerboard.chatterjeeXi) Filter.atTop (nhds l)

Conditional transfer lemma; the statistical consistency hypothesis remains explicit.