OAI/Combinatorics/EditApproximation/Refinement/ComputedExecutionCosts.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.computedExecutionRejectionWork_integrable line 13
2. theorem OAI.EditApproximation.computedExecutionAccepted_measurable line 29
3. theorem OAI.EditApproximation.computedExecutionAcceptedWork_integrable line 32
4. theorem OAI.EditApproximation.computedExecutionDictionaryWork_integrable line 41
5. theorem OAI.EditApproximation.computedExecutionDictionaryWork_expected_near_linear line 46
6. theorem OAI.EditApproximation.computedExecutionAddressWork_integrable line 61
7. theorem OAI.EditApproximation.computedExecutionAddressWork_expected_near_linear line 66
8. theorem OAI.EditApproximation.computedExecutionNonlocalWork_integrable line 83

   Source documentation

   These are the actual coarse, rejection-bit, dictionary and address-construction counters. The local arithmetic counter is kept separate until its kernel is composed.

    theorem computedExecutionNonlocalWork_integrable (source target : List ℕ) (N : ℕ) :
       Integrable (computedExecutionNonlocalWork source target N) (computedExecutionLaw source target N) :=
   …

   Mentions: OAI.EditApproximation.computedExecutionNonlocalWork, OAI.EditApproximation.computedExecutionLaw

9. theorem OAI.EditApproximation.constant_le_rpow_eventually line 90
10. theorem OAI.EditApproximation.computedExecutionNonlocalWork_expected_near_linear line 96