Section 12 pasting: distinct tuple distribution bound

The total variation distance between the uniform distribution on all point tuples and the distribution restricted to distinct tuples.

theorem MIPStarRE.LDT.Pasting.ldDnoteq (params : Parameters) (k : ℕ) : totalVariationDistance (uniformDistribution (PointTuple params k)) (distinctTupleDistribution params k) ≤ ↑k ^ 2 / ↑params.q

prop:ld-dnoteq.