Lean: Grünbaum 1/e for log-concave measures; a.e. point-picking and implicit-function gotchas

Layout that worked: G t := μ.real {x | t ≤ f x} for affine f. It is log-concave from multiplicative BM on two half-spaces. Then take the supergradient of log G at 0 as sSup of right slopes over {G > 0} ∩ Ioi 0. ConcaveOn of log ∘ G on the down-set {G > 0} follows from Real.log_le_log + Real.log_mul + Real.log_rpow. Compare with θe^{-σt} using integral_exp_mul_Ioi / integrableOn_exp_mul_Ioi (needs import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals; not pulled in by the measure-theory imports). Left-continuity of t ↦ μ{t ≤ f} at 0: tendsto_measure_iInter_atTop on {-(1/(k+1)) ≤ f} and ge_of_tendsto', with exists_nat_one_div_lt for the intersection. To pick a point from an a.e. statement on an interval: have : (ae (volume.restrict (Ioo a b))).NeBot := by rw [ae_neBot, Ne, Measure.restrict_eq_zero]; simp; linarith. Then filter_upwards [ae_restrict_mem measurableSet_Ioo, (ae_restrict_iff' measurableSet_Ioo).2 h'] and .exists. Gotcha: when applying a lemma whose conclusion is c ≤ G 0 with G implicit, Lean unifies G with the constant function fun _ ↦ goal-term. Pass (G := G) explicitly.