The running time of the product sampler

CL.TypedSampler.prodDirect runs the parameter routine of its direct half through the universal machine, then routes the query: at most one call to the typed half's program, again through the universal machine, on a query at most linearly larger than the typed query (route_call_size), and polynomial-time work on the parameters around it. So its running time is dominated, in the sense of MIPRE.Pipeline.PDom, as soon as the parameter routine's is and the typed half runs within a monomial coefficient at degree e (K + 1) (prog_time), on every input, well formed or not.

theorem MIPRE.CL.ProductSampler.size_treeHead_le (d : Cost.Data) : (Cost.PolyTimeFun.treeHead.toFun d).size ≤ d.size

theorem MIPRE.CL.ProductSampler.size_treeTail_le (d : Cost.Data) : (Cost.PolyTimeFun.treeTail.toFun d).size ≤ d.size

theorem MIPRE.CL.ProductSampler.length_rawList_le (d : Cost.Data) : (Detyping.Program.rawList d).length ≤ d.size

theorem MIPRE.CL.ProductSampler.length_readBits_le (d : Cost.Data) : List.length (Detyping.Program.readBits.toFun d) ≤ d.size

theorem MIPRE.CL.ProductSampler.length_leftBits_le (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (l : Cost.PolyTimeFun Cost.Data Cost.BitStr) (x : Cost.Data) : List.length ((leftBits D l).toFun x) ≤ List.length (l.toFun x)

A's half of a vector read off the query is no longer than the query.

theorem MIPRE.CL.ProductSampler.length_uD_le (pdn H nD' q : Cost.Data) : List.length (uD.toFun (pdn.cons (H.cons (nD'.cons q)))) ≤ q.size

The vectors of the parsed query are no longer than the typed query.

theorem MIPRE.CL.ProductSampler.length_yD_le (pdn H nD' q : Cost.Data) : List.length (yD.toFun (pdn.cons (H.cons (nD'.cons q)))) ≤ q.size

theorem MIPRE.CL.ProductSampler.size_queryA_le (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (j : Cost.PolyTimeFun Cost.Data ℕ) (ap pp : Cost.Prog) (ℓa n : ℕ) (pdn q : Cost.Data) (hj : j.toFun (pdn.cons ((Cost.encode (ap, ℓa, pp)).cons ((Cost.encode n).cons q))) ≤ ℓa) : ((queryA D j).toFun (pdn.cons ((Cost.encode (ap, ℓa, pp)).cons ((Cost.encode n).cons q)))).size ≤ Cost.esize n + 12 * q.size + 4 * ℓa + 20

The size of A's query at a level j, when j ≤ ℓa.

theorem MIPRE.CL.ProductSampler.route_call_size (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (ap pp : Cost.Prog) (ℓa n : ℕ) (pdn q payload : Cost.Data) (h : (route B D).toFun (pdn.cons ((Cost.encode (ap, ℓa, pp)).cons ((Cost.encode n).cons q))) = (true, payload)) : ∃ (a : Cost.Data) (ctx : Cost.Data), payload = ((Cost.encode ap).cons a).cons ctx ∧ a.size ≤ Cost.esize n + 12 * q.size + 4 * ℓa + 20

A forwarded query is linear in the typed query: the router calls A's program on the index and a query at most linearly larger than the typed query, whatever the input.

noncomputable def MIPRE.CL.ProductSampler.stageBound (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (ap : Cost.Prog) (ℓa n xs qs BA k : ℕ) : ℕ

The explicit bound on the routed stage: the router, one call through the universal machine to A's program on a query of size at most esize n + 12 |q| + 4 ℓa + 20, and the post-processing.

Equations

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

theorem MIPRE.CL.ProductSampler.stage_time (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (ap pp : Cost.Prog) (ℓa n : ℕ) (pdn q : Cost.Data) (BA k : ℕ) (hA : ∀ (d : Cost.Data), Cost.HaltsWithin ap ((Cost.encode n).cons d) (BA * (d.size + 1) ^ k)) : ∃ (r : Cost.Data), ∃ t ≤ stageBound B D ap ℓa n (pdn.cons ((Cost.encode (ap, ℓa, pp)).cons ((Cost.encode n).cons q))).size q.size BA k, (stage B D).Runs (pdn.cons ((Cost.encode (ap, ℓa, pp)).cons ((Cost.encode n).cons q))) r t

The routed stage halts within stageBound on every input, when A's program runs within BA (|d| + 1)^k at the index.

theorem MIPRE.CL.ProductSampler.prog_time (B : Cost.PolyTimeFun DirectInput Cost.BitStr) (D : Cost.PolyTimeFun Cost.Data Cost.Unary) (ℓa cp mp ep cs ms es cA mA eA : ℕ) : ∃ (C : ℕ) (M : ℕ) (E : ℕ), ∀ {W K : ℕ} (ap pp : Cost.Prog) (n : ℕ) (pdn : Cost.Data) (BA : ℕ), n ≤ W → (∀ {X : ℕ}, 1 ≤ X → Pipeline.PRuns W X K cp mp ep pp (Cost.encode n) pdn) → (∀ {X : ℕ}, 1 ≤ X → Pipeline.PDom W X K cs ms es (Cost.esize ap + Cost.esize pp)) → BA ≤ cA * (W + 1) ^ mA → (∀ (d : Cost.Data), Cost.HaltsWithin ap ((Cost.encode n).cons d) (BA * (d.size + 1) ^ (eA * (K + 1)))) → ∀ (q : Cost.Data), ∃ (r : Cost.Data) (t : ℕ), Pipeline.PDom W (q.size + 1) K C M E t ∧ (prog B D ap ℓa pp).Runs ((Cost.encode n).cons q) r t

The running time of the product sampler's program, on every input: dominated as soon as the parameter routine runs within a dominated time, the two programs have dominated sizes, and A's program runs within a monomial coefficient at degree eA (K + 1).