OAI/Combinatorics/EditApproximation/Binary/IntegerQueryWork.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.integerQueryWidths line 10

   Source documentation

   The actual computed widths of the encoded input index.

   theorem integerQueryWidths (C : ℕ) :
       ∀ᶠ N : ℕ in atTop, ∀ source target : List ℤ, source.length + target.length ≤ N →
         (∀ z ∈ source ++ target, z.natAbs ≤ (N + 2) ^ C) →
         integerInputSymbolBits source target ≤ inputHeight N ^ 3 ∧
         integerInputPositionBits target ≤ inputHeight N ^ 3 := by
   …

   Mentions: OAI.EditApproximation.integerInputSymbolBits, OAI.EditApproximation.inputHeight, OAI.EditApproximation.integerInputPositionBits

2. def OAI.EditApproximation.integerQueryLocalWork line 29
3. theorem OAI.EditApproximation.integerQueryLocalWork_cap line 33
4. def OAI.EditApproximation.integerQueryWork line 55

   Source documentation

   Complete integer-input cost with the proved local program, rather than an unspecified per-key annotation.

   noncomputable def integerQueryWork (source target : List ℤ) (N : ℕ) (epsilon : BinaryFraction) :=
   …

   Mentions: OAI.EditApproximation.BinaryFraction

5. theorem OAI.EditApproximation.integerQueryWork_expected_near_linear line 58