Log-likelihood Ratio

The likelihood ratio between two measures μ and ν is their Radon-Nikodym derivative μ.rnDeriv ν. The logarithm of that function is often used instead: this is the log-likelihood ratio.

This file contains a definition of the log-likelihood ratio (llr) and its properties.

Main definitions

• llr μ ν: Log-Likelihood Ratio between μ and ν, defined as the function x ↦ log (μ.rnDeriv ν x).toReal.

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

Log-Likelihood Ratio between two measures.

Equations

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

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

theorem MeasureTheory.exp_llr {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : ν.ae.EventuallyEq (fun (x : α) => (MeasureTheory.llr μ ν x).exp) fun (x : α) => if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal

theorem MeasureTheory.exp_llr_of_ac {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) : μ.ae.EventuallyEq (fun (x : α) => (MeasureTheory.llr μ ν x).exp) fun (x : α) => (μ.rnDeriv ν x).toReal

theorem MeasureTheory.exp_llr_of_ac' {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : ν.AbsolutelyContinuous μ) : ν.ae.EventuallyEq (fun (x : α) => (MeasureTheory.llr μ ν x).exp) fun (x : α) => (μ.rnDeriv ν x).toReal

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

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

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

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

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

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

theorem MeasureTheory.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 ≠ ⊤) : μ.ae.EventuallyEq (MeasureTheory.llr μ (c • ν)) fun (x : α) => MeasureTheory.llr μ ν x - c.toReal.log

theorem MeasureTheory.llr_tilted_left {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) (hf : MeasureTheory.Integrable (fun (x : α) => (f x).exp) μ) (hfν : AEMeasurable f ν) : μ.ae.EventuallyEq (MeasureTheory.llr (μ.tilted f) ν) fun (x : α) => f x - (∫ (z : α), (f z).exp ∂μ).log + MeasureTheory.llr μ ν x

theorem MeasureTheory.integrable_llr_tilted_left {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) (hf : MeasureTheory.Integrable f μ) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) (hfμ : MeasureTheory.Integrable (fun (x : α) => (f x).exp) μ) (hfν : AEMeasurable f ν) : MeasureTheory.Integrable (MeasureTheory.llr (μ.tilted f) ν) μ

theorem MeasureTheory.integral_llr_tilted_left {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) (hf : MeasureTheory.Integrable f μ) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) (hfμ : MeasureTheory.Integrable (fun (x : α) => (f x).exp) μ) (hfν : AEMeasurable f ν) : ∫ (x : α), MeasureTheory.llr (μ.tilted f) ν x ∂μ = ∫ (x : α), MeasureTheory.llr μ ν x ∂μ + ∫ (x : α), f x ∂μ - (∫ (x : α), (f x).exp ∂μ).log

theorem MeasureTheory.llr_tilted_right {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) (hf : MeasureTheory.Integrable (fun (x : α) => (f x).exp) ν) : μ.ae.EventuallyEq (MeasureTheory.llr μ (ν.tilted f)) fun (x : α) => -f x + (∫ (z : α), (f z).exp ∂ν).log + MeasureTheory.llr μ ν x

theorem MeasureTheory.integrable_llr_tilted_right {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) (hfμ : MeasureTheory.Integrable f μ) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) (hfν : MeasureTheory.Integrable (fun (x : α) => (f x).exp) ν) : MeasureTheory.Integrable (MeasureTheory.llr μ (ν.tilted f)) μ

theorem MeasureTheory.integral_llr_tilted_right {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) (hfμ : MeasureTheory.Integrable f μ) (hfν : MeasureTheory.Integrable (fun (x : α) => (f x).exp) ν) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) : ∫ (x : α), MeasureTheory.llr μ (ν.tilted f) x ∂μ = ∫ (x : α), MeasureTheory.llr μ ν x ∂μ - ∫ (x : α), f x ∂μ + (∫ (x : α), (f x).exp ∂ν).log