Proof of `Mixed moments of balanced predicates on independent coordinates` (3rd statement)
groundedproofs/Lax323828Proofs/ProductMoments.lean · lax-323828
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
Expand the square, interchange finite sums and expectations, and cancel every pair of distinct supports using the balanced mixed-moment identity.