3.13. SequentialLearning.ActionIndicator
The action indicator
actionIndicator A k n ω = 𝟙{A n ω = k} is the {0,1}-valued indicator that action k was chosen
at round n. It is the increment weight of every per-action sum attached to an action process:
pullCount A k n is its partial sum (sum_range_actionIndicator_eq_pullCount) and
sumRewards A Y k n is its reward-weighted partial sum (sum_actionIndicator_mul).
Main definitions
-
Learning.actionIndicator
Main results
-
Learning.sum_range_actionIndicator_eq_pullCount,Learning.sum_actionIndicator_mul— the two partial-sum identities. -
Learning.adapted_actionIndicator,Learning.integrable_actionIndicator.
Module LeanMachineLearning.SequentialLearning.ActionIndicator contains 12 exposed declarations.
-
Learning.actionIndicator -
Learning.actionIndicator_eq_one_iff -
Learning.actionIndicator_nonneg -
Learning.actionIndicator_le_one -
Learning.sum_actionIndicator -
Learning.sum_actionIndicator_eq_pullCount -
Learning.sum_actionIndicator_smul -
Learning.sum_actionIndicator_mul -
Learning.measurable_actionIndicator -
Learning.integrable_actionIndicator -
Learning.IsAlgEnvSeq.adapted_actionIndicator -
Learning.IsAlgEnvSeq.adapted_actionIndicator_filtrationAction