OAI/Combinatorics/EditApproximation/Geometry/RankedMemoKernelWork.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.rankedMemoKernelWork_le line 13

   Source documentation

   Count local arithmetic only on a cache miss, following exactly the recursive evaluator's returned values, requests and intermediate memories.

    theorem rankedMemoKernelWork_le {κ : Type*} (rank : κ → ℕ)
       (program : (key : κ) → FiniteQuery {child : κ // rank child < rank key})
       (bits : ℕ) (encode cost : κ → ℕ) (C : ℕ) (hcost : ∀ key, cost key ≤ C)
       (key : κ) (memory : BinaryMemo ℚ) :
       rankedMemoKernelWork rank program bits encode cost key memory ≤
         C * (rankedMemoEvaluate rank program bits encode key memory).requests := by
   …

   Mentions: OAI.EditApproximation.FiniteQuery, OAI.EditApproximation.BinaryMemo, OAI.EditApproximation.rankedMemoKernelWork, OAI.EditApproximation.rankedMemoEvaluate