OAI/Combinatorics/EditApproximation/Geometry/OccurrenceStorage.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EditApproximation.PositionCounts.CountsLE line 12

   Source documentation

   All counters allocated in the position trie are bounded.

   def CountsLE (C : ℕ) : PositionCounts → Prop
     | .empty => True
     | .node n l r => n ≤ C ∧ CountsLE C l ∧ CountsLE C r

   Mentions: OAI.EditApproximation.PositionCounts

2. theorem OAI.EditApproximation.PositionCounts.CountsLE.mono line 16
3. theorem OAI.EditApproximation.PositionCounts.CountsLE.count line 22
4. theorem OAI.EditApproximation.PositionCounts.CountsLE.left line 28
5. theorem OAI.EditApproximation.PositionCounts.CountsLE.right line 34
6. theorem OAI.EditApproximation.PositionCounts.CountsLE.add line 40
7. theorem OAI.EditApproximation.PositionCounts.storageBits_le line 54

   Source documentation

   A tag, two child pointers, and the binary counter at each allocated node.

   theorem storageBits_le {tree : PositionCounts} {C : ℕ} (h : tree.CountsLE C) :
       tree.storageBits ≤ (Nat.size C + 3) * tree.nodes := by
   …

   Mentions: OAI.EditApproximation.PositionCounts

8. theorem OAI.EditApproximation.BinaryMemo.valueStorage_le line 71

   Source documentation

   Concrete trie storage with the supplied stored-value representation.

   theorem valueStorage_le {α : Type*} (bits : α → ℕ) (W : ℕ) (memory : BinaryMemo α)
       (h : AllValues (fun a => bits a ≤ W) memory) :
       valueStorage bits memory ≤ (W + 3) * memory.nodes := by
   …

   Mentions: OAI.EditApproximation.BinaryMemo, OAI.EditApproximation.BinaryMemo.AllValues, OAI.EditApproximation.BinaryMemo.valueStorage

9. theorem OAI.EditApproximation.occurrenceBuild_nodes line 90
10. theorem OAI.EditApproximation.occurrenceBuild_values line 101
11. theorem OAI.EditApproximation.occurrenceBuild_storage line 124