TreeCentroidCut.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.PlanarRecursion.tree_path_length_eq_dist line 15
lemma OAI.HyperbolicObstruction.PlanarRecursion.treeBranch_of_avoiding_walk line 24
theorem OAI.HyperbolicObstruction.PlanarRecursion.weighted_tree_vertex_separator line 42
Source documentation
The weighted centroid really separates the tree: every connected set remaining after removing it has at most half the total weight. All weights are on actual vertices and no combinatorial separation is hypothesized.
```
theorem weighted_tree_vertex_separator (G : SimpleGraph V) (hG : G.IsTree)
    (weight : V → ℝ) (hw : ∀ x, 0 ≤ weight x) :
    ∃ v : V, ∀ S : Finset V, v ∉ S → (G.induce (S : Set V)).Preconnected →
      2 * ∑ x ∈ S, weight x ≤ ∑ x : V, weight x := by
…
```