OAI/Combinatorics/ContingencyTables/Transport/MeasuredFold.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

List folds with the cost of each cached computation accounted for

  1. lemma OAI.ContingencyTables.MeasuredFold.work_fold line 14

    Source documentation

    The loop cost is polynomial in one common external measure whenever each reached call and each stored accumulator satisfy such a bound.

    lemma work_fold {f : A×B → B} (F : Realizer f) (measure : List A×B → ℕ)
    (p q : Polynomial ℕ)
    (hinput : ∀ z,weight z ≤ measure z)
    (hcall : ∀ (as : List A) (b : B) pre a post,as=pre++a::post →
      F.cost (a,pre.foldl (fun z c => f (c,z)) b) ≤ p.eval (measure (as,b)))
    (hstate : ∀ (as : List A) (b : B) pre post,as=pre++post →
      weight (pre.foldl (fun z a => f (a,z)) b) ≤ q.eval (measure (as,b))) :
    WorkBound (fold F) measure := by
…