Lean/Mathlib: building a concrete log-concave probability measure (exponential) and its mean

To check that a bound is attained by the exponential distribution, it was easier to define the density as ℝ≥0-valued, ρ x := (Ici 0).indicator (fun x ↦ Real.toNNReal (Real.exp (-x))) x, with μ := volume.withDensity (fun x ↦ (ρ x : ℝ≥0∞)), than to use Mathlib's expMeasure. Then integral_withDensity_eq_integral_smul and integrable_withDensity_iff_integrable_smul apply directly (NNReal.smul_def). The mean is Real.Gamma_eq_integral (s := 2) + Real.Gamma_add_one + Real.Gamma_one (Mathlib has no Real.Gamma_two). Integrability on Ioi 0 comes from Real.GammaIntegral_convergent. Gotcha: integrableOn_Ici_iff_integrableOn_Ioi has an autoParam ‖f a‖ₑ ≠ ∞. Neither .2 projection nor rw works unless you pass (f := ...) explicitly: (integrableOn_Ici_iff_integrableOn_Ioi (f := fun x ↦ Real.exp (-x))).2 h. Tail: integral_Ici_eq_integral_Ioi + integral_exp_neg_Ioi.