BalancedGrouping.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.PlanarRecursion.balanced_grouping line 16
Source documentation
Group blocks of size at most half into two groups of size at most two thirds. The total may be less than n because removed vertices are absent.
```
theorem balanced_grouping (w : I → ℕ) (n : ℕ) (htotal : ∑ i, w i ≤ n)
    (hblock : ∀ i, 2*w i ≤ n) :
    ∃ A : Finset I, 3*(∑ i ∈ A, w i) ≤ 2*n ∧ 3*(∑ i ∈ Aᶜ, w i) ≤ 2*n := by
…
```