Blocks of a cube, and marginals

An assignment tester makes several reads, each with its own randomness. The Fourier layer supplies probability over one cube point (Pr) and over a pair (Pr₂), but not over k independent points, and building a k-fold product measure would be a detour.

The alternative taken here is to bundle: the tester's whole random string is a single point of a larger cube, and each read uses its own block. What makes this work is that the uniform measure on the big cube restricts to the uniform measure on each block — proved below — so the existing one-variable lemmas apply to each read, and the existing union bound combines them.

Main definitions

• Complexity.leftBlock, Complexity.rightBlock — the two halves of a point

Main results

• Complexity.prob_leftBlock, Complexity.prob_rightBlock — a block is uniformly distributed
• Complexity.prob_forall_ge — the union bound combining many reads
• Complexity.prob_leftBlock_rightBlock — marginals compose, so any fixed number of blocks can be bundled
• Complexity.prob₂_eq_prob_blocks — a probability over a pair is a probability over one bundled point
• Complexity.prob_le_of_imp_of_good — transferring an observed acceptance probability along a likely good event
• Complexity.prob_blocks, Complexity.prob_blocks_ge — conditioning on an earlier block, so a read point may depend on earlier randomness

def Complexity.leftBlock {a b : ℕ} (z : BooleanAnalysis.Cube (a + b)) : BooleanAnalysis.Cube a

The first block of a point of the combined cube.

Equations

• Complexity.leftBlock z i = z (Fin.castAdd b i)

def Complexity.rightBlock {a b : ℕ} (z : BooleanAnalysis.Cube (a + b)) : BooleanAnalysis.Cube b

The second block of a point of the combined cube.

Equations

• Complexity.rightBlock z j = z (Fin.natAdd a j)

theorem Complexity.leftBlock_append {a b : ℕ} (x : BooleanAnalysis.Cube a) (y : BooleanAnalysis.Cube b) : leftBlock (Fin.append x y) = x

theorem Complexity.rightBlock_append {a b : ℕ} (x : BooleanAnalysis.Cube a) (y : BooleanAnalysis.Cube b) : rightBlock (Fin.append x y) = y

noncomputable def Complexity.cubeBlockEquiv (a b : ℕ) : BooleanAnalysis.Cube a × BooleanAnalysis.Cube b ≃ BooleanAnalysis.Cube (a + b)

Splitting a point of the combined cube into its blocks is a bijection.

Equations

• Complexity.cubeBlockEquiv a b = Fin.appendEquiv a b

theorem Complexity.leftBlock_blockEquiv {a b : ℕ} (p : BooleanAnalysis.Cube a × BooleanAnalysis.Cube b) : leftBlock ((cubeBlockEquiv a b) p) = p.1

theorem Complexity.rightBlock_blockEquiv {a b : ℕ} (p : BooleanAnalysis.Cube a × BooleanAnalysis.Cube b) : rightBlock ((cubeBlockEquiv a b) p) = p.2

theorem Complexity.prob_leftBlock {a b : ℕ} (P : BooleanAnalysis.Cube a → Prop) : (BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (a + b)) => P (leftBlock z)) = BooleanAnalysis.prob P

The first block is uniform. A predicate depending only on the first block has the same probability over the combined cube as over its own.

theorem Complexity.prob_rightBlock {a b : ℕ} (P : BooleanAnalysis.Cube b → Prop) : (BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (a + b)) => P (rightBlock z)) = BooleanAnalysis.prob P

The second block is uniform too.

A union bound over many reads

theorem Complexity.prob_of_forall {m : ℕ} {P : BooleanAnalysis.Cube m → Prop} (h : ∀ (x : BooleanAnalysis.Cube m), P x) : BooleanAnalysis.prob P = 1

theorem Complexity.prob_forall_ge {m : ℕ} (k : ℕ) (P : Fin k → BooleanAnalysis.Cube m → Prop) (ε : ℝ) : (∀ (i : Fin k), 1 - ε ≤ BooleanAnalysis.prob (P i)) → 1 - ↑k * ε ≤ BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube m) => ∀ (i : Fin k), P i z

Union bound over k events. If each of k events holds except with probability ε, all hold except with probability k · ε. With the tester's randomness bundled into one point, each read's correctness is an event on that point, so this is the bound that combines them.

Composed blocks

theorem Complexity.prob_leftBlock_rightBlock {a b c : ℕ} (P : BooleanAnalysis.Cube b → Prop) : (BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (a + (b + c))) => P (leftBlock (rightBlock z))) = BooleanAnalysis.prob P

