OAI/Combinatorics/EditApproximation/Binary/IntegerKernelWork.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.computedFullKernelWork line 11

   Source documentation

   Full execution counter: the exact fallback branch or the charged randomized execution, including its concrete local kernel costs.

   noncomputable def computedFullKernelWork (source target : List ℕ) (N : ℕ)
       (cost : ComputedFamilyInput source target N → ComputedFamilyMemoKey source target N → ℕ)
       (setup : ℝ) : ComputedFullOutcome source target N → ℝ
     | .inl _ => setup + (chargedSuffixDP source target).2
     | .inr execution => setup + computedExecutionTotalWork source target N cost execution

   Mentions: OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.ComputedFamilyMemoKey, OAI.EditApproximation.ComputedFullOutcome, OAI.EditApproximation.chargedSuffixDP, OAI.EditApproximation.computedExecutionTotalWork

2. theorem OAI.EditApproximation.computedFullKernelWork_expected_le line 17
3. def OAI.EditApproximation.integerFullKernelWork line 34
4. theorem OAI.EditApproximation.integerFullKernelWork_expected_near_linear line 44

   Source documentation

   Runtime transport for the concrete local evaluator, with no additional probability hypothesis.

   theorem integerFullKernelWork_expected_near_linear (C D : ℕ)
       (epsilon : BinaryFraction) (hepsilon : 0 < epsilon.value)
       (epsilonTime : ℝ) (htime : 0 < epsilonTime) :
       ∀ᶠ N in atTop, ∀ source target : List ℤ, source.length + target.length ≤ N →
         (∀ z ∈ source ++ target, z.natAbs ≤ (N + 2) ^ C) →
         ∀ cost : ComputedFamilyInput (source.map integerSymbolCode) (target.map integerSymbolCode) N →
           ComputedFamilyMemoKey (source.map integerSymbolCode) (target.map integerSymbolCode) N → ℕ,
         (∀ input key, cost input key ≤ computedLocalKernelBudget D N) →
         (∫ outcome, integerFullKernelWork source target N epsilon cost outcome
           ∂computedFullLaw (source.map integerSymbolCode) (target.map integerSymbolCode) N epsilon) ≤
           (N + 2 : ℝ) ^ (1 + epsilonTime) := by
   …

   Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.integerSymbolCode, OAI.EditApproximation.ComputedFamilyMemoKey, OAI.EditApproximation.computedLocalKernelBudget, OAI.EditApproximation.integerFullKernelWork, OAI.EditApproximation.computedFullLaw