Documentation

MIPRE.Background.Introspection.PauliSamplerTotal

The uniformly bounded sampler at every index #

The positive-index sampler is unchanged. The exceptional branches have no question coordinates and execute without inspecting the source description.

source
noncomputable def MIPRE.Introspection.PauliSampler.finalSampler (c : ℕ) (hc : 1 ≤ c) (he : Even c) (ℓ lam : ℕ) :
CL.Sampler 5
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPRE.Introspection.PauliSampler.finalCompiler (c ℓ : ℕ) :
    Cost.PolyTimeFun ℕ Cost.Prog
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem MIPRE.Introspection.PauliSampler.finalCompiler_apply (c : ℕ) (hc : 1 ≤ c) (he : Even c) (ℓ lam : ℕ) :
      (finalCompiler c ℓ).toFun lam = (finalSampler c hc he ℓ lam).prog
      source
      @[simp]
      theorem MIPRE.Introspection.PauliSampler.finalSampler_dim_lam_zero (c : ℕ) (hc : 1 ≤ c) (he : Even c) (ℓ n : ℕ) :
      (finalSampler c hc he ℓ 0).dim n = 0
      source
      @[simp]
      theorem MIPRE.Introspection.PauliSampler.finalSampler_dim_index_zero (c : ℕ) (hc : 1 ≤ c) (he : Even c) (ℓ lam : ℕ) :
      (finalSampler c hc he ℓ lam).dim 0 = 0
      source
      theorem MIPRE.Introspection.PauliSampler.finalSampler_dim_zero (c : ℕ) (hc : 1 ≤ c) (he : Even c) (ℓ lam n : ℕ) (h : lam * n = 0) :
      (finalSampler c hc he ℓ lam).dim n = 0
      source
      theorem MIPRE.Introspection.PauliSampler.finalSampler_dim_pos (c : ℕ) (hc : 1 ≤ c) (he : Even c) (ℓ lam n : ℕ) (hl : lam ≠ 0) (hn : n ≠ 0) :
      (finalSampler c hc he ℓ lam).dim n = (fullSampler c hc he ℓ lam).dim n
      source
      theorem MIPRE.Introspection.PauliSampler.finalSampler_cl_pos (c : ℕ) (hc : 1 ≤ c) (he : Even c) (ℓ lam n : ℕ) (hl : lam ≠ 0) (hn : n ≠ 0) (w : Player) :
      (finalSampler c hc he ℓ lam).cl n w ≍ (fullSampler c hc he ℓ lam).cl n w
      source
      theorem MIPRE.Introspection.PauliSampler.finalSampler_uniform_bound (c : ℕ) (hc : 1 ≤ c) (he : Even c) (ℓ : ℕ) :
      ∃ (C : ℕ), ∀ (lam n : ℕ), (finalSampler c hc he ℓ lam).TimeBoundAt n ((lam * n + 1) ^ C) C ∧ (finalSampler c hc he ℓ lam).dim n ≤ (lam * n + 1) ^ C

      One exponent controls all indices, including both exceptional zero cases.