BanditRLProof.Algorithms.MOSSCanonicalReward

One-based centered reward table; sample zero is unused by MOSS.

def centeredRewardTable {k : ℕ} (mean : Fin k → ℝ) : Fin k → ℕ → UCB.ArmRewardStream k → ℝ

Exact MOSS bound on the canonical product space of arbitrary arm laws.

theorem integral_canonicalReward_regret_le {k : ℕ} (hk : 0 < k) (ν : Kernel (Fin k) ℝ) [IsMarkovKernel ν] (n : ℕ) (hkn : k ≤ n) (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)) : (∫ table, realMeanRegret mean (streamTrace hk n mean (centeredRewardTable mean) table) n ∂UCB.armStreamMeasure ν) ≤ 39*Real.sqrt ((n : ℝ)*k) + ∑ a, (mean best-mean a)

Centering is analytical only: positive-count empirical means use raw rewards.

theorem mean_add_centeredRewardTable_average {k : ℕ} (mean : Fin k → ℝ) (table : UCB.ArmRewardStream k) (a : Fin k) (s : ℕ) (hs : 0 < s) : mean a + streamMean (centeredRewardTable mean a) table s = (∑ j ∈ Finset.range s, table (j+1) a)/(s : ℝ)

After initialization each arm has a positive realized count.

theorem streamTrace_pullCount_pos {Ω : Type*} {k : ℕ} (hk : 0 < k) (n t : ℕ) (mean : Fin k → ℝ) (X : Fin k → ℕ → Ω → ℝ) (ω : Ω) (a : Fin k) (ht : k ≤ t) : 0 < pullCount (streamTrace hk n mean X ω) a t

The centered execution selects solely from raw empirical rewards and counts. The unknown means cancel; zero-count states are handled by initialization.

theorem canonicalReward_action_eq_raw {k : ℕ} (hk : 0 < k) (n t : ℕ) (mean : Fin k → ℝ) (table : UCB.ArmRewardStream k) : streamTrace hk n mean (centeredRewardTable mean) table t = action hk n t (fun a => (∑ j ∈ Finset.range (pullCount (streamTrace hk n mean (centeredRewardTable mean) table) a t), table (j+1) a)/(pullCount (streamTrace hk n mean (centeredRewardTable mean) table) a t : ℝ)) (fun a => pullCount (streamTrace hk n mean (centeredRewardTable mean) table) a t)