EReal-valued log likelihood ratio

Main definitions

• EReal.llr: log-likelihood ratio, with value in EReal.

Main statements

• EReal.exp_llr: EReal.exp (EReal.llr μ ν x) = μ.rnDeriv ν x

noncomputable def MeasureTheory.EReal.llr {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (x : α) : EReal

Log-likelihood ratio between two measures: logarithm (using ENNReal.log) of the Radon-Nikodym derivative.

Equations

• MeasureTheory.EReal.llr μ ν x = (μ.rnDeriv ν x).log

theorem MeasureTheory.EReal.llr_def {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : MeasureTheory.EReal.llr μ ν = fun (x : α) => (μ.rnDeriv ν x).log

theorem MeasureTheory.EReal.exp_llr {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) (x : α) : (MeasureTheory.EReal.llr μ ν x).exp = μ.rnDeriv ν x

theorem MeasureTheory.EReal.neg_llr {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) : -MeasureTheory.EReal.llr μ ν =ᵐ[μ] MeasureTheory.EReal.llr ν μ

theorem MeasureTheory.EReal.exp_neg_llr {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) : (fun (x : α) => (-MeasureTheory.EReal.llr μ ν x).exp) =ᵐ[μ] ν.rnDeriv μ

theorem MeasureTheory.EReal.exp_neg_llr' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : ν.AbsolutelyContinuous μ) : (fun (x : α) => (-MeasureTheory.EReal.llr μ ν x).exp) =ᵐ[ν] ν.rnDeriv μ

theorem MeasureTheory.measurable_ereal_llr {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : Measurable (MeasureTheory.EReal.llr μ ν)

theorem MeasureTheory.stronglyMeasurable_ereal_llr {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) : MeasureTheory.StronglyMeasurable (MeasureTheory.EReal.llr μ ν)

theorem MeasureTheory.EReal.llr_smul_left {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) (c : ENNReal) (hc_ne_top : c ≠ ⊤) : MeasureTheory.EReal.llr (c • μ) ν =ᵐ[μ] fun (x : α) => MeasureTheory.EReal.llr μ ν x + c.log

theorem MeasureTheory.EReal.llr_smul_right {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) (c : ENNReal) (hc : c ≠ 0) (hc_ne_top : c ≠ ⊤) : MeasureTheory.EReal.llr μ (c • ν) =ᵐ[μ] fun (x : α) => MeasureTheory.EReal.llr μ ν x - c.log