Summing over assignments to a block-decomposed index type #
A construction that reads only some coordinates of a uniformly random point needs to know that those coordinates are themselves uniform, and independent of the rest. In the form a sum identity takes, that is: when the index type is a sum, summing a function of the blocks' assignments over all assignments to the whole gives the iterated sum over the blocks --- once per assignment of whatever block the function ignores.
sum_arrow_pair--- both blocks, which is the product measure written as an iterated sum;sum_arrow_inl--- the left block alone, at the cost of one factor of the right block's count.
Nothing here is about fields, lines or games. The only reason the file exists is that the padded
space of the combining stage (MIPRE/Background/QLD/Padded.lean) is F_q^{4m} with its coordinates
split into blocks, and every distributional statement about that splitting reduces to these two.
An assignment to a sum index type is a pair of assignments to the summands. Spelled out rather
than taken from Equiv.sumArrowEquivProdArrow so that both directions compute by rfl.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Both blocks of a uniform assignment are uniform and independent.
The left block of a uniform assignment is uniform, each value counted once per assignment to the right block.
Rewriting, reordering and scaling nested sums #
A block decomposition turns one sum into two, and the new sums appear where the old one was. Getting
from there to a statement about each block's own law is bookkeeping: rewrite a sum that sits under
others, move one sum past its neighbours, and pull a constant multiplier out. These are the three
moves, stated at the arities the padded space needs, so that a proof can name the step it is taking
instead of rebuilding a Finset.sum_congr tower each time.
Moving the second of six nested sums inwards past the next two. A block decomposition produces the two sides' data interleaved, and this is what puts each side's data back together.
Swapping the fourth and fifth of six nested sums.
Only the first component of a pair is read.
Marginals of a uniform average #
A uniform average of a quantity that depends on only part of the sample is the uniform average over that part. Stated once, for an arbitrary splitting of the sample space given as an equivalence with a product, it is what relates the Pauli basis test's single content --- which carries both sides' points but one seed and one raw direction --- to a product of two independent line-point laws: each side's own data has the same marginal under both.