OAI/Combinatorics/EditApproximation/Refinement/ComputedKernelWork.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.computedFamilyKernelWork_le line 17

   Source documentation

   Local arithmetic annotations follow the actual memo run, hence are incurred once per cache miss, with the original program and draw values.

   theorem computedFamilyKernelWork_le (source target : List ℕ) (N : ℕ)
       (input : ComputedFamilyInput source target N)
       (cost : ComputedFamilyMemoKey source target N → ℕ) (C : ℕ)
       (hcost : ∀ key, cost key ≤ C) :
       computedFamilyKernelWork source target N input cost ≤
         C * (computedFamilyResult source target N input).requests :=
   …

   Mentions: OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.ComputedFamilyMemoKey, OAI.EditApproximation.computedFamilyKernelWork, OAI.EditApproximation.computedFamilyResult

2. theorem OAI.EditApproximation.computedFamilyKernelWork_near_linear line 25