TreeCentroid.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.PlanarRecursion.treeBranch line 15
Source documentation
The side of an oriented tree edge towards its second endpoint.
```
def treeBranch (G : SimpleGraph V) (v w : V) : Finset V :=
…
```
theorem OAI.HyperbolicObstruction.PlanarRecursion.weighted_tree_centroid line 21
Source documentation
A finite weighted tree has a centroid: each branch at the selected vertex has at most half the total weight. This is a genuine weighted-tree theorem, not a planar-separator assumption.
```
theorem weighted_tree_centroid (G : SimpleGraph V) (hG : G.IsTree) (weight : V → ℝ) :
    ∃ v : V, ∀ w : V, G.Adj v w →
      2 * ∑ x ∈ treeBranch G v w, weight x ≤ ∑ x : V, weight x := by
…
```
Mentions: OAI.HyperbolicObstruction.PlanarRecursion.treeBranch