OAI/Combinatorics/EditApproximation/Refinement/ComputedCoarseScratchSpace.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.physicalCoarseAllocationEntry line 12
2. theorem OAI.EditApproximation.physicalCoarseAllocationEntry_fits line 20
3. theorem OAI.EditApproximation.computedFamilyCoarseScratchCapacity_eq line 51

   Source documentation

   Reserve every fresh cell allocated by every coarse cache miss until termination. This deliberately bounds more than simultaneously live scratch.

   theorem computedFamilyCoarseScratchCapacity_eq (source target : List ℕ) (N : ℕ)
       (input : ComputedFamilyInput source target N) :
       computedFamilyCoarseScratchCapacity source target N input =
         ((computedFamilyResult source target N input).freshKeys.map
           (coarseHistoryKeyCost (fun _ => (N + 2) ^ 181))).sum :=
   …

   Mentions: OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.computedFamilyCoarseScratchCapacity, OAI.EditApproximation.computedFamilyResult, OAI.EditApproximation.coarseHistoryKeyCost

4. theorem OAI.EditApproximation.computedFamilyCoarseScratchCapacity_bound line 58
5. theorem OAI.EditApproximation.computedFamilyCoarseScratchCapacity_polynomial line 65