Theorems · Theorem · measure theory

MeasureTheory.toReal_rnDeriv_tilted_left

∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ℝ} {ν : MeasureTheory.Measure α}
  [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν],
  AEMeasurable f ν →
    (fun x => ((μ.tilted f).rnDeriv ν x).toReal) =ᵐ[ν] fun x =>
      (Real.exp (f x) / ∫ (x : α), Real.exp (f x) ∂μ) * (μ.rnDeriv ν x).toReal

Defined in

Mathlib.MeasureTheory.Measure.Tilted

Cited by

1 results in Mathlib

Foundations

Depth 254 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.SigmaFiniteMeasureTheory.SigmaFinite