OAI/Combinatorics/EditApproximation/Refinement/ComputedQueryWork.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.computedQueryWorkDegree line 11
2. theorem OAI.EditApproximation.computedQueryLocalWork_cap line 15

   Source documentation

   Complete local work, including binary denominator normalization.

   theorem computedQueryLocalWork_cap :
       ∀ᶠ 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 →
         (∀ z ∈ source, z < 2 ^ symbolBits) → (∀ z ∈ target, z < 2 ^ symbolBits) →
         target.length ≤ 2 ^ positionBits → occurrence = occurrenceBuild symbolBits positionBits target.zipIdx →
         ∀ key, computedQueryLocalWork source target N occurrence symbolBits positionBits input key ≤
           computedLocalKernelBudget computedQueryWorkDegree N := by
   …

   Mentions: OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.BinaryMemo, OAI.EditApproximation.PositionCounts, OAI.EditApproximation.inputHeight, OAI.EditApproximation.occurrenceBuild, OAI.EditApproximation.computedQueryLocalWork, OAI.EditApproximation.computedLocalKernelBudget, OAI.EditApproximation.computedQueryWorkDegree