OAI/Combinatorics/EditApproximation/Refinement/ComputedOutputWork.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.computedFullOutputWork_expected_le line 14

   Source documentation

   Execution cost including shared binary setup and the final conversion. The exact branch keeps its own charged dynamic program.

   theorem computedFullOutputWork_expected_le (source target : List ℕ) (N : ℕ)
       (cost : ComputedFamilyInput source target N → ComputedFamilyMemoKey source target N → ℕ)
       (setup : ℝ) (shared : ℕ) (output : ComputedFamilyInput source target N → ℕ)
       (fallbackOutput : ℕ) (epsilon : BinaryFraction) (hlarge : physicalLargeInput N epsilon)
       (budget outputBudget : ℝ)
       (hbudget : (∫ execution, computedExecutionTotalWork source target N cost execution
         ∂computedExecutionLaw source target N) ≤ budget)
       (houtput : ∀ input, (output input : ℝ) ≤ outputBudget) :
       (∫ outcome, computedFullOutputWork source target N cost setup shared output fallbackOutput outcome
         ∂computedFullLaw source target N epsilon) ≤ setup + shared + budget + outputBudget := by
   …

   Mentions: OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.ComputedFamilyMemoKey, OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.physicalLargeInput, OAI.EditApproximation.computedExecutionTotalWork, OAI.EditApproximation.computedExecutionLaw, OAI.EditApproximation.computedFullOutputWork, OAI.EditApproximation.computedFullLaw