3.6. SequentialLearning.IonescuTulceaSpace
Probability space for algorithm-environment interactions
For any algorithm and environment, we construct a probability space on which we can define a sequence of random variables representing the actions and feedback generated by the interaction of the algorithm and the environment. The main ingredient of the construction is the Ionescu-Tulcea theorem.
Main statements
-
isAlgEnvSeq_unique: the law of the sequence of actions and observations generated by an algorithm-environment pair is unique: it does not depend on the probability space used. IfA₁,R₁andA₂,R₂are two algorithm-environment sequences generated by the same algorithm-environment pair on probability spaces(Ω, P)and(Ω', P'), thenP.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω)).
Module LeanMachineLearning.SequentialLearning.IonescuTulceaSpace contains 49 exposed declarations.
-
Learning.trajMeasure -
Learning.instIsProbabilityMeasureForallNatProdTrajMeasure -
Learning.IsAlgEnvSeq.map_trajectory -
Learning.eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil -
Learning.isAlgEnvSeq_unique -
Learning.IsAlgEnvSeq.identDistrib_trajectory -
Learning.isAlgEnvSeqUntil_unique -
Learning.IT.step -
Learning.IT.action -
Learning.IT.feedback -
Learning.IT.hist -
Learning.IT.fst_comp_step -
Learning.IT.measurable_step -
Learning.IT.measurable_step_prod -
Learning.IT.measurable_action -
Learning.IT.measurable_action_prod -
Learning.IT.measurable_feedback -
Learning.IT.measurable_feedback_prod -
Learning.IT.measurable_hist -
Learning.IT.hist_eq_frestrictLe -
Learning.IT.filtration -
Learning.IT.filtration_eq_comap -
Learning.IT.step_eq_eval_comp_hist -
Learning.IT.action_eq_eval_comp_hist -
Learning.IT.feedback_eq_eval_comp_hist -
Learning.IT.adapted_step -
Learning.IT.adapted_hist -
Learning.IT.adapted_action -
Learning.IT.adapted_feedback -
Learning.IT.filtrationAction -
Learning.IT.filtrationAction_zero_eq_comap -
Learning.IT.filtrationAction_eq_comap -
Learning.IT.filtration_le_filtrationAction_add_one -
Learning.IT.filtration_le_filtrationAction -
Learning.IT.filtrationAction_le_filtration_self -
Learning.IT.filtrationAction_le_filtration -
Learning.IT.measurable_action_filtrationAction -
Learning.IT.hasLaw_step_zero -
Learning.IT.hasLaw_action_zero -
Learning.IT.hasCondDistrib_feedback_zero -
ProbabilityTheory.Kernel.hasCondDistrib_trajMeasure -
Learning.IT.hasCondDistrib_step -
Learning.IT.hasCondDistrib_action -
Learning.IT.hasCondDistrib_feedback -
Learning.IT.condDistrib_feedback_zero -
Learning.IT.condDistrib_step -
Learning.IT.condDistrib_action -
Learning.IT.condDistrib_feedback -
Learning.IT.isAlgEnvSeq_trajMeasure