Histogram collision counts for Chan–He

The native histogram counts ordered pairs of different input positions. For an injective array of integers and its Euclidean residue keys, this is exactly the existing Chan–He collision count. Injectivity is required because the mathematical reduction operates on sets. Equal input values must first be handled by the distinct-position frontend.

Main results

• coll_eq_histogramPairs: the existing coll is the counter computed by the histogram.

References

• T. M. Chan and Q. He, Reducing 3SUM to Convolution-3SUM

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.coll_eq_histogramPairs (values : ℕ → ℤ) (n M : ℕ) (hM : 0 < M) (hinj : Set.InjOn values ↑(Finset.range n)) : ThreeSum.ChanHe.coll (Finset.image values (Finset.range n)) M = Histogram.pairs (fun (i : ℕ) => (values i % ↑M).toNat) n

For distinct array values, histogramming Euclidean residues computes exactly the ordered distinct-element collision count of the existing Chan–He reduction.