Polynomial query time of the canonical Pauli sampler

The query degree is independent of the index and of the boundedness parameter. The coefficient includes the explicit canonical-parameter cost; no halting or complexity assumption on a supplied program is used.

noncomputable def MIPRE.Introspection.PauliSampler.costPolynomial (c lam n : ℕ) : Polynomial ℕ

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Introspection.PauliSampler.degree : ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Introspection.PauliSampler.shifted_degree (P : Polynomial ℕ) (a : ℕ) : (P.comp (Polynomial.X + Polynomial.C a)).natDegree ≤ P.natDegree

theorem MIPRE.Introspection.PauliSampler.costPolynomial_degree (c lam n : ℕ) : (costPolynomial c lam n).natDegree ≤ degree

theorem MIPRE.Introspection.PauliSampler.prog_runs_cost (c lam n : ℕ) (d : Cost.Data) : ∃ time ≤ Polynomial.eval d.size (costPolynomial c lam n), (prog c lam).Runs ((Cost.encode n).cons d) (QLD.PauliCL.SamplerProgram.query.toFun (PauliSamplerParameters.parameters c lam n, d)) time

noncomputable def MIPRE.Introspection.PauliSampler.coefficient (c lam n : ℕ) : ℕ

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Introspection.PauliSampler.sampler_timeBoundAt (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam n : ℕ) : (sampler c hc he lam).TimeBoundAt n (coefficient c lam n) degree

theorem MIPRE.Introspection.PauliSampler.coefficient_eq_eval_one (c lam n : ℕ) : coefficient c lam n = Polynomial.eval 1 (costPolynomial c lam n)

noncomputable def MIPRE.Introspection.PauliSampler.coefficientMajorant (c v : ℕ) : ℕ

A polynomial majorant uniform in both the boundedness parameter and index.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Introspection.PauliSampler.coefficient_le_majorant {c lam n v : ℕ} (hc : 1 ≤ c) (hl : lam ≤ v) (hn : n ≤ v) (hu : lam * n ≤ v) : coefficient c lam n ≤ coefficientMajorant c v

theorem MIPRE.Introspection.PauliSampler.coefficientMajorant_polyBounded (c : ℕ) : Cost.PolyBounded (coefficientMajorant c)

def MIPRE.Introspection.PauliSampler.dimensionMajorant (c v : ℕ) : ℕ

Equations

• MIPRE.Introspection.PauliSampler.dimensionMajorant c v = (3 * MIPRE.Introspection.PauliSamplerParameters.widthBound c v + 3) * MIPRE.Introspection.PauliSamplerParameters.widthBound c v

theorem MIPRE.Introspection.PauliSampler.dimension_le_majorant {c lam n v : ℕ} (hc : 1 ≤ c) (hu : lam * n ≤ v) : dimension c lam n ≤ dimensionMajorant c v

theorem MIPRE.Introspection.PauliSampler.dimensionMajorant_polyBounded (c : ℕ) : Cost.PolyBounded (dimensionMajorant c)