OAI/Combinatorics/EditApproximation/Refinement/ComputedCoarseControlSpace.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.physicalCoarseControlEntry line 12
2. theorem OAI.EditApproximation.physicalCoarseControlEntry_fits line 20
3. theorem OAI.EditApproximation.computedFamilyCoarseControlCapacity_eq line 59

   Source documentation

   A 64-word control-frame allowance for every recursive invocation of every coarse cache miss, conservatively retained until termination.

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

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

4. theorem OAI.EditApproximation.computedFamilyCoarseControlCapacity_bound line 66
5. theorem OAI.EditApproximation.computedFamilyCoarseControlCapacity_polynomial line 73