3.4. SequentialLearning.StationaryEnv
Oblivious and stationary environments
An oblivious environment is an environment in which the distribution of the next feedback depends only on the last action (and not on the past history). If the kernel that gives the distribution of the next feedback given the last action is the same at every time step, then we say that the environment is stationary.
Main definitions
We define a Prop-valued typeclass IsObliviousEnv to express that an environment is oblivious,
and we define two constructors for oblivious environments.
Typeclass and related definitions:
-
IsObliviousEnv env: the environmentenvis oblivious. -
feedbackCondAction env n: the kernel representing the conditional distribution of the feedback given the action at timenin an oblivious environmentenv.
Constructors for oblivious environments:
-
obliviousEnv ν: an oblivious environment, in which the distribution of the next feedback depends only on the last action, but in a possibly time-dependent manner, and is given by a sequence of Markov kernelsν : ℕ → Kernel 𝓐 𝓨. -
stationaryEnv ν: a stationary environment, in which the distribution of the next feedback depends only on the last action (and not on the past history), and is given by a Markov kernelν : Kernel 𝓐 𝓨.
Module LeanMachineLearning.SequentialLearning.StationaryEnv contains 28 exposed declarations.
-
Learning.IsObliviousEnv -
Learning.feedbackCondAction -
Learning.instIsMarkovKernelFeedbackCondAction -
Learning.ν0_eq_feedbackCondAction -
Learning.feedback_eq_feedbackCondAction -
Learning.IsObliviousEnv.hasCondDistrib_feedback_history_action -
Learning.IsObliviousEnv.hasCondDistrib_feedback -
Learning.IsObliviousEnv.condIndepFun_feedback_history_action -
Learning.IsObliviousEnv.condIndepFun_feedback_history_action_action -
Learning.IsObliviousEnv.condIndepFun_feedback_history_action_action' -
Learning.obliviousEnv -
Learning.obliviousEnv_feedback -
Learning.obliviousEnv_ν0 -
Learning.feedback_obliviousEnv -
Learning.ν0_obliviousEnv -
Learning.instIsObliviousEnvObliviousEnv -
Learning.feedbackCondAction_obliviousEnv -
Learning.stationaryEnv -
Learning.feedback_stationaryEnv -
Learning.ν0_stationaryEnv -
Learning.instIsObliviousEnvStationaryEnv -
Learning.feedbackCondAction_stationaryEnv -
Learning.IsAlgEnvSeq.hasCondDistrib_feedback_obliviousEnv -
Learning.IsAlgEnvSeq.hasCondDistrib_feedback_stationaryEnv -
Learning.IsAlgEnvSeq.condDistrib_feedback_stationaryEnv -
Learning.IsAlgEnvSeq.condIndepFun_feedback_history_action -
Learning.IsAlgEnvSeq.condIndepFun_feedback_history_action_action -
Learning.IsAlgEnvSeq.condIndepFun_feedback_history_action_action'