Lean module · Foundations
BanditRLProof.Algorithms.MOSSHistoryLaw
Generated source map for this Lean module.
Module map
Imports
BanditRLProof.Algorithms.MOSSConditionalReward, BanditRLProof.LowerBounds.BanditHistoryKL
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.canonical_initialPair_map
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.canonical_initialPair_mapReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem canonical_initialPair_map {k : ℕ} (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (ν : Kernel (Fin k) ℝ) [IsMarkovKernel ν] : (UCB.armStreamMeasure ν).map (fun table => (canonicalAction hk n mean table 0, canonicalReward hk n mean table 0)) = (historyAlgorithm hk n).initialAction.compProd ν
theorem
BanditRLProof.MOSS.canonical_action_condDistrib
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.canonical_action_condDistribReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem canonical_action_condDistrib {k : ℕ} [NeZero k] (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (t : ℕ) (ν : Kernel (Fin k) ℝ) [IsMarkovKernel ν] : Filter.EventuallyEq (ae ((UCB.armStreamMeasure ν).map (fun table => canonicalHistory hk n mean table t))) (condDistrib (fun table => canonicalAction hk n mean table (t+1)) (fun table => canonicalHistory hk n mean table t) (UCB.armStreamMeasure ν)) ((historyAlgorithm hk n).policy t)
theorem
BanditRLProof.MOSS.canonical_historySequence
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.canonical_historySequenceReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem canonical_historySequence {k : ℕ} [NeZero k] (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (ν : Kernel (Fin k) ℝ) [IsMarkovKernel ν] : Thompson.IsHistoryAlgorithmEnvironmentSequence (UCB.armStreamMeasure ν) (canonicalAction hk n mean) (canonicalReward hk n mean) (historyAlgorithm hk n) (LowerBounds.stationaryBanditHistoryEnvironment ν) where
theorem
BanditRLProof.MOSS.map_canonicalHistory_eq
Compiled
Canonical reward-table histories have exactly the common bandit history law.
Used in these reading views: Bandit Book
1. Finite bandits, traces, and regret
Canonical node identity
declaration:BanditRLProof.MOSS.map_canonicalHistory_eqReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem map_canonicalHistory_eq {k : ℕ} [NeZero k] (hk : 0 < k) (n : ℕ) (mean : Fin k → ℝ) (ν : Kernel (Fin k) ℝ) [IsMarkovKernel ν] (t : ℕ) : (UCB.armStreamMeasure ν).map (fun table => canonicalHistory hk n mean table t) = LowerBounds.canonicalBanditHistoryMeasure (historyAlgorithm hk n) ν t