OAI/Combinatorics/EditApproximation/Refinement/ComputedExecutionKernelWork.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.computedExecutionKernelWork_integrable line 13
2. theorem OAI.EditApproximation.computedExecutionKernelWork_expected_near_linear line 20
3. theorem OAI.EditApproximation.computedExecutionTotalWork_integrable line 40

   Source documentation

   Execution work combines the nonlocal charges with a local kernel annotation.

   theorem computedExecutionTotalWork_integrable (source target : List ℕ) (N : ℕ)
       (cost : ComputedFamilyInput source target N → ComputedFamilyMemoKey source target N → ℕ) :
       Integrable (computedExecutionTotalWork source target N cost)
         (computedExecutionLaw source target N) :=
   …

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

4. theorem OAI.EditApproximation.computedExecutionTotalWork_expected_near_linear line 47