OAI/Combinatorics/EditApproximation/Binary/IntegerPreprocessing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.EditApproximation.integerEqualWithWork_spec line 14
  2. theorem OAI.EditApproximation.input_length_bits_le line 36

    Source documentation

    Scans, integer encoding, indexed occurrence preprocessing and the exact equality guard are charged before the local evaluator starts.

     theorem input_length_bits_le (N : ℕ) : Nat.size (N + 2) ≤ inputHeight N + 1 := by
…

    Mentions: OAI.EditApproximation.inputHeight

  3. theorem OAI.EditApproximation.preprocessing_scalar_bound line 41
  4. theorem OAI.EditApproximation.integerPreprocessingWork_le line 60
  5. theorem OAI.EditApproximation.fixed_height_power_near_linear line 78
  6. theorem OAI.EditApproximation.integerPreprocessingWork_near_linear line 90