← Mathematical handbook

Statistical consistency, exact rank binning, and unit-cost work

theorem Papers.Rockel2025Approximation.majorization_sum_convex (a b : ℕ → ℝ) (n : ℕ) (f : ℝ → ℝ) (hf : ConvexOn ℝ Set.univ f) (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) : ∑ i ∈ Finset.range n, f (b i) ≤ ∑ i ∈ Finset.range n, f (a i)

theorem Papers.Rockel2025Approximation.rankCopula_cellMass {m r n : ℕ} (hn : 0 < n) (rx ry : Equiv.Perm (Fin n)) (P : ProbabilityTheory.Copula.IntervalPartition m) (Q : ProbabilityTheory.Copula.IntervalPartition r) (i : Fin m) (j : Fin r) : ((Verification.rankCopula n hn rx ry).cellMass P Q).mass i j = ↑n * ∑ k : Fin n, Verification.cellOverlap P (ProbabilityTheory.Copula.IntervalPartition.uniform n hn) i (rx k) * Verification.cellOverlap Q (ProbabilityTheory.Copula.IntervalPartition.uniform n hn) j (ry k)

theorem Papers.Rockel2025Approximation.sampleRankCopula_ae_rate {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (C : ProbabilityTheory.Copula 2) (X : ℕ → Ω → Fin 2 → ↑unitInterval) (hX : ∀ (i : ℕ), Measurable (X i)) (hI : ProbabilityTheory.iIndepFun X μ) (hlaw : ∀ (i : ℕ), MeasureTheory.Measure.map (X i) μ = C.toMeasure) : ∀ᵐ (ω : Ω) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (u v : ↑unitInterval), |(Verification.sampleRankCopula X n ω).cdf ![u, v] - C.cdf ![u, v]| ≤ 3 * Verification.empiricalCDFRadius n + 8 / (↑n + 1)

theorem Papers.Rockel2025Approximation.sampleCheckerboardEstimator_ae_tendsto {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (C : ProbabilityTheory.Copula 2) (X : ℕ → Ω → Fin 2 → ↑unitInterval) (hX : ∀ (i : ℕ), Measurable (X i)) (hI : ProbabilityTheory.iIndepFun X μ) (hlaw : ∀ (i : ℕ), MeasureTheory.Measure.map (X i) μ = C.toMeasure) (κ : ℝ) (hκ : 0 < κ) (hκ' : κ ≤ 1 / 3) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => Verification.sampleCheckerboardEstimator X κ n ω) Filter.atTop (nhds C.chatterjeeXi)

theorem Papers.Rockel2025Approximation.realSampleCheckerboardEstimator_ae_tendsto {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)) (hc : ∀ (d : Fin 2), Continuous ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal ν d))) (X : ℕ → Ω → Fin 2 → ℝ) (hX : ∀ (i : ℕ), Measurable (X i)) (hI : ProbabilityTheory.iIndepFun X μ) (hlaw : ∀ (i : ℕ), MeasureTheory.Measure.map (X i) μ = ↑ν) (κ : ℝ) (hκ : 0 < κ) (hκ' : κ ≤ 1 / 3) : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (n : ℕ) => Verification.realSampleCheckerboardEstimator X κ n ω) Filter.atTop (nhds (ProbabilityTheory.Copula.ofContinuousMarginals ν hc).chatterjeeXi)

theorem Papers.Rockel2025Approximation.rankCopula_cellMass_four_slots (K n : ℕ) (hK : 0 < K) (hn : 0 < n) (hKn : K ≤ n) (rx ry : Equiv.Perm (Fin n)) (i j : Fin K) : ((Verification.rankCopula n hn rx ry).cellMass (ProbabilityTheory.Copula.IntervalPartition.uniform K hK) (ProbabilityTheory.Copula.IntervalPartition.uniform K hK)).mass i j = ↑n * ∑ k : Fin n, ∑ a : Fin 2, ∑ b : Fin 2, (if ↑i = ↑(rx k) * K / n + ↑a then Verification.cellOverlap (ProbabilityTheory.Copula.IntervalPartition.uniform K hK) (ProbabilityTheory.Copula.IntervalPartition.uniform n hn) i (rx k) else 0) * if ↑j = ↑(ry k) * K / n + ↑b then Verification.cellOverlap (ProbabilityTheory.Copula.IntervalPartition.uniform K hK) (ProbabilityTheory.Copula.IntervalPartition.uniform n hn) j (ry k) else 0

theorem Papers.Rockel2025Approximation.checkerboardEstimatorWork_isBigO {α : Type u_1} {β : Type u_2} (leX : α → α → Bool) (leY : β → β → Bool) (xs : ℕ → List α) (ys : ℕ → List β) (hx : ∀ (n : ℕ), (xs n).length = n + 1) (hy : ∀ (n : ℕ), (ys n).length = n + 1) (κ : ℝ) (hκ : 0 ≤ κ) (hκ' : κ ≤ 1 / 3) : (fun (n : ℕ) => ↑(Verification.checkerboardEstimatorWork leX leY (xs n) (ys n) (Verification.powerGridIndex κ n + 1))) =O[Filter.atTop] fun (n : ℕ) => (↑n + 1) * Real.log (↑n + 1)