Theorems · Theorem · measure theory

MeasureTheory.exp_llr

∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ],
  (fun x => Real.exp (MeasureTheory.llr μ ν x)) =ᵐ[ν] fun x => if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

Defined in

Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SigmaFinite