A polynomial on a block of the variables

A coefficient vector in n variables read on a block of them, as a coefficient vector in the block's n' variables (LowIndDegPoly.blockPoly), and the exponent vectors that carry it (expandIdx). Moved from MIPRE/Background/QLD/Complete.lean, where the Pauli basis test's completion uses them, so that answer reduction can use them without importing that test.

A polynomial on a block of the variables

noncomputable def MIPRE.LIDT.expandIdx {n n' d : ℕ} (idx : Fin n' → Fin n) (e' : Fin n' → Fin (d + 1)) : Fin n → Fin (d + 1)

The exponent vector on Fin n carried by the injection idx from one on Fin n', zero off the range.

Equations

• MIPRE.LIDT.expandIdx idx e' k = if h : ∃ (j : Fin n'), idx j = k then e' h.choose else 0

theorem MIPRE.LIDT.expandIdx_apply_idx {n n' d : ℕ} {idx : Fin n' → Fin n} (hinj : Function.Injective idx) (e' : Fin n' → Fin (d + 1)) (j : Fin n') : expandIdx idx e' (idx j) = e' j

theorem MIPRE.LIDT.expandIdx_apply_of_not {n n' d : ℕ} {idx : Fin n' → Fin n} (e' : Fin n' → Fin (d + 1)) {k : Fin n} (hk : ∀ (j : Fin n'), idx j ≠ k) : expandIdx idx e' k = 0

theorem MIPRE.LIDT.prod_pow_expandIdx {F : Type u_1} [Field F] {n n' d : ℕ} {idx : Fin n' → Fin n} (hinj : Function.Injective idx) (u : Point F n) (e' : Fin n' → Fin (d + 1)) : ∏ k : Fin n, u k ^ ↑(expandIdx idx e' k) = ∏ j : Fin n', u (idx j) ^ ↑(e' j)

The monomial of an expanded exponent vector is the monomial on the block.

noncomputable def MIPRE.LIDT.LowIndDegPoly.blockPoly {F : Type u_1} {n n' d : ℕ} (idx : Fin n' → Fin n) (H : LowIndDegPoly) : LowIndDegPoly

A coefficient vector read on a block of the variables, as a coefficient vector on the block.

Equations

• MIPRE.LIDT.LowIndDegPoly.blockPoly idx H e' = H (MIPRE.LIDT.expandIdx idx e')

theorem MIPRE.LIDT.LowIndDegPoly.eval_blockPoly {F : Type u_1} [Field F] {n n' d : ℕ} {idx : Fin n' → Fin n} (hinj : Function.Injective idx) {H : LowIndDegPoly} (hsupp : ∀ (e : Fin n → Fin (d + 1)), H e ≠ 0 → ∀ (k : Fin n), (∀ (j : Fin n'), idx j ≠ k) → e k = 0) (u : Point F n) : ((blockPoly idx H).eval fun (j : Fin n') => u (idx j)) = H.eval u

A vector supported on the range of idx evaluates through the block.

def MIPRE.LIDT.LowIndDegPoly.liftIdx {F : Type u_1} [Field F] {n n' d : ℕ} (idx : Fin n' → Fin n) (g : LowIndDegPoly) : LowIndDegPoly

A coefficient vector in a block's variables, placed on the block: zero on every monomial that reads a variable off the block.

Equations

• MIPRE.LIDT.LowIndDegPoly.liftIdx idx g e = if ∀ (k : Fin n), (∀ (j : Fin n'), idx j ≠ k) → e k = 0 then g fun (j : Fin n') => e (idx j) else 0

theorem MIPRE.LIDT.LowIndDegPoly.blockPoly_liftIdx {F : Type u_1} [Field F] {n n' d : ℕ} {idx : Fin n' → Fin n} (hinj : Function.Injective idx) (g : LowIndDegPoly) : blockPoly idx (liftIdx idx g) = g

Reading a placed vector back on its block gives it back.

theorem MIPRE.LIDT.LowIndDegPoly.eval_liftIdx {F : Type u_1} [Field F] {n n' d : ℕ} {idx : Fin n' → Fin n} (hinj : Function.Injective idx) (g : LowIndDegPoly) (u : Point F n) : (liftIdx idx g).eval u = g.eval fun (j : Fin n') => u (idx j)

A placed vector evaluates through the block.