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 = Real.log (μ.rnDeriv ν x).toReal

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

theorem MeasureTheory.exp_llr {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] : (fun (x : α) => Real.exp (MeasureTheory.llr μ ν x)) =ᶠ[MeasureTheory.Measure.ae ν] 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 μ] [MeasureTheory.Measure.HaveLebesgueDecomposition μ ν] (hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν) : (fun (x : α) => Real.exp (MeasureTheory.llr μ ν x)) =ᶠ[MeasureTheory.Measure.ae μ] 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μν : MeasureTheory.Measure.AbsolutelyContinuous ν μ) : (fun (x : α) => Real.exp (MeasureTheory.llr μ ν x)) =ᶠ[MeasureTheory.Measure.ae ν] fun (x : α) => (μ.rnDeriv ν x).toReal

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

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

theorem MeasureTheory.exp_neg_llr' {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : MeasureTheory.Measure.AbsolutelyContinuous ν μ) : (fun (x : α) => Real.exp (-MeasureTheory.llr μ ν x)) =ᶠ[MeasureTheory.Measure.ae ν] 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 μ] [MeasureTheory.Measure.HaveLebesgueDecomposition μ ν] (hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν) (c : ENNReal) (hc : c ≠ 0) (hc_ne_top : c ≠ ⊤) : MeasureTheory.llr (c • μ) ν =ᶠ[MeasureTheory.Measure.ae μ] fun (x : α) => MeasureTheory.llr μ ν x + Real.log c.toReal

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

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

theorem MeasureTheory.integrable_llr_tilted_left {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.SigmaFinite ν] (hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν) (hf : MeasureTheory.Integrable f μ) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) (hfμ : MeasureTheory.Integrable (fun (x : α) => Real.exp (f x)) μ) (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μν : MeasureTheory.Measure.AbsolutelyContinuous μ ν) (hf : MeasureTheory.Integrable f μ) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) (hfμ : MeasureTheory.Integrable (fun (x : α) => Real.exp (f x)) μ) (hfν : AEMeasurable f ν) : ∫ (x : α), MeasureTheory.llr (μ.tilted f) ν x ∂μ = ∫ (x : α), MeasureTheory.llr μ ν x ∂μ + ∫ (x : α), f x ∂μ - Real.log (∫ (x : α), Real.exp (f x) ∂μ)

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

theorem MeasureTheory.integrable_llr_tilted_right {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.SigmaFinite ν] (hμν : MeasureTheory.Measure.AbsolutelyContinuous μ ν) (hfμ : MeasureTheory.Integrable f μ) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) (hfν : MeasureTheory.Integrable (fun (x : α) => Real.exp (f x)) ν) : 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μν : MeasureTheory.Measure.AbsolutelyContinuous μ ν) (hfμ : MeasureTheory.Integrable f μ) (hfν : MeasureTheory.Integrable (fun (x : α) => Real.exp (f x)) ν) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) : ∫ (x : α), MeasureTheory.llr μ (ν.tilted f) x ∂μ = ∫ (x : α), MeasureTheory.llr μ ν x ∂μ - ∫ (x : α), f x ∂μ + Real.log (∫ (x : α), Real.exp (f x) ∂ν)