BanditRLProof.Algorithms.MOSSStream

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

theorem neg_optimismDeficit_le_centeredIndex {Ω : Type*} [MeasurableSpace Ω] (X : ℕ → Ω → ℝ) (δ : ℝ) (n s : ℕ) (ω : Ω) (hs : 0 < s) (hsn : s ≤ n) : -optimismDeficit X δ n ω ≤ centeredIndex X δ s ω

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

theorem radius_eq_streamRadius (n k s : ℕ) (hn : 0 < n) (hk : 0 < k) : radius n k s = sqrt (4/(s : ℝ)*logPlus (1/((s : ℝ)*((k : ℝ)/(n : ℝ)))))

Empirical state indexed by actual arm pulls, using centered reward streams.

def streamEmpirical {Ω : Type*} {k : ℕ} (mean : Fin k → ℝ) (X : Fin k → ℕ → Ω → ℝ) (ω : Ω) (trace : ActionTrace (Fin k)) (t : ℕ) (a : Fin k) : ℝ

Pathwise large-gap count bound from the MOSS policy equation itself. The law identifying centered streams with observed rewards is not assumed here.

theorem pullCount_le_of_stream_policy {Ω : Type*} [MeasurableSpace Ω] {k : ℕ} (hk : 0 < k) (n : ℕ) (hkn : k ≤ n) (mean : Fin k → ℝ) (X : Fin k → ℕ → Ω → ℝ) (ω : Ω) (trace : ActionTrace (Fin k)) (hpolicy : ∀ t < n, trace t = action hk n t (streamEmpirical mean X ω trace t) (fun a => pullCount trace a t)) (best chosen : Fin k) (hgap : 2 * optimismDeficit (X best) ((k : ℝ)/(n : ℝ)) n ω < mean best - mean chosen) : (pullCount trace chosen n : ℝ) ≤ 1 + indexExceedanceCount (streamMean (X chosen) ω) ((k : ℝ)/(n : ℝ)) (mean best - mean chosen) n

Concrete MOSS execution on a fixed reward table, tracking pre-pull counts.

def streamCounts {Ω : Type*} {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (X : Fin k → ℕ → Ω → ℝ) (ω : Ω) : ℕ → Fin k → ℕ | 0 => fun _ => 0 | t+1 => fun a => let counts := streamCounts hk n mean X ω t counts a + if action hk n t (fun b => mean b + streamMean (X b) ω (counts b)) counts = a then 1 else 0 def streamTrace {Ω : Type*} {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (X : Fin k → ℕ → Ω → ℝ) (ω : Ω) : ActionTrace (Fin k)

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

def streamTrace {Ω : Type*} {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (X : Fin k → ℕ → Ω → ℝ) (ω : Ω) : ActionTrace (Fin k)

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

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

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

theorem streamTrace_policy {Ω : Type*} {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (X : Fin k → ℕ → Ω → ℝ) (ω : Ω) (t : ℕ) : streamTrace hk n mean X ω t = action hk n t (streamEmpirical mean X ω (streamTrace hk n mean X ω) t) (fun a => pullCount (streamTrace hk n mean X ω) a t)

Concrete generated-trace bound: no selected-event or policy-equation oracle.

theorem streamTrace_pullCount_le {Ω : Type*} [MeasurableSpace Ω] {k : ℕ} (hk : 0 < k) (n : ℕ) (hkn : k ≤ n) (mean : Fin k → ℝ) (X : Fin k → ℕ → Ω → ℝ) (ω : Ω) (best chosen : Fin k) (hgap : 2 * optimismDeficit (X best) ((k : ℝ)/(n : ℝ)) n ω < mean best - mean chosen) : (pullCount (streamTrace hk n mean X ω) chosen n : ℝ) ≤ 1 + indexExceedanceCount (streamMean (X chosen) ω) ((k : ℝ)/(n : ℝ)) (mean best - mean chosen) n