Documentation

Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

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 #

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

Log-Likelihood Ratio between two measures.

Equations
Instances For
    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)) =ᵐ[ν] 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 ν) :
    (fun (x : α) => Real.exp (MeasureTheory.llr μ ν x)) =ᵐ[μ] 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 μ) :
    (fun (x : α) => Real.exp (MeasureTheory.llr μ ν x)) =ᵐ[ν] fun (x : α) => (μ.rnDeriv ν x).toReal
    theorem MeasureTheory.neg_llr {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) :
    theorem MeasureTheory.exp_neg_llr {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (hμν : μ.AbsolutelyContinuous ν) :
    (fun (x : α) => Real.exp (-MeasureTheory.llr μ ν x)) =ᵐ[μ] 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 μ) :
    (fun (x : α) => Real.exp (-MeasureTheory.llr μ ν x)) =ᵐ[ν] fun (x : α) => (ν.rnDeriv μ x).toReal
    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 ) :
    MeasureTheory.llr (c μ) ν =ᵐ[μ] 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 μ] [μ.HaveLebesgueDecomposition ν] (hμν : μ.AbsolutelyContinuous ν) (c : ENNReal) (hc : c 0) (hc_ne_top : c ) :
    MeasureTheory.llr μ (c ν) =ᵐ[μ] 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μν : μ.AbsolutelyContinuous ν) (hf : MeasureTheory.Integrable (fun (x : α) => Real.exp (f x)) μ) (hfν : AEMeasurable f ν) :
    MeasureTheory.llr (μ.tilted f) ν =ᵐ[μ] 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μν : μ.AbsolutelyContinuous ν) (hf : MeasureTheory.Integrable f μ) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) (hfμ : MeasureTheory.Integrable (fun (x : α) => Real.exp (f x)) μ) (hfν : AEMeasurable 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 : α) => 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μν : μ.AbsolutelyContinuous ν) (hf : MeasureTheory.Integrable (fun (x : α) => Real.exp (f x)) ν) :
    MeasureTheory.llr μ (ν.tilted f) =ᵐ[μ] 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μν : μ.AbsolutelyContinuous ν) (hfμ : MeasureTheory.Integrable f μ) (h_int : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ) (hfν : MeasureTheory.Integrable (fun (x : α) => Real.exp (f x)) ν) :
    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 : α) => 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)ν)