OAI/Geometry/HyperbolicGroups/TreeCentroidComponents.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PlanarRecursion.deleteIncidence_reachable_center_iff line 16
2. lemma OAI.HyperbolicObstruction.PlanarRecursion.deleteIncidence_center_component_iff line 25
3. theorem OAI.HyperbolicObstruction.PlanarRecursion.weighted_tree_component_separator line 38

   Source documentation

   Actual components after deleting a weighted tree centroid carry at most half the total mass. The isolated centroid component is explicitly excluded.

   theorem weighted_tree_component_separator (G : SimpleGraph V) (hG : G.IsTree)
       (weight : V → ℝ) (hw : ∀ x, 0 ≤ weight x) :
       ∃ v : V, ∀ C : (G.deleteIncidenceSet v).ConnectedComponent,
         C ≠ (G.deleteIncidenceSet v).connectedComponentMk v →
         2 * ∑ x ∈ C.supp.toFinset, weight x ≤ ∑ x : V, weight x := by
   …