LeanMachineLearning

3.10. SequentialLearning.AlgorithmDensity🔗

Algorithm density

We define a density function that allows obtaining the law of the history under one algorithm from the law of the history under another algorithm when they are interacting with the same environment. This also requires one algorithm to be absolutely continuous with respect to another, a concept that we also introduce here.

Main definitions

  • AbsolutelyContinuous alg alg₀: alg is absolutely continuous with respect to alg₀ (also denoted alg ≪ₐ alg₀) when, in every situation, a set of actions with probability zero under alg₀ also has probability zero under alg. Intuitively, alg never acts in a way that alg₀ would never act.

  • density alg alg₀ n: a density function that allows obtaining the law of the history at time n under alg from the law of the history at time n under alg₀ when they are interacting with the same environment and alg ≪ₐ alg₀.

Main results

  • absolutelyContinuous_map_hist: the law of the history at time n under alg is absolutely continuous with respect to the law of the history at time n under alg₀ when they are interacting with the same environment and alg ≪ₐ alg₀.

  • hasLaw_history_withDensity: the law of the history at time n under alg is the law of the history at time n under alg₀ with density alg.density alg₀ n when they are interacting with the same environment and alg ≪ₐ alg₀.

Module LeanMachineLearning.SequentialLearning.AlgorithmDensity contains 6 exposed declarations.