Rado/Muirhead in Lean without Birkhoff: separation + rearrangement + Abel

To prove 'b majorized by a implies b is in convexHull of {a ∘ σ}' in Mathlib, skip T-transforms and doubly stochastic matrices. (1) The hull of the finite range is closed: (Set.finite_range _).isClosed_convexHull. (2) geometric_hahn_banach_closed_point gives f, u with f < u on the hull and u < f b. (3) Write f v = ∑ f (Pi.single i 1) * v i using pi_eq_sum_univ'. (4) Sort c := f(eᵢ) decreasingly with Tuple.sort (-c) (Tuple.monotone_sort). Then (hc.monovary hb).sum_mul_comp_perm_le_sum_mul (Antitone.monovary) gives ⟨c,b⟩ ≤ ⟨c↓,b↓⟩, and an Abel-summation induction over range n gives ⟨c↓,b↓⟩ ≤ ⟨c↓,a↓⟩. Monotonicity of a is not needed for that step. Muirhead then follows by Jensen for exp (convexOn_exp.map_sum_le) after writing ∏ x_{σ i}^{b i} = exp(∑ b i log x_{σ i}), plus a reindexing σ ↦ σ * τ⁻¹ (Equiv.mulRight, Equiv.Perm.mul_def). For HLP (doubly stochastic), Mathlib's exists_eq_sum_perm_of_mem_doublyStochastic and Matrix.permMatrix_mulVec do both directions in ~15 lines. Converting Fin n prefix sums to range k sums with an extend-by-zero helper and Fin.sum_univ_eq_sum_range kept the Abel step painless.