Documentation

MIPRE.Background.LIDT.PresentationQueries

The queries of the three-level presentation of the seeded test #

What a sampler program must compute for Regs.pres (MIPRE/Background/LIDT/Presentation), level by level: its marginals (eval_truncate_one, eval_truncate_two, eval_pres), its stage maps read off a prefix (mapOfPrefix_zero, mapOfPrefix_one, mapOfPrefix_two) and its factor spaces (factorOfPrefix_zero, factorOfPrefix_one, factorOfPrefix_two); from the fourth level on there is nothing (mapOfPrefix_three_le, factorOfPrefix_three_le).

The seed a stage map reads is the prefix's seed coordinate, and the diagonal line's direction is the prefix's direction register, already cut down by the selector.

source
noncomputable def MIPRE.LIDT.CL.Regs.ptMap {n : ℕ} {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) :
Ty → F → Point F n → Point F n →ₗ[F] Point F n

The linear map of the point register applied at the third stage.

Equations
Instances For
    source
    theorem MIPRE.LIDT.CL.Regs.seedLin_apply {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] (t : Ty) (x : ι → F) :
    (R.seedLin t) x = if t = Ty.point then 0 else (CL.proj R.coordSet) x
    source
    theorem MIPRE.LIDT.CL.Regs.secondLin_apply {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) (s : F) (x : ι → F) :
    (R.secondLin S t s) x = if t = Ty.dline then R.putDir (zeroBelow (S.χ s) (R.dirOf x)) else 0
    source
    theorem MIPRE.LIDT.CL.Regs.finalLin_apply {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) (s : F) (v : Point F n) (x : ι → F) :
    (R.finalLin S t s v) x = R.putPt ((ptMap S t s v) (R.ptOf x))
    source
    theorem MIPRE.LIDT.CL.Regs.coord_seedLin {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) (x : ι → F) (s : F) (h : t ≠ Ty.point → x R.coord = s) :
    R.secondLin S t ((R.seedLin t) x R.coord) = R.secondLin S t s
    source
    theorem MIPRE.LIDT.CL.Regs.dirSet_subset_compl {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) :
    R.dirSet ⊆ R.coordSetᶜ
    source
    theorem MIPRE.LIDT.CL.Regs.finalSet_subset_compl {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) :
    R.finalSet ⊆ R.dirSetᶜ ∩ R.coordSetᶜ

    The marginals #

    source
    theorem MIPRE.LIDT.CL.Regs.eval_truncate_one {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) (x : ι → F) :
    (CL.CLFun.truncate 1 (R.pres S t)).eval x = (R.seedLin t) x
    source
    theorem MIPRE.LIDT.CL.Regs.eval_truncate_two {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) (x : ι → F) :
    (CL.CLFun.truncate 2 (R.pres S t)).eval x = (R.seedLin t) x + (R.secondLin S t (x R.coord)) x
    source
    theorem MIPRE.LIDT.CL.Regs.dirOf_secondLin {ι : Type u_1} [DecidableEq ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) (s : F) (x : ι → F) :
    R.dirOf ((R.secondLin S t s) x) = if t = Ty.dline then zeroBelow (S.χ s) (R.dirOf x) else 0
    source
    theorem MIPRE.LIDT.CL.Regs.eval_pres {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) (x : ι → F) :
    (R.pres S t).eval x = (R.seedLin t) x + (R.secondLin S t (x R.coord)) x + R.putPt ((ptMap S t (x R.coord) (if t = Ty.dline then zeroBelow (S.χ (x R.coord)) (R.dirOf x) else 0)) (R.ptOf x))
    source
    theorem MIPRE.LIDT.CL.Regs.eval_truncate_three_le {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) {j : ℕ} (hj : 3 ≤ j) (x : ι → F) :
    (CL.CLFun.truncate j (R.pres S t)).eval x = (R.pres S t).eval x

    The stage maps and factor spaces, read off a prefix #

    source
    theorem MIPRE.LIDT.CL.Regs.mapOfPrefix_zero {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) (u : ι → F) :
    (R.pres S t).mapOfPrefix 0 u = (R.seedLin t).toLinearMap
    source
    theorem MIPRE.LIDT.CL.Regs.mapOfPrefix_one {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) (u : ι → F) :
    (R.pres S t).mapOfPrefix 1 u = (R.secondLin S t (u R.coord)).toLinearMap
    source
    theorem MIPRE.LIDT.CL.Regs.mapOfPrefix_two {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) (u : ι → F) :
    (R.pres S t).mapOfPrefix 2 u = (R.finalLin S t (u R.coord) (R.dirOf u)).toLinearMap
    source
    theorem MIPRE.LIDT.CL.Regs.mapOfPrefix_three_le {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) {j : ℕ} (hj : 3 ≤ j) (u : ι → F) :
    (R.pres S t).mapOfPrefix j u = 0
    source
    theorem MIPRE.LIDT.CL.Regs.factorOfPrefix_zero {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) (u : ι → F) :
    (R.pres S t).factorOfPrefix 0 u = R.coordSet
    source
    theorem MIPRE.LIDT.CL.Regs.factorOfPrefix_one {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) (u : ι → F) :
    (R.pres S t).factorOfPrefix 1 u = R.dirSet
    source
    theorem MIPRE.LIDT.CL.Regs.factorOfPrefix_two {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) (u : ι → F) :
    (R.pres S t).factorOfPrefix 2 u = R.finalSet
    source
    theorem MIPRE.LIDT.CL.Regs.factorOfPrefix_three_le {ι : Type u_1} [DecidableEq ι] [Fintype ι] {n : ℕ} (R : Regs ι n) {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [NeZero n] {hn : n ∣ Fintype.card F} (S : Sel F n hn) (t : Ty) {j : ℕ} (hj : 3 ≤ j) (u : ι → F) :
    (R.pres S t).factorOfPrefix j u = ∅