OAI/Combinatorics/EditApproximation/Refinement/ComputedQueryWidth.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.computedFamilyTableValue_abs_le line 10

   Source documentation

   Uniform magnitude bound for every table, independently of accuracy.

   theorem computedFamilyTableValue_abs_le (source target : List ℕ) (N : ℕ)
       (hsize : source.length + target.length ≤ N)
       (input : ComputedFamilyInput source target N) (key : ComputedFamilyTableKey source target N) :
       |computedFamilyTableValue source target N input key| ≤ (((32 * inputSmallLog N + 1) * N : ℕ) : ℚ) := by
   …

   Mentions: OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.ComputedFamilyTableKey, OAI.EditApproximation.computedFamilyTableValue, OAI.EditApproximation.inputSmallLog

2. theorem OAI.EditApproximation.computedQueryMemoNormalized_width line 44