Recording a polynomially bounded sequence of iterates

def MIPRE.Cost.recordIterates {α : Type u_1} (f : α → α) (u : Unary) (a : α) : List α

Print the initial point and each subsequent iterate, up to the unary budget.

Equations

• MIPRE.Cost.recordIterates f u a = List.ofFn fun (i : Fin (List.length u)) => f^[↑i] a

@[simp]

theorem MIPRE.Cost.recordIterates_nil {α : Type u_1} [SizedEncoding α] (f : α → α) (a : α) : recordIterates f [] a = []

theorem MIPRE.Cost.recordIterates_cons {α : Type u_1} [SizedEncoding α] (f : α → α) (u : Unary) (a : α) : recordIterates f (() :: u) a = a :: recordIterates f u (f a)

def MIPRE.Cost.recordStep {α : Type u_1} (f : α → α) (s : α × List α) : Unit → α × List α

Equations

• MIPRE.Cost.recordStep f s x✝ = (f s.1, s.1 :: s.2)

theorem MIPRE.Cost.fold_recordStep {α : Type u_1} [SizedEncoding α] (f : α → α) (u : Unary) (a : α) (acc : List α) : List.foldl (recordStep f) (a, acc) u = (f^[List.length u] a, (recordIterates f u a).reverse ++ acc)

theorem MIPRE.Cost.esize_recordIterates {α : Type u_1} [SizedEncoding α] (f : α → α) (B : Polynomial ℕ) (hB : ∀ (n : ℕ) (a : α), esize (f^[n] a) ≤ Polynomial.eval (esize a) B) (u : Unary) (a : α) : esize (recordIterates f u a) ≤ List.length u * (Polynomial.eval (esize a) B + 1) + 1

noncomputable def MIPRE.Cost.recordStepProg {α : Type u_1} [SizedEncoding α] (f : PolyTimeFun α α) : PolyTimeFun ((α × List α) × Unit) (α × List α)

Equations

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

noncomputable def MIPRE.Cost.recordIteratesProg {α : Type u_1} [SizedEncoding α] (f : PolyTimeFun α α) (B : Polynomial ℕ) (hB : ∀ (n : ℕ) (a : α), esize (f.toFun^[n] a) ≤ Polynomial.eval (esize a) B) : PolyTimeFun (Unary × α) (List α)

Any uniformly polynomially size-bounded orbit can be printed in polynomial time. The iteration count is unary, and the bound must hold on every raw input.

Equations

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

@[simp]

theorem MIPRE.Cost.recordIteratesProg_apply {α : Type u_1} [SizedEncoding α] (f : PolyTimeFun α α) (B : Polynomial ℕ) (hB : ∀ (n : ℕ) (a : α), esize (f.toFun^[n] a) ≤ Polynomial.eval (esize a) B) (u : Unary) (a : α) : (recordIteratesProg f B hB).toFun (u, a) = recordIterates f.toFun u a