Checked proof steps toward Theorems 4.2 and 4.5 #
theorem
Papers.Rockel2025Approximation.checkerboardEstimator_correction_bounds
{n : ℕ}
(A :
ProbabilityTheory.Copula.CellMass (ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯)
(ProbabilityTheory.Copula.IntervalPartition.uniform (n + 1) ⋯))
:
0 ≤ Verification.checkerboardEstimator A - A.checkerboard.chatterjeeXi ∧ Verification.checkerboardEstimator A - A.checkerboard.chatterjeeXi ≤ 1 / (↑n + 1) / 2
theorem
Papers.Rockel2025Approximation.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 : ℕ) => Verification.checkerboardEstimator (A k) - (A k).checkerboard.chatterjeeXi) Filter.atTop
(nhds 0)
theorem
Papers.Rockel2025Approximation.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 : ℕ) => Verification.checkerboardEstimator (A k)) Filter.atTop (nhds l) ↔ Filter.Tendsto (fun (k : ℕ) => (A k).checkerboard.chatterjeeXi) Filter.atTop (nhds l)
theorem
Papers.Rockel2025Approximation.majorization_sum_sq
(a b : ℕ → ℝ)
(n : ℕ)
(hb : ∀ i < n - 1, b (i + 1) ≤ b i)
(hp : ∀ k ≤ n, ∑ i ∈ Finset.range k, b i ≤ ∑ i ∈ Finset.range k, a i)
(ht : ∑ i ∈ Finset.range n, a i = ∑ i ∈ Finset.range n, b i)
: