BanditRLProof.Algorithms.MOSSCanonicalHistory

No declaration docstring is present; use the chapter context and exact statement below.

def canonicalAction {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ)

Consume the next unused one-based raw reward of the chosen arm.

def canonicalReward {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ)

No declaration docstring is present; use the chapter context and exact statement below.

def canonicalHistory {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (table : UCB.ArmRewardStream k) (t : ℕ)

No declaration docstring is present; use the chapter context and exact statement below.

theorem canonicalHistory_pullCount {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (table : UCB.ArmRewardStream k) (t : ℕ) (a : Fin k) : ETC.realHistoryPullCount t (canonicalHistory hk n mean table t) a = pullCount (canonicalAction hk n mean table) a (t+1)

No declaration docstring is present; use the chapter context and exact statement below.

theorem canonicalHistory_empiricalMean {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (table : UCB.ArmRewardStream k) (t : ℕ) (a : Fin k) : ETC.realHistoryEmpMean t (canonicalHistory hk n mean table t) a = (∑ j ∈ Finset.range (pullCount (canonicalAction hk n mean table) a (t+1)), table (j+1) a) / (pullCount (canonicalAction hk n mean table) a (t+1) : ℝ)

The realized next action is exactly the common finite-history MOSS selector.

theorem canonicalAction_succ_eq_historyAction {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (table : UCB.ArmRewardStream k) (t : ℕ) : canonicalAction hk n mean table (t+1) = historyAction hk n t (canonicalHistory hk n mean table t)

No declaration docstring is present; use the chapter context and exact statement below.

theorem canonicalAction_zero {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (table : UCB.ArmRewardStream k) : canonicalAction hk n mean table 0 = ⟨0, hk⟩

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_canonicalAction {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) : Measurable (fun table => canonicalAction hk n mean table t)

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_canonicalReward {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) : Measurable (fun table => canonicalReward hk n mean table t)

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_canonicalHistory {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) : Measurable (fun table => canonicalHistory hk n mean table t)

No declaration docstring is present; use the chapter context and exact statement below.

theorem canonicalHistory_succ {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (table : UCB.ArmRewardStream k) (t : ℕ) : canonicalHistory hk n mean table (t+1) = History.extendPairHistorySucc (canonicalHistory hk n mean table t) (historyAction hk n t (canonicalHistory hk n mean table t), table (ETC.realHistoryPullCount t (canonicalHistory hk n mean table t) (historyAction hk n t (canonicalHistory hk n mean table t))+1) (historyAction hk n t (canonicalHistory hk n mean table t)))

Changing rewards that have not been consumed cannot change the observed history.

theorem canonicalHistory_eq_of_eq_consumed {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (table table' : UCB.ArmRewardStream k) (t : ℕ) (hagrees : ∀ a j, j < pullCount (canonicalAction hk n mean table) a (t+1) → table (j+1) a = table' (j+1) a) : canonicalHistory hk n mean table t = canonicalHistory hk n mean table' t