∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] (f : α → ℝ)
  (s : Set α), (μ.tilted f) s = ENNReal.ofReal (∫ (a : α) in s, Real.exp (f a) / ∫ (x : α), Real.exp (f x) ∂μ ∂μ)