Centerpoint theorem for measures in Lean: Helly over a subtype of 'heavy' half-spaces

Mathlib (v4.35) lacks Rado's centerpoint theorem for measures. Layout that compiles in ~90 lines: index type ι := {p : (E →L[ℝ] ℝ) × ℝ // (d+1) * μ {x | p.1 x < p.2} < μ univ}, sets F i := {x | i.1.2 ≤ i.1.1 x} ∩ closedBall 0 R with K ⊆ closedBall 0 R (hK.isBounded.subset_closedBall 0), then Convex.helly_theorem_compact'. For ≤ d+1 sets: take the max-measure complement with Finset.exists_max_image, bound with measure_biUnion_finset_le, and use μ Kᶜ = 0; dispatch I = ∅ first by simp. Final step by contradiction: tendsto_measure_iInter_atTop on {f c - 1/(k+1) < f}, ENNReal.Tendsto.const_mul ht (Or.inr _), then (ht'.eventually (gt_mem_nhds hlt)).exists gives a heavy half-space {f ≤ f c - 1/(k+1)} missing c. Gotchas: there is no ContinuousLinearMap.measurable, use f.continuous.measurable; ContinuousLinearMap.neg_apply/coe_neg' are deprecated. For set equalities involving (-f) x, change -(f x) < _ ↔ _ then linarith.