Direct sums of families of CL functions: the repeated sampler's functions

The k-fold direct sum of a family of ℓ-level CL presentations on F^ι, as an ℓ-level presentation on F^κ for any κ in bijection with Fin k × ι (CLFun.famSum): stage by stage, the register subspaces are the unions of the blocks' and the maps act blockwise. This is lem:cl-closure (direct sums) iterated over k summands, in the form the repeated sampler of thm:parallel-repetition needs: its CL function at index n is the direct sum of k copies of the input sampler's on 𝔽₂^{k s(n)}, κ = Fin (k · s(n)) and e = finProdFinEquiv.

Everything the sampler's query interface asks is blockwise (the four runs_* clauses of MIPRE.CL.Sampler), and everything the game needs is blockwise too, so the lemmas are stated at the level of evaluation rather than as equalities of presentations:

• eval_famSum: (⊕ᵢ Pᵢ)(x) = join (fun i => Pᵢ (block i x));
• eval_truncate_famSum, factorOfPrefix_famSum, mapOfPrefix_famSum: the marginals, factor spaces and stage maps read off a prefix are blockwise;
• exactlyOn_famSum: exactness is inherited (lem:cl-kth, item (2));
• clDist_famSum: the conditionally linear distribution of a direct sum is the product of the blocks' — the repeated game is the direct repetition.

The vocabulary: block e i x is the i-th block of x : κ → F, join e v assembles blocks, and blockSet e T is the register subspace assembled from one per block.

Blocks

def MIPRE.CL.block {F : Type u} {ι : Type v} {κ : Type w} {k : ℕ} (e : Fin k × ι ≃ κ) (i : Fin k) (x : κ → F) : ι → F

The i-th block of a vector on κ ≃ Fin k × ι.

Equations

• MIPRE.CL.block e i x j = x (e (i, j))

def MIPRE.CL.join {F : Type u} {ι : Type v} {κ : Type w} {k : ℕ} (e : Fin k × ι ≃ κ) (v : Fin k → ι → F) : κ → F

The vector assembled from k blocks.

Equations

• MIPRE.CL.join e v p = v (e.symm p).1 (e.symm p).2

@[simp]

