Theorems · Theorem · measure theory

MeasureTheory.rnDeriv_tilted_right

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

Defined in

Mathlib.MeasureTheory.Measure.Tilted

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SigmaFiniteMeasureTheory.SigmaFinite