Theorems · Theorem · measure theory

MeasureTheory.integral_rnDeriv_mul_log

∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν →
    ∫ (a : α), (μ.rnDeriv ν a).toReal * Real.log (μ.rnDeriv ν a).toReal ∂ν = ∫ (a : α), MeasureTheory.llr μ ν a ∂μ

Defined in

Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.SigmaFiniteMeasureTheory.Measure.HaveLebesgueDecomposition