TreePreorder.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem310.TreePreorder.edgePaths line 10

Source documentation

Edge paths in the complete ordered q-ary tree, in depth-first preorder.

def edgePaths (q : ℕ) : ℕ → List (List (Fin q))
  | 0 => []
  | d + 1 => (List.finRange q).flatMap fun i =>
      [i] :: (edgePaths q d).map (List.cons i)

/-- Number of edges in the complete tree. -/

def OAI.Problem310.TreePreorder.edgeCount line 16
Source documentation
Number of edges in the complete tree.
```
def edgeCount (q : ℕ) : ℕ → ℕ
  | 0 => 0
  | d + 1 => q * (1 + edgeCount q d)
```
theorem OAI.Problem310.TreePreorder.edgePaths_zero line 20
theorem OAI.Problem310.TreePreorder.edgePaths_succ line 22
theorem OAI.Problem310.TreePreorder.mem_edgePaths_iff line 27
Source documentation
Exactly the nonempty paths of length at most the tree depth occur.
```
theorem mem_edgePaths_iff (q d : ℕ) (p : List (Fin q)) :
    p ∈ edgePaths q d ↔ p ≠ [] ∧ p.length ≤ d := by
…
```
Mentions: OAI.Problem310.TreePreorder.edgePaths
theorem OAI.Problem310.TreePreorder.length_edgePaths line 51
theorem OAI.Problem310.TreePreorder.mem_childBlock_prefix line 59
Source documentation
Each child block consists entirely of paths with that child as first entry.
```
theorem mem_childBlock_prefix (q d : ℕ) (i : Fin q) (p : List (Fin q))
    (hp : p ∈ [i] :: (edgePaths q d).map (List.cons i)) :
    ∃ s, p = i :: s := by
…
```
Mentions: OAI.Problem310.TreePreorder.edgePaths
theorem OAI.Problem310.TreePreorder.nodup_edgePaths line 68
Source documentation
The preorder contains no duplicate edge path.
```
theorem nodup_edgePaths (q d : ℕ) : (edgePaths q d).Nodup := by
…
```
Mentions: OAI.Problem310.TreePreorder.edgePaths
def OAI.Problem310.TreePreorder.Edge line 90
Source documentation
The finite type of tree edges, represented by nonempty bounded-depth paths.
```
def Edge (q d : ℕ) := {p : List (Fin q) // p ∈ edgePaths q d}
```
Mentions: OAI.Problem310.TreePreorder.edgePaths
instance OAI.Problem310.TreePreorder.(instance at line 92) line 92
theorem OAI.Problem310.TreePreorder.edge_nonempty line 97
theorem OAI.Problem310.TreePreorder.edge_length_le line 100
def OAI.Problem310.TreePreorder.mkEdge line 104
Source documentation
Convert a nonempty bounded path into the finite edge type.
```
def mkEdge {q d : ℕ} (p : List (Fin q)) (hne : p ≠ []) (hlen : p.length ≤ d) :
    Edge q d := ⟨p, (mem_edgePaths_iff q d p).mpr ⟨hne, hlen⟩⟩
```
Mentions: OAI.Problem310.TreePreorder.Edge, OAI.Problem310.TreePreorder.mem_edgePaths_iff
theorem OAI.Problem310.TreePreorder.mkEdge_val line 107
def OAI.Problem310.TreePreorder.edgeEquivFin line 112
Source documentation
The preorder gives the canonical enumeration of finite tree edges.
```
def edgeEquivFin (q d : ℕ) : Edge q d ≃ Fin (edgeCount q d) :=
…
```
Mentions: OAI.Problem310.TreePreorder.Edge, OAI.Problem310.TreePreorder.edgeCount
theorem OAI.Problem310.TreePreorder.card_Edge line 116
def OAI.Problem310.TreePreorder.childEdge line 120
Source documentation
Edges corresponding to appending a child at a strict internal node.
```
def childEdge {q d : ℕ} (P : List (Fin q)) (hP : P.length < d) (i : Fin q) :
    Edge q d := mkEdge (P ++ [i]) (by simp) (by simp; omega)
```
Mentions: OAI.Problem310.TreePreorder.Edge, OAI.Problem310.TreePreorder.mkEdge
theorem OAI.Problem310.TreePreorder.childEdge_val line 123
theorem OAI.Problem310.TreePreorder.childEdge_injective line 127
Source documentation
Child edges at fixed parent are distinct.
```
theorem childEdge_injective {q d : ℕ} (P : List (Fin q)) (hP : P.length < d) :
    Function.Injective (childEdge P hP) := by
…
```
Mentions: OAI.Problem310.TreePreorder.childEdge

theorem OAI.Problem310.TreePreorder.subtree_block line 135

Source documentation

The incoming edge of a subtree and all its descendants form one consecutive block in the depth-first edge preorder.

theorem subtree_block (q d : ℕ) (p : List (Fin q)) (hne : p ≠ []) (hlen : p.length ≤ d) :
    ∃ pre post : List (List (Fin q)),
      edgePaths q d = pre ++
        (p :: (edgePaths q (d - p.length)).map (fun s => p ++ s)) ++ post := by
…

Mentions: OAI.Problem310.TreePreorder.edgePaths

theorem OAI.Problem310.TreePreorder.subtree_block_index line 168

Source documentation

In the subtree decomposition, the prefix length is exactly the preorder index.

theorem subtree_block_index (q d : ℕ) (p : List (Fin q))
    (hne : p ≠ []) (hlen : p.length ≤ d) :
    ∃ pre post : List (List (Fin q)),
      edgePaths q d = pre ++
        (p :: (edgePaths q (d - p.length)).map (fun s => p ++ s)) ++ post ∧
      pre.length = (edgePaths q d).idxOf p := by
…

Mentions: OAI.Problem310.TreePreorder.edgePaths