BanditRLProof.Algorithms.MOSSRegret

Pathwise regret split with a deterministic large-gap filter for integration.

theorem streamTrace_gapSum_le {Ω : Type*} [MeasurableSpace Ω] {k : ℕ} (hk : 0 < k) (n : ℕ) (hkn : k ≤ n) (mean : Fin k → ℝ) (X : Fin k → ℕ → Ω → ℝ) (ω : Ω) (best : Fin k) (hbest : ∀ a, mean a ≤ mean best) : (∑ a, (mean best - mean a) * (pullCount (streamTrace hk n mean X ω) a n : ℝ)) ≤ (8*sqrt ((k : ℝ)/(n : ℝ)) + 2*optimismDeficit (X best) ((k : ℝ)/(n : ℝ)) n ω)*(n : ℝ) + ∑ a, if 8*sqrt ((k : ℝ)/(n : ℝ)) ≤ mean best - mean a then (mean best - mean a) * (1 + indexExceedanceCount (streamMean (X a) ω) ((k : ℝ)/(n : ℝ)) (mean best - mean a) n) else 0

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

theorem streamTrace_realMeanRegret_le {Ω : Type*} [MeasurableSpace Ω] {k : ℕ} (hk : 0 < k) (n : ℕ) (hkn : k ≤ n) (mean : Fin k → ℝ) (X : Fin k → ℕ → Ω → ℝ) (ω : Ω) (best : Fin k) (hbest : ∀ a, mean a ≤ mean best) : realMeanRegret mean (streamTrace hk n mean X ω) n ≤ (8*sqrt ((k : ℝ)/(n : ℝ)) + 2*optimismDeficit (X best) ((k : ℝ)/(n : ℝ)) n ω)*(n : ℝ) + ∑ a, if 8*sqrt ((k : ℝ)/(n : ℝ)) ≤ mean best - mean a then (mean best - mean a) * (1 + indexExceedanceCount (streamMean (X a) ω) ((k : ℝ)/(n : ℝ)) (mean best - mean a) n) else 0

Integrated large-gap contribution, with the single initialization gap term.

theorem integral_largeGapCountSum_le {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] {k : ℕ} (mean : Fin k → ℝ) (X : Fin k → ℕ → Ω → ℝ) (best : Fin k) (hbest : ∀ a, mean a ≤ mean best) (hXm : ∀ a i, StronglyMeasurable (X a i)) (hind : ∀ a, iIndepFun (X a) μ) (hmean : ∀ a i, ∫ ω, X a i ω ∂μ = 0) (hsubG : ∀ a i, HasSubgaussianMGF (X a i) 1 μ) (δ : ℝ) (hδ : 0 < δ) (n : ℕ) : (∫ ω, ∑ a, if 8*sqrt δ ≤ mean best - mean a then (mean best - mean a)*(1+indexExceedanceCount (streamMean (X a) ω) δ (mean best-mean a) n) else 0 ∂μ) ≤ (∑ a, (mean best-mean a)) + (k : ℝ)*(15/sqrt δ)