Proof of `A tuple sampler with alphabet-independent mixing` (3rd statement)
groundedproofs/Lax253009Proofs/TupleSampler.lean · lax-253009
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Test the centered sampler density against its sign. The adjoint identity turns this pairing into the restricted centered tuple average, whose second moment has already been bounded independently of the alphabet.