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 α} (μ ν : Measure α) (x : α) : ℝ

Log-Likelihood Ratio between two measures.

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

theorem MeasureTheory.llr_self {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] : llr μ μ =ᵐ[μ] 0

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

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

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

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

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

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

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

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

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

theorem MeasureTheory.llr_smul_nnreal_left {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) (c : NNReal) (hc : c ≠ 0) : llr (c • μ) ν =ᵐ[μ] fun (x : α) => llr μ ν x + Real.log ↑c

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

theorem MeasureTheory.llr_smul_nnreal_right {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) (c : NNReal) (hc : c ≠ 0) : llr μ (c • ν) =ᵐ[μ] fun (x : α) => llr μ ν x - Real.log ↑c

theorem MeasureTheory.llr_smul_inv_left_eq_smul_right {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) (c : ENNReal) (hc : c ≠ 0) (hc_ne_top : c ≠ ⊤) : llr (c⁻¹ • μ) ν =ᵐ[μ] llr μ (c • ν)

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

theorem MeasureTheory.llr_smul_nnreal_same {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) (c : NNReal) (hc : c ≠ 0) : llr (c • μ) (c • ν) =ᵐ[μ] llr μ ν

theorem MeasureTheory.integrable_rnDeriv_mul_log_iff {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} [SigmaFinite μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) : Integrable (fun (a : α) => (μ.rnDeriv ν a).toReal * Real.log (μ.rnDeriv ν a).toReal) ν ↔ Integrable (llr μ ν) μ

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

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

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

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

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

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

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