3.15. SequentialLearning.EvaluationEnv
Function evaluation environments
We define two environments, onlineEvalEnv and evalEnv, where the feedback is given by evaluating
a measurable function at the chosen action. The first one allows the function to change at every
time step, while the second one uses a fixed function at every time step.
Main definitions
-
onlineEvalEnv g hg: A stationary environment where the feedback at timenis given by a deterministic kernel that evaluates the measurable functiong nat the chosen action. -
evalEnv f hf: A stationary environment where the feedback is given by a deterministic kernel that evaluates a fixed measurable functionfat the chosen action.
They both satisfy the typeclasses IsObliviousEnv and IsDeterministicEnv.
Main statements
-
forall_feedback_onlineEvalEnv_ae_eq_eval_action: For almost allω, the feedback at timenis equal tog nevaluated at the action taken at timen. -
forall_feedback_evalEnv_ae_eq_eval_action: For almost allω, the feedback at timenis equal tofevaluated at the action taken at timen.
Module LeanMachineLearning.SequentialLearning.EvaluationEnv contains 19 exposed declarations.
-
Learning.onlineEvalEnv -
Learning.instIsObliviousEnvOnlineEvalEnv -
Learning.instIsDeterministicEnvOnlineEvalEnv -
Learning.feedbackCondAction_onlineEvalEnv -
Learning.feedbackFunZero_onlineEvalEnv -
Learning.feedbackFun_onlineEvalEnv -
Learning.hascondDistrib_feedback_onlineEvalEnv -
Learning.feedback_onlineEvalEnv_ae_eq_eval_action -
Learning.forall_feedback_onlineEvalEnv_ae_eq_eval_action -
Learning.evalEnv -
Learning.instIsObliviousEnvEvalEnv -
Learning.instIsDeterministicEnvEvalEnv -
Learning.feedbackCondAction_evalEnv -
Learning.feedbackFunZero_evalEnv -
Learning.feedbackFun_evalEnv -
Learning.hascondDistrib_feedback_evalEnv -
Learning.feedback_evalEnv_ae_eq_eval_action -
Learning.forall_feedback_evalEnv_ae_eq_eval_action -
Learning.feedback_evalEnv_ae_eq_eval_action_comp