theorem MIPRE.CL.block_join {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (v : Fin k → ι → F) (i : Fin k) : block e i (join e v) = v i

@[simp]

theorem MIPRE.CL.join_block {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (x : κ → F) : (join e fun (i : Fin k) => block e i x) = x

@[simp]

theorem MIPRE.CL.block_add {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (i : Fin k) (x y : κ → F) : block e i (x + y) = block e i x + block e i y

@[simp]

theorem MIPRE.CL.block_zero {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (i : Fin k) : block e i 0 = 0

@[simp]

theorem MIPRE.CL.join_apply {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (v : Fin k → ι → F) (p : κ) : join e v p = v (e.symm p).1 (e.symm p).2

@[simp]

theorem MIPRE.CL.join_apply_e {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (v : Fin k → ι → F) (i : Fin k) (j : ι) : join e v (e (i, j)) = v i j

theorem MIPRE.CL.join_eq_iff {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (v : Fin k → ι → F) (x : κ → F) : join e v = x ↔ ∀ (i : Fin k), v i = block e i x

def MIPRE.CL.blockEquiv {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) : (κ → F) ≃ (Fin k → ι → F)

The blocks of a vector, as an equivalence.

Equations

• MIPRE.CL.blockEquiv e = { toFun := fun (x : κ → F) (i : Fin k) => MIPRE.CL.block e i x, invFun := MIPRE.CL.join e, left_inv := ⋯, right_inv := ⋯ }

def MIPRE.CL.blockSet {ι : Type v} [DecidableEq ι] {κ : Type w} [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (T : Fin k → Finset ι) : Finset κ

The register subspace assembled from one register subspace per block.

Equations

• MIPRE.CL.blockSet e T = {p : κ | (e.symm p).2 ∈ T (e.symm p).1}

@[simp]

theorem MIPRE.CL.mem_blockSet {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (T : Fin k → Finset ι) (p : κ) : p ∈ blockSet e T ↔ (e.symm p).2 ∈ T (e.symm p).1

theorem MIPRE.CL.e_mem_blockSet {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (T : Fin k → Finset ι) (i : Fin k) (j : ι) : e (i, j) ∈ blockSet e T ↔ j ∈ T i

theorem MIPRE.CL.blockSet_compl {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (T : Fin k → Finset ι) : (blockSet e T)ᶜ = blockSet e fun (i : Fin k) => (T i)ᶜ

theorem MIPRE.CL.blockSet_sdiff {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (T T' : Fin k → Finset ι) : blockSet e T \ blockSet e T' = blockSet e fun (i : Fin k) => T i \ T' i

theorem MIPRE.CL.blockSet_subset {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) {T T' : Fin k → Finset ι} (h : ∀ (i : Fin k), T i ⊆ T' i) : blockSet e T ⊆ blockSet e T'

theorem MIPRE.CL.blockSet_eq_empty_iff {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (T : Fin k → Finset ι) : blockSet e T = ∅ ↔ ∀ (i : Fin k), T i = ∅

@[simp]

theorem MIPRE.CL.blockSet_univ {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) : (blockSet e fun (x : Fin k) => Finset.univ) = Finset.univ

theorem MIPRE.CL.block_proj {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (T : Fin k → Finset ι) (i : Fin k) (x : κ → F) : block e i ((proj (blockSet e T)) x) = (proj (T i)) (block e i x)

Direct sums of register-linear maps

def MIPRE.CL.RegLinear.blockSum {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) {T : Fin k → Finset ι} (L : (i : Fin k) → RegLinear F (T i)) : RegLinear F (blockSet e T)

The direct sum of a family of maps, one per block.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.CL.RegLinear.blockSum_apply {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) {T : Fin k → Finset ι} (L : (i : Fin k) → RegLinear F (T i)) (x : κ → F) : (blockSum e L) x = join e fun (i : Fin k) => (L i) (block e i x)

Direct sums of families of presentations

def MIPRE.CL.CLFun.hdS {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] {ℓ : ℕ} : CLFun F ι (ℓ + 1) → Finset ι

The register subspace at the head of a presentation of positive level.

Equations

• (MIPRE.CL.CLFun.cons S L₁ next).hdS = S

def MIPRE.CL.CLFun.hdL {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] {ℓ : ℕ} (P : CLFun F ι (ℓ + 1)) : RegLinear F P.hdS

The map at the head of a presentation of positive level.

Equations

• (MIPRE.CL.CLFun.cons S L₁ next).hdL = match MIPRE.CL.CLFun.cons S L₁ next with | MIPRE.CL.CLFun.cons S L₁ next => L₁

def MIPRE.CL.CLFun.tl {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] {ℓ : ℕ} : CLFun F ι (ℓ + 1) → (ι → F) → CLFun F ι ℓ

The continuation of a presentation of positive level.

Equations

• (MIPRE.CL.CLFun.cons S L₁ next).tl = next

theorem MIPRE.CL.CLFun.eta {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {ℓ : ℕ} (P : CLFun F ι (ℓ + 1)) : P = cons P.hdS P.hdL P.tl

def MIPRE.CL.CLFun.famSum {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (ℓ : ℕ) : (Fin k → CLFun F ι ℓ) → CLFun F κ ℓ

The direct sum of a family of presentations, one per block, on F^κ, κ ≃ Fin k × ι.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.CL.CLFun.famSum e 0 x_2 = MIPRE.CL.CLFun.zero

@[simp]

theorem MIPRE.CL.CLFun.famSum_zero {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (P : Fin k → CLFun F ι 0) : famSum e 0 P = zero

theorem MIPRE.CL.CLFun.famSum_succ {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k ℓ : ℕ} (e : Fin k × ι ≃ κ) (S : Fin k → Finset ι) (L : (i : Fin k) → RegLinear F (S i)) (next : Fin k → (ι → F) → CLFun F ι ℓ) : (famSum e (ℓ + 1) fun (i : Fin k) => cons (S i) (L i) (next i)) = cons (blockSet e S) (RegLinear.blockSum e L) fun (v : κ → F) => famSum e ℓ fun (i : Fin k) => next i (block e i v)

theorem MIPRE.CL.CLFun.eval_famSum {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (ℓ : ℕ) (P : Fin k → CLFun F ι ℓ) (x : κ → F) : (famSum e ℓ P).eval x = join e fun (i : Fin k) => (P i).eval (block e i x)

Evaluation is blockwise.

theorem MIPRE.CL.CLFun.supportedOn_famSum {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (ℓ : ℕ) (P : Fin k → CLFun F ι ℓ) (T : Fin k → Finset ι) : (∀ (i : Fin k), (P i).SupportedOn (T i)) → (famSum e ℓ P).SupportedOn (blockSet e T)

Support is blockwise.

theorem MIPRE.CL.CLFun.exactlyOn_famSum {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (ℓ : ℕ) (P : Fin k → CLFun F ι ℓ) (T : Fin k → Finset ι) : (∀ (i : Fin k), (P i).ExactlyOn (T i)) → (famSum e ℓ P).ExactlyOn (blockSet e T)

Exactness is blockwise (lem:cl-kth, item (2), for the direct sum).

theorem MIPRE.CL.CLFun.eval_truncate_famSum {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (j ℓ : ℕ) (P : Fin k → CLFun F ι ℓ) (x : κ → F) : (truncate j (famSum e ℓ P)).eval x = join e fun (i : Fin k) => (truncate j (P i)).eval (block e i x)

The marginals are blockwise.

theorem MIPRE.CL.CLFun.factorOfPrefix_famSum {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (ℓ : ℕ) (P : Fin k → CLFun F ι ℓ) (j : ℕ) (u : κ → F) : (famSum e ℓ P).factorOfPrefix j u = blockSet e fun (i : Fin k) => (P i).factorOfPrefix j (block e i u)

The factor spaces read off a prefix are blockwise.

theorem MIPRE.CL.CLFun.mapOfPrefix_famSum {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) (ℓ : ℕ) (P : Fin k → CLFun F ι ℓ) (j : ℕ) (u y : κ → F) : ((famSum e ℓ P).mapOfPrefix j u) y = join e fun (i : Fin k) => ((P i).mapOfPrefix j (block e i u)) (block e i y)

The stage maps read off a prefix are blockwise.

The paper's statement, and the distribution

theorem MIPRE.CL.IsCLFun.famSum {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} (e : Fin k × ι ≃ κ) {ℓ : ℕ} {T : Fin k → Finset ι} {f : Fin k → (ι → F) → ι → F} (hf : ∀ (i : Fin k), IsCLFun ℓ (T i) (f i)) : IsCLFun ℓ (blockSet e T) fun (x : κ → F) => join e fun (i : Fin k) => f i (block e i x)

lem:cl-closure (direct sums), k summands: the blockwise assembly of ℓ-level CL functions on V_{T i} is an ℓ-level CL function on the assembled register subspace.

theorem MIPRE.CL.clDist_famSum {F : Type u} [Semiring F] {ι : Type v} [DecidableEq ι] [Fintype ι] {κ : Type w} [DecidableEq κ] [Fintype κ] {k : ℕ} [Fintype F] [DecidableEq F] (e : Fin k × ι ≃ κ) {ℓ : ℕ} (L R : Fin k → CLFun F ι ℓ) (a b : κ → F) : clDist (CLFun.famSum e ℓ L).eval (CLFun.famSum e ℓ R).eval a b = ∏ i : Fin k, clDist (L i).eval (R i).eval (block e i a) (block e i b)

The CL distribution of a direct sum is the product of the blocks' distributions.