Treedepth
Lax183560.TreeDepth · concepts/Lax183560/TreeDepth.lean · lax-183560
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The treedepth of a graph is the minimum height of a rooted forest on its vertex set whose closure contains the graph. The closure joins every vertex to each of its ancestors, and height counts the vertices on a longest root-to-leaf path. The empty graph has treedepth zero.
Concept map
Lean source view on GitHub
| 1 | import Lax183560.AncestorForest |
| 2 | import Mathlib.Order.Lattice.Nat |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Treedepth |
| 7 | type: definition |
| 8 | --- |
| 9 | The treedepth of a graph is the minimum height of a rooted forest on its |
| 10 | vertex set whose closure contains the graph. The closure joins every vertex |
| 11 | to each of its ancestors, and height counts the vertices on a longest |
| 12 | root-to-leaf path. The empty graph has treedepth zero. |
| 13 | -/ |
| 14 | |
| 15 | namespace Lax183560.TreeDepth |
| 16 | |
| 17 | open Lax183560.AncestorForest |
| 18 | |
| 19 | /-- `G` lies in the closure of a forest of vertex height at most `k`. -/ |
| 20 | def HasTreedepthAtMost {V : Type} (G : SimpleGraph V) (k : ℕ) : Prop := |
| 21 | ∃ F : AncestorForest V, |
| 22 | (∀ ⦃u v : V⦄, G.Adj u v → (F.ancestor u v ∨ F.ancestor v u)) ∧ |
| 23 | ∃ rank : V → Fin k, |
| 24 | ∀ ⦃u v : V⦄, F.ancestor u v → rank u < rank v |
| 25 | |
| 26 | /-- The minimum height of a rooted forest whose closure contains `G`. -/ |
| 27 | noncomputable def treedepth {V : Type} [Fintype V] [DecidableEq V] |
| 28 | (G : SimpleGraph V) : ℕ := |
| 29 | sInf {k | HasTreedepthAtMost G k} |
| 30 | |
| 31 | end Lax183560.TreeDepth |
| 32 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments