ChannelCapacity.ChainRule

Bridge lemmas relating mutual information to KL divergences against fixed output references.

The main theorem rewrites the KL divergence from the joint law p ⊗ k to the product p ⊗ const ν as the mutual information plus the KL divergence of the induced output law against ν.

theorem ChannelCapacity.klDiv_mutualInformation_chain {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [StandardBorelSpace α] [Nonempty α] (k : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel k] (p : MeasureTheory.ProbabilityMeasure α) (ν : MeasureTheory.Measure β) [MeasureTheory.IsFiniteMeasure ν] : InformationTheory.klDiv (↑(jointLaw k p)) ((↑p).compProd (ProbabilityTheory.Kernel.const α ν)) = InformationTheory.klDiv ↑(jointLaw k p) ↑(independentJointLaw k p) + InformationTheory.klDiv (↑(outputPrior k p)) ν