Padding to a given level, and the product of two presentations

Two constructions the answer-reduced sampler needs (sec:ar-verifier, ld_compiler.tex): its CL functions are the direct sums of the oracularized sampler's, with ℓ levels, and the downsized PCP sampler's, with three, on disjoint registers, at the common level max ℓ 3.

• CLFun.liftTo T L h P pads P with trivial levels to exactly L ≥ ℓ levels (liftN pads by a number of levels, and ℓ + (L - ℓ) is not L by definition, so the level is cast along castLevel). Evaluation and exactness are unchanged (eval_liftTo, ExactlyOn.liftTo).
• CLFun.prod P Q is the presentation on ι ⊕ κ running P on the left coordinates and Q on the right: the paper's direct sum on V₁ ⊕ V₂, as directSum of the two embeddings. It is exact on everything when both are (ExactlyOn.prod), and evaluates componentwise (eval_prod).

Casting and padding the level

def MIPRE.CL.CLFun.castLevel {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {a b : ℕ} (h : a = b) (P : CLFun F ι a) : CLFun F ι b

A presentation with a levels as one with b = a levels.

Equations

• MIPRE.CL.CLFun.castLevel h P = h ▸ P

theorem MIPRE.CL.CLFun.ExactlyOn.castLevel {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {a b : ℕ} (h : a = b) {P : CLFun F ι a} {T : Finset ι} (hP : P.ExactlyOn T) : (CLFun.castLevel h P).ExactlyOn T

@[simp]

theorem MIPRE.CL.CLFun.eval_castLevel {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {a b : ℕ} (h : a = b) (P : CLFun F ι a) (x : ι → F) : (castLevel h P).eval x = P.eval x

@[simp]

theorem MIPRE.CL.CLFun.truncate_castLevel {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {a b : ℕ} (h : a = b) (P : CLFun F ι a) (j : ℕ) : truncate j (castLevel h P) = truncate j P

@[simp]

theorem MIPRE.CL.CLFun.factorOfPrefix_castLevel {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {a b : ℕ} (h : a = b) (P : CLFun F ι a) (j : ℕ) (u : ι → F) : (castLevel h P).factorOfPrefix j u = P.factorOfPrefix j u

@[simp]

theorem MIPRE.CL.CLFun.mapOfPrefix_castLevel {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {a b : ℕ} (h : a = b) (P : CLFun F ι a) (j : ℕ) (u : ι → F) : (castLevel h P).mapOfPrefix j u = P.mapOfPrefix j u

def MIPRE.CL.CLFun.liftTo {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} (T : Finset ι) (L : ℕ) (h : ℓ ≤ L) (P : CLFun F ι ℓ) : CLFun F ι L

Pad to exactly L levels, the extra levels trivial on V_T.

Equations

• MIPRE.CL.CLFun.liftTo T L h P = MIPRE.CL.CLFun.castLevel ⋯ (MIPRE.CL.CLFun.liftN T (L - ℓ) P)

theorem MIPRE.CL.CLFun.ExactlyOn.liftTo {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} {P : CLFun F ι ℓ} {T : Finset ι} (hP : P.ExactlyOn T) (L : ℕ) (h : ℓ ≤ L) : (CLFun.liftTo T L h P).ExactlyOn T

@[simp]

theorem MIPRE.CL.CLFun.eval_liftTo {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} [Fintype ι] (T : Finset ι) (L : ℕ) (h : ℓ ≤ L) (P : CLFun F ι ℓ) (x : ι → F) : (liftTo T L h P).eval x = P.eval x

The product of two presentations

noncomputable def MIPRE.CL.CLFun.prod {F : Type u_1} [Semiring F] {ι : Type u_2} {κ : Type u_3} [DecidableEq ι] [DecidableEq κ] {ℓ : ℕ} (P : CLFun F ι ℓ) (Q : CLFun F κ ℓ) : CLFun F (ι ⊕ κ) ℓ

The product: P on the left coordinates, Q on the right.

Equations

• P.prod Q = (MIPRE.CL.CLFun.embed Function.Embedding.inl P).directSum (MIPRE.CL.CLFun.embed Function.Embedding.inr Q)

theorem MIPRE.CL.CLFun.disjoint_map_inl_inr {ι : Type u_2} {κ : Type u_3} (S : Finset ι) (S' : Finset κ) : Disjoint (Finset.map Function.Embedding.inl S) (Finset.map Function.Embedding.inr S')

theorem MIPRE.CL.CLFun.ExactlyOn.prod {F : Type u_1} [Semiring F] {ι : Type u_2} {κ : Type u_3} [DecidableEq ι] [DecidableEq κ] {ℓ : ℕ} [Fintype ι] [Fintype κ] {P : CLFun F ι ℓ} {Q : CLFun F κ ℓ} (hP : P.ExactlyOn Finset.univ) (hQ : Q.ExactlyOn Finset.univ) : (P.prod Q).ExactlyOn Finset.univ

theorem MIPRE.CL.CLFun.eval_prod {F : Type u_1} [Semiring F] {ι : Type u_2} {κ : Type u_3} [DecidableEq ι] [DecidableEq κ] {ℓ : ℕ} [Fintype ι] [Fintype κ] (P : CLFun F ι ℓ) (Q : CLFun F κ ℓ) (hP : P.ExactlyOn Finset.univ) (hQ : Q.ExactlyOn Finset.univ) (x : ι ⊕ κ → F) : (P.prod Q).eval x = Sum.elim (P.eval fun (i : ι) => x (Sum.inl i)) (Q.eval fun (j : κ) => x (Sum.inr j))

The queries of a direct sum

A sampler answers marginal, linear-map and factor queries (truncate, mapOfPrefix, factorOfPrefix). For a direct sum of presentations on disjoint register subspaces each query is answered componentwise; for a padded presentation, as for the unpadded one.

theorem MIPRE.CL.CLFun.SupportedOn.factorOfPrefix_proj {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} [Fintype ι] {P : CLFun F ι ℓ} {T U : Finset ι} (hP : P.SupportedOn T) (h : T ⊆ U) (j : ℕ) (u : ι → F) : P.factorOfPrefix j ((proj U) u) = P.factorOfPrefix j u

A presentation on V_T reads its prefix only on T.

theorem MIPRE.CL.CLFun.SupportedOn.mapOfPrefix_proj {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} [Fintype ι] {P : CLFun F ι ℓ} {T U : Finset ι} (hP : P.SupportedOn T) (h : T ⊆ U) (j : ℕ) (u : ι → F) : P.mapOfPrefix j ((proj U) u) = P.mapOfPrefix j u

A presentation on V_T reads its prefix only on T.

theorem MIPRE.CL.CLFun.sdiff_subset_compl_union {ι : Type u_2} [DecidableEq ι] [Fintype ι] {S S' T T' : Finset ι} (hS' : S' ⊆ T') (hTT' : Disjoint T T') : T \ S ⊆ (S ∪ S')ᶜ

theorem MIPRE.CL.CLFun.sdiff_subset_compl {ι : Type u_2} [DecidableEq ι] [Fintype ι] {S T : Finset ι} : T \ S ⊆ Sᶜ

theorem MIPRE.CL.CLFun.factorOfPrefix_directSum {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} [Fintype ι] {P Q : CLFun F ι ℓ} {T T' : Finset ι} (hP : P.SupportedOn T) (hQ : Q.SupportedOn T') (hTT' : Disjoint T T') (j : ℕ) (u : ι → F) : (P.directSum Q).factorOfPrefix j u = P.factorOfPrefix j u ∪ Q.factorOfPrefix j u

theorem MIPRE.CL.CLFun.mapOfPrefix_directSum {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} [Fintype ι] {P Q : CLFun F ι ℓ} {T T' : Finset ι} (hP : P.SupportedOn T) (hQ : Q.SupportedOn T') (hTT' : Disjoint T T') (j : ℕ) (u : ι → F) : (P.directSum Q).mapOfPrefix j u = P.mapOfPrefix j u + Q.mapOfPrefix j u

theorem MIPRE.CL.CLFun.eval_truncate_directSum {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} [Fintype ι] {P Q : CLFun F ι ℓ} {T T' : Finset ι} (hP : P.SupportedOn T) (hQ : Q.SupportedOn T') (hTT' : Disjoint T T') (j : ℕ) (x : ι → F) : (truncate j (P.directSum Q)).eval x = (truncate j P).eval x + (truncate j Q).eval x

The queries of a padded presentation

theorem MIPRE.CL.CLFun.eval_truncate_lift {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} [Fintype ι] (T : Finset ι) (P : CLFun F ι ℓ) (j : ℕ) (x : ι → F) : (truncate j (lift T P)).eval x = (truncate j P).eval x

theorem MIPRE.CL.CLFun.factorOfPrefix_lift {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} [Fintype ι] {P : CLFun F ι ℓ} {T : Finset ι} (hP : P.ExactlyOn T) (j : ℕ) (u : ι → F) : (lift T P).factorOfPrefix j u = P.factorOfPrefix j u

theorem MIPRE.CL.CLFun.mapOfPrefix_lift {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} [Fintype ι] (T : Finset ι) (P : CLFun F ι ℓ) (j : ℕ) (u : ι → F) : (lift T P).mapOfPrefix j u = P.mapOfPrefix j u

theorem MIPRE.CL.CLFun.eval_truncate_liftN {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} [Fintype ι] (T : Finset ι) (n : ℕ) (P : CLFun F ι ℓ) (j : ℕ) (x : ι → F) : (truncate j (liftN T n P)).eval x = (truncate j P).eval x

theorem MIPRE.CL.CLFun.factorOfPrefix_liftN {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} [Fintype ι] {P : CLFun F ι ℓ} {T : Finset ι} (hP : P.ExactlyOn T) (n j : ℕ) (u : ι → F) : (liftN T n P).factorOfPrefix j u = P.factorOfPrefix j u

theorem MIPRE.CL.CLFun.mapOfPrefix_liftN {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} [Fintype ι] (T : Finset ι) (n : ℕ) (P : CLFun F ι ℓ) (j : ℕ) (u : ι → F) : (liftN T n P).mapOfPrefix j u = P.mapOfPrefix j u

@[simp]

theorem MIPRE.CL.CLFun.eval_truncate_liftTo {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} [Fintype ι] (T : Finset ι) (L : ℕ) (h : ℓ ≤ L) (P : CLFun F ι ℓ) (j : ℕ) (x : ι → F) : (truncate j (liftTo T L h P)).eval x = (truncate j P).eval x

theorem MIPRE.CL.CLFun.factorOfPrefix_liftTo {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} [Fintype ι] {P : CLFun F ι ℓ} {T : Finset ι} (hP : P.ExactlyOn T) (L : ℕ) (h : ℓ ≤ L) (j : ℕ) (u : ι → F) : (liftTo T L h P).factorOfPrefix j u = P.factorOfPrefix j u

@[simp]

theorem MIPRE.CL.CLFun.mapOfPrefix_liftTo {F : Type u_1} [Semiring F] {ι : Type u_2} [DecidableEq ι] {ℓ : ℕ} [Fintype ι] (T : Finset ι) (L : ℕ) (h : ℓ ≤ L) (P : CLFun F ι ℓ) (j : ℕ) (u : ι → F) : (liftTo T L h P).mapOfPrefix j u = P.mapOfPrefix j u

The queries of a product

theorem MIPRE.CL.CLFun.eval_truncate_prod {F : Type u_1} [Semiring F] {ι : Type u_2} {κ : Type u_3} [DecidableEq ι] [DecidableEq κ] {ℓ : ℕ} [Fintype ι] [Fintype κ] (P : CLFun F ι ℓ) (Q : CLFun F κ ℓ) (hP : P.ExactlyOn Finset.univ) (hQ : Q.ExactlyOn Finset.univ) (j : ℕ) (x : ι ⊕ κ → F) : (truncate j (P.prod Q)).eval x = Sum.elim ((truncate j P).eval fun (i : ι) => x (Sum.inl i)) ((truncate j Q).eval fun (i : κ) => x (Sum.inr i))

theorem MIPRE.CL.CLFun.factorOfPrefix_prod {F : Type u_1} [Semiring F] {ι : Type u_2} {κ : Type u_3} [DecidableEq ι] [DecidableEq κ] {ℓ : ℕ} [Fintype ι] [Fintype κ] (P : CLFun F ι ℓ) (Q : CLFun F κ ℓ) (hP : P.ExactlyOn Finset.univ) (hQ : Q.ExactlyOn Finset.univ) (j : ℕ) (u : ι ⊕ κ → F) : (P.prod Q).factorOfPrefix j u = Finset.map Function.Embedding.inl (P.factorOfPrefix j fun (i : ι) => u (Sum.inl i)) ∪ Finset.map Function.Embedding.inr (Q.factorOfPrefix j fun (i : κ) => u (Sum.inr i))

theorem MIPRE.CL.CLFun.mapOfPrefix_prod {F : Type u_1} [Semiring F] {ι : Type u_2} {κ : Type u_3} [DecidableEq ι] [DecidableEq κ] {ℓ : ℕ} [Fintype ι] [Fintype κ] (P : CLFun F ι ℓ) (Q : CLFun F κ ℓ) (hP : P.ExactlyOn Finset.univ) (hQ : Q.ExactlyOn Finset.univ) (j : ℕ) (u y : ι ⊕ κ → F) : ((P.prod Q).mapOfPrefix j u) y = Sum.elim ((P.mapOfPrefix j fun (i : ι) => u (Sum.inl i)) fun (i : ι) => y (Sum.inl i)) ((Q.mapOfPrefix j fun (i : κ) => u (Sum.inr i)) fun (i : κ) => y (Sum.inr i))