Lean module · Foundations
BanditRLProof.Algorithms.MOSSStreamMeasurable
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.Algorithms.MOSSRegret, BanditRLProof.Algorithms.MOSSHistory, BanditRLProof.ExpectationRegretPullCount
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.measurable_streamMean_at_count
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.MOSS.measurable_streamMean_at_countReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_streamMean_at_count (X : ℕ → Ω → ℝ) (hXm : ∀ i, StronglyMeasurable (X i)) (c : Ω → ℕ) (hc : Measurable c) : Measurable (fun ω => streamMean X ω (c ω))
theorem
BanditRLProof.MOSS.measurable_action_of_state
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.MOSS.measurable_action_of_stateReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_action_of_state {k : ℕ} (hk : 0 < k) (n t : ℕ) (emp : Ω → Fin k → ℝ) (counts : Ω → Fin k → ℕ) (he : ∀ a, Measurable (fun ω => emp ω a)) (hc : ∀ a, Measurable (fun ω => counts ω a)) : Measurable (fun ω => action hk n t (emp ω) (counts ω))
theorem
BanditRLProof.MOSS.measurable_streamCounts
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.MOSS.measurable_streamCountsReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_streamCounts {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (X : Fin k → ℕ → Ω → ℝ) (hXm : ∀ a i, StronglyMeasurable (X a i)) (t : ℕ) (a : Fin k) : Measurable (fun ω => streamCounts hk n mean X ω t a)
theorem
BanditRLProof.MOSS.measurable_streamTrace
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.MOSS.measurable_streamTraceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_streamTrace {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (X : Fin k → ℕ → Ω → ℝ) (hXm : ∀ a i, StronglyMeasurable (X a i)) (t : ℕ) : Measurable (fun ω => streamTrace hk n mean X ω t)
theorem
BanditRLProof.MOSS.integrable_streamTrace_regret
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.MOSS.integrable_streamTrace_regretReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integrable_streamTrace_regret (μ : Measure Ω) [IsFiniteMeasure μ] {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (X : Fin k → ℕ → Ω → ℝ) (hXm : ∀ a i, StronglyMeasurable (X a i)) : Integrable (fun ω => realMeanRegret mean (streamTrace hk n mean X ω) n) μ