OAI/MeasureTheory/DyadicAvoidance/WindowMetadata.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem310.WindowMetadata.edgeIndex line 14

   Source documentation

   The canonical preorder index of an edge.

   def edgeIndex {q d : ℕ} (e : Edge q d) : ℕ := (edgePaths q d).idxOf e.val

2. def OAI.Problem310.WindowMetadata.edgeHeight line 17

   Source documentation

   Numeric incoming-window height for an edge path.

   def edgeHeight {q d : ℕ} (e : Edge q d) : ℕ := d + 1 - e.val.length

3. def OAI.Problem310.WindowMetadata.lengths line 20

   Source documentation

   Window lengths in precisely the canonical tree-edge preorder.

   def lengths (q d g r₀ : ℕ) : List ℕ :=
   …

4. def OAI.Problem310.WindowMetadata.lengthAt line 24

   Source documentation

   The length function consumed by the canonical numeric placement API.

   def lengthAt (q d g r₀ : ℕ) : ℕ → ℕ :=
   …

5. def OAI.Problem310.WindowMetadata.start line 27
6. def OAI.Problem310.WindowMetadata.finish line 30
7. def OAI.Problem310.WindowMetadata.window line 33
8. theorem OAI.Problem310.WindowMetadata.edgeIndex_lt line 36
9. theorem OAI.Problem310.WindowMetadata.edgeHeight_pos line 39
10. theorem OAI.Problem310.WindowMetadata.lengthAt_edgeIndex line 44
11. theorem OAI.Problem310.WindowMetadata.lengthAt_edgeIndex_pos line 50
12. theorem OAI.Problem310.WindowMetadata.threshold_le_window_length line 55
13. theorem OAI.Problem310.WindowMetadata.card_window line 60
14. theorem OAI.Problem310.WindowMetadata.three_le_start line 64
15. theorem OAI.Problem310.WindowMetadata.start_le_finish line 67
16. theorem OAI.Problem310.WindowMetadata.mem_window line 71
17. theorem OAI.Problem310.WindowMetadata.three_le_of_mem line 75
18. theorem OAI.Problem310.WindowMetadata.gap_of_index_lt line 79
19. theorem OAI.Problem310.WindowMetadata.child_height line 83
20. theorem OAI.Problem310.WindowMetadata.child_window_card line 87