Theorems · Theorem · measure theory

MeasureTheory.toReal_rnDeriv_tilted_right

∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℝ} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  MeasureTheory.Integrable (fun x => Real.exp (f x)) ν →
    (fun x => (μ.rnDeriv (ν.tilted f) 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 259 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.SigmaFiniteMeasureTheory.SigmaFinite