Marginals compose: a block of a block is still uniform. Iterating this gives a bundled random string with any fixed number of independent blocks, which is all a tester with constantly many reads needs.

theorem Complexity.prob_rightBlock_rightBlock {a b c : ℕ} (P : BooleanAnalysis.Cube c → Prop) : (BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (a + (b + c))) => P (rightBlock (rightBlock z))) = BooleanAnalysis.prob P

Pairs are two blocks

theorem Complexity.prob₂_eq_prob_blocks {n : ℕ} (P : BooleanAnalysis.Cube n → BooleanAnalysis.Cube n → Prop) : BooleanAnalysis.prob₂ P = BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (n + n)) => P (leftBlock z) (rightBlock z)

Pr₂ is a bundled Pr. The Fourier layer's probability over a pair of independent points is the probability over a single point of the doubled cube, read as two blocks.

This is the bridge that lets the pair-based statements (the consistency check) and the block-based statements (the self-corrected reads) be combined: after rewriting, both are probabilities over one cube, so a union bound applies.

theorem Complexity.prob_pair_block {n c : ℕ} (P : BooleanAnalysis.Cube n → BooleanAnalysis.Cube n → Prop) : (BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (n + n + c)) => P (leftBlock (leftBlock z)) (rightBlock (leftBlock z))) = BooleanAnalysis.prob₂ P

A pair drawn from the first block of a bundled string is a uniform pair, so a Pr₂ statement can be read as a statement about the bundled randomness that the tester's other reads also draw from.

theorem Complexity.prob_le_of_imp_of_good {m : ℕ} {E F A : BooleanAnalysis.Cube m → Prop} (h : ∀ (z : BooleanAnalysis.Cube m), E z → A z → F z) : BooleanAnalysis.prob E ≤ BooleanAnalysis.prob F + (1 - BooleanAnalysis.prob A)

Transfer along a likely good event. If E implies F whenever A holds, then E is no likelier than F plus the chance that A fails.

This is how a tester's observed acceptance is converted into a statement about the decoded tables: E is "the tester accepts", A is "every self-corrected read returned the true value", and F is the check as made on the decoded codewords.

Conditioning on an earlier block

theorem Complexity.prob_blocks {a b : ℕ} (Q : BooleanAnalysis.Cube a → BooleanAnalysis.Cube b → Prop) : (BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (a + b)) => Q (leftBlock z) (rightBlock z)) = BooleanAnalysis.expect fun (u : BooleanAnalysis.Cube a) => BooleanAnalysis.prob (Q u)

Fubini for blocks. A predicate reading both blocks has probability equal to the average, over the first block, of its conditional probability in the second.

This is what lets a tester choose where to read using early randomness and still get a uniform correction string: the read point is fixed by u, and the inner probability is the ordinary one-variable statement.

theorem Complexity.prob_blocks_ge {a b : ℕ} (Q : BooleanAnalysis.Cube a → BooleanAnalysis.Cube b → Prop) (c : ℝ) (h : ∀ (u : BooleanAnalysis.Cube a), c ≤ BooleanAnalysis.prob (Q u)) : c ≤ BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube (a + b)) => Q (leftBlock z) (rightBlock z)

A bound that holds for every earlier outcome holds overall.

theorem Complexity.prob_and_ge {m : ℕ} {P Q : BooleanAnalysis.Cube m → Prop} {p q : ℝ} (hP : 1 - p ≤ BooleanAnalysis.prob P) (hQ : 1 - q ≤ BooleanAnalysis.prob Q) : 1 - (p + q) ≤ BooleanAnalysis.prob fun (z : BooleanAnalysis.Cube m) => P z ∧ Q z

Two likely events are jointly likely. The union bound in the form the tester uses: each read fails with its own probability, and the failures add.

theorem Complexity.exists_of_prob_pos {m : ℕ} {P : BooleanAnalysis.Cube m → Prop} (h : 0 < BooleanAnalysis.prob P) : ∃ (z : BooleanAnalysis.Cube m), P z

A likely event happens. Used to turn a probabilistic guarantee about a tester's reads into a single random string on which every read is right — the argument for a check whose conclusion is deterministic.

theorem Complexity.prob_eq_card_div {m : ℕ} (P : BooleanAnalysis.Cube m → Prop) [DecidablePred P] : BooleanAnalysis.prob P = ↑(Finset.filter P Finset.univ).card / 2 ^ m

A probability is a count over the cube.