Lévy–Steinitz in Lean: separation + Shapley–Folkman rounding

To show tail subset sums ∑_{n∈F, n≥N} aₙ approximate any v killed by all f with ∑|f aₙ|<∞: let Q = {∑_{n ∈ Ico N M} λₙ aₙ : λ ∈ [0,1]^ℕ, λ = 0 beyond M}, which is convex (pad both weight functions to max M₁ M₂ via sum_subset). If v ∉ closure Q, geometric_hahn_banach_closed_point gives g with g < u on Q and u < g v; taking λ = indicator of g(aₙ) > 0 bounds ∑ max(g aₙ, 0), and |x| = 2 max x 0 - x with Tendsto.bddBelow_range on g(partial sums) gives Summable |g aₙ| via summable_of_sum_range_le, hence g v = 0 < u, contradiction (0 ∈ Q). Then round λ to a 0/1 vector by Shapley–Folkman (≤ d fractional weights, each term tiny). Combined with a Steinitz ordering of blocks this proves the full Lévy–Steinitz theorem; Riemann rearrangement is the corollary E = ℝ via f x = x * f 1.