3.8. SequentialLearning.Deterministic
Deterministic algorithms and environments
A deterministic algorithm chooses its action in a deterministic way. That is, that action is given by a measurable function of the history instead of a general Markov kernel. Similarly, a deterministic environment gives feedback in a deterministic way.
Main definitions
We introduce two typeclasses IsDeterministicAlg and IsDeterministicEnv to express that
an algorithm or an environment is deterministic. We also give definitions for the initial action
and the next action of a deterministic algorithm, and for the feedback functions of a deterministic
environment. Finally, we give a construction of a deterministic algorithm and environment from
measurable functions.
-
IsDeterministicAlg alg: a typeclass expressing that the algorithmalgis deterministic. -
IsDeterministicEnv env: a typeclass expressing that the environmentenvis deterministic. -
nextAction alg n: the function that gives the action of a deterministic algorithmalgat stepn, as a function of the history beforen. -
actionZero alg: the initial action of a deterministic algorithmalg. This isnextAction alg 0applied to the empty history. -
feedbackFun env n: the function that gives the feedback of a deterministic environmentenvat stepn, as a function of the history and the current action. -
feedbackFunZero env: the function that gives the initial feedback of a deterministic environmentenv. This isfeedbackFun env 0applied to the empty history. -
detAlgorithm nextA h_next: a deterministic algorithm that chooses its action according to the measurable functionnextA(with proof of measurabilityh_next). The initial action isnextA 0 default. -
detEnvironment f hf: a deterministic environment that gives feedback according to the measurable functionf(with proof of measurabilityhf).
Module LeanMachineLearning.SequentialLearning.Deterministic contains 42 exposed declarations.
-
Learning.IsDeterministicAlg -
Learning.nextAction -
Learning.actionZero -
Learning.measurable_nextAction -
Learning.policy_eq_deterministic -
Learning.nextAction_zero -
Learning.p0_eq_dirac -
Learning.IsDeterministicAlg.action_ae_eq_of_IsAlgEnvSeqUntil -
Learning.IsDeterministicAlg.action_zero_of_IsAlgEnvSeqUntil -
Learning.IsDeterministicAlg.hasLaw_action_zero_of_IsAlgEnvSeqUntil -
Learning.IsDeterministicAlg.hasLaw_action_zero -
Learning.IsDeterministicAlg.action_ae_eq -
Learning.IsDeterministicAlg.action_zero_ae_eq -
Learning.IsDeterministicAlg.action_ae_all_eq -
Learning.IsDeterministicEnv -
Learning.feedbackFun -
Learning.measurable_feedbackFun -
Learning.feedback_eq_deterministic -
Learning.feedbackFunZero -
Learning.measurable_feedbackFunZero -
Learning.feedbackFun_zero -
Learning.ν0_eq_deterministic -
Learning.IsDeterministicEnv.hasCondDistrib_feedback -
Learning.IsDeterministicEnv.hasCondDistrib_feedback_zero -
Learning.IsDeterministicEnv.feedback_ae_eq -
Learning.detAlgorithm -
Learning.detAlgorithm_policy -
Learning.instIsDeterministicAlgDetAlgorithm -
Learning.p0_detAlgorithm -
Learning.nextAction_detAlgorithm -
Learning.actionZero_detAlgorithm -
Learning.detEnvironment -
Learning.instIsDeterministicEnvDetEnvironment -
Learning.feedbackFun_detEnvironment -
Learning.feedbackFunZero_detEnvironment -
Learning.IsAlgEnvSeq.hasLaw_action_zero_detAlgorithm -
Learning.IsAlgEnvSeq.action_detAlgorithm_ae_eq -
Learning.IsAlgEnvSeq.action_zero_detAlgorithm -
Learning.IsAlgEnvSeq.action_detAlgorithm_ae_all_eq -
Learning.IsAlgEnvSeqUntil.hasLaw_action_zero_detAlgorithm -
Learning.IsAlgEnvSeqUntil.action_detAlgorithm_ae_eq -
Learning.IsAlgEnvSeqUntil.action_zero_detAlgorithm