3.2. SequentialLearning.FiniteActions
Bookkeeping definitions for finite action space sequential learning problems
If the number of actions is finite, it makes sense to define the number of times each action was chosen, the time at which an action was chosen for the nth time, the value of the reward at that time, the sum of rewards obtained for each action, the empirical mean reward for each action, etc.
For each definition that take as arguments a time t : ℕ, a history h : ℕ → 𝓐 × R, and possibly
other parameters, we put the time and history at the end in this order, so that the definition can
be seen as a stochastic process indexed by time t on the measurable space ℕ → 𝓐 × R.
Module LeanMachineLearning.SequentialLearning.FiniteActions contains 75 exposed declarations.
-
Learning.pullCount -
Learning.pullCount' -
Learning.pullCount_zero -
Learning.pullCount_zero_apply -
Learning.pullCount_one -
Learning.monotone_pullCount -
Learning.pullCount_mono -
Learning.pullCount_action_eq_pullCount_add_one -
Learning.pullCount_eq_pullCount_of_action_ne -
Learning.pullCount_add_one -
Learning.pullCount_eq_sum -
Learning.pullCount'_eq_sum -
Learning.pullCount_add_one_eq_pullCount' -
Learning.pullCount_eq_pullCount' -
Learning.pullCount'_mono -
Learning.pullCount_le -
Learning.pullCount_congr -
Learning.pullCount_lt_of_forall_ne -
Learning.exists_pullCount_eq_of_le -
Learning.pullCount_le_add -
Learning.measurable_pullCount -
Learning.measurable_uncurry_pullCount -
Learning.measurable_uncurry_pullCount_comp -
Learning.measurable_pullCount' -
Learning.measurable_uncurry_pullCount' -
Learning.adapted_pullCount_add_one -
Learning.stronglyAdapted_pullCount_add_one -
Learning.isStronglyPredictable_pullCount -
Learning.integrable_pullCount -
Learning.stepsUntil -
Learning.stepsUntil_eq_top_iff -
Learning.stepsUntil_ne_top -
Learning.exists_pullCount_eq -
Learning.stepsUntil_zero_of_ne -
Learning.stepsUntil_zero_of_eq -
Learning.stepsUntil_eq_dite -
Learning.stepsUntil_eq_leastGE -
Learning.stepsUntil_mono -
Learning.stepsUntil_pullCount_le -
Learning.stepsUntil_pullCount_eq -
Learning.stepsUntil_one_of_eq -
Learning.stepsUntil_eq_zero_iff -
Learning.action_stepsUntil -
Learning.action_eq_of_stepsUntil_eq_coe -
Learning.pullCount_stepsUntil_add_one -
Learning.pullCount_stepsUntil -
Learning.pullCount_lt_of_le_stepsUntil -
Learning.pullCount_eq_of_stepsUntil_eq_coe -
Learning.pullCount_add_one_eq_of_stepsUntil_eq_coe -
Learning.stepsUntil_eq_iff -
Learning.stepsUntil_eq_iff' -
Learning.stepsUntil_eq_congr -
Learning.isStoppingTime_stepsUntil -
Learning.measurable_stepsUntil -
Learning.measurable_stepsUntil' -
Learning.measurable_comap_indicator_stepsUntil_eq -
Learning.measurable_indicator_stepsUntil_eq -
Learning.measurableSet_stepsUntil_eq_zero -
Learning.measurable_comap_indicator_stepsUntil_eq_zero -
Learning.measurableSet_stepsUntil_eq -
Learning.isStoppingTime_stepsUntil_filtrationAction -
Learning.rewardByCount -
Learning.rewardByCount_eq_ite -
Learning.rewardByCount_eq_add -
Learning.rewardByCount_of_stepsUntil_eq_top -
Learning.rewardByCount_of_stepsUntil_ne_top -
Learning.rewardByCount_eq_stoppedValue -
Learning.rewardByCount_of_stepsUntil_eq_coe -
Learning.rewardByCount_zero -
Learning.rewardByCount_pullCount_add_one_eq_reward -
Learning.measurable_rewardByCount -
Learning.sum_pullCount_mul -
Learning.sum_pullCount -
Learning.sum_comp_pullCount -
Learning.sum_pullCount'