Lean module · Foundations
BanditRLProof.Algorithms.MOSSExpectedRegret
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.Algorithms.MOSSStreamMeasurable
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.MOSS.integral_streamTrace_regret_le
Compiled
Theorem 9.1's exact constant for the concrete centered reward-table execution. Identification with the common bandit history law is a separate theorem.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.MOSS.integral_streamTrace_regret_leReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_streamTrace_regret_le {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] {k : ℕ} (hk : 0 < k) (n : ℕ) (hkn : k ≤ n) (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 μ) : (∫ ω, realMeanRegret mean (streamTrace hk n mean X ω) n ∂μ) ≤ 39*sqrt ((n : ℝ)*k) + ∑ a, (mean best-mean a)