Theorems · Theorem · information theory

InformationTheory.integral_llr_compProd_eq_add

∀ {𝓧 : 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 κ) →
      ∫ (p : 𝓧 × 𝓨), MeasureTheory.llr (μ.compProd κ) (ν.compProd η) p ∂μ.compProd κ =
        ∫ (a : 𝓧), MeasureTheory.llr μ ν a ∂μ +
          ∫ (p : 𝓧 × 𝓨), MeasureTheory.llr (μ.compProd κ) (μ.compProd η) p ∂μ.compProd κ

Chain rule for the integral of the log-likelihood ratio, under absolute continuity and integrability assumptions.

Defined in

Mathlib.InformationTheory.KullbackLeibler.ChainRule

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasureProbabilityTheory.IsMarkovKernelProbabilityTheory.IsMarkovKernel