OAI/Combinatorics/EditApproximation/Refinement/ComputedReadChargedWork.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.computedExecutionReadChargedWork_integrable line 17

   Source documentation

   Execution budget including indexed coarse computation, consumed threshold bits, rejection sampling, dictionary operations, address construction and unit charges.

   theorem computedExecutionReadChargedWork_integrable (source target : List ℕ) (N : ℕ) :
       Integrable (computedExecutionReadChargedWork source target N) (computedExecutionLaw source target N) :=
   …

   Mentions: OAI.EditApproximation.computedExecutionReadChargedWork, OAI.EditApproximation.computedExecutionLaw

2. theorem OAI.EditApproximation.computedExecutionReadChargedWork_expected_near_linear line 24