2.9. Online.Bandit.RewardByCountMeasure
Laws of stepsUntil and rewardByCount
Independence of the rewards by count
We prove that the family (rewardByCount A R a (m + 1))_{(a, m)} is independent, with
rewardByCount A R a (m + 1) distributed according to ν a.
The proof goes through the time-truncated arrays rewardByCountUntil A R t, in which the entries
corresponding to pulls that happen at time t or later are replaced by the auxiliary array. Under
the product measure 𝔓, the law of rewardByCountUntil A R t does not depend on t: going from
t to t + 1 replaces the entry (A t, pullCount A (A t) t), which was an auxiliary reward with
law ν (A t) independent of everything else, by the reward R t, which conditionally on the
history and on A t also has law ν (A t). For t = 0 the array is a sub-array of the auxiliary
array, whose law is the product measure. Finally rewardByCountUntil A R t converges to
rewardByCount entrywise as t → ∞, which gives the law of the latter.
Module LeanMachineLearning.Online.Bandit.RewardByCountMeasure contains 28 exposed declarations.
-
Bandits.«term𝓛[_|_;_]» -
Bandits.«term𝓛[_|_In_;_]» -
Bandits.«term𝓛[_|_←_;_]» -
Bandits.condDistrib_reward'' -
Bandits.reward_cond_action -
Bandits.condIndepFun_reward_stepsUntil_action' -
Bandits.condIndepFun_reward_stepsUntil_action -
Bandits.reward_cond_stepsUntil -
Bandits.condDistrib_rewardByCount_stepsUntil -
Bandits.hasLaw_rewardByCount -
Bandits.identDistrib_rewardByCount -
Bandits.identDistrib_rewardByCount_id -
Bandits.identDistrib_rewardByCount_eval -
Bandits.hasLaw_rewardByCountUntil_zero -
Bandits.indepFun_update_rewardByCountUntil_eval -
Bandits.indepFun_history_reward_cond -
Bandits.hasLaw_reward_cond -
Bandits.hasLaw_reward_cond_prod -
Bandits.indepFun_update_rewardByCountUntil_reward -
Bandits.identDistrib_rewardByCountUntil_add_one_cond -
Bandits.identDistrib_rewardByCountUntil_add_one -
Bandits.hasLaw_rewardByCountUntil -
Bandits.hasLaw_rewardByCount_infinitePi -
Bandits.hasLaw_rewardByCount_add_one -
Bandits.iIndepFun_rewardByCount_add_one -
Bandits.iIndepFun_rewardByCount -
Bandits.iIndepFun_rewardByCount_add_one_action -
Bandits.indepFun_rewardByCount