Theorems · Theorem · information theory

InformationTheory.integrable_llr_of_integrable_llr_compProd

∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  {κ η : ProbabilityTheory.Kernel 𝓧 𝓨} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η],
  (μ.compProd κ).AbsolutelyContinuous (ν.compProd η) →
    MeasureTheory.Integrable (MeasureTheory.llr (μ.compProd κ) (ν.compProd η)) (μ.compProd κ) →
      MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ

If the log-likelihood ration between two composition-products is integrable, then so is the log-likelihood ratio between the two measures on the first space.

Defined in

Mathlib.InformationTheory.KullbackLeibler.ChainRule

Cited by

1 results in Mathlib

Foundations

Depth 270 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasureProbabilityTheory.IsMarkovKernelProbabilityTheory.IsMarkovKernel