RankedMemoAddressWork.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EditApproximation.FiniteQuery.requestWork_le line 13
Source documentation
Annotate exactly the requests made by an existing adaptive run.
```
 theorem requestWork_le {ι κ : Type*} (ask : ι → BinaryMemo ℚ → RecursiveMemoResult κ)
    (cost : ι → BinaryMemo ℚ → ℕ) (C : ℕ)
    (hcost : ∀ key memory, cost key memory ≤ C * (ask key memory).requests)
    (program : FiniteQuery ι) (memory : BinaryMemo ℚ) :
    requestWork ask cost program memory ≤ C * (run ask program memory).requests := by
…
```
Mentions: OAI.EditApproximation.BinaryMemo, OAI.EditApproximation.RecursiveMemoResult, OAI.EditApproximation.FiniteQuery.cost, OAI.EditApproximation.FiniteQuery, OAI.EditApproximation.FiniteQuery.requestWork, OAI.EditApproximation.FiniteQuery.run

theorem OAI.EditApproximation.rankedMemoAddressWork_le line 32

Source documentation

Code construction is incurred for lookup and, on a miss, for insertion. The recursive calls use the exact same returned values and cache states.

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

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