Lean module · Foundations
BanditRLProof.Algorithms.MOSSConditionalReward
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.Algorithms.MOSSRewardBranch
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.map_condition_reward_eq_compProd
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.map_condition_reward_eq_compProdReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem map_condition_reward_eq_compProd {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (ν : Kernel (Fin k) ℝ) [IsMarkovKernel ν] : Measure.map (fun table => (canonicalCondition hk n mean t table, canonicalReward hk n mean table (t+1))) (UCB.armStreamMeasure ν) = (Measure.map (canonicalCondition hk n mean t) (UCB.armStreamMeasure ν)).compProd (UCB.armStreamSelectedRewardKernel t ν)
theorem
BanditRLProof.MOSS.canonicalReward_condDistrib
Compiled
The actual successor reward has the selected arm law conditionally on history/action.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.MOSS.canonicalReward_condDistribReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem canonicalReward_condDistrib {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (ν : Kernel (Fin k) ℝ) [IsMarkovKernel ν] : Filter.EventuallyEq (ae ((UCB.armStreamMeasure ν).map (canonicalCondition hk n mean t))) (condDistrib (fun table => canonicalReward hk n mean table (t+1)) (canonicalCondition hk n mean t) (UCB.armStreamMeasure ν)) (UCB.armStreamSelectedRewardKernel t ν)