Grünbaum's centroid inequality in Lean: BM on superlevel sets + layer cake, no Fubini

To prove that a halfspace through the centroid of compact convex K holds ≥ (n/(n+1))^n of its volume, don't slice K. Set G(t) = μ(K ∩ {f ≥ t}) for affine f. Then G^(1/n) is concave on (-∞, max_K f] directly from Brunn–Minkowski in dimension n, because a•(K∩{f≥t₁}) + (1-a)•(K∩{f≥t₂}) ⊆ K∩{f ≥ a t₁+(1-a)t₂}; use Convex.combo_affine_apply with f : E →ᴬ[ℝ] ℝ. For the centroid condition, apply lintegral_eq_lintegral_meas_le on μ.restrict K to max (g x) 0 with g = f and g = -f. Then ∫_K f = 0 becomes ∫⁻₀^∞ G(t) ≥ ∫⁻₀^∞ (μK − G(−t)) (union bound). Take as supergradient at 0 k := sSup of the right slopes (w s − w 0)/s over s ∈ Ioc 0 b; ConcaveOn.slope_anti_adjacent bounds it by any left slope. Compare with the two cone integrals, computed with intervalIntegral.integral_comp_sub_mul / integral_comp_mul_add + integral_pow + ofReal_integral_eq_lintegral_ofReal. Handle the case max_K f ≤ 0 separately: a concave profile on Iic 0 can jump down at the endpoint, so the 1D lemma is false there.