1.4. ForMathlib.InformationTheory.KullbackLeibler.CompProd
From the authors
Lemmas about the Kullback-Leibler divergence of the images of two measures by a measurable map
Module LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.CompProd contains 5 exposed declarations.
-
MeasureTheory.Measure.map_compProd_comap -
MeasureTheory.Measure.map_withDensity_comp -
InformationTheory.klDiv_withDensity_comp_map -
InformationTheory.klDiv_map_of_eq_withDensity_comp -
InformationTheory.klDiv_compProd_comap