Runtime transfer for the actual introspection sampler

The auxiliary extension makes at most one Pauli-sampler call. Its explicit polynomial majorant has a degree independent of the input index and the number of hiding types. Composing this bound with the actual detyping compiler gives a polynomial query bound for the final five-level sampler.

noncomputable def MIPRE.Introspection.typedSamplerCost (n B k : ℕ) : Polynomial ℕ

Equations

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

noncomputable def MIPRE.Introspection.typedSamplerDegree (k : ℕ) : ℕ

Equations

• MIPRE.Introspection.typedSamplerDegree k = MIPRE.Cost.Prog.routeDegree MIPRE.Introspection.SamplerProgram.route MIPRE.Introspection.SamplerProgram.post k

theorem MIPRE.Introspection.typedSamplerCost_natDegree_le (n B k : ℕ) : (typedSamplerCost n B k).natDegree ≤ typedSamplerDegree k

noncomputable def MIPRE.Introspection.typedSamplerCoefficient (n B k : ℕ) : ℕ

Equations

• MIPRE.Introspection.typedSamplerCoefficient n B k = ∑ i ∈ Finset.range ((MIPRE.Introspection.typedSamplerCost n B k).natDegree + 1), (MIPRE.Introspection.typedSamplerCost n B k).coeff i

theorem MIPRE.Introspection.typedSampler_haltsWithin {P : Type u_1} [Cost.SizedEncoding P] (ℓ : ℕ) (S : CL.TypedSampler 3 P) (n B k : ℕ) (h : S.TimeBoundAt n B k) (q : Cost.Data) : Cost.HaltsWithin (typedSampler ℓ S).prog ((Cost.encode n).cons q) (Polynomial.eval q.size (typedSamplerCost n B k))

theorem MIPRE.Introspection.typedSampler_timeBoundAt {P : Type u_1} [Cost.SizedEncoding P] (ℓ : ℕ) (S : CL.TypedSampler 3 P) (n B k : ℕ) (h : S.TimeBoundAt n B k) : (typedSampler ℓ S).TimeBoundAt n (typedSamplerCoefficient n B k) (typedSamplerDegree k)

Typed introspection preserves polynomial query time with a common exponent.

theorem MIPRE.Introspection.typedSampler_timeBound {P : Type u_1} [Cost.SizedEncoding P] (ℓ : ℕ) (S : CL.TypedSampler 3 P) (B : ℕ → ℕ) (k : ℕ) (h : ∀ (n : ℕ), S.TimeBoundAt n (B n) k) (n : ℕ) : (typedSampler ℓ S).TimeBoundAt n (typedSamplerCoefficient n (B n) k) (typedSamplerDegree k)

theorem MIPRE.Introspection.detypedSampler_timeBound {P : Type u_1} [Cost.SizedEncoding P] [Fintype P] [DecidableEq P] (E : P → P → Bool) (X Z : P) (ℓ : ℕ) (S : CL.TypedSampler 3 P) (B : ℕ → ℕ) (k : ℕ) (h : ∀ (n : ℕ), S.TimeBoundAt n (B n) k) : ∃ (B' : ℕ → ℕ) (k' : ℕ), (detypedSampler E X Z ℓ S).TimeBound B' k'

The executable five-level sampler inherits a global polynomial query bound.