Documentation

MIPRE.Background.Introspection.PauliSamplerZero

A zero-dimensional sampler at the exceptional index #

The branch inspects the index in place. At zero it returns the empty answer without copying the query or reading the underlying sampler description.

source
def MIPRE.Introspection.ZeroIndexSampler.emptySampler (ℓ : ℕ) :
CL.Sampler ℓ
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MIPRE.Introspection.ZeroIndexSampler.emptySampler_timeBound (ℓ n : ℕ) :
    (emptySampler ℓ).TimeBoundAt n 1 0
    source
    def MIPRE.Introspection.ZeroIndexSampler.wrap (p : Cost.Prog) :
    Cost.Prog
    Equations
    Instances For
      source
      theorem MIPRE.Introspection.ZeroIndexSampler.wrap_closed {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) :
      Cost.Prog.WellScoped 1 (wrap p)
      source
      theorem MIPRE.Introspection.ZeroIndexSampler.wrap_zero (p : Cost.Prog) (d : Cost.Data) :
      (wrap p).Runs ((Cost.encode 0).cons d) Cost.Data.nil 3
      source
      theorem MIPRE.Introspection.ZeroIndexSampler.wrap_positive {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) {n : ℕ} (hn : n ≠ 0) (d r : Cost.Data) (t : ℕ) (hr : p.Runs ((Cost.encode n).cons d) r t) :
      (wrap p).Runs ((Cost.encode n).cons d) r (((Cost.encode n).cons d).size + t + 4)
      source
      noncomputable def MIPRE.Introspection.ZeroIndexSampler.compiler :
      Cost.PolyTimeFun Cost.Prog Cost.Prog
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem MIPRE.Introspection.ZeroIndexSampler.compiler_apply (p : Cost.Prog) :
        compiler.toFun p = wrap p
        source
        def MIPRE.Introspection.ZeroIndexSampler.chosen {ℓ : ℕ} (S : CL.Sampler ℓ) (n : ℕ) :
        CL.Sampler ℓ
        Equations
        Instances For
          source
          theorem MIPRE.Introspection.ZeroIndexSampler.wrap_chosen {ℓ : ℕ} (S : CL.Sampler ℓ) (n : ℕ) (d r : Cost.Data) (t : ℕ) (h : (chosen S n).prog.Runs ((Cost.encode n).cons d) r t) :
          ∃ (s : ℕ), (wrap S.prog).Runs ((Cost.encode n).cons d) r s
          source
          def MIPRE.Introspection.ZeroIndexSampler.atZero {ℓ : ℕ} (S : CL.Sampler ℓ) :
          CL.Sampler ℓ
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem MIPRE.Introspection.ZeroIndexSampler.atZero_dim_zero {ℓ : ℕ} (S : CL.Sampler ℓ) :
            (atZero S).dim 0 = 0
            source
            theorem MIPRE.Introspection.ZeroIndexSampler.atZero_dim_pos {ℓ n : ℕ} (S : CL.Sampler ℓ) (hn : n ≠ 0) :
            (atZero S).dim n = S.dim n
            source
            theorem MIPRE.Introspection.ZeroIndexSampler.atZero_cl_pos {ℓ n : ℕ} (S : CL.Sampler ℓ) (hn : n ≠ 0) (w : Player) :
            (atZero S).cl n w ≍ S.cl n w
            source
            theorem MIPRE.Introspection.ZeroIndexSampler.atZero_timeBound_zero {ℓ : ℕ} (S : CL.Sampler ℓ) :
            (atZero S).TimeBoundAt 0 1 2
            source
            theorem MIPRE.Introspection.ZeroIndexSampler.atZero_timeBound_pos {ℓ n B k : ℕ} (S : CL.Sampler ℓ) (hn : n ≠ 0) (h : S.TimeBoundAt n B k) :
            (atZero S).TimeBoundAt n (B + Cost.esize n + 5) (max k 1)

            The positive branch only copies the original input once before running the sampler.