The running time of the repeated sampler

repSampler_timeBound: when the input sampler runs within R.S (|d| + 1)^{R.k} at index n and has dimension at most R.d there, the repeated sampler on (λ, τ) runs within c (W + 1)^m (|d| + 1)^{e (R.k + 1)} for constants c, m, e independent of everything, W any number dominating R.S, R.d, λ, τ, n, the description length of the input sampler, the repetition count and 10^{R.k} (the input's time on the dimension query). The cost is the explicit one of repSampCore_runs_any, each of whose pieces is a sum and product of quantities below W, below |d| + 1, or of the cost of a call to the input sampler through the universal machine, bounded by Dom combinators.

noncomputable def MIPRE.Repeat.cU : ℕ

The constants of the self-interpreter's overhead polynomial.

Equations

• MIPRE.Repeat.cU = ∑ i ∈ Finset.range (MIPRE.Cost.selfUniversal.bound.natDegree + 1), MIPRE.Cost.selfUniversal.bound.coeff i

noncomputable def MIPRE.Repeat.dU : ℕ

The degree of the self-interpreter's overhead polynomial.

Equations

• MIPRE.Repeat.dU = MIPRE.Cost.selfUniversal.bound.natDegree

theorem MIPRE.Repeat.univ_bound_le {y : ℕ} (hy : 1 ≤ y) : Polynomial.eval y Cost.selfUniversal.bound ≤ cU * y ^ dU

theorem MIPRE.Repeat.size_le_of_mem_blockQueries (s : ℕ) (d q : Cost.Data) (hq : q ∈ blockQueries s d) : q.size ≤ d.size

The size of every block query is at most the size of the query datum.

structure MIPRE.Repeat.SampDom {ℓ : ℕ} (S : CL.Sampler ℓ) (lam tau n : ℕ) (R : Budget) (W : ℕ) : Prop

The hypotheses on the dominating number W.

• S_le : R.S ≤ W
• d_le : R.d ≤ W
• lam_le : lam ≤ W
• tau_le : tau ≤ W
• n_le : n ≤ W
• size_le : Cost.esize S.prog ≤ W
• pow_le : 10 ^ R.k ≤ W
• reps_le : Repetition.reps lam tau n ≤ W
• dim_le : S.dim n ≤ W

theorem MIPRE.Repeat.nat_size_le_self (x : ℕ) : x.size ≤ x

theorem MIPRE.Repeat.esize_nat_le' (x : ℕ) : Cost.esize x ≤ 4 * x + 1

theorem MIPRE.Repeat.dim_call_time {ℓ : ℕ} (S : CL.Sampler ℓ) (n : ℕ) (R : Budget) (hS : S.TimeBoundAt n R.S R.k) : ∃ td ≤ Polynomial.eval (Cost.esize S.prog + (Cost.esize n + 10) + R.S * 10 ^ R.k) Cost.selfUniversal.bound, Cost.Eval [(Cost.encode S.prog).cons ((Cost.encode n).cons (Cost.encode CL.Sampler.Query.dimension))] Cost.selfUniversal.univ (Cost.encode (S.dim n)) td

The time of the dimension query through the universal machine.

theorem MIPRE.Repeat.block_calls_time {ℓ : ℕ} (S : CL.Sampler ℓ) (n : ℕ) (R : Budget) (hS : S.TimeBoundAt n R.S R.k) (d : Cost.Data) : ∃ (fq : Cost.Data → Cost.Data), ∀ q ∈ blockQueries (S.dim n) d, ∃ t ≤ Polynomial.eval (Cost.esize S.prog + (Cost.esize n + d.size + 1) + R.S * (d.size + 1) ^ R.k) Cost.selfUniversal.bound, Cost.Eval [(Cost.encode S.prog).cons ((Cost.encode n).cons q)] Cost.selfUniversal.univ (fq q) t

The block queries through the universal machine, within a uniform bound.

theorem MIPRE.Repeat.repSampler_halts_within {ℓ : ℕ} (S : CL.Sampler ℓ) (lam tau n : ℕ) (R : Budget) (hS : S.TimeBoundAt n R.S R.k) (d : Cost.Data) : ∃ (r : Cost.Data), ∃ t ≤ anyCost lam tau n (Cost.encode S.prog) (S.dim n) d.size (Polynomial.eval (Cost.esize S.prog + (Cost.esize n + 10) + R.S * 10 ^ R.k) Cost.selfUniversal.bound) (Polynomial.eval (Cost.esize S.prog + (Cost.esize n + d.size + 1) + R.S * (d.size + 1) ^ R.k) Cost.selfUniversal.bound) + (Cost.esize S.prog + Cost.esize lam + Cost.esize tau + 2) + (Cost.esize n + d.size + 1) + 3, (repSamplerProg S.prog lam tau).Runs ((Cost.encode n).cons d) r t

The repeated sampler halts within anyCost plus the s-m-n overhead.

The domination chain

Each lemma below produces constants c, m, e that are uniform in everything, as the existential outside the universal quantifiers records; the proofs are the Dom combinators applied in the shape of the cost expression, and Lean assembles the constants.

theorem MIPRE.Repeat.dom_esize {W X K x : ℕ} (hx : x ≤ W) : Dom W X K (4 + 1) 1 0 (Cost.esize x)

The constants of each lemma are natural metavariables assigned by the final exact, so they must be closed terms; exact ⟨_, _, _, fun … => by …⟩ rather than refine ⟨?c, …⟩, whose synthetic goals the unifier will not assign and instead reduces max chains against.

theorem MIPRE.Repeat.dom_toUnaryCost : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {x : ℕ}, 1 ≤ X → x ≤ W → Dom W X K c m e (Cost.Prog.toUnaryCost x)

theorem MIPRE.Repeat.dom_powCost : ∃ (c : ℕ) (m : ℕ) (e' : ℕ), ∀ (W X K : ℕ) {e L sz : ℕ}, 1 ≤ X → e ≤ W → L ≤ 2 * W → sz ≤ 12 * W + 3 → Dom W X K c m e' (Cost.Prog.powCost e L sz)

theorem MIPRE.Repeat.dom_dimCost : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {tau L Λ N Ssz : ℕ}, 1 ≤ X → tau ≤ W → L ≤ 2 * W → Λ ≤ 4 * W + 1 → N ≤ 4 * W + 1 → Ssz ≤ 4 * W + 1 → Dom W X K c m e (Cost.Prog.dimCost tau L Λ N Ssz)

theorem MIPRE.Repeat.dom_mapIter (cZ mZ eZ : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {Z : ℕ}, 1 ≤ X → Dom W X K cZ mZ eZ Z → Dom W X K c m e (Cost.Prog.mapIter Z)

theorem MIPRE.Repeat.dom_zBound (cT mT eT : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {sD : Cost.Data} {n s D Tu : ℕ}, 1 ≤ X → Dom W X K cT mT eT Tu → sD.size ≤ W → n ≤ W → s ≤ W → D + 1 ≤ X → Dom W X K c m e (zBound sD n s D Tu)

theorem MIPRE.Repeat.dom_lockCost (cC mC eC cZ mZ eZ : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {s C U Y Z : ℕ}, 1 ≤ X → s ≤ W → Dom W X K cC mC eC C → U + 1 ≤ X → Y + 1 ≤ X → Dom W X K cZ mZ eZ Z → Dom W X K c m e (Cost.Prog.lockCost s C U Y Z)

theorem MIPRE.Repeat.dom_anyCost (cd md ed cT mT eT : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {lam tau n : ℕ} {sD : Cost.Data} {s D td Tu : ℕ}, 1 ≤ X → Dom W X K cd md ed td → Dom W X K cT mT eT Tu → sD.size ≤ W → lam ≤ W → tau ≤ W → n ≤ W → s ≤ W → D + 1 ≤ X → Dom W X K c m e (anyCost lam tau n sD s D td Tu)

theorem MIPRE.Repeat.dom_univ_bound (cy my ey : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {y : ℕ}, 1 ≤ X → 1 ≤ y → Dom W X K cy my ey y → Dom W X K c m e (Polynomial.eval y Cost.selfUniversal.bound)

The self-interpreter's overhead polynomial at a dominated argument.

theorem MIPRE.Repeat.dom_yd : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {p n RS pk : ℕ}, 1 ≤ X → p ≤ W → n ≤ W → RS ≤ W → pk ≤ W → Dom W X K c m e (p + (Cost.esize n + 10) + RS * pk)

The argument of the dimension query's bound.

theorem MIPRE.Repeat.dom_yT : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ (W X K : ℕ) {p n RS D : ℕ}, 1 ≤ X → p ≤ W → n ≤ W → RS ≤ W → D + 1 = X → Dom W X K c m e (p + (Cost.esize n + D + 1) + RS * (D + 1) ^ K)

The argument of the block queries' bound.

theorem MIPRE.Repeat.repSampler_timeBound : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {ℓ : ℕ} (S : CL.Sampler ℓ) (lam tau n : ℕ) (R : Budget) (W : ℕ), SampDom S lam tau n R W → S.TimeBoundAt n R.S R.k → (repSampler S lam tau).TimeBoundAt n (c * (W + 1) ^ m) (e * (R.k + 1))

The running time of the repeated sampler: constants c, m, e uniform in everything such that, whenever W dominates the parameters at n and the input sampler runs within R.S (|d| + 1)^{R.k} there, the repeated sampler runs within c (W + 1)^m (|d| + 1)^{e (R.k + 1)}.