TreePathHull.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.PlanarRecursion.rootedTreePath line 17
Source documentation
The unique actual tree path; uniqueness is proved, not assumed by a surrogate tree structure. The distance-minimizing library witness fixes it.
```
def rootedTreePath (G : SimpleGraph V) (hG : G.IsTree) (r a : V) : G.Walk r a :=
…
```
lemma OAI.HyperbolicObstruction.PlanarRecursion.rootedTreePath_isPath line 20
lemma OAI.HyperbolicObstruction.PlanarRecursion.rootedTreePath_length line 24
def OAI.HyperbolicObstruction.PlanarRecursion.treePathHull line 31
Source documentation
Union of the root paths to a finite collection of terminals.
```
def treePathHull (G : SimpleGraph V) (hG : G.IsTree) (r : V) (A : Finset V) : Finset V :=
…
```
lemma OAI.HyperbolicObstruction.PlanarRecursion.mem_treePathHull line 34
lemma OAI.HyperbolicObstruction.PlanarRecursion.subset_treePathHull line 38
lemma OAI.HyperbolicObstruction.PlanarRecursion.treePathHull_rootClosed line 43
theorem OAI.HyperbolicObstruction.PlanarRecursion.treePathHull_card_le line 57
Source documentation
The bounded-radius part of the planar-separator size estimate. A face with at most three distinct corners contributes at most 3*(radius+1) vertices to its rooted path hull. No bound on the number of other vertices or on the tree's valence is imposed.
```
theorem treePathHull_card_le (G : SimpleGraph V) (hG : G.IsTree) (r : V) (A : Finset V)
    (R : ℕ) (hR : ∀ a ∈ A, G.dist r a ≤ R) :
    (treePathHull G hG r A).card ≤ A.card * (R+1) := by
…
```
Mentions: OAI.HyperbolicObstruction.PlanarRecursion.treePathHull