Weight inequalities on forests

Monien and Preis's weighted-tree lemma finds a light adjacent pair when the leaves are heavy. We prove the underlying inequality by deleting a leaf, or a leaf together with its negative-weight neighbor. This avoids choosing rooted subtrees in the weighted argument.

theorem Algebraic.Cutwidth.Bisection.WeightedTree.Internal.sum_nonneg_of_leaf_nonneg {W : Type} [Fintype W] (H : SimpleGraph W) (forest : H.IsAcyclic) (w : W → ℝ) (leaves : ∀ (v : W), H.degree v ≤ 1 → 0 ≤ w v) (edges : ∀ (u v : W), H.Adj u v → 0 ≤ w u + w v) : 0 ≤ ∑ v : W, w v

theorem Algebraic.Cutwidth.Bisection.WeightedTree.Internal.exists_adjacent_pair_lt_of_sum_lt {W : Type} [Fintype W] (H : SimpleGraph W) (forest : H.IsAcyclic) (w : W → ℝ) {A : ℝ} (leaves : ∀ (v : W), H.degree v ≤ 1 → A ≤ w v) (total : ∑ v : W, w v < A * ↑(Fintype.card W)) : ∃ (u : W) (v : W), H.Adj u v ∧ w u + w v < 2 * A

theorem Algebraic.Cutwidth.Bisection.WeightedTree.Internal.exists_adjacent_pair_le_real {W : Type} [Fintype W] (H : SimpleGraph W) (tree : H.IsTree) (size : 1 < Fintype.card W) (w : W → ℝ) (nonneg : ∀ (v : W), 0 ≤ w v) (leaves : ∀ (v : W), H.degree v = 1 → ∑ x : W, w x ≤ (↑(Fintype.card W) - 1) * w v) : ∃ (u : W) (v : W), H.Adj u v ∧ (↑(Fintype.card W) - 1) * (w u + w v) ≤ 2 * ∑ x : W, w x

theorem Algebraic.Cutwidth.Bisection.WeightedTree.Internal.exists_adjacent_pair_le {W : Type} [Fintype W] (H : SimpleGraph W) (tree : H.IsTree) (size : 1 < Fintype.card W) (w : W → ℕ) (leaves : ∀ (v : W), H.degree v = 1 → ∑ x : W, w x ≤ (Fintype.card W - 1) * w v) : ∃ (u : W) (v : W), H.Adj u v ∧ (Fintype.card W - 1) * (w u + w v) ≤ 2 * ∑ x : W, w x