Theorems · Theorem · information theory

InformationTheory.integrable_llr_compProd_iff

∀ {𝓧 : 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 μ ν) μ ∧
        MeasureTheory.Integrable (MeasureTheory.llr (μ.compProd κ) (μ.compProd η)) (μ.compProd κ))

Defined in

Mathlib.InformationTheory.KullbackLeibler.ChainRule

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasureProbabilityTheory.IsMarkovKernelProbabilityTheory.IsMarkovKernel