BanditRLProof.Algorithms.MOSSHistoryRegret

Inclusive finite-history counts agree with trace counts through t+1.

theorem finiteHistoryPullCountENNReal_trace {k : ℕ} {Reward : Type*} (action : ActionTrace (Fin k)) (reward : RewardTrace Reward) (t : ℕ) (a : Fin k) : LowerBounds.finiteHistoryPullCountENNReal t (History.finitePairHistoryOfTrace action reward t) a = (pullCount action a (t+1) : ℝ≥0∞)

The history gap functional is exactly the executed real pseudo-regret.

theorem canonicalHistory_gapRegret_toReal {k : ℕ} (hk : 0 < k) (n t : ℕ) (mean : Fin k → ℝ) (best : Fin k) (hbest : ∀ a, mean a ≤ mean best) (table : UCB.ArmRewardStream k) : (LowerBounds.finiteHistoryGapPseudoRegret (fun a => mean best-mean a) t (canonicalHistory hk n mean table t)).toReal = realMeanRegret mean (canonicalAction hk n mean table) (t+1)

Exact transport of the common-history expected regret to the reward table.

theorem canonicalGapExpectedRegret_eq_integral {k : ℕ} [NeZero k] (hk : 0 < k) (n t : ℕ) (ν : Kernel (Fin k) ℝ) [IsMarkovKernel ν] (mean : Fin k → ℝ) (best : Fin k) (hbest : ∀ a, mean a ≤ mean best) : LowerBounds.canonicalGapExpectedPseudoRegretReal (historyAlgorithm hk n) ν (fun a => mean best-mean a) t = ∫ table, realMeanRegret mean (canonicalAction hk n mean table) (t+1) ∂UCB.armStreamMeasure ν

Source constant 39, now for the same history-law regret used by lower bounds.

theorem canonicalGapExpectedRegret_le {k : ℕ} [NeZero k] (hk : 0 < k) (ν : Kernel (Fin k) ℝ) [IsMarkovKernel ν] (t : ℕ) (hkt : k ≤ t+1) (mean : Fin k → ℝ) (best : Fin k) (hbest : ∀ a, mean a ≤ mean best) (hmean : ∀ a, ∫ r, r ∂ν a = mean a) (hsubG : ∀ a, HasSubgaussianMGF (fun r => r-mean a) 1 (ν a)) : LowerBounds.canonicalGapExpectedPseudoRegretReal (historyAlgorithm hk (t+1)) ν (fun a => mean best-mean a) t ≤ 39*Real.sqrt (((t+1 : ℕ) : ℝ)*k) + ∑ a, (mean best-mean a)