OAI/Combinatorics/EditApproximation/Refinement/ComputedPreparedWords.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.computedPreparedWords_numeric line 10

   Source documentation

   The numeric record is inhabited by the actual constructed scalar words.

   theorem computedPreparedWords_numeric :
       ∀ᶠ N : ℕ in atTop, ∀ nx ny : ℕ, nx + ny ≤ N → ∀ t : ℕ, t ≤ inputHeight N ^ 2 →
         ∀ (pass : ℕ) (word : List Bool) (hpositive : 0 < bitWordValue word),
         bitWordValue word = inputSmallLog N → word.length ≤ Nat.size (inputSmallLog N) →
         ∀ integer : ℕ → TargetInterval ny → ℕ,
         (∀ b r, Nat.size (integer b r) ≤ inputHeight N) →
         let values := (refinementParameterWordsWithWork N pass word hpositive).1
   …

   Mentions: OAI.EditApproximation.inputHeight, OAI.EditApproximation.bitWordValue, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.refinementParameterWordsWithWork