Theorems · Theorem · measure theory

MeasureTheory.rnDeriv_tilted_left

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

Defined in

Mathlib.MeasureTheory.Measure.Tilted

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SigmaFiniteMeasureTheory.SigmaFinite