OAI/Combinatorics/EditApproximation/Coarse/CoarseReadNumericalBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.coarseDescriptorWithWork_height_bound line 10

   Source documentation

   The same small numerical envelope covers constructing a node's length.

   theorem coarseDescriptorWithWork_height_bound (B d n offset H : ℕ)
       (hH : 10 ≤ H) (hd : d ≤ H) (hB : Nat.size B ≤ H ^ 3)
       (hn : Nat.size n ≤ H ^ 3) (ho : Nat.size offset ≤ H ^ 3) :
       (coarseDescriptorWithWork B d n offset).2 ≤ H ^ 30 := by
   …

   Mentions: OAI.EditApproximation.coarseDescriptorWithWork

2. theorem OAI.EditApproximation.coarseChildOffsetWithWork_height_bound line 30
3. theorem OAI.EditApproximation.coarseReadShiftWithWork_height_bound line 40