∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f : α → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable f μ →
      MeasureTheory.Integrable (fun x => Real.exp (f x)) ν →
        MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
          ∫ (x : α), MeasureTheory.llr μ (ν.tilted f) x ∂μ =
            ∫ (x : α), MeasureTheory.llr μ ν x ∂μ - ∫ (x : α), f x ∂μ + Real.log (∫ (x : α), Real.exp (f x) ∂ν)