OAI/Combinatorics/EditApproximation/Refinement/ComputedQueryBudgetAlgebra.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.computedLocalKernelBudget_mono line 8

   Source documentation

   Enlarge the exponent of the common computed kernel scale.

   theorem computedLocalKernelBudget_mono (N D E : ℕ) (h : D ≤ E) :
       computedLocalKernelBudget D N ≤ computedLocalKernelBudget E N := by
   …

   Mentions: OAI.EditApproximation.computedLocalKernelBudget

2. theorem OAI.EditApproximation.computedLocalKernelBudget_three line 14
3. theorem OAI.EditApproximation.computed_kernel_guard_cost line 38

   Source documentation

   The fixed guard overhead at the eight-power word bound.

   theorem computed_kernel_guard_cost (N : ℕ) (hH : 64 ≤ inputHeight N) :
       50 * inputHeight N ^ 8 + 100 ≤ computedLocalKernelBudget 1 N := by
   …

   Mentions: OAI.EditApproximation.inputHeight, OAI.EditApproximation.computedLocalKernelBudget