LeanMachineLearning

3.17. SequentialLearning.DivergenceDecomposition🔗

From the authors

The divergence decomposition

Let alg, alg' be algorithms, env, env' be environments, and consider two algorithm-environment sequences (O, A, Y) and (O', A', Y') of alg against env and of alg' against env', on arbitrary probability spaces (Ω, P) and (Ω', P'). The Kullback-Leibler divergence between the laws of the histories of the first M rounds is the sum, over the rounds t < M, of the conditional divergences of the step at round t given the first t rounds. Note that both arguments of the conditional term use the law of the first history, so that term measures only how the two step kernels differ. The same identity holds for the whole trajectory trajectory O A Y : Ω → (ℕ → Round 𝓞 𝓐 𝓨), with a series in place of the finite sum.

For a single algorithm run against two stationary environments with reward kernels κ and κ', the two step kernels share the observation kernel and the policy and differ only in the reward kernel, so the conditional divergence of a step is the conditional divergence of the reward given the played action. This is the divergence decomposition of bandit lower bounds.

Main statements

  • IsAlgEnvSeq.klDiv_map_history_stepKernel, IsAlgEnvSeq.klDiv_map_trajectory_stepKernel: the chain rule for the law of the history of the first M rounds and for the law of the trajectory.

  • IsAlgEnvSeq.klDiv_map_history_compProd, IsAlgEnvSeq.klDiv_map_history: the divergence decomposition for two stationary environments, in composition-product and in integral form.

  • IsAlgEnvSeq.klDiv_map_trajectory_compProd, IsAlgEnvSeq.klDiv_map_trajectory: the same two forms for the trajectory.

Module LeanMachineLearning.SequentialLearning.DivergenceDecomposition contains 9 exposed declarations.