3.3. SequentialLearning.Algorithm
Algorithms and environments
We define structures for stochastic, sequential algorithms and environments, and the notion of an algorithm-environment sequence, which is a sequence of actions and feedbacks generated by an algorithm interacting with an environment.
Main definitions
-
Algorithm 𝓐 𝓨: a stochastic, sequential algorithm. -
Environment 𝓐 𝓨: a stochastic environment. -
IsAlgEnvSeq A 𝓨 alg env P: an algorithm-environment sequence. That is, a sequence of actionsAand feedbackYthat have the correct conditional distributions to be generated by an algorithmalginteracting with an environmentenv, defined on a probability space(Ω, P). -
IsAlgEnvSeqUntil A Y alg env P N:AandYform an algorithm-environment sequence until timeN. -
prod_left alg: anAlgorithm 𝓐 (𝓧 × 𝓨)obtained from an algorithmalg : Algorithm 𝓐 𝓨by ignoring the𝓧component of each observation.
Module LeanMachineLearning.SequentialLearning.Algorithm contains 50 exposed declarations.
-
Learning.Algorithm -
Learning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdPolicy -
Learning.instIsProbabilityMeasureP0 -
Learning.Algorithm.prodLeft -
Learning.Algorithm.prodLeft_p0 -
Learning.Algorithm.prodLeft_policy -
Learning.Environment -
Learning.instIsMarkovKernelProdForallSubtypeNatMemFinsetIicFeedback -
Learning.instIsMarkovKernelν0 -
Learning.stepKernel -
Learning.instIsMarkovKernelForallSubtypeNatMemFinsetIicProdStepKernel -
Learning.stepKernel_def -
Learning.fst_stepKernel -
Learning.step -
Learning.measurable_step -
Learning.trajectory -
Learning.measurable_trajectory -
Learning.history -
Learning.measurable_history -
Learning.eval_comp_history -
Learning.fst_eval_comp_history -
Learning.snd_eval_comp_history -
Learning.history_succ -
Learning.IsAlgEnvSeq -
Learning.IsAlgEnvSeqUntil -
Learning.IsAlgEnvSeqUntil.mono -
Learning.IsAlgEnvSeq.isAlgEnvSeqUntil -
Learning.IsAlgEnvSeq.measurable_step -
Learning.IsAlgEnvSeq.measurable_history -
Learning.IsAlgEnvSeq.hasLaw_step_zero -
Learning.IsAlgEnvSeqUntil.hasLaw_step_zero -
Learning.IsAlgEnvSeq.hasCondDistrib_step -
Learning.IsAlgEnvSeqUntil.hasCondDistrib_step -
Learning.IsAlgEnvSeq.hasLaw_history_zero -
Learning.IsAlgEnvSeq.hasLaw_action_comp -
Learning.IsAlgEnvSeq.hasLaw_feedback_comp -
Learning.IsAlgEnvSeq.hasLaw_feedback_zero_comp -
Learning.IsAlgEnvSeq.filtration -
Learning.IsAlgEnvSeq.adapted_history -
Learning.IsAlgEnvSeq.adapted_step -
Learning.IsAlgEnvSeq.adapted_action -
Learning.IsAlgEnvSeq.adapted_feedback -
Learning.IsAlgEnvSeq.filtrationAction -
Learning.IsAlgEnvSeq.filtrationAction_zero_eq_comap -
Learning.IsAlgEnvSeq.filtrationAction_eq_comap -
Learning.IsAlgEnvSeq.measurable_history_filtrationAction_add_one -
Learning.IsAlgEnvSeq.filtration_le_filtrationAction_succ -
Learning.IsAlgEnvSeq.filtrationAction_le_filtration -
Learning.IsAlgEnvSeq.adapted_action_filtrationAction -
Learning.IsAlgEnvSeq.measurable_feedback_filtrationAction_of_lt