OAI/Combinatorics/EditApproximation/Refinement/ComputedParameterRegisters.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.computedParameterPower_word line 10

   Source documentation

   A single logarithmic word accommodates every power exponent needed by the global integer and online-mass constructors.

    theorem computedParameterPower_word :
       ∀ᶠ N in atTop, ∀ k : ℕ,
         k ≤ 8000 * (coarseExponent (inputSmallLog N) + 1) →
         Nat.size (inputHeight N ^ k) ≤ inputHeight N := by
   …

   Mentions: OAI.EditApproximation.coarseExponent, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.inputHeight

2. theorem OAI.EditApproximation.inputLength_register_word line 19