OAI/Combinatorics/EditApproximation/Geometry/RankedMemoKernelFresh.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.FiniteQuery.requestWork_eq_fresh_sum line 8
2. theorem OAI.EditApproximation.rankedMemoKernelWork_eq_fresh_sum line 23

   Source documentation

   The local kernel annotation is exactly the sum over the freshly evaluated keys, including the actual adaptive recursive execution.

   theorem rankedMemoKernelWork_eq_fresh_sum {κ : Type*} (rank : κ → ℕ)
       (program : (key : κ) → FiniteQuery {child : κ // rank child < rank key})
       (bits : ℕ) (encode cost : κ → ℕ) (key : κ) (memory : BinaryMemo ℚ) :
       rankedMemoKernelWork rank program bits encode cost key memory =
         ((rankedMemoEvaluate rank program bits encode key memory).freshKeys.map cost).sum := by
   …

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