← Mathematical handbook

theorem Verification.uniform_overlap_candidates (K n : ℕ) (hK : 0 < K) (hn : 0 < n) (hKn : K ≤ n) (i : Fin K) (r : Fin n) (h : 0 < cellOverlap (ProbabilityTheory.Copula.IntervalPartition.uniform K hK) (ProbabilityTheory.Copula.IntervalPartition.uniform n hn) i r) : ↑i = ↑r * K / n ∨ ↑i = ↑r * K / n + 1

A fine rank cell can overlap only these two explicitly computable coarse bins.

theorem Verification.uniform_overlap_two_slots (K n : ℕ) (hK : 0 < K) (hn : 0 < n) (hKn : K ≤ n) (i : Fin K) (r : Fin n) : (∑ b : Fin 2, if ↑i = ↑r * K / n + ↑b then cellOverlap (ProbabilityTheory.Copula.IntervalPartition.uniform K hK) (ProbabilityTheory.Copula.IntervalPartition.uniform n hn) i r else 0) = cellOverlap (ProbabilityTheory.Copula.IntervalPartition.uniform K hK) (ProbabilityTheory.Copula.IntervalPartition.uniform n hn) i r

theorem Verification.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) : ((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 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 cellOverlap (ProbabilityTheory.Copula.IntervalPartition.uniform K hK) (ProbabilityTheory.Copula.IntervalPartition.uniform n hn) j (ry k) else 0

Four candidate slots per observation reconstruct the exact source matrix. The two candidate indices in each coordinate are obtained by integer division.