The Kullback–Leibler divergence of restrictions of measures

The Kullback–Leibler divergence of two finite measures is the sum of the divergences of their restrictions to a measurable set and to its complement, so that restricting both measures to a measurable set does not increase the divergence, and the divergence is the supremum of the divergences of the restrictions to an increasing sequence of measurable sets covering the space.

Main statements

• klDiv_restrict_add_restrict_compl: the divergence is the sum of the divergences of the restrictions to a measurable set and to its complement.

• klDiv_restrict_le: restricting both measures to a measurable set does not increase the divergence.

• klDiv_eq_iSup_restrict: the divergence is the supremum of the divergences of the restrictions to an increasing sequence of measurable sets covering the space.