OAI/Combinatorics/EditApproximation/Geometry/RankedMemoWork.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Counts of the actual persistent interpreter. Dictionary operations are charged on every request, including hits; insertion and retained-node costs are charged only when a value is computed.

  1. def OAI.EditApproximation.FiniteQuery.cost line 13
  2. def OAI.EditApproximation.FiniteQuery.keys line 17
  3. theorem OAI.EditApproximation.FiniteQuery.cost_eq_sum line 21
  4. theorem OAI.EditApproximation.FiniteQuery.run_resource_bounds line 28
  5. theorem OAI.EditApproximation.FiniteQuery.run_requests_le line 47
  6. theorem OAI.EditApproximation.rankedMemoEvaluate_resource_bounds line 69
  7. def OAI.EditApproximation.rankedUncachedCalls line 122

    Source documentation

    Number of requests in the same adaptive program without cache hits. It is a dominating execution tree, not the size of the full table.

    def rankedUncachedCalls {κ : Type*} (rank : κ → ℕ)
    (program : (key : κ) → FiniteQuery {child : κ // rank child < rank key}) (key : κ) : ℕ :=
…

    Mentions: OAI.EditApproximation.FiniteQuery

  8. theorem OAI.EditApproximation.rankedUncachedCalls_pos line 129
  9. theorem OAI.EditApproximation.rankedMemoEvaluate_requests_le line 135