OAI/Combinatorics/EditApproximation/Refinement/ComputedBaseStorage.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.computedFamilyStorageCapacity line 12

   Source documentation

   Retained dictionary, all copied coarse inputs, all coarse-array capacities, and all local workspace allocations. Summing all allocations is a conservative bound on simultaneous storage.

   noncomputable def computedFamilyStorageCapacity (source target : List ℕ) (N : ℕ)
       (input : ComputedFamilyInput source target N)
       (localSpace : ComputedFamilyMemoKey source target N → ℕ) : ℕ :=
   …

   Mentions: OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.ComputedFamilyMemoKey

2. theorem OAI.EditApproximation.computedFamilyKernelWork_polynomial line 20
3. theorem OAI.EditApproximation.storage_sum_bound line 32
4. theorem OAI.EditApproximation.computedFamilyStorageCapacity_polynomial line 46