OAI/Combinatorics/EditApproximation/Refinement/ComputedQueryTableWork.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.EditApproximation.ComputedQueryTableParent line 13
2. abbrev OAI.EditApproximation.ComputedQueryTableKey line 18
3. def OAI.EditApproximation.computedQueryTableProgram line 23
4. theorem OAI.EditApproximation.computedQueryTable_work_width line 35

   Source documentation

   Complete dispatcher cost on any oracle storing the proved semantic values.

   theorem computedQueryTable_work_width :
       ∀ᶠ N : ℕ in atTop, ∀ source target : List ℕ, source.length + target.length ≤ N →
         ∀ (input : ComputedFamilyInput source target N)
         (occurrence : BinaryMemo PositionCounts) (symbolBits positionBits : ℕ),
         symbolBits ≤ inputHeight N ^ 3 → positionBits ≤ inputHeight N ^ 3 →
         ∀ (parent : ComputedQueryTableParent source target N)
         (oracle : ComputedQueryTableKey source target N parent → BinaryFraction),
         (∀ key, (oracle key).width ≤ inputHeight N ^ 3) →
         (∀ child, (oracle (Sum.inr child)).value = computedFamilyTableValue source target N input child.val) →
         (computedQueryTableProgram source target N occurrence symbolBits positionBits parent).work
           oracle (fun _ => 1) ≤ computedLocalKernelBudget computedTableQueryDegree N ∧
         ((computedQueryTableProgram source target N occurrence symbolBits positionBits parent).value oracle).width ≤
   …

   Mentions: OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.BinaryMemo, OAI.EditApproximation.PositionCounts, OAI.EditApproximation.inputHeight, OAI.EditApproximation.ComputedQueryTableParent, OAI.EditApproximation.ComputedQueryTableKey, OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.computedFamilyTableValue, OAI.EditApproximation.computedQueryTableProgram, OAI.EditApproximation.computedLocalKernelBudget, OAI.EditApproximation.computedTableQueryDegree