Theorems · Theorem · information theory

InformationTheory.rnDeriv_compProd_mul_log_eq_mul_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 η) →
    ∀ᵐ (p : 𝓧 × 𝓨) ∂ν.compProd η,
      ((μ.compProd κ).rnDeriv (ν.compProd η) p).toReal * Real.log ((μ.compProd κ).rnDeriv (ν.compProd η) p).toReal =
        ((μ.compProd κ).rnDeriv (ν.compProd η) p).toReal *
          (Real.log (μ.rnDeriv ν p.1).toReal + Real.log ((μ.compProd κ).rnDeriv (μ.compProd η) p).toReal)

Defined in

Mathlib.InformationTheory.KullbackLeibler.ChainRule

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasureProbabilityTheory.IsMarkovKernelProbabilityTheory.IsMarkovKernel