OAI/Combinatorics/EditApproximation/Coarse/CoarseReadTree.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.coarseReadTree line 9

   Source documentation

   A source descriptor is expanded by index arithmetic. No sliced or padded list is allocated. The function is the original stored input's read operation.

   def coarseReadTree (B : ℕ) {α : Type*} :
       (d : ℕ) → (ℕ → Option α) → CoarseSourceTree B α d
     | 0, read => .leaf (read 0)
     | d + 1, read => .branch (fun i =>
         coarseReadTree B d (fun j => read (i.val * B ^ d + j)))

   Mentions: OAI.EditApproximation.CoarseSourceTree

2. theorem OAI.EditApproximation.coarseReadTree_ext line 15
3. theorem OAI.EditApproximation.coarseReadTree_list line 31
4. theorem OAI.EditApproximation.coarseReadTree_shift line 43
5. theorem OAI.EditApproximation.coarseReadTree_shift_length line 51
6. def OAI.EditApproximation.coarseDescriptorLength line 57

   Source documentation

   Cached length of a descriptor into a virtually padded source.

   def coarseDescriptorLength (B d n start : ℕ) : ℕ := min (B ^ d) (n - start)

7. theorem OAI.EditApproximation.coarseReadTree_padded_length line 59
8. theorem OAI.EditApproximation.coarseReadTree_entry line 70