LeanMachineLearning

3.10. SequentialLearning.Comap🔗

From the authors

Transport of algorithms and environments

Main definitions

  • Round.map fo fa fy, Hist.map fo fa fy: round-wise transport of a round and a history along maps of the observation, the action and the feedback, with the special cases mapObs, mapAction and mapFeedback that transport a single component.

  • Algorithm.comap alg F hF: the algorithm that transforms the pair (past rounds, current observation) by the measurable map F n at round n before applying the policy of alg.

  • Algorithm.comapObs alg f: the algorithm that sees f o when the observation is o, both in the current round and in the past rounds.

  • Algorithm.comapFeedback alg g: the algorithm that sees g y when the feedback of a past round is y.

  • Environment.comap env F hF f hf: the environment that reads the summary F n of the past rounds and reads f a when the algorithm plays a in the current round.

  • Environment.comapAction env f: the environment that reads f a when the algorithm plays a, both in the current round and in the past rounds.

  • Algorithm.congr alg e𝓞 e𝓐 e𝓨, Environment.congr env e𝓞 e𝓐 e𝓨: relabelling of the observations, the actions and the feedbacks of a player along measurable equivalences.

Main statements

  • IsAlgEnvSeq.hasCondDistrib_action_comapObs, IsAlgEnvSeq.hasCondDistrib_action_comapFeedback: in a run of alg.comapObs f (resp. alg.comapFeedback g) against any environment, the conditional distribution of the action given the transported history and the transported observation is alg.policy n.

  • IsAlgEnvSeq.hasCondDistrib_obs_comapAction, IsAlgEnvSeq.hasCondDistrib_feedback_comapAction: in a run against env.comapAction f, the observations and feedbacks have the conditional distributions of a run of env on the transported actions.

Module LeanMachineLearning.SequentialLearning.Comap contains 69 exposed declarations.